Refine the suppression of RuntimeRep variables
[ghc.git] / compiler / iface / IfaceType.hs
index dbca426..f4032d2 100644 (file)
@@ -7,35 +7,39 @@ This module defines interface types and binders
 -}
 
 {-# LANGUAGE CPP, FlexibleInstances, BangPatterns #-}
 -}
 
 {-# LANGUAGE CPP, FlexibleInstances, BangPatterns #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TupleSections #-}
     -- FlexibleInstances for Binary (DefMethSpec IfaceType)
 
 module IfaceType (
         IfExtName, IfLclName,
 
         IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
     -- FlexibleInstances for Binary (DefMethSpec IfaceType)
 
 module IfaceType (
         IfExtName, IfLclName,
 
         IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
+        IfaceMCoercion(..),
         IfaceUnivCoProv(..),
         IfaceUnivCoProv(..),
-        IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..), IsPromoted(..),
-        IfaceTyLit(..), IfaceTcArgs(..),
+        IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..),
+        IfaceTyLit(..), IfaceAppArgs(..),
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
-        IfaceForAllBndr, ArgFlag(..),
+        IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
+        mkIfaceForAllTvBndr,
 
 
-        ifTyConBinderTyVar, ifTyConBinderName,
+        ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
+        ifTyConBinderVar, ifTyConBinderName,
 
         -- Equality testing
 
         -- Equality testing
-        IfRnEnv2, emptyIfRnEnv2, eqIfaceType, eqIfaceTypes,
-        eqIfaceTcArgs, eqIfaceTvBndrs, isIfaceLiftedTypeKind,
+        isIfaceLiftedTypeKind,
 
 
-        -- Conversion from IfaceTcArgs -> [IfaceType]
-        tcArgsIfaceTypes,
+        -- Conversion from IfaceAppArgs to IfaceTypes/ArgFlags
+        appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
 
         -- Printing
 
         -- Printing
-        pprIfaceType, pprParendIfaceType,
+        pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
         pprIfaceContext, pprIfaceContextArr,
         pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
         pprIfaceContext, pprIfaceContextArr,
         pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
-        pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
-        pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType,
-        pprIfaceTyLit,
+        pprIfaceBndrs, pprIfaceAppArgs, pprParendIfaceAppArgs,
+        pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
+        pprIfaceSigmaType, pprIfaceTyLit,
         pprIfaceCoercion, pprParendIfaceCoercion,
         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
         pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
         pprIfaceCoercion, pprParendIfaceCoercion,
         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
         pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
@@ -43,16 +47,19 @@ module IfaceType (
         suppressIfaceInvisibles,
         stripIfaceInvisVars,
         stripInvisArgs,
         suppressIfaceInvisibles,
         stripIfaceInvisVars,
         stripInvisArgs,
-        substIfaceType, substIfaceTyVar, substIfaceTcArgs, mkIfaceTySubst,
-        eqIfaceTvBndr
+
+        mkIfaceTySubst, substIfaceTyVar, substIfaceAppArgs, inDomIfaceTySubst
     ) where
 
 #include "HsVersions.h"
 
     ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TysWiredIn ( ptrRepLiftedDataConTyCon )
+import GhcPrelude
+
+import {-# SOURCE #-} TysWiredIn ( coercibleTyCon, heqTyCon
+                                 , liftedRepDataConTyCon )
+import {-# SOURCE #-} TyCoRep    ( isRuntimeRepTy )
 
 import DynFlags
 
 import DynFlags
-import StaticFlags ( opt_PprStyle_Debug )
 import TyCon hiding ( pprPromotionQuote )
 import CoAxiom
 import Var
 import TyCon hiding ( pprPromotionQuote )
 import CoAxiom
 import Var
@@ -63,10 +70,10 @@ import Binary
 import Outputable
 import FastString
 import FastStringEnv
 import Outputable
 import FastString
 import FastStringEnv
-import UniqFM
 import Util
 
 import Util
 
-import Data.List (foldl')
+import Data.Maybe( isJust )
+import qualified Data.Semigroup as Semi
 
 {-
 ************************************************************************
 
 {-
 ************************************************************************
@@ -91,6 +98,13 @@ type IfaceTvBndr  = (IfLclName, IfaceKind)
 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
 ifaceTvBndrName (n,_) = n
 
 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
 ifaceTvBndrName (n,_) = n
 
+ifaceIdBndrName :: IfaceIdBndr -> IfLclName
+ifaceIdBndrName (n,_) = n
+
+ifaceBndrName :: IfaceBndr -> IfLclName
+ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr
+ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr
+
 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
 
 data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
 
 data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
@@ -109,23 +123,30 @@ data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
 -------------------------------
 type IfaceKind     = IfaceType
 
 -------------------------------
 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
+-- | A kind of universal type, used for types and kinds.
+--
+-- Any time a 'Type' is pretty-printed, it is first converted to an 'IfaceType'
+-- before being printed. See Note [Pretty printing via IfaceSyn] in PprTyThing
+data IfaceType
+  = IfaceFreeTyVar TyVar                -- See Note [Free tyvars in IfaceType]
+  | IfaceTyVar     IfLclName            -- Type/coercion variable only, not tycon
+  | IfaceLitTy     IfaceTyLit
+  | IfaceAppTy     IfaceType IfaceAppArgs
+                             -- See Note [Suppressing invisible arguments] for
+                             -- an explanation of why the second field isn't
+                             -- IfaceType, analogous to AppTy.
+  | IfaceFunTy     IfaceType IfaceType
+  | IfaceDFunTy    IfaceType IfaceType
+  | IfaceForAllTy  IfaceForAllBndr IfaceType
+  | IfaceTyConApp  IfaceTyCon IfaceAppArgs  -- Not necessarily saturated
+                                            -- Includes newtypes, synonyms, tuples
   | IfaceCastTy     IfaceType IfaceCoercion
   | IfaceCoercionTy IfaceCoercion
 
   | IfaceTupleTy                  -- Saturated tuples (unsaturated ones use IfaceTyConApp)
        TupleSort                  -- What sort of tuple?
   | IfaceCastTy     IfaceType IfaceCoercion
   | IfaceCoercionTy IfaceCoercion
 
   | IfaceTupleTy                  -- Saturated tuples (unsaturated ones use IfaceTyConApp)
        TupleSort                  -- What sort of tuple?
-       IsPromoted                 -- A bit like IfaceTyCon
-       IfaceTcArgs                -- arity = length args
+       PromotionFlag                 -- A bit like IfaceTyCon
+       IfaceAppArgs               -- arity = length args
           -- For promoted data cons, the kind args are omitted
 
 type IfacePredType = IfaceType
           -- For promoted data cons, the kind args are omitted
 
 type IfacePredType = IfaceType
@@ -136,25 +157,38 @@ data IfaceTyLit
   | IfaceStrTyLit FastString
   deriving (Eq)
 
   | IfaceStrTyLit FastString
   deriving (Eq)
 
-type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis
-type IfaceForAllBndr  = TyVarBndr IfaceTvBndr ArgFlag
-
--- See Note [Suppressing invisible arguments]
--- We use a new list type (rather than [(IfaceType,Bool)], because
--- it'll be more compact and faster to parse in interface
--- files. Rather than two bytes and two decisions (nil/cons, and
--- type/kind) there'll just be one.
-data IfaceTcArgs
-  = ITC_Nil
-  | ITC_Vis   IfaceType IfaceTcArgs   -- "Vis" means show when pretty-printing
-  | ITC_Invis IfaceKind IfaceTcArgs   -- "Invis" means don't show when pretty-printing
-                                      --         except with -fprint-explicit-kinds
-
-instance Monoid IfaceTcArgs where
-  mempty = ITC_Nil
-  ITC_Nil `mappend` xs           = xs
-  ITC_Vis ty rest `mappend` xs   = ITC_Vis ty (rest `mappend` xs)
-  ITC_Invis ki rest `mappend` xs = ITC_Invis ki (rest `mappend` xs)
+type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
+type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
+
+-- | Make an 'IfaceForAllBndr' from an 'IfaceTvBndr'.
+mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr
+mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis
+
+-- | Stores the arguments in a type application as a list.
+-- See @Note [Suppressing invisible arguments]@.
+data IfaceAppArgs
+  = IA_Nil
+  | IA_Arg IfaceType    -- The type argument
+
+           ArgFlag      -- The argument's visibility. We store this here so
+                        -- that we can:
+                        --
+                        -- 1. Avoid pretty-printing invisible (i.e., specified
+                        --    or inferred) arguments when
+                        --    -fprint-explicit-kinds isn't enabled, or
+                        -- 2. When -fprint-explicit-kinds *is*, enabled, print
+                        --    specified arguments in @(...) and inferred
+                        --    arguments in @{...}.
+
+           IfaceAppArgs -- The rest of the arguments
+
+instance Semi.Semigroup IfaceAppArgs where
+  IA_Nil <> xs              = xs
+  IA_Arg ty argf rest <> xs = IA_Arg ty argf (rest Semi.<> xs)
+
+instance Monoid IfaceAppArgs where
+  mempty = IA_Nil
+  mappend = (Semi.<>)
 
 -- Encodes type constructors, kind constructors,
 -- coercion constructors, the lot.
 
 -- Encodes type constructors, kind constructors,
 -- coercion constructors, the lot.
@@ -164,10 +198,6 @@ data IfaceTyCon = IfaceTyCon { ifaceTyConName :: IfExtName
                              , ifaceTyConInfo :: IfaceTyConInfo }
     deriving (Eq)
 
                              , ifaceTyConInfo :: IfaceTyConInfo }
     deriving (Eq)
 
--- | Is a TyCon a promoted data constructor or just a normal type constructor?
-data IsPromoted = IsNotPromoted | IsPromoted
-    deriving (Eq)
-
 -- | The various types of TyCons which have special, built-in syntax.
 data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
 
 -- | The various types of TyCons which have special, built-in syntax.
 data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
 
@@ -180,103 +210,143 @@ data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
                     | IfaceSumTyCon !Arity
                       -- ^ e.g. @(a | b | c)@
 
                     | IfaceSumTyCon !Arity
                       -- ^ e.g. @(a | b | c)@
 
-                    | IfaceEqualityTyCon !Bool
-                      -- ^ a type equality. 'True' indicates kind-homogeneous.
-                      -- See Note [Equality predicates in IfaceType] for
-                      -- details.
+                    | IfaceEqualityTyCon
+                      -- ^ A heterogeneous equality TyCon
+                      --   (i.e. eqPrimTyCon, eqReprPrimTyCon, heqTyCon)
+                      -- that is actually being applied to two types
+                      -- of the same kind.  This affects pretty-printing
+                      -- only: see Note [Equality predicates in IfaceType]
                     deriving (Eq)
 
                     deriving (Eq)
 
-{- Note [TcTyVars in IfaceType]
+{- Note [Free tyvars in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Nowadays (since Nov 16) we pretty-print a Type by converting to an
-IfaceType and pretty printing that.  This eliminates a lot of
-pretty-print duplication, and it matches what we do with
-pretty-printing TyThings.
+Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
+an IfaceType and pretty printing that.  This eliminates a lot of
+pretty-print duplication, and it matches what we do with pretty-
+printing TyThings. See Note [Pretty printing via IfaceSyn] in PprTyThing.
 
 It works fine for closed types, but when printing debug traces (e.g.
 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.
 
 
 It works fine for closed types, but when printing debug traces (e.g.
 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:
 
 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.
 
   and then pretty-print" pipeline.
 
+We do the same for covars, naturally.
 
 Note [Equality predicates in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC has several varieties of type equality (see Note [The equality types story]
 
 Note [Equality predicates in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC has several varieties of type equality (see Note [The equality types story]
-in TysPrim for details) which all must be rendered with different surface syntax
-during pretty-printing. Which syntax we use depends upon,
-
- 1. Which predicate tycon was used
- 2. Whether the types being compared are of the same kind.
-
-Unfortunately, determining (2) from an IfaceType isn't possible since we can't
-see through type synonyms. Consequently, we need to record whether the equality
-is homogeneous or not in IfaceTyConSort for the purposes of pretty-printing.
-
-Namely we handle these cases,
-
-    Predicate               Homogeneous        Heterogeneous
-    ----------------        -----------        -------------
-    eqTyCon                 ~                  N/A
-    heqTyCon                ~                  ~~
-    eqPrimTyCon             ~#                 ~~
-    eqReprPrimTyCon         Coercible          Coercible
-
+in TysPrim for details).  In an effort to avoid confusing users, we suppress
+the differences during pretty printing unless certain flags are enabled.
+Here is how each equality predicate* is printed in homogeneous and
+heterogeneous contexts, depending on which combination of the
+-fprint-explicit-kinds and -fprint-equality-relations flags is used:
+
+--------------------------------------------------------------------------------------------
+|         Predicate             |        Neither flag        |    -fprint-explicit-kinds   |
+|-------------------------------|----------------------------|-----------------------------|
+| a ~ b         (homogeneous)   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| a ~# b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
+| a ~# b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      homogeneously   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
+|-------------------------------|----------------------------|-----------------------------|
+|         Predicate             | -fprint-equality-relations |          Both flags         |
+|-------------------------------|----------------------------|-----------------------------|
+| a ~ b         (homogeneous)   |        a ~  b              | (a :: Type) ~  (b :: Type)  |
+| a ~~ b,       homogeneously   |        a ~~ b              | (a :: Type) ~~ (b :: Type)  |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
+| a ~# b,       homogeneously   |        a ~# b              | (a :: Type) ~# (b :: Type)  |
+| a ~# b,       heterogeneously |        a ~# c              | (a :: Type) ~# (c :: k)     |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
+| a ~R# b,      homogeneously   |        a ~R# b             | (a :: Type) ~R# (b :: Type) |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
+--------------------------------------------------------------------------------------------
+
+(* There is no heterogeneous, representational, lifted equality counterpart
+to (~~). There could be, but there seems to be no use for it.)
+
+This table adheres to the following rules:
+
+A. With -fprint-equality-relations, print the true equality relation.
+B. Without -fprint-equality-relations:
+     i. If the equality is representational and homogeneous, use Coercible.
+    ii. Otherwise, if the equality is representational, use ~R#.
+   iii. If the equality is nominal and homogeneous, use ~.
+    iv. Otherwise, if the equality is nominal, use ~~.
+C. With -fprint-explicit-kinds, print kinds on both sides of an infix operator,
+   as above; or print the kind with Coercible.
+D. Without -fprint-explicit-kinds, don't print kinds.
+
+A hetero-kinded equality is used homogeneously when it is applied to two
+identical kinds. Unfortunately, determining this from an IfaceType isn't
+possible since we can't see through type synonyms. Consequently, we need to
+record whether this particular application is homogeneous in IfaceTyConSort
+for the purposes of pretty-printing.
+
+See Note [The equality types story] in TysPrim.
 -}
 
 data IfaceTyConInfo   -- Used to guide pretty-printing
                       -- and to disambiguate D from 'D (they share a name)
 -}
 
 data IfaceTyConInfo   -- Used to guide pretty-printing
                       -- and to disambiguate D from 'D (they share a name)
-  = IfaceTyConInfo { ifaceTyConIsPromoted :: IsPromoted
+  = IfaceTyConInfo { ifaceTyConIsPromoted :: PromotionFlag
                    , ifaceTyConSort       :: IfaceTyConSort }
     deriving (Eq)
 
                    , ifaceTyConSort       :: IfaceTyConSort }
     deriving (Eq)
 
+data IfaceMCoercion
+  = IfaceMRefl
+  | IfaceMCo IfaceCoercion
+
 data IfaceCoercion
 data IfaceCoercion
-  = IfaceReflCo       Role IfaceType
+  = IfaceReflCo       IfaceType
+  | IfaceGReflCo      Role IfaceType (IfaceMCoercion)
   | IfaceFunCo        Role IfaceCoercion IfaceCoercion
   | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
   | IfaceAppCo        IfaceCoercion IfaceCoercion
   | IfaceFunCo        Role IfaceCoercion IfaceCoercion
   | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
   | IfaceAppCo        IfaceCoercion IfaceCoercion
-  | IfaceForAllCo     IfaceTvBndr IfaceCoercion IfaceCoercion
+  | IfaceForAllCo     IfaceBndr IfaceCoercion IfaceCoercion
   | IfaceCoVarCo      IfLclName
   | IfaceAxiomInstCo  IfExtName BranchIndex [IfaceCoercion]
   | IfaceCoVarCo      IfLclName
   | IfaceAxiomInstCo  IfExtName BranchIndex [IfaceCoercion]
+  | IfaceAxiomRuleCo  IfLclName [IfaceCoercion]
+       -- There are only a fixed number of CoAxiomRules, so it suffices
+       -- to use an IfaceLclName to distinguish them.
+       -- See Note [Adding built-in type families] in TcTypeNats
   | IfaceUnivCo       IfaceUnivCoProv Role IfaceType IfaceType
   | IfaceSymCo        IfaceCoercion
   | IfaceTransCo      IfaceCoercion IfaceCoercion
   | IfaceNthCo        Int IfaceCoercion
   | IfaceLRCo         LeftOrRight IfaceCoercion
   | IfaceInstCo       IfaceCoercion IfaceCoercion
   | IfaceUnivCo       IfaceUnivCoProv Role IfaceType IfaceType
   | IfaceSymCo        IfaceCoercion
   | IfaceTransCo      IfaceCoercion IfaceCoercion
   | IfaceNthCo        Int IfaceCoercion
   | IfaceLRCo         LeftOrRight IfaceCoercion
   | IfaceInstCo       IfaceCoercion IfaceCoercion
-  | IfaceCoherenceCo  IfaceCoercion IfaceCoercion
   | IfaceKindCo       IfaceCoercion
   | IfaceSubCo        IfaceCoercion
   | IfaceKindCo       IfaceCoercion
   | IfaceSubCo        IfaceCoercion
-  | IfaceAxiomRuleCo  IfLclName [IfaceCoercion]
+  | IfaceFreeCoVar    CoVar    -- See Note [Free tyvars in IfaceType]
+  | IfaceHoleCo       CoVar    -- ^ See Note [Holes in IfaceCoercion]
 
 data IfaceUnivCoProv
   = IfaceUnsafeCoerceProv
   | IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
 
 data IfaceUnivCoProv
   = IfaceUnsafeCoerceProv
   | IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
-  | IfaceHoleProv Unique
-    -- ^ See Note [Holes in IfaceUnivCoProv]
 
 
-{-
-Note [Holes in IfaceUnivCoProv]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When typechecking fails the typechecker will produce a HoleProv UnivCoProv to
-stand in place of the unproven assertion. While we generally don't want to let
-these unproven assertions leak into interface files, we still need to be able to
-pretty-print them as we use IfaceType's pretty-printer to render Types. For this
-reason IfaceUnivCoProv has a IfaceHoleProv constructor; however, we fails when
-asked to serialize to a IfaceHoleProv to ensure that they don't end up in an
-interface file. To avoid an import loop between IfaceType and TyCoRep we only
-keep the hole's Unique, since that is all we need to print.
--}
+{- Note [Holes in IfaceCoercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When typechecking fails the typechecker will produce a HoleCo to stand
+in place of the unproven assertion. While we generally don't want to
+let these unproven assertions leak into interface files, we still need
+to be able to pretty-print them as we use IfaceType's pretty-printer
+to render Types. For this reason IfaceCoercion has a IfaceHoleCo
+constructor; however, we fails when asked to serialize to a
+IfaceHoleCo to ensure that they don't end up in an interface file.
+
 
 
-{-
 %************************************************************************
 %*                                                                      *
                 Functions over IFaceTypes
 %************************************************************************
 %*                                                                      *
                 Functions over IFaceTypes
@@ -287,22 +357,35 @@ keep the hole's Unique, since that is all we need to print.
 ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
 ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
 
 ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
 ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
 
-eqIfaceTvBndr :: IfaceTvBndr -> IfaceTvBndr -> Bool
-eqIfaceTvBndr (occ1, _) (occ2, _) = occ1 == occ2
-
 isIfaceLiftedTypeKind :: IfaceKind -> Bool
 isIfaceLiftedTypeKind :: IfaceKind -> Bool
-isIfaceLiftedTypeKind (IfaceTyConApp tc ITC_Nil)
+isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
   = isLiftedTypeKindTyConName (ifaceTyConName tc)
 isIfaceLiftedTypeKind (IfaceTyConApp tc
   = isLiftedTypeKindTyConName (ifaceTyConName tc)
 isIfaceLiftedTypeKind (IfaceTyConApp tc
-                       (ITC_Vis (IfaceTyConApp ptr_rep_lifted ITC_Nil) ITC_Nil))
+                       (IA_Arg (IfaceTyConApp ptr_rep_lifted IA_Nil)
+                               Required IA_Nil))
   =  tc `ifaceTyConHasKey` tYPETyConKey
   =  tc `ifaceTyConHasKey` tYPETyConKey
-  && ptr_rep_lifted `ifaceTyConHasKey` ptrRepLiftedDataConKey
+  && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
 isIfaceLiftedTypeKind _ = False
 
 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
 -- Mainly for printing purposes
 isIfaceLiftedTypeKind _ = False
 
 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
 -- Mainly for printing purposes
+--
+-- Here we split nested IfaceSigmaTy properly.
+--
+-- @
+-- forall t. T t => forall m a b. M m => (a -> m b) -> t a -> m (t b)
+-- @
+--
+-- If you called @splitIfaceSigmaTy@ on this type:
+--
+-- @
+-- ([t, m, a, b], [T t, M m], (a -> m b) -> t a -> m (t b))
+-- @
 splitIfaceSigmaTy ty
 splitIfaceSigmaTy ty
-  = (bndrs, theta, tau)
+  = case (bndrs, theta) of
+      ([], []) -> (bndrs, theta, tau)
+      _        -> let (bndrs', theta', tau') = splitIfaceSigmaTy tau
+                   in (bndrs ++ bndrs', theta ++ theta', tau')
   where
     (bndrs, rho)   = split_foralls ty
     (theta, tau)   = split_rho rho
   where
     (bndrs, rho)   = split_foralls ty
     (theta, tau)   = split_rho rho
@@ -322,22 +405,30 @@ suppressIfaceInvisibles dflags tys xs
     where
       suppress _       []      = []
       suppress []      a       = a
     where
       suppress _       []      = []
       suppress []      a       = a
-      suppress (k:ks) a@(_:xs)
-        | isInvisibleTyConBinder k = suppress ks xs
-        | otherwise                = a
+      suppress (k:ks) (x:xs)
+        | isInvisibleTyConBinder k =     suppress ks xs
+        | otherwise                = x : suppress ks xs
 
 stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
 stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
   | otherwise = filterOut isInvisibleTyConBinder tyvars
 
 
 stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
 stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
   | otherwise = filterOut isInvisibleTyConBinder tyvars
 
--- | Extract a IfaceTvBndr from a IfaceTyConBinder
-ifTyConBinderTyVar :: IfaceTyConBinder -> IfaceTvBndr
-ifTyConBinderTyVar = binderVar
+-- | Extract an 'IfaceBndr' from an 'IfaceForAllBndr'.
+ifForAllBndrVar :: IfaceForAllBndr -> IfaceBndr
+ifForAllBndrVar = binderVar
+
+-- | Extract the variable name from an 'IfaceForAllBndr'.
+ifForAllBndrName :: IfaceForAllBndr -> IfLclName
+ifForAllBndrName fab = ifaceBndrName (ifForAllBndrVar fab)
 
 
--- | Extract the variable name from a IfaceTyConBinder
+-- | Extract an 'IfaceBndr' from an 'IfaceTyConBinder'.
+ifTyConBinderVar :: IfaceTyConBinder -> IfaceBndr
+ifTyConBinderVar = binderVar
+
+-- | Extract the variable name from an 'IfaceTyConBinder'.
 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
-ifTyConBinderName tcb = ifaceTvBndrName (ifTyConBinderTyVar tcb)
+ifTyConBinderName tcb = ifaceBndrName (ifTyConBinderVar tcb)
 
 ifTypeIsVarFree :: IfaceType -> Bool
 -- Returns True if the type definitely has no variables at all
 
 ifTypeIsVarFree :: IfaceType -> Bool
 -- Returns True if the type definitely has no variables at all
@@ -345,8 +436,8 @@ ifTypeIsVarFree :: IfaceType -> Bool
 ifTypeIsVarFree ty = go ty
   where
     go (IfaceTyVar {})         = False
 ifTypeIsVarFree ty = go ty
   where
     go (IfaceTyVar {})         = False
-    go (IfaceTcTyVar {})       = False
-    go (IfaceAppTy fun arg)    = go fun && go arg
+    go (IfaceFreeTyVar {})     = False
+    go (IfaceAppTy fun args)   = go fun && go_args args
     go (IfaceFunTy arg res)    = go arg && go res
     go (IfaceDFunTy arg res)   = go arg && go res
     go (IfaceForAllTy {})      = False
     go (IfaceFunTy arg res)    = go arg && go res
     go (IfaceDFunTy arg res)   = go arg && go res
     go (IfaceForAllTy {})      = False
@@ -356,43 +447,54 @@ ifTypeIsVarFree ty = go ty
     go (IfaceCastTy {})        = False -- Safe
     go (IfaceCoercionTy {})    = False -- Safe
 
     go (IfaceCastTy {})        = False -- Safe
     go (IfaceCoercionTy {})    = False -- Safe
 
-    go_args ITC_Nil = True
-    go_args (ITC_Vis   arg args) = go arg && go_args args
-    go_args (ITC_Invis arg args) = go arg && go_args args
+    go_args IA_Nil = True
+    go_args (IA_Arg arg _ args) = go arg && go_args args
 
 
-{-
-Substitutions on IfaceType. This is only used during pretty-printing to construct
-the result type of a GADT, and does not deal with binders (eg IfaceForAll), so
-it doesn't need fancy capture stuff.
--}
+{- Note [Substitution on IfaceType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Substitutions on IfaceType are done only during pretty-printing to
+construct the result type of a GADT, and does not deal with binders
+(eg IfaceForAll), so it doesn't need fancy capture stuff.  -}
+
+type IfaceTySubst = FastStringEnv IfaceType -- Note [Substitution on IfaceType]
 
 
-type IfaceTySubst = FastStringEnv IfaceType
+mkIfaceTySubst :: [(IfLclName,IfaceType)] -> IfaceTySubst
+-- See Note [Substitution on IfaceType]
+mkIfaceTySubst eq_spec = mkFsEnv eq_spec
 
 
-mkIfaceTySubst :: [IfaceTvBndr] -> [IfaceType] -> IfaceTySubst
-mkIfaceTySubst tvs tys = mkFsEnv $ zipWithEqual "mkIfaceTySubst" (\(fs,_) ty -> (fs,ty)) tvs tys
+inDomIfaceTySubst :: IfaceTySubst -> IfaceTvBndr -> Bool
+-- See Note [Substitution on IfaceType]
+inDomIfaceTySubst subst (fs, _) = isJust (lookupFsEnv subst fs)
 
 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
 
 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
+-- See Note [Substitution on IfaceType]
 substIfaceType env ty
   = go ty
   where
 substIfaceType env ty
   = go ty
   where
-    go (IfaceTcTyVar tv)      = IfaceTcTyVar tv
+    go (IfaceFreeTyVar tv)    = IfaceFreeTyVar tv
     go (IfaceTyVar tv)        = substIfaceTyVar env tv
     go (IfaceTyVar tv)        = substIfaceTyVar env tv
-    go (IfaceAppTy  t1 t2)    = IfaceAppTy  (go t1) (go t2)
+    go (IfaceAppTy  t ts)     = IfaceAppTy  (go t) (substIfaceAppArgs env ts)
     go (IfaceFunTy  t1 t2)    = IfaceFunTy  (go t1) (go t2)
     go (IfaceDFunTy t1 t2)    = IfaceDFunTy (go t1) (go t2)
     go ty@(IfaceLitTy {})     = ty
     go (IfaceFunTy  t1 t2)    = IfaceFunTy  (go t1) (go t2)
     go (IfaceDFunTy t1 t2)    = IfaceDFunTy (go t1) (go t2)
     go ty@(IfaceLitTy {})     = ty
-    go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceTcArgs env tys)
-    go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceTcArgs env tys)
+    go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceAppArgs env tys)
+    go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceAppArgs env tys)
     go (IfaceForAllTy {})     = pprPanic "substIfaceType" (ppr ty)
     go (IfaceCastTy ty co)    = IfaceCastTy (go ty) (go_co co)
     go (IfaceCoercionTy co)   = IfaceCoercionTy (go_co co)
 
     go (IfaceForAllTy {})     = pprPanic "substIfaceType" (ppr ty)
     go (IfaceCastTy ty co)    = IfaceCastTy (go ty) (go_co co)
     go (IfaceCoercionTy co)   = IfaceCoercionTy (go_co co)
 
-    go_co (IfaceReflCo r ty)     = IfaceReflCo r (go ty)
-    go_co (IfaceFunCo r c1 c2)   = IfaceFunCo r (go_co c1) (go_co c2)
+    go_mco IfaceMRefl    = IfaceMRefl
+    go_mco (IfaceMCo co) = IfaceMCo $ go_co co
+
+    go_co (IfaceReflCo ty)           = IfaceReflCo (go ty)
+    go_co (IfaceGReflCo r ty mco)    = IfaceGReflCo r (go ty) (go_mco mco)
+    go_co (IfaceFunCo r c1 c2)       = IfaceFunCo r (go_co c1) (go_co c2)
     go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
     go_co (IfaceAppCo c1 c2)         = IfaceAppCo (go_co c1) (go_co c2)
     go_co (IfaceForAllCo {})         = pprPanic "substIfaceCoercion" (ppr ty)
     go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
     go_co (IfaceAppCo c1 c2)         = IfaceAppCo (go_co c1) (go_co c2)
     go_co (IfaceForAllCo {})         = pprPanic "substIfaceCoercion" (ppr ty)
+    go_co (IfaceFreeCoVar cv)        = IfaceFreeCoVar cv
     go_co (IfaceCoVarCo cv)          = IfaceCoVarCo cv
     go_co (IfaceCoVarCo cv)          = IfaceCoVarCo cv
+    go_co (IfaceHoleCo cv)           = IfaceHoleCo cv
     go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
     go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
     go_co (IfaceSymCo co)            = IfaceSymCo (go_co co)
     go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
     go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
     go_co (IfaceSymCo co)            = IfaceSymCo (go_co co)
@@ -400,7 +502,6 @@ substIfaceType env ty
     go_co (IfaceNthCo n co)          = IfaceNthCo n (go_co co)
     go_co (IfaceLRCo lr co)          = IfaceLRCo lr (go_co co)
     go_co (IfaceInstCo c1 c2)        = IfaceInstCo (go_co c1) (go_co c2)
     go_co (IfaceNthCo n co)          = IfaceNthCo n (go_co co)
     go_co (IfaceLRCo lr co)          = IfaceLRCo lr (go_co co)
     go_co (IfaceInstCo c1 c2)        = IfaceInstCo (go_co c1) (go_co c2)
-    go_co (IfaceCoherenceCo c1 c2)   = IfaceCoherenceCo (go_co c1) (go_co c2)
     go_co (IfaceKindCo co)           = IfaceKindCo (go_co co)
     go_co (IfaceSubCo co)            = IfaceSubCo (go_co co)
     go_co (IfaceAxiomRuleCo n cos)   = IfaceAxiomRuleCo n (go_cos cos)
     go_co (IfaceKindCo co)           = IfaceKindCo (go_co co)
     go_co (IfaceSubCo co)            = IfaceSubCo (go_co co)
     go_co (IfaceAxiomRuleCo n cos)   = IfaceAxiomRuleCo n (go_cos cos)
@@ -411,166 +512,152 @@ substIfaceType env ty
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
     go_prov (IfacePluginProv str)    = IfacePluginProv str
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
     go_prov (IfacePluginProv str)    = IfacePluginProv str
-    go_prov (IfaceHoleProv h)        = IfaceHoleProv h
 
 
-substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs
-substIfaceTcArgs env args
+substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
+substIfaceAppArgs env args
   = go args
   where
   = go args
   where
-    go ITC_Nil            = ITC_Nil
-    go (ITC_Vis ty tys)   = ITC_Vis   (substIfaceType env ty) (go tys)
-    go (ITC_Invis ty tys) = ITC_Invis (substIfaceType env ty) (go tys)
+    go IA_Nil              = IA_Nil
+    go (IA_Arg ty arg tys) = IA_Arg (substIfaceType env ty) arg (go tys)
 
 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
 substIfaceTyVar env tv
   | Just ty <- lookupFsEnv env tv = ty
   | otherwise                     = IfaceTyVar tv
 
 
 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
 substIfaceTyVar env tv
   | Just ty <- lookupFsEnv env tv = ty
   | otherwise                     = IfaceTyVar tv
 
-{-
-************************************************************************
-*                                                                      *
-                Equality over IfaceTypes
-*                                                                      *
-************************************************************************
-
-Note [No kind check in ifaces]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We check iface types for equality only when checking the consistency
-between two user-written signatures. In these cases, there is no possibility
-for a kind mismatch. So we omit the kind check (which would be impossible to
-write, anyway.)
-
--}
-
--- Like an RnEnv2, but mapping from FastString to deBruijn index
--- DeBruijn; see eqTypeX
-type BoundVar = Int
-data IfRnEnv2
-  = IRV2 { ifenvL :: UniqFM BoundVar -- from FastString
-         , ifenvR :: UniqFM BoundVar
-         , ifenv_next :: BoundVar
-         }
-
-emptyIfRnEnv2 :: IfRnEnv2
-emptyIfRnEnv2 = IRV2 { ifenvL = emptyUFM
-                     , ifenvR = emptyUFM
-                     , ifenv_next = 0 }
-
-rnIfOccL :: IfRnEnv2 -> IfLclName -> Maybe BoundVar
-rnIfOccL env = lookupUFM (ifenvL env)
-
-rnIfOccR :: IfRnEnv2 -> IfLclName -> Maybe BoundVar
-rnIfOccR env = lookupUFM (ifenvR env)
-
-extendIfRnEnv2 :: IfRnEnv2 -> IfLclName -> IfLclName -> IfRnEnv2
-extendIfRnEnv2 IRV2 { ifenvL = lenv
-                    , ifenvR = renv
-                    , ifenv_next = n } tv1 tv2
-             = IRV2 { ifenvL = addToUFM lenv tv1 n
-                    , ifenvR = addToUFM renv tv2 n
-                    , ifenv_next = n + 1
-                    }
-
--- See Note [No kind check in ifaces]
-eqIfaceType :: IfRnEnv2 -> IfaceType -> IfaceType -> Bool
-eqIfaceType _ (IfaceTcTyVar tv1) (IfaceTcTyVar tv2)
-    = tv1 == tv2   -- Should not happen
-eqIfaceType env (IfaceTyVar tv1) (IfaceTyVar tv2) =
-    case (rnIfOccL env tv1, rnIfOccR env tv2) of
-        (Just v1, Just v2) -> v1 == v2
-        (Nothing, Nothing) -> tv1 == tv2
-        _ -> False
-eqIfaceType _   (IfaceLitTy l1) (IfaceLitTy l2) = l1 == l2
-eqIfaceType env (IfaceAppTy t11 t12) (IfaceAppTy t21 t22)
-    = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
-eqIfaceType env (IfaceFunTy t11 t12) (IfaceFunTy t21 t22)
-    = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
-eqIfaceType env (IfaceDFunTy t11 t12) (IfaceDFunTy t21 t22)
-    = eqIfaceType env t11 t21 && eqIfaceType env t12 t22
-eqIfaceType env (IfaceForAllTy bndr1 t1) (IfaceForAllTy bndr2 t2)
-    = eqIfaceForAllBndr env bndr1 bndr2 (\env' -> eqIfaceType env' t1 t2)
-eqIfaceType env (IfaceTyConApp tc1 tys1) (IfaceTyConApp tc2 tys2)
-    = tc1 == tc2 && eqIfaceTcArgs env tys1 tys2
-eqIfaceType env (IfaceTupleTy s1 tc1 tys1) (IfaceTupleTy s2 tc2 tys2)
-    = s1 == s2 && tc1 == tc2 && eqIfaceTcArgs env tys1 tys2
-eqIfaceType env (IfaceCastTy t1 _) (IfaceCastTy t2 _)
-    = eqIfaceType env t1 t2
-eqIfaceType _   (IfaceCoercionTy {}) (IfaceCoercionTy {})
-    = True
-eqIfaceType _ _ _ = False
-
-eqIfaceTypes :: IfRnEnv2 -> [IfaceType] -> [IfaceType] -> Bool
-eqIfaceTypes env tys1 tys2 = and (zipWith (eqIfaceType env) tys1 tys2)
-
-eqIfaceForAllBndr :: IfRnEnv2 -> IfaceForAllBndr -> IfaceForAllBndr
-                  -> (IfRnEnv2 -> Bool)  -- continuation
-                  -> Bool
-eqIfaceForAllBndr env (TvBndr (tv1, k1) vis1) (TvBndr (tv2, k2) vis2) k
-  = eqIfaceType env k1 k2 && vis1 == vis2 &&
-    k (extendIfRnEnv2 env tv1 tv2)
-
-eqIfaceTcArgs :: IfRnEnv2 -> IfaceTcArgs -> IfaceTcArgs -> Bool
-eqIfaceTcArgs _ ITC_Nil ITC_Nil = True
-eqIfaceTcArgs env (ITC_Vis ty1 tys1) (ITC_Vis ty2 tys2)
-    = eqIfaceType env ty1 ty2 && eqIfaceTcArgs env tys1 tys2
-eqIfaceTcArgs env (ITC_Invis ty1 tys1) (ITC_Invis ty2 tys2)
-    = eqIfaceType env ty1 ty2 && eqIfaceTcArgs env tys1 tys2
-eqIfaceTcArgs _ _ _ = False
-
--- | Similar to 'eqTyVarBndrs', checks that tyvar lists
--- are the same length and have matching kinds; if so, extend the
--- 'IfRnEnv2'.  Returns 'Nothing' if they don't match.
-eqIfaceTvBndrs :: IfRnEnv2 -> [IfaceTvBndr] -> [IfaceTvBndr] -> Maybe IfRnEnv2
-eqIfaceTvBndrs env [] [] = Just env
-eqIfaceTvBndrs env ((tv1, k1):tvs1) ((tv2, k2):tvs2)
-  | eqIfaceType env k1 k2
-  = eqIfaceTvBndrs (extendIfRnEnv2 env tv1 tv2) tvs1 tvs2
-eqIfaceTvBndrs _ _ _ = Nothing
 
 {-
 ************************************************************************
 *                                                                      *
 
 {-
 ************************************************************************
 *                                                                      *
-                Functions over IFaceTcArgs
+                Functions over IfaceAppArgs
 *                                                                      *
 ************************************************************************
 -}
 
 *                                                                      *
 ************************************************************************
 -}
 
-stripInvisArgs :: DynFlags -> IfaceTcArgs -> IfaceTcArgs
+stripInvisArgs :: DynFlags -> IfaceAppArgs -> IfaceAppArgs
 stripInvisArgs dflags tys
   | gopt Opt_PrintExplicitKinds dflags = tys
   | otherwise = suppress_invis tys
     where
       suppress_invis c
         = case c of
 stripInvisArgs dflags tys
   | gopt Opt_PrintExplicitKinds dflags = tys
   | otherwise = suppress_invis tys
     where
       suppress_invis c
         = case c of
-            ITC_Invis _ ts -> suppress_invis ts
-            _ -> c
-
-tcArgsIfaceTypes :: IfaceTcArgs -> [IfaceType]
-tcArgsIfaceTypes ITC_Nil = []
-tcArgsIfaceTypes (ITC_Invis t ts) = t : tcArgsIfaceTypes ts
-tcArgsIfaceTypes (ITC_Vis   t ts) = t : tcArgsIfaceTypes ts
-
-ifaceVisTcArgsLength :: IfaceTcArgs -> Int
-ifaceVisTcArgsLength = go 0
+            IA_Nil -> IA_Nil
+            IA_Arg t argf ts
+              |  isVisibleArgFlag argf
+              -> IA_Arg t argf $ suppress_invis ts
+              -- Keep recursing through the remainder of the arguments, as it's
+              -- possible that there are remaining invisible ones.
+              -- See the "In type declarations" section of Note [VarBndrs,
+              -- TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
+              |  otherwise
+              -> suppress_invis ts
+
+appArgsIfaceTypes :: IfaceAppArgs -> [IfaceType]
+appArgsIfaceTypes IA_Nil = []
+appArgsIfaceTypes (IA_Arg t _ ts) = t : appArgsIfaceTypes ts
+
+appArgsIfaceTypesArgFlags :: IfaceAppArgs -> [(IfaceType, ArgFlag)]
+appArgsIfaceTypesArgFlags IA_Nil = []
+appArgsIfaceTypesArgFlags (IA_Arg t a ts)
+                                 = (t, a) : appArgsIfaceTypesArgFlags ts
+
+ifaceVisAppArgsLength :: IfaceAppArgs -> Int
+ifaceVisAppArgsLength = go 0
   where
   where
-    go !n ITC_Nil            = n
-    go n  (ITC_Vis _ rest)   = go (n+1) rest
-    go n  (ITC_Invis _ rest) = go n rest
+    go !n IA_Nil = n
+    go n  (IA_Arg _ argf rest)
+      | isVisibleArgFlag argf = go (n+1) rest
+      | otherwise             = go n rest
 
 {-
 Note [Suppressing invisible arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 {-
 Note [Suppressing invisible arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We use the IfaceTcArgs to specify which of the arguments to a type
-constructor should be displayed when pretty-printing, under
-the control of -fprint-explicit-kinds.
+We use the IfaceAppArgs data type to specify which of the arguments to a type
+should be displayed when pretty-printing, under the control of
+-fprint-explicit-kinds.
 See also Type.filterOutInvisibleTypes.
 For example, given
 See also Type.filterOutInvisibleTypes.
 For example, given
+
     T :: forall k. (k->*) -> k -> *    -- Ordinary kind polymorphism
     'Just :: forall k. k -> 'Maybe k   -- Promoted
     T :: forall k. (k->*) -> k -> *    -- Ordinary kind polymorphism
     'Just :: forall k. k -> 'Maybe k   -- Promoted
+
 we want
 we want
-  T * Tree Int    prints as    T Tree Int
-  'Just *         prints as    Just *
 
 
+    T * Tree Int    prints as    T Tree Int
+    'Just *         prints as    Just *
+
+For type constructors (IfaceTyConApp), IfaceAppArgs is a quite natural fit,
+since the corresponding Core constructor:
+
+    data Type
+      = ...
+      | TyConApp TyCon [Type]
+
+Already puts all of its arguments into a list. So when converting a Type to an
+IfaceType (see toIfaceAppArgsX in ToIface), we simply use the kind of the TyCon
+(which is cached) to guide the process of converting the argument Types into an
+IfaceAppArgs list.
+
+We also want this behavior for IfaceAppTy, since given:
+
+    data Proxy (a :: k)
+    f :: forall (t :: forall a. a -> Type). Proxy Type (t Bool True)
+
+We want to print the return type as `Proxy (t True)` without the use of
+-fprint-explicit-kinds (#15330). Accomplishing this is trickier than in the
+tycon case, because the corresponding Core constructor for IfaceAppTy:
+
+    data Type
+      = ...
+      | AppTy Type Type
+
+Only stores one argument at a time. Therefore, when converting an AppTy to an
+IfaceAppTy (in toIfaceTypeX in ToIface), we:
+
+1. Flatten the chain of AppTys down as much as possible
+2. Use typeKind to determine the function Type's kind
+3. Use this kind to guide the process of converting the argument Types into an
+   IfaceAppArgs list.
+
+By flattening the arguments like this, we obtain two benefits:
+
+(a) We can reuse the same machinery to pretty-print IfaceTyConApp arguments as
+    we do IfaceTyApp arguments, which means that we only need to implement the
+    logic to filter out invisible arguments once.
+(b) Unlike for tycons, finding the kind of a type in general (through typeKind)
+    is not a constant-time operation, so by flattening the arguments first, we
+    decrease the number of times we have to call typeKind.
+
+Note [Pretty-printing invisible arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Suppressing invisible arguments] is all about how to avoid printing
+invisible arguments when the -fprint-explicit-kinds flag is disables. Well,
+what about when it's enabled? Then we can and should print invisible kind
+arguments, and this Note explains how we do it.
+
+As two running examples, consider the following code:
+
+  {-# LANGUAGE PolyKinds #-}
+  data T1 a
+  data T2 (a :: k)
+
+When displaying these types (with -fprint-explicit-kinds on), we could just
+do the following:
+
+  T1 k a
+  T2 k a
+
+That certainly gets the job done. But it lacks a crucial piece of information:
+is the `k` argument inferred or specified? To communicate this, we use visible
+kind application syntax to distinguish the two cases:
+
+  T1 @{k} a
+  T2 @k   a
+
+Here, @{k} indicates that `k` is an inferred argument, and @k indicates that
+`k` is a specified argument. (See
+Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep for
+a lengthier explanation on what "inferred" and "specified" mean.)
 
 ************************************************************************
 *                                                                      *
 
 ************************************************************************
 *                                                                      *
@@ -590,15 +677,15 @@ if_print_coercions yes no
     then yes
     else no
 
     then yes
     else no
 
-pprIfaceInfixApp :: (TyPrec -> a -> SDoc) -> TyPrec -> SDoc -> a -> a -> SDoc
-pprIfaceInfixApp pp p pp_tc ty1 ty2
-  = maybeParen p FunPrec $
-    sep [pp FunPrec ty1, pprInfixVar True pp_tc <+> pp FunPrec ty2]
+pprIfaceInfixApp :: PprPrec -> SDoc -> SDoc -> SDoc -> SDoc
+pprIfaceInfixApp ctxt_prec pp_tc pp_ty1 pp_ty2
+  = maybeParen ctxt_prec opPrec $
+    sep [pp_ty1, pp_tc <+> pp_ty2]
 
 
-pprIfacePrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
-pprIfacePrefixApp p pp_fun pp_tys
+pprIfacePrefixApp :: PprPrec -> SDoc -> [SDoc] -> SDoc
+pprIfacePrefixApp ctxt_prec pp_fun pp_tys
   | null pp_tys = pp_fun
   | null pp_tys = pp_fun
-  | otherwise   = maybeParen p TyConPrec $
+  | otherwise   = maybeParen ctxt_prec appPrec $
                   hang pp_fun 2 (sep pp_tys)
 
 -- ----------------------------- Printing binders ------------------------------------
                   hang pp_fun 2 (sep pp_tys)
 
 -- ----------------------------- Printing binders ------------------------------------
@@ -628,7 +715,17 @@ pprIfaceTvBndr use_parens (tv, ki)
 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
 pprIfaceTyConBinders = sep . map go
   where
 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
 pprIfaceTyConBinders = sep . map go
   where
-    go tcb = pprIfaceTvBndr True (ifTyConBinderTyVar tcb)
+    go :: IfaceTyConBinder -> SDoc
+    go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr
+    go (Bndr (IfaceTvBndr bndr) vis) =
+      -- See Note [Pretty-printing invisible arguments]
+      case vis of
+        AnonTCB            -> ppr_bndr True
+        NamedTCB Required  -> ppr_bndr True
+        NamedTCB Specified -> char '@' <> ppr_bndr True
+        NamedTCB Inferred  -> char '@' <> braces (ppr_bndr False)
+      where
+        ppr_bndr use_parens = pprIfaceTvBndr use_parens bndr
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
@@ -663,54 +760,58 @@ instance Outputable IfaceType where
   ppr ty = pprIfaceType ty
 
 pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
   ppr ty = pprIfaceType ty
 
 pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
-pprIfaceType       = eliminateRuntimeRep (ppr_ty TopPrec)
-pprParendIfaceType = eliminateRuntimeRep (ppr_ty TyConPrec)
+pprIfaceType       = pprPrecIfaceType topPrec
+pprParendIfaceType = pprPrecIfaceType appPrec
+
+pprPrecIfaceType :: PprPrec -> IfaceType -> SDoc
+-- We still need `eliminateRuntimeRep`, since the `pprPrecIfaceType` maybe
+-- called from other places, besides `:type` and `:info`.
+pprPrecIfaceType prec ty = eliminateRuntimeRep (ppr_ty prec) ty
 
 
-ppr_ty :: TyPrec -> IfaceType -> SDoc
-ppr_ty _         (IfaceTcTyVar tyvar)   = ppr tyvar  -- This is the main reson for IfaceTcTyVar!
+ppr_ty :: PprPrec -> IfaceType -> SDoc
+ppr_ty _         (IfaceFreeTyVar tyvar) = ppr tyvar  -- This is the main reason 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 _         (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
+ppr_ty ctxt_prec (IfaceTupleTy i p tys) = pprTuple ctxt_prec i p tys
 ppr_ty _         (IfaceLitTy n)         = pprIfaceTyLit n
         -- Function types
 ppr_ty ctxt_prec (IfaceFunTy ty1 ty2)
   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
 ppr_ty _         (IfaceLitTy n)         = pprIfaceTyLit n
         -- Function types
 ppr_ty ctxt_prec (IfaceFunTy ty1 ty2)
   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
-    maybeParen ctxt_prec FunPrec $
-    sep [ppr_ty FunPrec ty1, sep (ppr_fun_tail ty2)]
+    maybeParen ctxt_prec funPrec $
+    sep [ppr_ty funPrec ty1, sep (ppr_fun_tail ty2)]
   where
     ppr_fun_tail (IfaceFunTy ty1 ty2)
   where
     ppr_fun_tail (IfaceFunTy ty1 ty2)
-      = (arrow <+> ppr_ty FunPrec ty1) : ppr_fun_tail ty2
+      = (arrow <+> ppr_ty funPrec ty1) : ppr_fun_tail ty2
     ppr_fun_tail other_ty
       = [arrow <+> pprIfaceType other_ty]
 
     ppr_fun_tail other_ty
       = [arrow <+> pprIfaceType other_ty]
 
-ppr_ty ctxt_prec (IfaceAppTy ty1 ty2)
+ppr_ty ctxt_prec (IfaceAppTy t ts)
   = if_print_coercions
       ppr_app_ty
       ppr_app_ty_no_casts
   where
     ppr_app_ty =
   = if_print_coercions
       ppr_app_ty
       ppr_app_ty_no_casts
   where
     ppr_app_ty =
-        maybeParen ctxt_prec TyConPrec
-        $ ppr_ty FunPrec ty1 <+> ppr_ty TyConPrec ty2
+        sdocWithDynFlags $ \dflags ->
+        pprIfacePrefixApp ctxt_prec
+                          (ppr_ty funPrec t)
+                          (map (ppr_app_arg appPrec) (tys_wo_kinds dflags))
+
+    tys_wo_kinds dflags = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags ts
 
     -- Strip any casts from the head of the application
     ppr_app_ty_no_casts =
 
     -- Strip any casts from the head of the application
     ppr_app_ty_no_casts =
-        case split_app_tys ty1 (ITC_Vis ty2 ITC_Nil) of
-          (IfaceCastTy head _, args) -> ppr_ty ctxt_prec (mk_app_tys head args)
-          _                          -> ppr_app_ty
-
-    split_app_tys :: IfaceType -> IfaceTcArgs -> (IfaceType, IfaceTcArgs)
-    split_app_tys (IfaceAppTy t1 t2) args = split_app_tys t1 (t2 `ITC_Vis` args)
-    split_app_tys head               args = (head, args)
+        case t of
+          IfaceCastTy head _ -> ppr_ty ctxt_prec (mk_app_tys head ts)
+          _                  -> ppr_app_ty
 
 
-    mk_app_tys :: IfaceType -> IfaceTcArgs -> IfaceType
+    mk_app_tys :: IfaceType -> IfaceAppArgs -> IfaceType
     mk_app_tys (IfaceTyConApp tc tys1) tys2 =
         IfaceTyConApp tc (tys1 `mappend` tys2)
     mk_app_tys (IfaceTyConApp tc tys1) tys2 =
         IfaceTyConApp tc (tys1 `mappend` tys2)
-    mk_app_tys t1                      tys2 =
-        foldl' IfaceAppTy t1 (tcArgsIfaceTypes tys2)
+    mk_app_tys t1 tys2 = IfaceAppTy t1 tys2
 
 ppr_ty ctxt_prec (IfaceCastTy ty co)
   = if_print_coercions
 
 ppr_ty ctxt_prec (IfaceCastTy ty co)
   = if_print_coercions
-      (parens (ppr_ty TopPrec ty <+> text "|>" <+> ppr co))
+      (parens (ppr_ty topPrec ty <+> text "|>" <+> ppr co))
       (ppr_ty ctxt_prec ty)
 
 ppr_ty ctxt_prec (IfaceCoercionTy co)
       (ppr_ty ctxt_prec ty)
 
 ppr_ty ctxt_prec (IfaceCoercionTy co)
@@ -718,18 +819,17 @@ ppr_ty ctxt_prec (IfaceCoercionTy co)
       (ppr_co ctxt_prec co)
       (text "<>")
 
       (ppr_co ctxt_prec co)
       (text "<>")
 
-ppr_ty ctxt_prec ty
-  = maybeParen ctxt_prec FunPrec (ppr_iface_sigma_type True ty)
-
-{-
-Note [Defaulting RuntimeRep variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ppr_ty ctxt_prec ty -- IfaceForAllTy
+  = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
 
 
-RuntimeRep variables are considered by many (most?) users to be little more than
-syntactic noise. When the notion was introduced there was a signficant and
-understandable push-back from those with pedagogy in mind, which argued that
-RuntimeRep variables would throw a wrench into nearly any teach approach since
-they appear in even the lowly ($) function's type,
+{- Note [Defaulting RuntimeRep variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+RuntimeRep variables are considered by many (most?) users to be little
+more than syntactic noise. When the notion was introduced there was a
+signficant and understandable push-back from those with pedagogy in
+mind, which argued that RuntimeRep variables would throw a wrench into
+nearly any teach approach since they appear in even the lowly ($)
+function's type,
 
     ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
 
 
     ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
 
@@ -737,14 +837,30 @@ which is significantly less readable than its non RuntimeRep-polymorphic type of
 
     ($) :: (a -> b) -> a -> b
 
 
     ($) :: (a -> b) -> a -> b
 
-Moreover, unboxed types don't appear all that often in run-of-the-mill Haskell
-programs, so it makes little sense to make all users pay this syntactic
-overhead.
-
-For this reason it was decided that we would hide RuntimeRep variables for now
-(see #11549). We do this by defaulting all type variables of kind RuntimeRep to
-PtrLiftedRep. This is done in a pass right before pretty-printing
-(defaultRuntimeRepVars, controlled by -fprint-explicit-runtime-reps)
+Moreover, unboxed types don't appear all that often in run-of-the-mill
+Haskell programs, so it makes little sense to make all users pay this
+syntactic overhead.
+
+For this reason it was decided that we would hide RuntimeRep variables
+for now (see #11549). We do this by defaulting all type variables of
+kind RuntimeRep to LiftedRep. This is done in a pass right before
+pretty-printing (defaultRuntimeRepVars, controlled by
+-fprint-explicit-runtime-reps)
+
+This applies to /quantified/ variables like 'w' above.  What about
+variables that are /free/ in the type being printed, which certainly
+happens in error messages.  Suppose (Trac #16074) we are reporting a
+mismatch between two skolems
+          (a :: RuntimeRep) ~ (b :: RuntimeRep)
+We certainly don't want to say "Can't match LiftedRep ~ LiftedRep"!
+
+But if we are printing the type
+    (forall (a :: Type r). blah
+we do want to turn that (free) r into LiftedRep, so it prints as
+    (forall a. blah)
+
+Conclusion: keep track of whether we we are in the kind of a
+binder; ohly if so, convert free RuntimeRep variables to LiftedRep.
 -}
 
 -- | Default 'RuntimeRep' variables to 'LiftedPtr'. e.g.
 -}
 
 -- | Default 'RuntimeRep' variables to 'LiftedPtr'. e.g.
@@ -763,42 +879,72 @@ PtrLiftedRep. This is done in a pass right before pretty-printing
 -- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
 --
 defaultRuntimeRepVars :: IfaceType -> IfaceType
 -- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
 --
 defaultRuntimeRepVars :: IfaceType -> IfaceType
-defaultRuntimeRepVars = go emptyFsEnv
+defaultRuntimeRepVars ty = go False emptyFsEnv ty
   where
   where
-    go :: FastStringEnv () -> IfaceType -> IfaceType
-    go subs (IfaceForAllTy bndr ty)
-      | isRuntimeRep var_kind
+    go :: Bool              -- True <=> Inside the kind of a binder
+       -> FastStringEnv ()  -- Set of enclosing forall-ed RuntimeRep variables
+       -> IfaceType         --  (replace them with LiftedRep)
+       -> IfaceType
+    go ink subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
+     | isRuntimeRep var_kind
+      , isInvisibleArgFlag argf -- Don't default *visible* quantification
+                                -- or we get the mess in #13963
       = let subs' = extendFsEnv subs var ()
       = let subs' = extendFsEnv subs var ()
-        in go subs' ty
-      | otherwise
-      = IfaceForAllTy (TvBndr (var, go subs var_kind) (binderArgFlag bndr))
-        (go subs ty)
-      where
-        var :: IfLclName
-        (var, var_kind) = binderVar bndr
+            -- Record that we should replace it with LiftedRep,
+            -- and recurse, discarding the forall
+        in go ink subs' ty
 
 
-    go subs (IfaceTyVar tv)
+    go ink subs (IfaceForAllTy bndr ty)
+      = IfaceForAllTy (go_ifacebndr subs bndr) (go ink subs ty)
+
+    go _ subs ty@(IfaceTyVar tv)
       | tv `elemFsEnv` subs
       | tv `elemFsEnv` subs
-      = IfaceTyConApp ptrRepLifted ITC_Nil
+      = IfaceTyConApp liftedRep IA_Nil
+      | otherwise
+      = ty
+
+    go in_kind _ ty@(IfaceFreeTyVar tv)
+      -- See Note [Defaulting RuntimeRep variables], about free vars
+      | in_kind && TyCoRep.isRuntimeRepTy (tyVarKind tv)
+      = IfaceTyConApp liftedRep IA_Nil
+      | otherwise
+      = ty
+
+    go ink subs (IfaceTyConApp tc tc_args)
+      = IfaceTyConApp tc (go_args ink subs tc_args)
 
 
-    go subs (IfaceFunTy kind ty)
-      = IfaceFunTy (go subs kind) (go subs ty)
+    go ink subs (IfaceTupleTy sort is_prom tc_args)
+      = IfaceTupleTy sort is_prom (go_args ink subs tc_args)
 
 
-    go subs (IfaceAppTy x y)
-      = IfaceAppTy (go subs x) (go subs y)
+    go ink subs (IfaceFunTy arg res)
+      = IfaceFunTy (go ink subs arg) (go ink subs res)
 
 
-    go subs (IfaceDFunTy x y)
-      = IfaceDFunTy (go subs x) (go subs y)
+    go ink subs (IfaceAppTy t ts)
+      = IfaceAppTy (go ink subs t) (go_args ink subs ts)
 
 
-    go subs (IfaceCastTy x co)
-      = IfaceCastTy (go subs x) co
+    go ink subs (IfaceDFunTy x y)
+      = IfaceDFunTy (go ink subs x) (go ink subs y)
 
 
-    go _ other = other
+    go ink subs (IfaceCastTy x co)
+      = IfaceCastTy (go ink subs x) co
 
 
-    ptrRepLifted :: IfaceTyCon
-    ptrRepLifted =
-        IfaceTyCon dc_name (IfaceTyConInfo IsPromoted IfaceNormalTyCon)
-      where dc_name = getName ptrRepLiftedDataConTyCon
+    go _ _ ty@(IfaceLitTy {}) = ty
+    go _ _ ty@(IfaceCoercionTy {}) = ty
+
+    go_ifacebndr :: FastStringEnv () -> IfaceForAllBndr -> IfaceForAllBndr
+    go_ifacebndr subs (Bndr (IfaceIdBndr (n, t)) argf)
+      = Bndr (IfaceIdBndr (n, go True subs t)) argf
+    go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
+      = Bndr (IfaceTvBndr (n, go True subs t)) argf
+
+    go_args :: Bool -> FastStringEnv () -> IfaceAppArgs -> IfaceAppArgs
+    go_args _ _ IA_Nil = IA_Nil
+    go_args ink subs (IA_Arg ty argf args)
+      = IA_Arg (go ink subs ty) argf (go_args ink subs args)
+
+    liftedRep :: IfaceTyCon
+    liftedRep = IfaceTyCon dc_name (IfaceTyConInfo IsPromoted IfaceNormalTyCon)
+      where dc_name = getName liftedRepDataConTyCon
 
     isRuntimeRep :: IfaceType -> Bool
     isRuntimeRep (IfaceTyConApp tc _) =
 
     isRuntimeRep :: IfaceType -> Bool
     isRuntimeRep (IfaceTyConApp tc _) =
@@ -806,57 +952,71 @@ defaultRuntimeRepVars = go emptyFsEnv
     isRuntimeRep _ = False
 
 eliminateRuntimeRep :: (IfaceType -> SDoc) -> IfaceType -> SDoc
     isRuntimeRep _ = False
 
 eliminateRuntimeRep :: (IfaceType -> SDoc) -> IfaceType -> SDoc
-eliminateRuntimeRep f ty = sdocWithDynFlags $ \dflags ->
-    if gopt Opt_PrintExplicitRuntimeReps dflags
-      then f ty
-      else f (defaultRuntimeRepVars ty)
-
-instance Outputable IfaceTcArgs where
-  ppr tca = pprIfaceTcArgs tca
-
-pprIfaceTcArgs, pprParendIfaceTcArgs :: IfaceTcArgs -> SDoc
-pprIfaceTcArgs  = ppr_tc_args TopPrec
-pprParendIfaceTcArgs = ppr_tc_args TyConPrec
-
-ppr_tc_args :: TyPrec -> IfaceTcArgs -> SDoc
-ppr_tc_args ctx_prec args
- = let pprTys t ts = ppr_ty ctx_prec t <+> ppr_tc_args ctx_prec ts
-   in case args of
-        ITC_Nil        -> empty
-        ITC_Vis   t ts -> pprTys t ts
-        ITC_Invis t ts -> pprTys t ts
+eliminateRuntimeRep f ty
+  = sdocWithDynFlags $ \dflags ->
+    getPprStyle      $ \sty    ->
+    if userStyle sty && not (gopt Opt_PrintExplicitRuntimeReps dflags)
+      then f (defaultRuntimeRepVars ty)
+      else f ty
 
 
--------------------
-ppr_iface_sigma_type :: Bool -> IfaceType -> SDoc
-ppr_iface_sigma_type show_foralls_unconditionally ty
-  = ppr_iface_forall_part show_foralls_unconditionally tvs theta (ppr tau)
+instance Outputable IfaceAppArgs where
+  ppr tca = pprIfaceAppArgs tca
+
+pprIfaceAppArgs, pprParendIfaceAppArgs :: IfaceAppArgs -> SDoc
+pprIfaceAppArgs  = ppr_app_args topPrec
+pprParendIfaceAppArgs = ppr_app_args appPrec
+
+ppr_app_args :: PprPrec -> IfaceAppArgs -> SDoc
+ppr_app_args ctx_prec = go
   where
   where
-    (tvs, theta, tau) = splitIfaceSigmaTy ty
+    go :: IfaceAppArgs -> SDoc
+    go IA_Nil             = empty
+    go (IA_Arg t argf ts) = ppr_app_arg ctx_prec (t, argf) <+> go ts
+
+-- See Note [Pretty-printing invisible arguments]
+ppr_app_arg :: PprPrec -> (IfaceType, ArgFlag) -> SDoc
+ppr_app_arg ctx_prec (t, argf) =
+  sdocWithDynFlags $ \dflags ->
+  let print_kinds = gopt Opt_PrintExplicitKinds dflags
+  in case argf of
+       Required  -> ppr_ty ctx_prec t
+       Specified |  print_kinds
+                 -> char '@' <> ppr_ty appPrec t
+       Inferred  |  print_kinds
+                 -> char '@' <> braces (ppr_ty topPrec t)
+       _         -> empty
 
 -------------------
 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
 
 -------------------
 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
-pprIfaceForAllPart tvs ctxt sdoc = ppr_iface_forall_part False tvs ctxt sdoc
+pprIfaceForAllPart tvs ctxt sdoc
+  = ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc
+
+-- | Like 'pprIfaceForAllPart', but always uses an explicit @forall@.
+pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
+pprIfaceForAllPartMust tvs ctxt sdoc
+  = ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
 
 pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
 
 pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
-pprIfaceForAllCoPart tvs sdoc =
-    sep [ pprIfaceForAllCo tvs, sdoc ]
+pprIfaceForAllCoPart tvs sdoc
+  = sep [ pprIfaceForAllCo tvs, sdoc ]
 
 
-ppr_iface_forall_part :: Bool
+ppr_iface_forall_part :: ShowForAllFlag
                       -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
                       -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
-ppr_iface_forall_part show_foralls_unconditionally tvs ctxt sdoc
-  = sep [ if show_foralls_unconditionally
-          then pprIfaceForAll tvs
-          else pprUserIfaceForAll tvs
+ppr_iface_forall_part show_forall tvs ctxt sdoc
+  = sep [ case show_forall of
+            ShowForAllMust -> pprIfaceForAll tvs
+            ShowForAllWhen -> pprUserIfaceForAll tvs
         , pprIfaceContextArr ctxt
         , sdoc]
 
 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprIfaceForAll [] = empty
         , pprIfaceContextArr ctxt
         , sdoc]
 
 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprIfaceForAll [] = empty
-pprIfaceForAll bndrs@(TvBndr _ vis : _)
-  = add_separator (forAllLit <+> doc) <+> pprIfaceForAll bndrs'
+pprIfaceForAll bndrs@(Bndr _ vis : _)
+  = sep [ add_separator (forAllLit <+> fsep docs)
+        , pprIfaceForAll bndrs' ]
   where
   where
-    (bndrs', doc) = ppr_itv_bndrs bndrs vis
+    (bndrs', docs) = ppr_itv_bndrs bndrs vis
 
     add_separator stuff = case vis of
                             Required -> stuff <+> arrow
 
     add_separator stuff = case vis of
                             Required -> stuff <+> arrow
@@ -868,12 +1028,12 @@ pprIfaceForAll bndrs@(TvBndr _ vis : _)
 -- No anonymous binders here!
 ppr_itv_bndrs :: [IfaceForAllBndr]
              -> ArgFlag  -- ^ visibility of the first binder in the list
 -- No anonymous binders here!
 ppr_itv_bndrs :: [IfaceForAllBndr]
              -> ArgFlag  -- ^ visibility of the first binder in the list
-             -> ([IfaceForAllBndr], SDoc)
-ppr_itv_bndrs all_bndrs@(bndr@(TvBndr _ vis) : bndrs) vis1
+             -> ([IfaceForAllBndr], [SDoc])
+ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
   | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
   | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
-                         (bndrs', pprIfaceForAllBndr bndr <+> doc)
-  | otherwise   = (all_bndrs, empty)
-ppr_itv_bndrs [] _ = ([], empty)
+                         (bndrs', pprIfaceForAllBndr bndr : doc)
+  | otherwise   = (all_bndrs, [])
+ppr_itv_bndrs [] _ = ([], [])
 
 pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCo []  = empty
 
 pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCo []  = empty
@@ -883,114 +1043,244 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 
 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 
 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
-pprIfaceForAllBndr (TvBndr tv Inferred) = sdocWithDynFlags $ \dflags ->
-                                           if gopt Opt_PrintExplicitForalls dflags
-                                           then braces $ pprIfaceTvBndr False tv
-                                           else pprIfaceTvBndr True tv
-pprIfaceForAllBndr (TvBndr tv _)        = pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) Inferred)
+  = sdocWithDynFlags $ \dflags ->
+                          if gopt Opt_PrintExplicitForalls dflags
+                          then braces $ pprIfaceTvBndr False tv
+                          else pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) _)  = pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceIdBndr idv) _) = pprIfaceIdBndr idv
 
 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 pprIfaceForAllCoBndr (tv, kind_co)
   = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
 
 
 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 pprIfaceForAllCoBndr (tv, kind_co)
   = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
 
-pprIfaceSigmaType :: IfaceType -> SDoc
-pprIfaceSigmaType ty = ppr_iface_sigma_type False ty
+-- | Show forall flag
+--
+-- Unconditionally show the forall quantifier with ('ShowForAllMust')
+-- or when ('ShowForAllWhen') the names used are free in the binder
+-- or when compiling with -fprint-explicit-foralls.
+data ShowForAllFlag = ShowForAllMust | ShowForAllWhen
+
+pprIfaceSigmaType :: ShowForAllFlag -> IfaceType -> SDoc
+pprIfaceSigmaType show_forall ty
+  = eliminateRuntimeRep ppr_fn ty
+  where
+    ppr_fn iface_ty =
+      let (tvs, theta, tau) = splitIfaceSigmaTy iface_ty
+       in ppr_iface_forall_part show_forall tvs theta (ppr tau)
 
 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprUserIfaceForAll tvs
    = sdocWithDynFlags $ \dflags ->
 
 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprUserIfaceForAll tvs
    = sdocWithDynFlags $ \dflags ->
-     ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
+     -- See Note [When to print foralls]
+     ppWhen (any tv_has_kind_var tvs
+             || any tv_is_required tvs
+             || gopt Opt_PrintExplicitForalls dflags) $
      pprIfaceForAll tvs
    where
      pprIfaceForAll tvs
    where
-     tv_has_kind_var (TvBndr (_,kind) _) = not (ifTypeIsVarFree kind)
+     tv_has_kind_var (Bndr (IfaceTvBndr (_,kind)) _)
+       = not (ifTypeIsVarFree kind)
+     tv_has_kind_var _ = False
+
+     tv_is_required = isVisibleArgFlag . binderArgFlag
+
+{-
+Note [When to print foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We opt to explicitly pretty-print `forall`s if any of the following
+criteria are met:
+
+1. -fprint-explicit-foralls is on.
+
+2. A bound type variable has a polymorphic kind. E.g.,
+
+     forall k (a::k). Proxy a -> Proxy a
+
+   Since a's kind mentions a variable k, we print the foralls.
+
+3. A bound type variable is a visible argument (#14238).
+   Suppose we are printing the kind of:
+
+     T :: forall k -> k -> Type
+
+   The "forall k ->" notation means that this kind argument is required.
+   That is, it must be supplied at uses of T. E.g.,
+
+     f :: T (Type->Type)  Monad -> Int
+
+   So we print an explicit "T :: forall k -> k -> Type",
+   because omitting it and printing "T :: k -> Type" would be
+   utterly misleading.
+
+   See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
+   in TyCoRep.
+
+N.B. Until now (Aug 2018) we didn't check anything for coercion variables.
+
+Note [Printing foralls in type family instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use the same criteria as in Note [When to print foralls] to determine
+whether a type family instance should be pretty-printed with an explicit
+`forall`. Example:
+
+  type family Foo (a :: k) :: k where
+    Foo Maybe       = []
+    Foo (a :: Type) = Int
+    Foo a           = a
+
+Without -fprint-explicit-foralls enabled, this will be pretty-printed as:
+
+type family Foo (a :: k) :: k where
+  Foo Maybe = []
+  Foo a = Int
+  forall k (a :: k). Foo a = a
+
+Note that only the third equation has an explicit forall, since it has a type
+variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then
+the second equation would be preceded with `forall a.`.)
+
+There is one tricky point in the implementation: what visibility
+do we give the type variables in a type family instance? Type family instances
+only store type *variables*, not type variable *binders*, and only the latter
+has visibility information. We opt to default the visibility of each of these
+type variables to Specified because users can't ever instantiate these
+variables manually, so the choice of visibility is only relevant to
+pretty-printing. (This is why the `k` in `forall k (a :: k). ...` above is
+printed the way it is, even though it wasn't written explicitly in the
+original source code.)
+
+We adopt the same strategy for data family instances. Example:
+
+  data family DF (a :: k)
+  data instance DF '[a, b] = DFList
+
+That data family instance is pretty-printed as:
+
+  data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList
+
+This is despite that the representation tycon for this data instance (call it
+$DF:List) actually has different visibilities for its binders.
+However, the visibilities of these binders are utterly irrelevant to the
+programmer, who cares only about the specificity of variables in `DF`'s type,
+not $DF:List's type. Therefore, we opt to pretty-print all variables in data
+family instances as Specified.
+
+Note [Printing promoted type constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this GHCi session (Trac #14343)
+    > _ :: Proxy '[ 'True ]
+    error:
+      Found hole: _ :: Proxy '['True]
+
+This would be bad, because the '[' looks like a character literal.
+Solution: in type-level lists and tuples, add a leading space
+if the first type is itself promoted.  See pprSpaceIfPromotedTyCon.
+-}
 
 
 -------------------
 
 
 
 -------------------
 
+-- | Prefix a space if the given 'IfaceType' is a promoted 'TyCon'.
+-- See Note [Printing promoted type constructors]
+pprSpaceIfPromotedTyCon :: IfaceType -> SDoc -> SDoc
+pprSpaceIfPromotedTyCon (IfaceTyConApp tyCon _)
+  = case ifaceTyConIsPromoted (ifaceTyConInfo tyCon) of
+      IsPromoted -> (space <>)
+      _ -> id
+pprSpaceIfPromotedTyCon _
+  = id
+
 -- See equivalent function in TyCoRep.hs
 -- See equivalent function in TyCoRep.hs
-pprIfaceTyList :: TyPrec -> IfaceType -> IfaceType -> SDoc
+pprIfaceTyList :: PprPrec -> IfaceType -> IfaceType -> SDoc
 -- Given a type-level list (t1 ': t2), see if we can print
 -- it in list notation [t1, ...].
 -- Precondition: Opt_PrintExplicitKinds is off
 pprIfaceTyList ctxt_prec ty1 ty2
   = case gather ty2 of
       (arg_tys, Nothing)
 -- Given a type-level list (t1 ': t2), see if we can print
 -- it in list notation [t1, ...].
 -- Precondition: Opt_PrintExplicitKinds is off
 pprIfaceTyList ctxt_prec ty1 ty2
   = case gather ty2 of
       (arg_tys, Nothing)
-        -> char '\'' <> brackets (fsep (punctuate comma
-                        (map (ppr_ty TopPrec) (ty1:arg_tys))))
+        -> char '\'' <> brackets (pprSpaceIfPromotedTyCon ty1 (fsep
+                        (punctuate comma (map (ppr_ty topPrec) (ty1:arg_tys)))))
       (arg_tys, Just tl)
       (arg_tys, Just tl)
-        -> maybeParen ctxt_prec FunPrec $ hang (ppr_ty FunPrec ty1)
-           2 (fsep [ colon <+> ppr_ty FunPrec ty | ty <- arg_tys ++ [tl]])
+        -> maybeParen ctxt_prec funPrec $ hang (ppr_ty funPrec ty1)
+           2 (fsep [ colon <+> ppr_ty funPrec ty | ty <- arg_tys ++ [tl]])
   where
     gather :: IfaceType -> ([IfaceType], Maybe IfaceType)
      -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
     gather (IfaceTyConApp tc tys)
       | tc `ifaceTyConHasKey` consDataConKey
   where
     gather :: IfaceType -> ([IfaceType], Maybe IfaceType)
      -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
     gather (IfaceTyConApp tc tys)
       | tc `ifaceTyConHasKey` consDataConKey
-      , (ITC_Invis _ (ITC_Vis ty1 (ITC_Vis ty2 ITC_Nil))) <- tys
+      , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
+      , isInvisibleArgFlag argf
       , (args, tl) <- gather ty2
       = (ty1:args, tl)
       | tc `ifaceTyConHasKey` nilDataConKey
       = ([], Nothing)
     gather ty = ([], Just ty)
 
       , (args, tl) <- gather ty2
       = (ty1:args, tl)
       | tc `ifaceTyConHasKey` nilDataConKey
       = ([], Nothing)
     gather ty = ([], Just ty)
 
-pprIfaceTypeApp :: TyPrec -> IfaceTyCon -> IfaceTcArgs -> SDoc
+pprIfaceTypeApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
 pprIfaceTypeApp prec tc args = pprTyTcApp prec tc args
 
 pprIfaceTypeApp prec tc args = pprTyTcApp prec tc args
 
-pprTyTcApp :: TyPrec -> IfaceTyCon -> IfaceTcArgs -> SDoc
+pprTyTcApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
 pprTyTcApp ctxt_prec tc tys =
     sdocWithDynFlags $ \dflags ->
     getPprStyle $ \style ->
     pprTyTcApp' ctxt_prec tc tys dflags style
 
 pprTyTcApp ctxt_prec tc tys =
     sdocWithDynFlags $ \dflags ->
     getPprStyle $ \style ->
     pprTyTcApp' ctxt_prec tc tys dflags style
 
-pprTyTcApp' :: TyPrec -> IfaceTyCon -> IfaceTcArgs
+pprTyTcApp' :: PprPrec -> IfaceTyCon -> IfaceAppArgs
             -> DynFlags -> PprStyle -> SDoc
 pprTyTcApp' ctxt_prec tc tys dflags style
   | ifaceTyConName tc `hasKey` ipClassKey
             -> DynFlags -> PprStyle -> SDoc
 pprTyTcApp' ctxt_prec tc tys dflags style
   | ifaceTyConName tc `hasKey` ipClassKey
-  , ITC_Vis (IfaceLitTy (IfaceStrTyLit n)) (ITC_Vis ty ITC_Nil) <- tys
-  = maybeParen ctxt_prec FunPrec
-    $ char '?' <> ftext n <> text "::" <> ppr_ty TopPrec ty
+  , IA_Arg (IfaceLitTy (IfaceStrTyLit n))
+           Required (IA_Arg ty Required IA_Nil) <- tys
+  = maybeParen ctxt_prec funPrec
+    $ char '?' <> ftext n <> text "::" <> ppr_ty topPrec ty
 
   | IfaceTupleTyCon arity sort <- ifaceTyConSort info
   , not (debugStyle style)
 
   | IfaceTupleTyCon arity sort <- ifaceTyConSort info
   , not (debugStyle style)
-  , arity == ifaceVisTcArgsLength tys
-  = pprTuple sort (ifaceTyConIsPromoted info) tys
+  , arity == ifaceVisAppArgsLength tys
+  = pprTuple ctxt_prec sort (ifaceTyConIsPromoted info) tys
 
   | IfaceSumTyCon arity <- ifaceTyConSort info
   = pprSum arity (ifaceTyConIsPromoted info) tys
 
   | tc `ifaceTyConHasKey` consDataConKey
   , not (gopt Opt_PrintExplicitKinds dflags)
 
   | IfaceSumTyCon arity <- ifaceTyConSort info
   = pprSum arity (ifaceTyConIsPromoted info) tys
 
   | tc `ifaceTyConHasKey` consDataConKey
   , not (gopt Opt_PrintExplicitKinds dflags)
-  , ITC_Invis _ (ITC_Vis ty1 (ITC_Vis ty2 ITC_Nil)) <- tys
+  , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
+  , isInvisibleArgFlag argf
   = pprIfaceTyList ctxt_prec ty1 ty2
 
   | tc `ifaceTyConHasKey` tYPETyConKey
   = pprIfaceTyList ctxt_prec ty1 ty2
 
   | tc `ifaceTyConHasKey` tYPETyConKey
-  , ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil <- tys
-  , rep `ifaceTyConHasKey` ptrRepLiftedDataConKey
-  = unicodeSyntax (char '★') (char '*')
+  , IA_Arg (IfaceTyConApp rep IA_Nil) Required IA_Nil <- tys
+  , rep `ifaceTyConHasKey` liftedRepDataConKey
+  = kindType
 
 
-  | tc `ifaceTyConHasKey` tYPETyConKey
-  , ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil <- tys
-  , rep `ifaceTyConHasKey` ptrRepUnliftedDataConKey
-  = char '#'
-
-  | not opt_PprStyle_Debug
-  , tc `ifaceTyConHasKey` errorMessageTypeErrorFamKey
-  = text "(TypeError ...)"   -- Suppress detail unles you _really_ want to see
+  | otherwise
+  = getPprDebug $ \dbg ->
+    if | not dbg && tc `ifaceTyConHasKey` errorMessageTypeErrorFamKey
+         -- Suppress detail unles you _really_ want to see
+         -> text "(TypeError ...)"
 
 
-  | Just doc <- ppr_equality tc (tcArgsIfaceTypes tys)
-  = doc
+       | Just doc <- ppr_equality ctxt_prec tc (appArgsIfaceTypes tys)
+         -> doc
 
 
-  | otherwise
-  = ppr_iface_tc_app ppr_ty ctxt_prec tc tys_wo_kinds
+       | otherwise
+         -> ppr_iface_tc_app ppr_app_arg ctxt_prec tc tys_wo_kinds
   where
     info = ifaceTyConInfo tc
   where
     info = ifaceTyConInfo tc
-    tys_wo_kinds = tcArgsIfaceTypes $ stripInvisArgs dflags tys
+    tys_wo_kinds = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags tys
 
 -- | Pretty-print a type-level equality.
 
 -- | Pretty-print a type-level equality.
+-- Returns (Just doc) if the argument is a /saturated/ application
+-- of   eqTyCon          (~)
+--      eqPrimTyCon      (~#)
+--      eqReprPrimTyCon  (~R#)
+--      heqTyCon         (~~)
 --
 --
--- See Note [Equality predicates in IfaceType].
-ppr_equality :: IfaceTyCon -> [IfaceType] -> Maybe SDoc
-ppr_equality tc args
+-- See Note [Equality predicates in IfaceType]
+-- and Note [The equality types story] in TysPrim
+ppr_equality :: PprPrec -> IfaceTyCon -> [IfaceType] -> Maybe SDoc
+ppr_equality ctxt_prec tc args
   | hetero_eq_tc
   , [k1, k2, t1, t2] <- args
   = Just $ print_equality (k1, k2, t1, t2)
   | hetero_eq_tc
   , [k1, k2, t1, t2] <- args
   = Just $ print_equality (k1, k2, t1, t2)
@@ -1002,95 +1292,136 @@ ppr_equality tc args
   | otherwise
   = Nothing
   where
   | otherwise
   = Nothing
   where
-    homogeneous = case ifaceTyConSort $ ifaceTyConInfo tc of
-                    IfaceEqualityTyCon hom -> hom
-                    _other -> pprPanic "ppr_equality: homogeneity" (ppr tc)
+    homogeneous = tc_name `hasKey` eqTyConKey -- (~)
+               || hetero_tc_used_homogeneously
+      where
+        hetero_tc_used_homogeneously
+          = case ifaceTyConSort $ ifaceTyConInfo tc of
+                          IfaceEqualityTyCon -> True
+                          _other             -> False
+             -- True <=> a heterogeneous equality whose arguments
+             --          are (in this case) of the same kind
+
     tc_name = ifaceTyConName tc
     pp = ppr_ty
     hom_eq_tc = tc_name `hasKey` eqTyConKey            -- (~)
     hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey     -- (~#)
                 || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
                 || tc_name `hasKey` heqTyConKey        -- (~~)
     tc_name = ifaceTyConName tc
     pp = ppr_ty
     hom_eq_tc = tc_name `hasKey` eqTyConKey            -- (~)
     hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey     -- (~#)
                 || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
                 || tc_name `hasKey` heqTyConKey        -- (~~)
-
+    nominal_eq_tc = tc_name `hasKey` heqTyConKey       -- (~~)
+                 || tc_name `hasKey` eqPrimTyConKey    -- (~#)
     print_equality args =
     print_equality args =
-        sdocWithDynFlags
-        $ \dflags -> getPprStyle
-        $ \style -> print_equality' args style dflags
+        sdocWithDynFlags $ \dflags ->
+        getPprStyle      $ \style  ->
+        print_equality' args style dflags
 
     print_equality' (ki1, ki2, ty1, ty2) style dflags
 
     print_equality' (ki1, ki2, ty1, ty2) style dflags
-      | print_eqs
+      | -- If -fprint-equality-relations is on, just print the original TyCon
+        print_eqs
       = ppr_infix_eq (ppr tc)
 
       = ppr_infix_eq (ppr tc)
 
-      | hetero_eq_tc
-      , print_kinds || not homogeneous
-      = ppr_infix_eq (text "~~")
+      | -- Homogeneous use of heterogeneous equality (ty1 ~~ ty2)
+        --                 or unlifted equality      (ty1 ~# ty2)
+        nominal_eq_tc, homogeneous
+      = ppr_infix_eq (text "~")
 
 
+      | -- Heterogeneous use of unlifted equality (ty1 ~# ty2)
+        not homogeneous
+      = ppr_infix_eq (ppr heqTyCon)
+
+      | -- Homogeneous use of representational unlifted equality (ty1 ~R# ty2)
+        tc_name `hasKey` eqReprPrimTyConKey, homogeneous
+      = let ki | print_kinds = [pp appPrec ki1]
+               | otherwise   = []
+        in pprIfacePrefixApp ctxt_prec (ppr coercibleTyCon)
+                            (ki ++ [pp appPrec ty1, pp appPrec ty2])
+
+        -- The other cases work as you'd expect
       | otherwise
       | otherwise
-      = if tc_name `hasKey` eqReprPrimTyConKey
-        then text "Coercible"
-             <+> sep [ pp TyConPrec ty1, pp TyConPrec ty2 ]
-        else sep [pp TyOpPrec ty1, char '~', pp TyOpPrec ty2]
+      = ppr_infix_eq (ppr tc)
       where
       where
-        ppr_infix_eq eq_op
-           = sep [ parens (pp TyOpPrec ty1 <+> dcolon <+> pp TyOpPrec ki1)
-                 , eq_op
-                 , parens (pp TyOpPrec ty2 <+> dcolon <+> pp TyOpPrec ki2) ]
+        ppr_infix_eq :: SDoc -> SDoc
+        ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op
+                               (pp_ty_ki ty1 ki1) (pp_ty_ki ty2 ki2)
+          where
+            pp_ty_ki ty ki
+              | print_kinds
+              = parens (pp topPrec ty <+> dcolon <+> pp opPrec ki)
+              | otherwise
+              = pp opPrec ty
 
         print_kinds = gopt Opt_PrintExplicitKinds dflags
         print_eqs   = gopt Opt_PrintEqualityRelations dflags ||
                       dumpStyle style || debugStyle style
 
 
 
         print_kinds = gopt Opt_PrintExplicitKinds dflags
         print_eqs   = gopt Opt_PrintEqualityRelations dflags ||
                       dumpStyle style || debugStyle style
 
 
-pprIfaceCoTcApp :: TyPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
-pprIfaceCoTcApp ctxt_prec tc tys = ppr_iface_tc_app ppr_co ctxt_prec tc tys
+pprIfaceCoTcApp :: PprPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
+pprIfaceCoTcApp ctxt_prec tc tys =
+  ppr_iface_tc_app (\prec (co, _) -> ppr_co prec co) ctxt_prec tc
+    (map (, Required) tys)
+    -- We are trying to re-use ppr_iface_tc_app here, which requires its
+    -- arguments to be accompanied by visibilities. But visibility is
+    -- irrelevant when printing coercions, so just default everything to
+    -- Required.
 
 
-ppr_iface_tc_app :: (TyPrec -> a -> SDoc) -> TyPrec -> IfaceTyCon -> [a] -> SDoc
+-- | Pretty-prints an application of a type constructor to some arguments
+-- (whose visibilities are known). This is polymorphic (over @a@) since we use
+-- this function to pretty-print two different things:
+--
+-- 1. Types (from `pprTyTcApp'`)
+--
+-- 2. Coercions (from 'pprIfaceCoTcApp')
+ppr_iface_tc_app :: (PprPrec -> (a, ArgFlag) -> SDoc)
+                 -> PprPrec -> IfaceTyCon -> [(a, ArgFlag)] -> SDoc
 ppr_iface_tc_app pp _ tc [ty]
 ppr_iface_tc_app pp _ tc [ty]
-  | tc `ifaceTyConHasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp TopPrec ty)
-  | tc `ifaceTyConHasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
+  | tc `ifaceTyConHasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp topPrec ty)
 
 ppr_iface_tc_app pp ctxt_prec tc tys
 
 ppr_iface_tc_app pp ctxt_prec tc tys
-  | not (isSymOcc (nameOccName tc_name))
-  = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp TyConPrec) tys)
+  | tc `ifaceTyConHasKey` liftedTypeKindTyConKey
+  = kindType
 
 
-  | [ty1,ty2] <- tys  -- Infix, two arguments;
-                      -- we know nothing of precedence though
-  = pprIfaceInfixApp pp ctxt_prec (ppr tc) ty1 ty2
+  | not (isSymOcc (nameOccName (ifaceTyConName tc)))
+  = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp appPrec) tys)
 
 
-  |  tc `ifaceTyConHasKey` starKindTyConKey
-  || tc `ifaceTyConHasKey` unliftedTypeKindTyConKey
-  || tc `ifaceTyConHasKey` unicodeStarKindTyConKey
-  = ppr tc   -- Do not wrap *, # in parens
+  | [ ty1@(_, Required)
+    , ty2@(_, Required) ] <- tys
+      -- Infix, two visible arguments (we know nothing of precedence though).
+      -- Don't apply this special case if one of the arguments is invisible,
+      -- lest we print something like (@LiftedRep -> @LiftedRep) (#15941).
+  = pprIfaceInfixApp ctxt_prec (ppr tc)
+                     (pp opPrec ty1) (pp opPrec ty2)
 
   | otherwise
 
   | otherwise
-  = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp TyConPrec) tys)
-  where
-    tc_name = ifaceTyConName tc
+  = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp appPrec) tys)
 
 
-pprSum :: Arity -> IsPromoted -> IfaceTcArgs -> SDoc
+pprSum :: Arity -> PromotionFlag -> IfaceAppArgs -> SDoc
 pprSum _arity is_promoted args
   =   -- drop the RuntimeRep vars.
       -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
 pprSum _arity is_promoted args
   =   -- drop the RuntimeRep vars.
       -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
-    let tys   = tcArgsIfaceTypes args
+    let tys   = appArgsIfaceTypes args
         args' = drop (length tys `div` 2) tys
     in pprPromotionQuoteI is_promoted
         args' = drop (length tys `div` 2) tys
     in pprPromotionQuoteI is_promoted
-       <> sumParens (pprWithBars (ppr_ty TopPrec) args')
+       <> sumParens (pprWithBars (ppr_ty topPrec) args')
 
 
-pprTuple :: TupleSort -> IsPromoted -> IfaceTcArgs -> SDoc
-pprTuple ConstraintTuple IsNotPromoted ITC_Nil
-  = text "() :: Constraint"
+pprTuple :: PprPrec -> TupleSort -> PromotionFlag -> IfaceAppArgs -> SDoc
+pprTuple ctxt_prec ConstraintTuple NotPromoted IA_Nil
+  = maybeParen ctxt_prec appPrec $
+    text "() :: Constraint"
 
 -- All promoted constructors have kind arguments
 
 -- All promoted constructors have kind arguments
-pprTuple sort IsPromoted args
-  = let tys = tcArgsIfaceTypes args
+pprTuple sort IsPromoted args
+  = let tys = appArgsIfaceTypes args
         args' = drop (length tys `div` 2) tys
         args' = drop (length tys `div` 2) tys
+        spaceIfPromoted = case args' of
+          arg0:_ -> pprSpaceIfPromotedTyCon arg0
+          _ -> id
     in pprPromotionQuoteI IsPromoted <>
     in pprPromotionQuoteI IsPromoted <>
-       tupleParens sort (pprWithCommas pprIfaceType args')
+       tupleParens sort (spaceIfPromoted (pprWithCommas pprIfaceType args'))
 
 
-pprTuple sort promoted args
+pprTuple sort promoted args
   =   -- drop the RuntimeRep vars.
       -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
   =   -- drop the RuntimeRep vars.
       -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
-    let tys   = tcArgsIfaceTypes args
+    let tys   = appArgsIfaceTypes args
         args' = case sort of
                   UnboxedTuple -> drop (length tys `div` 2) tys
                   _            -> tys
         args' = case sort of
                   UnboxedTuple -> drop (length tys `div` 2) tys
                   _            -> tys
@@ -1103,79 +1434,84 @@ pprIfaceTyLit (IfaceNumTyLit n) = integer n
 pprIfaceTyLit (IfaceStrTyLit n) = text (show n)
 
 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc
 pprIfaceTyLit (IfaceStrTyLit n) = text (show n)
 
 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc
-pprIfaceCoercion = ppr_co TopPrec
-pprParendIfaceCoercion = ppr_co TyConPrec
-
-ppr_co :: TyPrec -> IfaceCoercion -> SDoc
-ppr_co _         (IfaceReflCo r ty) = angleBrackets (ppr ty) <> ppr_role r
+pprIfaceCoercion = ppr_co topPrec
+pprParendIfaceCoercion = ppr_co appPrec
+
+ppr_co :: PprPrec -> IfaceCoercion -> SDoc
+ppr_co _         (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal
+ppr_co _         (IfaceGReflCo r ty IfaceMRefl)
+  = angleBrackets (ppr ty) <> ppr_role r
+ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co))
+  = ppr_special_co ctxt_prec
+    (text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co]
 ppr_co ctxt_prec (IfaceFunCo r co1 co2)
 ppr_co ctxt_prec (IfaceFunCo r co1 co2)
-  = maybeParen ctxt_prec FunPrec $
-    sep (ppr_co FunPrec co1 : ppr_fun_tail co2)
+  = maybeParen ctxt_prec funPrec $
+    sep (ppr_co funPrec co1 : ppr_fun_tail co2)
   where
     ppr_fun_tail (IfaceFunCo r co1 co2)
   where
     ppr_fun_tail (IfaceFunCo r co1 co2)
-      = (arrow <> ppr_role r <+> ppr_co FunPrec co1) : ppr_fun_tail co2
+      = (arrow <> ppr_role r <+> ppr_co funPrec co1) : ppr_fun_tail co2
     ppr_fun_tail other_co
       = [arrow <> ppr_role r <+> pprIfaceCoercion other_co]
 
 ppr_co _         (IfaceTyConAppCo r tc cos)
     ppr_fun_tail other_co
       = [arrow <> ppr_role r <+> pprIfaceCoercion other_co]
 
 ppr_co _         (IfaceTyConAppCo r tc cos)
-  = parens (pprIfaceCoTcApp TopPrec tc cos) <> ppr_role r
+  = parens (pprIfaceCoTcApp topPrec tc cos) <> ppr_role r
 ppr_co ctxt_prec (IfaceAppCo co1 co2)
 ppr_co ctxt_prec (IfaceAppCo co1 co2)
-  = maybeParen ctxt_prec TyConPrec $
-    ppr_co FunPrec co1 <+> pprParendIfaceCoercion co2
+  = maybeParen ctxt_prec appPrec $
+    ppr_co funPrec co1 <+> pprParendIfaceCoercion co2
 ppr_co ctxt_prec co@(IfaceForAllCo {})
 ppr_co ctxt_prec co@(IfaceForAllCo {})
-  = maybeParen ctxt_prec FunPrec (pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co))
+  = maybeParen ctxt_prec funPrec $
+    pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co)
   where
     (tvs, inner_co) = split_co co
 
   where
     (tvs, inner_co) = split_co co
 
-    split_co (IfaceForAllCo (name, _) kind_co co')
+    split_co (IfaceForAllCo (IfaceTvBndr (name, _)) kind_co co')
+      = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
+    split_co (IfaceForAllCo (IfaceIdBndr (name, _)) kind_co co')
       = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
     split_co co' = ([], co')
 
       = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
     split_co co' = ([], co')
 
-ppr_co _         (IfaceCoVarCo covar)       = ppr covar
+-- Why these three? See Note [TcTyVars in IfaceType]
+ppr_co _ (IfaceFreeCoVar covar) = ppr covar
+ppr_co _ (IfaceCoVarCo covar)   = ppr covar
+ppr_co _ (IfaceHoleCo covar)    = braces (ppr covar)
 
 ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
 
 ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
-  = maybeParen ctxt_prec TyConPrec $
+  = maybeParen ctxt_prec appPrec $
     text "UnsafeCo" <+> ppr r <+>
     pprParendIfaceType ty1 <+> pprParendIfaceType ty2
 
     text "UnsafeCo" <+> ppr r <+>
     pprParendIfaceType ty1 <+> pprParendIfaceType ty2
 
-ppr_co ctxt_prec (IfaceUnivCo (IfaceHoleProv u) _ _ _)
- = maybeParen ctxt_prec TyConPrec $
-   sdocWithDynFlags $ \dflags ->
-     if gopt Opt_PrintExplicitCoercions dflags
-       then braces $ ppr u
-       else braces $ text "a hole"
-
-ppr_co _         (IfaceUnivCo _ _ ty1 ty2)
-  = angleBrackets ( ppr ty1 <> comma <+> ppr ty2 )
+ppr_co _ (IfaceUnivCo prov role ty1 ty2)
+  = text "Univ" <> (parens $
+      sep [ ppr role <+> pprIfaceUnivCoProv prov
+          , dcolon <+>  ppr ty1 <> comma <+> ppr ty2 ])
 
 ppr_co ctxt_prec (IfaceInstCo co ty)
 
 ppr_co ctxt_prec (IfaceInstCo co ty)
-  = maybeParen ctxt_prec TyConPrec $
+  = maybeParen ctxt_prec appPrec $
     text "Inst" <+> pprParendIfaceCoercion co
                         <+> pprParendIfaceCoercion ty
 
 ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
     text "Inst" <+> pprParendIfaceCoercion co
                         <+> pprParendIfaceCoercion ty
 
 ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
-  = maybeParen ctxt_prec TyConPrec $ ppr tc <+> parens (interpp'SP cos)
+  = maybeParen ctxt_prec appPrec $ ppr tc <+> parens (interpp'SP cos)
 
 ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
   = ppr_special_co ctxt_prec (ppr n <> brackets (ppr i)) cos
 ppr_co ctxt_prec (IfaceSymCo co)
   = ppr_special_co ctxt_prec (text "Sym") [co]
 ppr_co ctxt_prec (IfaceTransCo co1 co2)
 
 ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
   = ppr_special_co ctxt_prec (ppr n <> brackets (ppr i)) cos
 ppr_co ctxt_prec (IfaceSymCo co)
   = ppr_special_co ctxt_prec (text "Sym") [co]
 ppr_co ctxt_prec (IfaceTransCo co1 co2)
-  = ppr_special_co ctxt_prec  (text "Trans") [co1,co2]
+  = maybeParen ctxt_prec opPrec $
+    ppr_co opPrec co1 <+> semi <+> ppr_co opPrec co2
 ppr_co ctxt_prec (IfaceNthCo d co)
   = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
 ppr_co ctxt_prec (IfaceLRCo lr co)
   = ppr_special_co ctxt_prec (ppr lr) [co]
 ppr_co ctxt_prec (IfaceSubCo co)
   = ppr_special_co ctxt_prec (text "Sub") [co]
 ppr_co ctxt_prec (IfaceNthCo d co)
   = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
 ppr_co ctxt_prec (IfaceLRCo lr co)
   = ppr_special_co ctxt_prec (ppr lr) [co]
 ppr_co ctxt_prec (IfaceSubCo co)
   = ppr_special_co ctxt_prec (text "Sub") [co]
-ppr_co ctxt_prec (IfaceCoherenceCo co1 co2)
-  = ppr_special_co ctxt_prec (text "Coh") [co1,co2]
 ppr_co ctxt_prec (IfaceKindCo co)
   = ppr_special_co ctxt_prec (text "Kind") [co]
 
 ppr_co ctxt_prec (IfaceKindCo co)
   = ppr_special_co ctxt_prec (text "Kind") [co]
 
-ppr_special_co :: TyPrec -> SDoc -> [IfaceCoercion] -> SDoc
+ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
 ppr_special_co ctxt_prec doc cos
 ppr_special_co ctxt_prec doc cos
-  = maybeParen ctxt_prec TyConPrec
+  = maybeParen ctxt_prec appPrec
                (sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
 
 ppr_role :: Role -> SDoc
                (sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
 
 ppr_role :: Role -> SDoc
@@ -1185,6 +1521,17 @@ ppr_role r = underscore <> pp_role
                     Representational -> char 'R'
                     Phantom          -> char 'P'
 
                     Representational -> char 'R'
                     Phantom          -> char 'P'
 
+------------------
+pprIfaceUnivCoProv :: IfaceUnivCoProv -> SDoc
+pprIfaceUnivCoProv IfaceUnsafeCoerceProv
+  = text "unsafe"
+pprIfaceUnivCoProv (IfacePhantomProv co)
+  = text "phantom" <+> pprParendIfaceCoercion co
+pprIfaceUnivCoProv (IfaceProofIrrelProv co)
+  = text "irrel" <+> pprParendIfaceCoercion co
+pprIfaceUnivCoProv (IfacePluginProv s)
+  = text "plugin" <+> doubleQuotes (text s)
+
 -------------------
 instance Outputable IfaceTyCon where
   ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
 -------------------
 instance Outputable IfaceTyCon where
   ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
@@ -1193,8 +1540,8 @@ pprPromotionQuote :: IfaceTyCon -> SDoc
 pprPromotionQuote tc =
     pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
 
 pprPromotionQuote tc =
     pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
 
-pprPromotionQuoteI  :: IsPromoted -> SDoc
-pprPromotionQuoteI IsNotPromoted = empty
+pprPromotionQuoteI  :: PromotionFlag -> SDoc
+pprPromotionQuoteI NotPromoted = empty
 pprPromotionQuoteI IsPromoted    = char '\''
 
 instance Outputable IfaceCoercion where
 pprPromotionQuoteI IsPromoted    = char '\''
 
 instance Outputable IfaceCoercion where
@@ -1207,24 +1554,11 @@ instance Binary IfaceTyCon where
                i <- get bh
                return (IfaceTyCon n i)
 
                i <- get bh
                return (IfaceTyCon n i)
 
-instance Binary IsPromoted where
-   put_ bh IsNotPromoted = putByte bh 0
-   put_ bh IsPromoted    = putByte bh 1
-
-   get bh = do
-       n <- getByte bh
-       case n of
-         0 -> return IsNotPromoted
-         1 -> return IsPromoted
-         _ -> fail "Binary(IsPromoted): fail)"
-
 instance Binary IfaceTyConSort where
    put_ bh IfaceNormalTyCon             = putByte bh 0
    put_ bh (IfaceTupleTyCon arity sort) = putByte bh 1 >> put_ bh arity >> put_ bh sort
    put_ bh (IfaceSumTyCon arity)        = putByte bh 2 >> put_ bh arity
 instance Binary IfaceTyConSort where
    put_ bh IfaceNormalTyCon             = putByte bh 0
    put_ bh (IfaceTupleTyCon arity sort) = putByte bh 1 >> put_ bh arity >> put_ bh sort
    put_ bh (IfaceSumTyCon arity)        = putByte bh 2 >> put_ bh arity
-   put_ bh (IfaceEqualityTyCon hom)
-     | hom                              = putByte bh 3
-     | otherwise                        = putByte bh 4
+   put_ bh IfaceEqualityTyCon           = putByte bh 3
 
    get bh = do
        n <- getByte bh
 
    get bh = do
        n <- getByte bh
@@ -1232,9 +1566,7 @@ instance Binary IfaceTyConSort where
          0 -> return IfaceNormalTyCon
          1 -> IfaceTupleTyCon <$> get bh <*> get bh
          2 -> IfaceSumTyCon <$> get bh
          0 -> return IfaceNormalTyCon
          1 -> IfaceTupleTyCon <$> get bh <*> get bh
          2 -> IfaceSumTyCon <$> get bh
-         3 -> return $ IfaceEqualityTyCon True
-         4 -> return $ IfaceEqualityTyCon False
-         _ -> fail "Binary(IfaceTyConSort): fail"
+         _ -> return IfaceEqualityTyCon
 
 instance Binary IfaceTyConInfo where
    put_ bh (IfaceTyConInfo i s) = put_ bh i >> put_ bh s
 
 instance Binary IfaceTyConInfo where
    put_ bh (IfaceTyConInfo i s) = put_ bh i >> put_ bh s
@@ -1257,26 +1589,22 @@ instance Binary IfaceTyLit where
                  ; return (IfaceStrTyLit n) }
          _ -> panic ("get IfaceTyLit " ++ show tag)
 
                  ; return (IfaceStrTyLit n) }
          _ -> panic ("get IfaceTyLit " ++ show tag)
 
-instance Binary IfaceTcArgs where
+instance Binary IfaceAppArgs where
   put_ bh tk =
     case tk of
   put_ bh tk =
     case tk of
-      ITC_Vis   t ts -> putByte bh 0 >> put_ bh t >> put_ bh ts
-      ITC_Invis t ts -> putByte bh 1 >> put_ bh t >> put_ bh ts
-      ITC_Nil        -> putByte bh 2
+      IA_Arg t a ts -> putByte bh 0 >> put_ bh t >> put_ bh a >> put_ bh ts
+      IA_Nil        -> putByte bh 1
 
   get bh =
     do c <- getByte bh
        case c of
          0 -> do
            t  <- get bh
 
   get bh =
     do c <- getByte bh
        case c of
          0 -> do
            t  <- get bh
+           a  <- get bh
            ts <- get bh
            ts <- get bh
-           return $! ITC_Vis t ts
-         1 -> do
-           t  <- get bh
-           ts <- get bh
-           return $! ITC_Invis t ts
-         2 -> return ITC_Nil
-         _ -> panic ("get IfaceTcArgs " ++ show c)
+           return $! IA_Arg t a ts
+         1 -> return IA_Nil
+         _ -> panic ("get IfaceAppArgs " ++ show c)
 
 -------------------
 
 
 -------------------
 
@@ -1284,7 +1612,7 @@ instance Binary IfaceTcArgs where
 --
 -- In the event that we are printing a singleton context (e.g. @Eq a@) we can
 -- omit parentheses. However, we must take care to set the precedence correctly
 --
 -- In the event that we are printing a singleton context (e.g. @Eq a@) we can
 -- omit parentheses. However, we must take care to set the precedence correctly
--- to TyOpPrec, since something like @a :~: b@ must be parenthesized (see
+-- to opPrec, since something like @a :~: b@ must be parenthesized (see
 -- #9658).
 --
 -- When printing a larger context we use 'fsep' instead of 'sep' so that
 -- #9658).
 --
 -- When printing a larger context we use 'fsep' instead of 'sep' so that
@@ -1311,24 +1639,28 @@ instance Binary IfaceTcArgs where
 
 
 
 
 
 
--- | Prints "(C a, D b) =>", including the arrow. This is used when we want to
--- print a context in a type.
+-- | Prints "(C a, D b) =>", including the arrow.
+-- Used when we want to print a context in a type, so we
+-- use 'funPrec' to decide whether to parenthesise a singleton
+-- predicate; e.g.   Num a => a -> a
 pprIfaceContextArr :: [IfacePredType] -> SDoc
 pprIfaceContextArr []     = empty
 pprIfaceContextArr :: [IfacePredType] -> SDoc
 pprIfaceContextArr []     = empty
-pprIfaceContextArr [pred] = ppr_ty TyOpPrec pred <+> darrow
-pprIfaceContextArr preds  =
-    parens (fsep (punctuate comma (map ppr preds))) <+> darrow
+pprIfaceContextArr [pred] = ppr_ty funPrec pred <+> darrow
+pprIfaceContextArr preds  = ppr_parend_preds preds <+> darrow
 
 
--- | Prints a context or @()@ if empty. This is used when, e.g., we want to
--- display a context in an error message.
-pprIfaceContext :: [IfacePredType] -> SDoc
-pprIfaceContext []     = parens empty
-pprIfaceContext [pred] = ppr_ty TyOpPrec pred
-pprIfaceContext preds  = parens (fsep (punctuate comma (map ppr preds)))
+-- | Prints a context or @()@ if empty
+-- You give it the context precedence
+pprIfaceContext :: PprPrec -> [IfacePredType] -> SDoc
+pprIfaceContext _    []     = text "()"
+pprIfaceContext prec [pred] = ppr_ty prec pred
+pprIfaceContext _    preds  = ppr_parend_preds preds
+
+ppr_parend_preds :: [IfacePredType] -> SDoc
+ppr_parend_preds preds = parens (fsep (punctuate comma (map ppr preds)))
 
 instance Binary IfaceType where
 
 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
 
     put_ bh (IfaceForAllTy aa ab) = do
             putByte bh 0
@@ -1389,64 +1721,79 @@ instance Binary IfaceType where
               _  -> do n <- get bh
                        return (IfaceLitTy n)
 
               _  -> do n <- get bh
                        return (IfaceLitTy n)
 
+instance Binary IfaceMCoercion where
+  put_ bh IfaceMRefl = do
+          putByte bh 1
+  put_ bh (IfaceMCo co) = do
+          putByte bh 2
+          put_ bh co
+
+  get bh = do
+    tag <- getByte bh
+    case tag of
+         1 -> return IfaceMRefl
+         2 -> do a <- get bh
+                 return $ IfaceMCo a
+         _ -> panic ("get IfaceMCoercion " ++ show tag)
+
 instance Binary IfaceCoercion where
 instance Binary IfaceCoercion where
-  put_ bh (IfaceReflCo a b) = do
+  put_ bh (IfaceReflCo a) = do
           putByte bh 1
           put_ bh a
           putByte bh 1
           put_ bh a
+  put_ bh (IfaceGReflCo a b c) = do
+          putByte bh 2
+          put_ bh a
           put_ bh b
           put_ bh b
+          put_ bh c
   put_ bh (IfaceFunCo a b c) = do
   put_ bh (IfaceFunCo a b c) = do
-          putByte bh 2
+          putByte bh 3
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceTyConAppCo a b c) = do
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceTyConAppCo a b c) = do
-          putByte bh 3
+          putByte bh 4
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceAppCo a b) = do
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceAppCo a b) = do
-          putByte bh 4
+          putByte bh 5
           put_ bh a
           put_ bh b
   put_ bh (IfaceForAllCo a b c) = do
           put_ bh a
           put_ bh b
   put_ bh (IfaceForAllCo a b c) = do
-          putByte bh 5
+          putByte bh 6
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceCoVarCo a) = do
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceCoVarCo a) = do
-          putByte bh 6
+          putByte bh 7
           put_ bh a
   put_ bh (IfaceAxiomInstCo a b c) = do
           put_ bh a
   put_ bh (IfaceAxiomInstCo a b c) = do
-          putByte bh 7
+          putByte bh 8
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceUnivCo a b c d) = do
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceUnivCo a b c d) = do
-          putByte bh 8
+          putByte bh 9
           put_ bh a
           put_ bh b
           put_ bh c
           put_ bh d
   put_ bh (IfaceSymCo a) = do
           put_ bh a
           put_ bh b
           put_ bh c
           put_ bh d
   put_ bh (IfaceSymCo a) = do
-          putByte bh 9
-          put_ bh a
-  put_ bh (IfaceTransCo a b) = do
           putByte bh 10
           put_ bh a
           putByte bh 10
           put_ bh a
-          put_ bh b
-  put_ bh (IfaceNthCo a b) = do
+  put_ bh (IfaceTransCo a b) = do
           putByte bh 11
           put_ bh a
           put_ bh b
           putByte bh 11
           put_ bh a
           put_ bh b
-  put_ bh (IfaceLRCo a b) = do
+  put_ bh (IfaceNthCo a b) = do
           putByte bh 12
           put_ bh a
           put_ bh b
           putByte bh 12
           put_ bh a
           put_ bh b
-  put_ bh (IfaceInstCo a b) = do
+  put_ bh (IfaceLRCo a b) = do
           putByte bh 13
           put_ bh a
           put_ bh b
           putByte bh 13
           put_ bh a
           put_ bh b
-  put_ bh (IfaceCoherenceCo a b) = do
+  put_ bh (IfaceInstCo a b) = do
           putByte bh 14
           put_ bh a
           put_ bh b
           putByte bh 14
           put_ bh a
           put_ bh b
@@ -1460,56 +1807,61 @@ instance Binary IfaceCoercion where
           putByte bh 17
           put_ bh a
           put_ bh b
           putByte bh 17
           put_ bh a
           put_ bh b
+  put_ _ (IfaceFreeCoVar cv)
+       = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
+  put_ _  (IfaceHoleCo cv)
+       = pprPanic "Can't serialise IfaceHoleCo" (ppr cv)
+          -- See Note [Holes in IfaceCoercion]
 
   get bh = do
       tag <- getByte bh
       case tag of
            1 -> do a <- get bh
 
   get bh = do
       tag <- getByte bh
       case tag of
            1 -> do a <- get bh
-                   b <- get bh
-                   return $ IfaceReflCo a b
+                   return $ IfaceReflCo a
            2 -> do a <- get bh
                    b <- get bh
                    c <- get bh
            2 -> do a <- get bh
                    b <- get bh
                    c <- get bh
-                   return $ IfaceFunCo a b c
+                   return $ IfaceGReflCo a b c
            3 -> do a <- get bh
                    b <- get bh
                    c <- get bh
            3 -> do a <- get bh
                    b <- get bh
                    c <- get bh
-                   return $ IfaceTyConAppCo a b c
+                   return $ IfaceFunCo a b c
            4 -> do a <- get bh
                    b <- get bh
            4 -> do a <- get bh
                    b <- get bh
-                   return $ IfaceAppCo a b
+                   c <- get bh
+                   return $ IfaceTyConAppCo a b c
            5 -> do a <- get bh
                    b <- get bh
            5 -> do a <- get bh
                    b <- get bh
+                   return $ IfaceAppCo a b
+           6 -> do a <- get bh
+                   b <- get bh
                    c <- get bh
                    return $ IfaceForAllCo a b c
                    c <- get bh
                    return $ IfaceForAllCo a b c
-           6 -> do a <- get bh
-                   return $ IfaceCoVarCo a
            7 -> do a <- get bh
            7 -> do a <- get bh
+                   return $ IfaceCoVarCo a
+           8 -> do a <- get bh
                    b <- get bh
                    c <- get bh
                    return $ IfaceAxiomInstCo a b c
                    b <- get bh
                    c <- get bh
                    return $ IfaceAxiomInstCo a b c
-           8 -> do a <- get bh
+           9 -> do a <- get bh
                    b <- get bh
                    c <- get bh
                    d <- get bh
                    return $ IfaceUnivCo a b c d
                    b <- get bh
                    c <- get bh
                    d <- get bh
                    return $ IfaceUnivCo a b c d
-           9 -> do a <- get bh
-                   return $ IfaceSymCo a
            10-> do a <- get bh
            10-> do a <- get bh
-                   b <- get bh
-                   return $ IfaceTransCo a b
+                   return $ IfaceSymCo a
            11-> do a <- get bh
                    b <- get bh
            11-> do a <- get bh
                    b <- get bh
-                   return $ IfaceNthCo a b
+                   return $ IfaceTransCo a b
            12-> do a <- get bh
                    b <- get bh
            12-> do a <- get bh
                    b <- get bh
-                   return $ IfaceLRCo a b
+                   return $ IfaceNthCo a b
            13-> do a <- get bh
                    b <- get bh
            13-> do a <- get bh
                    b <- get bh
-                   return $ IfaceInstCo a b
+                   return $ IfaceLRCo a b
            14-> do a <- get bh
                    b <- get bh
            14-> do a <- get bh
                    b <- get bh
-                   return $ IfaceCoherenceCo a b
+                   return $ IfaceInstCo a b
            15-> do a <- get bh
                    return $ IfaceKindCo a
            16-> do a <- get bh
            15-> do a <- get bh
                    return $ IfaceKindCo a
            16-> do a <- get bh
@@ -1530,9 +1882,6 @@ instance Binary IfaceUnivCoProv where
   put_ bh (IfacePluginProv a) = do
           putByte bh 4
           put_ bh a
   put_ bh (IfacePluginProv a) = do
           putByte bh 4
           put_ bh a
-  put_ _  (IfaceHoleProv _) =
-          pprPanic "Binary(IfaceUnivCoProv) hit a hole" empty
-  -- See Note [Holes in IfaceUnivCoProv]
 
   get bh = do
       tag <- getByte bh
 
   get bh = do
       tag <- getByte bh