Improve pretty-printing of types

When doing debug-printing it's really important that the free vars
of a type are printed with their uniques.  The IfaceTcTyVar thing
was a stab in that direction, but it only worked for TcTyVars, not
TyVars.

This patch does it properly, by keeping track of the free vars of the
type when translating Type -> IfaceType, and passing that down through
toIfaceTypeX.  Then when we find a variable, look in that set, and
translate it to IfaceFreeTyVar if so.  (I renamed IfaceTcTyVar to
IfaceFreeTyVar.)

Fiddly but not difficult.

10 files changed, 136 insertions, 104 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index 1b11a0f900..69307bbf60 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -679,8 +679,8 @@ rnIfaceIdDetails (IfRecSelId (Right decl) b) = IfRecSelId <$> fmap Right (rnIfac
 rnIfaceIdDetails details = pure details
 
 rnIfaceType :: Rename IfaceType
-rnIfaceType (IfaceTcTyVar n) = pure (IfaceTcTyVar n)
-rnIfaceType (IfaceTyVar   n) = pure (IfaceTyVar n)
+rnIfaceType (IfaceFreeTyVar n) = pure (IfaceFreeTyVar n)
+rnIfaceType (IfaceTyVar   n)   = pure (IfaceTyVar n)
 rnIfaceType (IfaceAppTy t1 t2)
     = IfaceAppTy <$> rnIfaceType t1 <*> rnIfaceType t2
 rnIfaceType (IfaceLitTy l)         = return (IfaceLitTy l)
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 7150e228ba..f00e334bf9 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -1347,7 +1347,7 @@ freeNamesIfTcArgs (ITC_Invis k ks) = freeNamesIfKind k &&& freeNamesIfTcArgs ks
 freeNamesIfTcArgs ITC_Nil          = emptyNameSet
 
 freeNamesIfType :: IfaceType -> NameSet
-freeNamesIfType (IfaceTcTyVar _)      = emptyNameSet
+freeNamesIfType (IfaceFreeTyVar _)    = emptyNameSet
 freeNamesIfType (IfaceTyVar _)        = emptyNameSet
 freeNamesIfType (IfaceAppTy s t)      = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfTcArgs ts
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 75a2afcc7d..41cf4f69e4 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -110,15 +110,15 @@ data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
 type IfaceKind     = IfaceType
 
 data IfaceType     -- A kind of universal type, used for types and kinds
-  = IfaceTcTyVar  TyVar                   -- See Note [TcTyVars in IfaceType]
-  | IfaceTyVar    IfLclName               -- Type/coercion variable only, not tycon
-  | IfaceLitTy    IfaceTyLit
-  | IfaceAppTy    IfaceType IfaceType
-  | IfaceFunTy    IfaceType IfaceType
-  | IfaceDFunTy   IfaceType IfaceType
-  | IfaceForAllTy IfaceForAllBndr IfaceType
-  | IfaceTyConApp IfaceTyCon IfaceTcArgs  -- Not necessarily saturated
-                                          -- Includes newtypes, synonyms, tuples
+  = IfaceFreeTyVar TyVar                 -- See Note [Free tyvars in IfaceType]
+  | IfaceTyVar     IfLclName            -- Type/coercion variable only, not tycon
+  | IfaceLitTy     IfaceTyLit
+  | IfaceAppTy     IfaceType IfaceType
+  | IfaceFunTy     IfaceType IfaceType
+  | IfaceDFunTy    IfaceType IfaceType
+  | IfaceForAllTy  IfaceForAllBndr IfaceType
+  | IfaceTyConApp  IfaceTyCon IfaceTcArgs  -- Not necessarily saturated
+                                           -- Includes newtypes, synonyms, tuples
   | IfaceCastTy     IfaceType IfaceCoercion
   | IfaceCoercionTy IfaceCoercion
 
@@ -186,7 +186,7 @@ data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
                       -- details.
                     deriving (Eq)
 
-{- Note [TcTyVars in IfaceType]
+{- Note [Free tyvars in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to an
 IfaceType and pretty printing that.  This eliminates a lot of
@@ -198,11 +198,11 @@ when using -ddump-tc-trace) we print a lot of /open/ types.  These
 types are full of TcTyVars, and it's absolutely crucial to print them
 in their full glory, with their unique, TcTyVarDetails etc.
 
-So we simply embed a TcTyVar in IfaceType with the IfaceTcTyVar constructor.
+So we simply embed a TyVar in IfaceType with the IfaceFreeTyVar constructor.
 Note that:
 
-* We never expect to serialise an IfaceTcTyVar into an interface file, nor
-  to deserialise one.  IfaceTcTyVar is used only in the "convert to IfaceType
+* We never expect to serialise an IfaceFreeTyVar into an interface file, nor
+  to deserialise one.  IfaceFreeTyVar is used only in the "convert to IfaceType
   and then pretty-print" pipeline.
 
 
@@ -345,7 +345,7 @@ ifTypeIsVarFree :: IfaceType -> Bool
 ifTypeIsVarFree ty = go ty
   where
     go (IfaceTyVar {})         = False
-    go (IfaceTcTyVar {})       = False
+    go (IfaceFreeTyVar {})     = False
     go (IfaceAppTy fun arg)    = go fun && go arg
     go (IfaceFunTy arg res)    = go arg && go res
     go (IfaceDFunTy arg res)   = go arg && go res
@@ -375,7 +375,7 @@ substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
 substIfaceType env ty
   = go ty
   where
-    go (IfaceTcTyVar tv)      = IfaceTcTyVar tv
+    go (IfaceFreeTyVar tv)    = IfaceFreeTyVar tv
     go (IfaceTyVar tv)        = substIfaceTyVar env tv
     go (IfaceAppTy  t1 t2)    = IfaceAppTy  (go t1) (go t2)
     go (IfaceFunTy  t1 t2)    = IfaceFunTy  (go t1) (go t2)
@@ -473,7 +473,7 @@ extendIfRnEnv2 IRV2 { ifenvL = lenv
 
 -- See Note [No kind check in ifaces]
 eqIfaceType :: IfRnEnv2 -> IfaceType -> IfaceType -> Bool
-eqIfaceType _ (IfaceTcTyVar tv1) (IfaceTcTyVar tv2)
+eqIfaceType _ (IfaceFreeTyVar tv1) (IfaceFreeTyVar tv2)
     = tv1 == tv2   -- Should not happen
 eqIfaceType env (IfaceTyVar tv1) (IfaceTyVar tv2) =
     case (rnIfOccL env tv1, rnIfOccR env tv2) of
@@ -667,7 +667,7 @@ pprIfaceType       = eliminateRuntimeRep (ppr_ty TopPrec)
 pprParendIfaceType = eliminateRuntimeRep (ppr_ty TyConPrec)
 
 ppr_ty :: TyPrec -> IfaceType -> SDoc
-ppr_ty _         (IfaceTcTyVar tyvar)   = ppr tyvar  -- This is the main reson for IfaceTcTyVar!
+ppr_ty _         (IfaceFreeTyVar tyvar) = ppr tyvar  -- This is the main reson for IfaceFreeTyVar!
 ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar  -- See Note [TcTyVars in IfaceType]
 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = pprTyTcApp ctxt_prec tc tys
 ppr_ty _         (IfaceTupleTy i p tys) = pprTuple i p tys
@@ -1322,8 +1322,8 @@ pprIfaceContext [pred] = ppr_ty TyOpPrec pred
 pprIfaceContext preds  = parens (fsep (punctuate comma (map ppr preds)))
 
 instance Binary IfaceType where
-    put_ _ (IfaceTcTyVar tv)
-       = pprPanic "Can't serialise IfaceTcTyVar" (ppr tv)
+    put_ _ (IfaceFreeTyVar tv)
+       = pprPanic "Can't serialise IfaceFreeTyVar" (ppr tv)
 
     put_ bh (IfaceForAllTy aa ab) = do
             putByte bh 0
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index a920945e16..002df8d6ef 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -1177,7 +1177,7 @@ tcIfaceType :: IfaceType -> IfL Type
 tcIfaceType = go
   where
     go (IfaceTyVar n)         = TyVarTy <$> tcIfaceTyVar n
-    go (IfaceTcTyVar n)       = pprPanic "tcIfaceType:IfaceTcTyVar" (ppr n)
+    go (IfaceFreeTyVar n)     = pprPanic "tcIfaceType:IfaceFreeTyVar" (ppr n)
     go (IfaceAppTy t1 t2)     = AppTy <$> go t1 <*> go t2
     go (IfaceLitTy l)         = LitTy <$> tcIfaceTyLit l
     go (IfaceFunTy t1 t2)     = FunTy <$> go t1 <*> go t2
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index c0229b8e62..97d25129f2 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -11,7 +11,7 @@ module ToIface
     , toIfaceTyVarBinders
     , toIfaceTyVar
       -- * Types
-    , toIfaceType
+    , toIfaceType, toIfaceTypeX
     , toIfaceKind
     , toIfaceTcArgs
     , toIfaceTyCon
@@ -64,6 +64,7 @@ import FastString
 import Util
 import Var
 import VarEnv
+import VarSet
 import TyCoRep
 import Demand ( isTopSig )
 
@@ -105,44 +106,51 @@ toIfaceKind = toIfaceType
 
 ---------------------
 toIfaceType :: Type -> IfaceType
+toIfaceType = toIfaceTypeX emptyVarSet
+
+toIfaceTypeX :: VarSet -> Type -> IfaceType
+-- (toIfaceTypeX free ty)
+--    translates the tyvars in 'free' as IfaceFreeTyVars
+--
 -- Synonyms are retained in the interface type
-toIfaceType (TyVarTy tv)   -- See Note [TcTyVars in IfaceType] in IfaceType
-  | isTcTyVar tv            = IfaceTcTyVar tv
-  | otherwise               = IfaceTyVar (toIfaceTyVar tv)
-toIfaceType (AppTy t1 t2)   = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
-toIfaceType (LitTy n)       = IfaceLitTy (toIfaceTyLit n)
-toIfaceType (ForAllTy b t)  = IfaceForAllTy (toIfaceForAllBndr b) (toIfaceType t)
-toIfaceType (FunTy t1 t2)
-  | isPredTy t1             = IfaceDFunTy (toIfaceType t1) (toIfaceType t2)
-  | otherwise               = IfaceFunTy  (toIfaceType t1) (toIfaceType t2)
-toIfaceType (CastTy ty co)  = IfaceCastTy (toIfaceType ty) (toIfaceCoercion co)
-toIfaceType (CoercionTy co) = IfaceCoercionTy (toIfaceCoercion co)
-
-toIfaceType (TyConApp tc tys)
+toIfaceTypeX fr (TyVarTy tv)   -- See Note [TcTyVars in IfaceType] in IfaceType
+  | tv `elemVarSet` fr         = IfaceFreeTyVar tv
+  | otherwise                  = IfaceTyVar (toIfaceTyVar tv)
+toIfaceTypeX fr (AppTy t1 t2)  = IfaceAppTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
+toIfaceTypeX _  (LitTy n)      = IfaceLitTy (toIfaceTyLit n)
+toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndr b)
+                                               (toIfaceTypeX (fr `delVarSet` binderVar b) t)
+toIfaceTypeX fr (FunTy t1 t2)
+  | isPredTy t1                 = IfaceDFunTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
+  | otherwise                   = IfaceFunTy  (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
+toIfaceTypeX fr (CastTy ty co)  = IfaceCastTy (toIfaceTypeX fr ty) (toIfaceCoercionX fr co)
+toIfaceTypeX fr (CoercionTy co) = IfaceCoercionTy (toIfaceCoercionX fr co)
+
+toIfaceTypeX fr (TyConApp tc tys)
     -- tuples
   | Just sort <- tyConTuple_maybe tc
   , n_tys == arity
-  = IfaceTupleTy sort IsNotPromoted (toIfaceTcArgs tc tys)
+  = IfaceTupleTy sort IsNotPromoted (toIfaceTcArgsX fr tc tys)
 
   | Just dc <- isPromotedDataCon_maybe tc
   , isTupleDataCon dc
   , n_tys == 2*arity
-  = IfaceTupleTy BoxedTuple IsPromoted (toIfaceTcArgs tc (drop arity tys))
+  = IfaceTupleTy BoxedTuple IsPromoted (toIfaceTcArgsX fr tc (drop arity tys))
 
     -- type equalities: see Note [Equality predicates in IfaceType]
   | tyConName tc == eqTyConName
   = let info = IfaceTyConInfo IsNotPromoted (IfaceEqualityTyCon True)
-    in IfaceTyConApp (IfaceTyCon (tyConName tc) info) (toIfaceTcArgs tc tys)
+    in IfaceTyConApp (IfaceTyCon (tyConName tc) info) (toIfaceTcArgsX fr tc tys)
 
   | tc `elem` [ eqPrimTyCon, eqReprPrimTyCon, heqTyCon ]
   , [k1, k2, _t1, _t2] <- tys
   = let homogeneous = k1 `eqType` k2
         info = IfaceTyConInfo IsNotPromoted (IfaceEqualityTyCon homogeneous)
-    in IfaceTyConApp (IfaceTyCon (tyConName tc) info) (toIfaceTcArgs tc tys)
+    in IfaceTyConApp (IfaceTyCon (tyConName tc) info) (toIfaceTcArgsX fr tc tys)
 
     -- other applications
   | otherwise
-  = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTcArgs tc tys)
+  = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTcArgsX fr tc tys)
   where
     arity = tyConArity tc
     n_tys = length tys
@@ -200,50 +208,63 @@ toIfaceTyLit (StrTyLit x) = IfaceStrTyLit x
 
 ----------------
 toIfaceCoercion :: Coercion -> IfaceCoercion
-toIfaceCoercion (Refl r ty)         = IfaceReflCo r (toIfaceType ty)
-toIfaceCoercion co@(TyConAppCo r tc cos)
-  | tc `hasKey` funTyConKey
-  , [_,_,_,_] <- cos                = pprPanic "toIfaceCoercion" (ppr co)
-  | otherwise                       = IfaceTyConAppCo r (toIfaceTyCon tc)
-                                                        (map toIfaceCoercion cos)
-toIfaceCoercion (AppCo co1 co2)     = IfaceAppCo  (toIfaceCoercion co1)
-                                                  (toIfaceCoercion co2)
-toIfaceCoercion (ForAllCo tv k co)  = IfaceForAllCo (toIfaceTvBndr tv)
-                                                    (toIfaceCoercion k)
-                                                    (toIfaceCoercion co)
-toIfaceCoercion (FunCo r co1 co2)   = IfaceFunCo r (toIfaceCoercion co1)
-                                                   (toIfaceCoercion co2)
-toIfaceCoercion (CoVarCo cv)        = IfaceCoVarCo  (toIfaceCoVar cv)
-toIfaceCoercion (AxiomInstCo con ind cos)
-                                    = IfaceAxiomInstCo (coAxiomName con) ind
-                                                       (map toIfaceCoercion cos)
-toIfaceCoercion (UnivCo p r t1 t2)  = IfaceUnivCo (toIfaceUnivCoProv p) r
-                                                  (toIfaceType t1)
-                                                  (toIfaceType t2)
-toIfaceCoercion (SymCo co)          = IfaceSymCo (toIfaceCoercion co)
-toIfaceCoercion (TransCo co1 co2)   = IfaceTransCo (toIfaceCoercion co1)
-                                                   (toIfaceCoercion co2)
-toIfaceCoercion (NthCo d co)        = IfaceNthCo d (toIfaceCoercion co)
-toIfaceCoercion (LRCo lr co)        = IfaceLRCo lr (toIfaceCoercion co)
-toIfaceCoercion (InstCo co arg)     = IfaceInstCo (toIfaceCoercion co)
-                                                  (toIfaceCoercion arg)
-toIfaceCoercion (CoherenceCo c1 c2) = IfaceCoherenceCo (toIfaceCoercion c1)
-                                                       (toIfaceCoercion c2)
-toIfaceCoercion (KindCo c)          = IfaceKindCo (toIfaceCoercion c)
-toIfaceCoercion (SubCo co)          = IfaceSubCo (toIfaceCoercion co)
-toIfaceCoercion (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co)
-                                          (map toIfaceCoercion cs)
-
-toIfaceUnivCoProv :: UnivCoProvenance -> IfaceUnivCoProv
-toIfaceUnivCoProv UnsafeCoerceProv    = IfaceUnsafeCoerceProv
-toIfaceUnivCoProv (PhantomProv co)    = IfacePhantomProv (toIfaceCoercion co)
-toIfaceUnivCoProv (ProofIrrelProv co) = IfaceProofIrrelProv (toIfaceCoercion co)
-toIfaceUnivCoProv (PluginProv str)    = IfacePluginProv str
-toIfaceUnivCoProv (HoleProv h)        = IfaceHoleProv (chUnique h)
+toIfaceCoercion = toIfaceCoercionX emptyVarSet
+
+toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
+-- (toIfaceCoercionX free ty)
+--    translates the tyvars in 'free' as IfaceFreeTyVars
+toIfaceCoercionX fr co
+  = go co
+  where
+    go (Refl r ty)          = IfaceReflCo r (toIfaceType ty)
+    go (CoVarCo cv)         = IfaceCoVarCo  (toIfaceCoVar cv)
+    go (AppCo co1 co2)      = IfaceAppCo  (go co1) (go co2)
+    go (SymCo co)           = IfaceSymCo (go co)
+    go (TransCo co1 co2)    = IfaceTransCo (go co1) (go co2)
+    go (NthCo d co)         = IfaceNthCo d (go co)
+    go (LRCo lr co)         = IfaceLRCo lr (go co)
+    go (InstCo co arg)      = IfaceInstCo (go co) (go arg)
+    go (CoherenceCo c1 c2)  = IfaceCoherenceCo (go c1) (go c2)
+    go (KindCo c)           = IfaceKindCo (go c)
+    go (SubCo co)           = IfaceSubCo (go co)
+    go (AxiomRuleCo co cs)  = IfaceAxiomRuleCo (coaxrName co) (map go cs)
+    go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs)
+    go (UnivCo p r t1 t2)   = IfaceUnivCo (go_prov p) r
+                                          (toIfaceTypeX fr t1)
+                                          (toIfaceTypeX fr t2)
+    go (TyConAppCo r tc cos)
+      | tc `hasKey` funTyConKey
+      , [_,_,_,_] <- cos         = pprPanic "toIfaceCoercion" (ppr co)
+      | otherwise                = IfaceTyConAppCo r (toIfaceTyCon tc) (map go cos)
+    go (FunCo r co1 co2)    = IfaceFunCo r (toIfaceCoercion co1)
+                                           (toIfaceCoercion co2)
+
+    go (ForAllCo tv k co) = IfaceForAllCo (toIfaceTvBndr tv)
+                                          (toIfaceCoercionX fr' k)
+                                          (toIfaceCoercionX fr' co)
+                          where
+                            fr' = fr `delVarSet` tv
+
+    go_prov :: UnivCoProvenance -> IfaceUnivCoProv
+    go_prov UnsafeCoerceProv    = IfaceUnsafeCoerceProv
+    go_prov (PhantomProv co)    = IfacePhantomProv (go co)
+    go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
+    go_prov (PluginProv str)    = IfacePluginProv str
+    go_prov (HoleProv h)        = IfaceHoleProv (chUnique h)
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
+toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
+
+toIfaceTcArgsX :: VarSet -> TyCon -> [Type] -> IfaceTcArgs
 -- See Note [Suppressing invisible arguments]
-toIfaceTcArgs tc ty_args
+-- We produce a result list of args describing visiblity
+-- The awkward case is
+--    T :: forall k. * -> k
+-- And consider
+--    T (forall j. blah) * blib
+-- Is 'blib' visible?  It depends on the visibility flag on j,
+-- so we have to substitute for k.  Annoying!
+toIfaceTcArgsX fr tc ty_args
   = go (mkEmptyTCvSubst in_scope) (tyConKind tc) ty_args
   where
     in_scope = mkInScopeSet (tyCoVarsOfTypes ty_args)
@@ -256,16 +277,16 @@ toIfaceTcArgs tc ty_args
       | isVisibleArgFlag vis = ITC_Vis   t' ts'
       | otherwise            = ITC_Invis t' ts'
       where
-        t'  = toIfaceType t
+        t'  = toIfaceTypeX fr t
         ts' = go (extendTvSubst env tv t) res ts
 
     go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
-      = ITC_Vis (toIfaceType t) (go env res ts)
+      = ITC_Vis (toIfaceTypeX fr t) (go env res ts)
 
     go env (TyVarTy tv) ts
       | Just ki <- lookupTyVar env tv = go env ki ts
     go env kind (t:ts) = WARN( True, ppr tc $$ ppr (tyConKind tc) $$ ppr ty_args )
-                         ITC_Vis (toIfaceType t) (go env kind ts) -- Ill-kinded
+                         ITC_Vis (toIfaceTypeX fr t) (go env kind ts) -- Ill-kinded
 
 tidyToIfaceType :: TidyEnv -> Type -> IfaceType
 tidyToIfaceType env ty = toIfaceType (tidyType env ty)
diff --git a/compiler/iface/ToIface.hs-boot b/compiler/iface/ToIface.hs-boot
index bf6c120d8e..04ceab673f 100644
--- a/compiler/iface/ToIface.hs-boot
+++ b/compiler/iface/ToIface.hs-boot
@@ -4,9 +4,11 @@ import {-# SOURCE #-} TyCoRep
 import {-# SOURCE #-} IfaceType
 import Var ( TyVar, TyVarBinder )
 import TyCon ( TyCon )
+import VarSet( VarSet )
 
 -- For TyCoRep
 toIfaceType :: Type -> IfaceType
+toIfaceTypeX :: VarSet -> Type -> IfaceType
 toIfaceTyLit :: TyLit -> IfaceTyLit
 toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
 toIfaceTvBndr :: TyVar -> IfaceTvBndr
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index f0ca574cd4..67eb982b91 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1765,8 +1765,9 @@ tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
 tyCoFVsOfImplic :: Implication -> FV
 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
 tyCoFVsOfImplic (Implic { ic_skols = skols
-                         , ic_given = givens, ic_wanted = wanted })
-  = FV.delFVs (mkVarSet skols)
+                        , ic_given = givens
+                        , ic_wanted = wanted })
+  = FV.delFVs (mkVarSet skols `unionVarSet` mkVarSet givens)
       (tyCoFVsOfWC wanted `unionFV` tyCoFVsOfTypes (map evVarPred givens))
 
 tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1e90fa7aee..6b693ef97b 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -61,7 +61,7 @@ module TyCoRep (
         pprTyVar, pprTyVars,
         pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprTyLit,
-        TyPrec(..), maybeParen, pprTcAppCo, pprTcAppTy,
+        TyPrec(..), maybeParen, pprTcAppCo,
         pprPrefixApp, pprArrowChain,
         pprDataCons, ppSuggestExplicitKinds,
 
@@ -137,12 +137,14 @@ import {-# SOURCE #-} DataCon( dataConFullSig
                              , DataCon, filterEqSpec )
 import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
                           , tyCoVarsOfTypesWellScoped
+                          , tyCoVarsOfTypeWellScoped
                           , coreView, typeKind )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
 import {-# SOURCE #-} Coercion
 import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
-import {-# SOURCE #-} ToIface
+import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
+                             , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercion )
 
 -- friends:
 import IfaceType
@@ -2460,7 +2462,14 @@ pprParendKind = pprParendType
 tidyToIfaceType :: Type -> IfaceType
 -- It's vital to tidy before converting to an IfaceType
 -- or nested binders will become indistinguishable!
-tidyToIfaceType = toIfaceType . tidyTopType
+--
+-- Also for the free type variables, tell toIfaceTypeX to
+-- leave them as IfaceFreeTyVar.  This is super-important
+-- for debug printing.
+tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty)
+  where
+    env       = tidyFreeTyCoVars emptyTidyEnv free_tcvs
+    free_tcvs = tyCoVarsOfTypeWellScoped ty
 
 ------------
 pprClassPred :: Class -> [Type] -> SDoc
@@ -2483,7 +2492,7 @@ instance Outputable TyLit where
 ------------------
 
 pprSigmaType :: Type -> SDoc
-pprSigmaType = (pprIfaceSigmaType ShowForAllWhen) . tidyToIfaceType
+pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType
 
 pprForAll :: [TyVarBinder] -> SDoc
 pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs)
@@ -2578,12 +2587,10 @@ pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
 
 
 pprTypeApp :: TyCon -> [Type] -> SDoc
-pprTypeApp = pprTcAppTy TopPrec
-
-pprTcAppTy :: TyPrec -> TyCon -> [Type] -> SDoc
-pprTcAppTy p tc tys
+pprTypeApp tc tys
+  = pprIfaceTypeApp TopPrec (toIfaceTyCon tc)
+                            (toIfaceTcArgs tc tys)
     -- TODO: toIfaceTcArgs seems rather wasteful here
-  = pprIfaceTypeApp p (toIfaceTyCon tc) (toIfaceTcArgs tc tys)
 
 pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc)
            -> TyCon -> [Coercion] -> SDoc
@@ -2649,16 +2656,16 @@ getHelpfulOccName tyvar = occ1
   where
     name = tyVarName tyvar
     occ  = getOccName name
-    -- System Names are for unification variables;
+    -- A TcTyVar with a System Name is probably a unification variable;
     -- when we tidy them we give them a trailing "0" (or 1 etc)
     -- so that they don't take precedence for the un-modified name
     -- Plus, indicating a unification variable in this way is a
     -- helpful clue for users
     occ1 | isSystemName name
-         = if isTyVar tyvar
-           then mkTyVarOcc (occNameString occ ++ "0")
-           else mkVarOcc   (occNameString occ ++ "0")
-         | otherwise         = occ
+         , isTcTyVar tyvar
+         = mkTyVarOcc (occNameString occ ++ "0")
+         | otherwise
+         = occ
 
 tidyTyVarBinder :: TidyEnv -> TyVarBndr TyVar vis
                 -> (TidyEnv, TyVarBndr TyVar vis)
@@ -2820,7 +2827,7 @@ tidyCos env = map (tidyCo env)
 --     recursion across a hi-boot file, we don't get the CPR property
 --     and these functions allocate a tremendous amount of rubbish.
 --     It's not critical (because typeSize is really only used in
---     debug mode, but I tripped over and example (T5642) in which
+--     debug mode, but I tripped over an example (T5642) in which
 --     typeSize was one of the biggest single allocators in all of GHC.
 --     And it's easy to fix, so I did.
 
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 460eb5e5e4..6c01c741b0 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -187,7 +187,7 @@ module Type (
         pprTheta, pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprSourceTyCon,
         TyPrec(..), maybeParen,
-        pprTyVar, pprTyVars, pprTcAppTy, pprPrefixApp, pprArrowChain,
+        pprTyVar, pprTyVars, pprPrefixApp, pprArrowChain,
 
         -- * Tidying type related things up for printing
         tidyType,      tidyTypes,
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index 560c251f1b..ceeba1bad8 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -22,5 +22,6 @@ partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
 coreView :: Type -> Maybe Type
 
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
+tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
 
 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])