Refine the suppression of RuntimeRep variables
[ghc.git] / compiler / iface / IfaceType.hs
index e83c25e..f4032d2 100644 (file)
@@ -6,65 +6,74 @@
 This module defines interface types and binders
 -}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, FlexibleInstances, BangPatterns #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TupleSections #-}
+    -- FlexibleInstances for Binary (DefMethSpec IfaceType)
+
 module IfaceType (
         IfExtName, IfLclName,
 
-        IfaceType(..), IfacePredType, IfaceKind, IfaceTyCon(..), IfaceCoercion(..),
-        IfaceTyLit(..), IfaceTcArgs(..),
-        IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr, IfaceTvBndr, IfaceIdBndr,
+        IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
+        IfaceMCoercion(..),
+        IfaceUnivCoProv(..),
+        IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..),
+        IfaceTyLit(..), IfaceAppArgs(..),
+        IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
+        IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
+        IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
+        mkIfaceForAllTvBndr,
 
-        -- Conversion from Type -> IfaceType
-        toIfaceType, toIfaceTypes, toIfaceKind, toIfaceTyVar,
-        toIfaceContext, toIfaceBndr, toIfaceIdBndr,
-        toIfaceTvBndrs, toIfaceTyCon, toIfaceTyCon_name,
-        toIfaceTcArgs,
+        ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
+        ifTyConBinderVar, ifTyConBinderName,
 
-        -- Conversion from IfaceTcArgs -> IfaceType
-        tcArgsIfaceTypes,
+        -- Equality testing
+        isIfaceLiftedTypeKind,
 
-        -- Conversion from Coercion -> IfaceCoercion
-        toIfaceCoercion,
+        -- Conversion from IfaceAppArgs to IfaceTypes/ArgFlags
+        appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
 
         -- Printing
-        pprIfaceType, pprParendIfaceType,
-        pprIfaceContext, pprIfaceContextArr, pprIfaceContextMaybe,
-        pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTvBndrs,
-        pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
-        pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType,
+        pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
+        pprIfaceContext, pprIfaceContextArr,
+        pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
+        pprIfaceBndrs, pprIfaceAppArgs, pprParendIfaceAppArgs,
+        pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
+        pprIfaceSigmaType, pprIfaceTyLit,
         pprIfaceCoercion, pprParendIfaceCoercion,
         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
+        pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
+
+        suppressIfaceInvisibles,
+        stripIfaceInvisVars,
+        stripInvisArgs,
 
-        suppressIfaceKinds,
-        stripIfaceKindVars,
-        stripKindArgs,
-        substIfaceType, substIfaceTyVar, substIfaceTcArgs, mkIfaceTySubst
+        mkIfaceTySubst, substIfaceTyVar, substIfaceAppArgs, inDomIfaceTySubst
     ) where
 
 #include "HsVersions.h"
 
-import Coercion
-import DataCon ( dataConTyCon )
-import TcType
+import GhcPrelude
+
+import {-# SOURCE #-} TysWiredIn ( coercibleTyCon, heqTyCon
+                                 , liftedRepDataConTyCon )
+import {-# SOURCE #-} TyCoRep    ( isRuntimeRepTy )
+
 import DynFlags
-import TypeRep
-import Unique( hasKey )
-import Util ( filterOut, lengthIs, zipWithEqual )
 import TyCon hiding ( pprPromotionQuote )
 import CoAxiom
-import Id
 import Var
--- import RnEnv( FastStringEnv, mkFsEnv, lookupFsEnv )
-import TysWiredIn
-import TysPrim
-import PrelNames( funTyConKey, ipClassName )
+import PrelNames
 import Name
 import BasicTypes
 import Binary
 import Outputable
 import FastString
-import UniqSet
-import Data.Maybe( fromMaybe )
+import FastStringEnv
+import Util
+
+import Data.Maybe( isJust )
+import qualified Data.Semigroup as Semi
 
 {-
 ************************************************************************
@@ -86,26 +95,59 @@ data IfaceBndr          -- Local (non-top-level) binders
 type IfaceIdBndr  = (IfLclName, IfaceType)
 type IfaceTvBndr  = (IfLclName, IfaceKind)
 
+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
   = IfaceNoOneShot   -- and Note [The oneShot function] in MkId
   | IfaceOneShot
 
-type IfaceLamBndr
-  = (IfaceBndr, IfaceOneShot)
+
+{-
+%************************************************************************
+%*                                                                      *
+                IfaceType
+%*                                                                      *
+%************************************************************************
+-}
 
 -------------------------------
 type IfaceKind     = IfaceType
 
-data IfaceType     -- A kind of universal type, used for types and kinds
-  = IfaceTyVar    IfLclName               -- Type/coercion variable only, not tycon
-  | IfaceAppTy    IfaceType IfaceType
-  | IfaceFunTy    IfaceType IfaceType
-  | IfaceDFunTy   IfaceType IfaceType
-  | IfaceForAllTy IfaceTvBndr IfaceType
-  | IfaceTyConApp IfaceTyCon IfaceTcArgs  -- Not necessarily saturated
-                                          -- Includes newtypes, synonyms, tuples
-  | IfaceLitTy IfaceTyLit
+-- | 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?
+       PromotionFlag                 -- A bit like IfaceTyCon
+       IfaceAppArgs               -- arity = length args
+          -- For promoted data cons, the kind args are omitted
 
 type IfacePredType = IfaceType
 type IfaceContext = [IfacePredType]
@@ -113,207 +155,510 @@ type IfaceContext = [IfacePredType]
 data IfaceTyLit
   = IfaceNumTyLit Integer
   | IfaceStrTyLit FastString
+  deriving (Eq)
+
+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 @{...}.
 
--- See Note [Suppressing kinds]
--- 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_Type IfaceType IfaceTcArgs
-  | ITC_Kind IfaceKind IfaceTcArgs
+           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.
 -- We have to tag them in order to pretty print them
 -- properly.
-data IfaceTyCon
-  = IfaceTc              { ifaceTyConName :: IfExtName }
-  | IfacePromotedDataCon { ifaceTyConName :: IfExtName }
-  | IfacePromotedTyCon   { ifaceTyConName :: IfExtName }
+data IfaceTyCon = IfaceTyCon { ifaceTyConName :: IfExtName
+                             , ifaceTyConInfo :: IfaceTyConInfo }
+    deriving (Eq)
+
+-- | The various types of TyCons which have special, built-in syntax.
+data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
+
+                    | IfaceTupleTyCon !Arity !TupleSort
+                      -- ^ e.g. @(a, b, c)@ or @(#a, b, c#)@.
+                      -- The arity is the tuple width, not the tycon arity
+                      -- (which is twice the width in the case of unboxed
+                      -- tuples).
+
+                    | IfaceSumTyCon !Arity
+                      -- ^ e.g. @(a | b | c)@
+
+                    | 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)
+
+{- Note [Free tyvars in IfaceType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
+an IfaceType and pretty printing that.  This eliminates a lot of
+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.
+
+So we simply embed a TyVar in IfaceType with the IfaceFreeTyVar constructor.
+Note that:
+
+* 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.
+
+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]
+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 IfaceCoercion
-  = IfaceReflCo      Role IfaceType
-  | IfaceFunCo       Role IfaceCoercion IfaceCoercion
-  | IfaceTyConAppCo  Role IfaceTyCon [IfaceCoercion]
-  | IfaceAppCo       IfaceCoercion IfaceCoercion
-  | IfaceForAllCo    IfaceTvBndr IfaceCoercion
-  | IfaceCoVarCo     IfLclName
-  | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
-  | IfaceUnivCo      FastString Role IfaceType IfaceType
-  | IfaceSymCo       IfaceCoercion
-  | IfaceTransCo     IfaceCoercion IfaceCoercion
-  | IfaceNthCo       Int IfaceCoercion
-  | IfaceLRCo        LeftOrRight IfaceCoercion
-  | IfaceInstCo      IfaceCoercion IfaceType
-  | IfaceSubCo       IfaceCoercion
-  | IfaceAxiomRuleCo IfLclName [IfaceType] [IfaceCoercion]
+data IfaceTyConInfo   -- Used to guide pretty-printing
+                      -- and to disambiguate D from 'D (they share a name)
+  = IfaceTyConInfo { ifaceTyConIsPromoted :: PromotionFlag
+                   , ifaceTyConSort       :: IfaceTyConSort }
+    deriving (Eq)
 
-{-
-************************************************************************
-*                                                                      *
+data IfaceMCoercion
+  = IfaceMRefl
+  | IfaceMCo IfaceCoercion
+
+data IfaceCoercion
+  = IfaceReflCo       IfaceType
+  | IfaceGReflCo      Role IfaceType (IfaceMCoercion)
+  | IfaceFunCo        Role IfaceCoercion IfaceCoercion
+  | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
+  | IfaceAppCo        IfaceCoercion IfaceCoercion
+  | IfaceForAllCo     IfaceBndr IfaceCoercion 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
+  | IfaceKindCo       IfaceCoercion
+  | IfaceSubCo        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
+
+{- 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
 *                                                                      *
 ************************************************************************
 -}
 
-splitIfaceSigmaTy :: IfaceType -> ([IfaceTvBndr], [IfacePredType], IfaceType)
+ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
+ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
+
+isIfaceLiftedTypeKind :: IfaceKind -> Bool
+isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
+  = isLiftedTypeKindTyConName (ifaceTyConName tc)
+isIfaceLiftedTypeKind (IfaceTyConApp tc
+                       (IA_Arg (IfaceTyConApp ptr_rep_lifted IA_Nil)
+                               Required IA_Nil))
+  =  tc `ifaceTyConHasKey` tYPETyConKey
+  && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
+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
-  = (tvs, theta, tau)
+  = case (bndrs, theta) of
+      ([], []) -> (bndrs, theta, tau)
+      _        -> let (bndrs', theta', tau') = splitIfaceSigmaTy tau
+                   in (bndrs ++ bndrs', theta ++ theta', tau')
   where
-    (tvs,   rho)   = split_foralls ty
+    (bndrs, rho)   = split_foralls ty
     (theta, tau)   = split_rho rho
 
-    split_foralls (IfaceForAllTy tv ty)
-        = case split_foralls ty of { (tvs, rho) -> (tv:tvs, rho) }
+    split_foralls (IfaceForAllTy bndr ty)
+        = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
     split_foralls rho = ([], rho)
 
     split_rho (IfaceDFunTy ty1 ty2)
         = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
     split_rho tau = ([], tau)
 
-suppressIfaceKinds :: DynFlags -> [IfaceTvBndr] -> [a] -> [a]
-suppressIfaceKinds dflags tys xs
+suppressIfaceInvisibles :: DynFlags -> [IfaceTyConBinder] -> [a] -> [a]
+suppressIfaceInvisibles dflags tys xs
   | gopt Opt_PrintExplicitKinds dflags = xs
   | otherwise = suppress tys xs
     where
       suppress _       []      = []
       suppress []      a       = a
-      suppress (k:ks) a@(_:xs)
-        | isIfaceKindVar k = suppress ks xs
-        | otherwise        = a
+      suppress (k:ks) (x:xs)
+        | isInvisibleTyConBinder k =     suppress ks xs
+        | otherwise                = x : suppress ks xs
 
-stripIfaceKindVars :: DynFlags -> [IfaceTvBndr] -> [IfaceTvBndr]
-stripIfaceKindVars dflags tyvars
+stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
+stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
-  | otherwise = filterOut isIfaceKindVar tyvars
-
-isIfaceKindVar :: IfaceTvBndr -> Bool
-isIfaceKindVar (_, IfaceTyConApp tc _) = ifaceTyConName tc == superKindTyConName
-isIfaceKindVar _                       = False
-
-ifTyVarsOfType :: IfaceType -> UniqSet IfLclName
-ifTyVarsOfType ty
-  = case ty of
-      IfaceTyVar v -> unitUniqSet v
-      IfaceAppTy fun arg
-        -> ifTyVarsOfType fun `unionUniqSets` ifTyVarsOfType arg
-      IfaceFunTy arg res
-        -> ifTyVarsOfType arg `unionUniqSets` ifTyVarsOfType res
-      IfaceDFunTy arg res
-        -> ifTyVarsOfType arg `unionUniqSets` ifTyVarsOfType res
-      IfaceForAllTy (var,t) ty
-        -> delOneFromUniqSet (ifTyVarsOfType ty) var `unionUniqSets`
-           ifTyVarsOfType t
-      IfaceTyConApp _ args -> ifTyVarsOfArgs args
-      IfaceLitTy    _      -> emptyUniqSet
-
-ifTyVarsOfArgs :: IfaceTcArgs -> UniqSet IfLclName
-ifTyVarsOfArgs args = argv emptyUniqSet args
-   where
-     argv vs (ITC_Type t ts) = argv (vs `unionUniqSets` (ifTyVarsOfType t)) ts
-     argv vs (ITC_Kind k ks) = argv (vs `unionUniqSets` (ifTyVarsOfType k)) ks
-     argv vs ITC_Nil         = vs
+  | otherwise = filterOut isInvisibleTyConBinder tyvars
 
-{-
-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.
--}
+-- | Extract an 'IfaceBndr' from an 'IfaceForAllBndr'.
+ifForAllBndrVar :: IfaceForAllBndr -> IfaceBndr
+ifForAllBndrVar = binderVar
 
-type IfaceTySubst = FastStringEnv IfaceType
+-- | Extract the variable name from an 'IfaceForAllBndr'.
+ifForAllBndrName :: IfaceForAllBndr -> IfLclName
+ifForAllBndrName fab = ifaceBndrName (ifForAllBndrVar fab)
 
-mkIfaceTySubst :: [IfaceTvBndr] -> [IfaceType] -> IfaceTySubst
-mkIfaceTySubst tvs tys = mkFsEnv $ zipWithEqual "mkIfaceTySubst" (\(fs,_) ty -> (fs,ty)) tvs tys
+-- | Extract an 'IfaceBndr' from an 'IfaceTyConBinder'.
+ifTyConBinderVar :: IfaceTyConBinder -> IfaceBndr
+ifTyConBinderVar = binderVar
+
+-- | Extract the variable name from an 'IfaceTyConBinder'.
+ifTyConBinderName :: IfaceTyConBinder -> IfLclName
+ifTyConBinderName tcb = ifaceBndrName (ifTyConBinderVar tcb)
+
+ifTypeIsVarFree :: IfaceType -> Bool
+-- Returns True if the type definitely has no variables at all
+-- Just used to control pretty printing
+ifTypeIsVarFree ty = go ty
+  where
+    go (IfaceTyVar {})         = False
+    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 (IfaceTyConApp _ args)  = go_args args
+    go (IfaceTupleTy _ _ args) = go_args args
+    go (IfaceLitTy _)          = True
+    go (IfaceCastTy {})        = False -- Safe
+    go (IfaceCoercionTy {})    = False -- Safe
+
+    go_args IA_Nil = True
+    go_args (IA_Arg arg _ args) = go arg && go_args args
+
+{- 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]
+
+mkIfaceTySubst :: [(IfLclName,IfaceType)] -> IfaceTySubst
+-- See Note [Substitution on IfaceType]
+mkIfaceTySubst eq_spec = mkFsEnv eq_spec
+
+inDomIfaceTySubst :: IfaceTySubst -> IfaceTvBndr -> Bool
+-- See Note [Substitution on IfaceType]
+inDomIfaceTySubst subst (fs, _) = isJust (lookupFsEnv subst fs)
 
 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
+-- See Note [Substitution on IfaceType]
 substIfaceType env ty
   = go ty
   where
+    go (IfaceFreeTyVar tv)    = IfaceFreeTyVar 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 (IfaceTyConApp tc tys) = IfaceTyConApp tc (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)
-
-substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs
-substIfaceTcArgs env args
+    go (IfaceCastTy ty co)    = IfaceCastTy (go ty) (go_co co)
+    go (IfaceCoercionTy co)   = IfaceCoercionTy (go_co co)
+
+    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 (IfaceFreeCoVar cv)        = IfaceFreeCoVar 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 (IfaceTransCo co1 co2)     = IfaceTransCo (go_co co1) (go_co co2)
+    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 (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_cos = map go_co
+
+    go_prov IfaceUnsafeCoerceProv    = IfaceUnsafeCoerceProv
+    go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
+    go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
+    go_prov (IfacePluginProv str)    = IfacePluginProv str
+
+substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
+substIfaceAppArgs env args
   = go args
   where
-    go ITC_Nil           = ITC_Nil
-    go (ITC_Type ty tys) = ITC_Type (substIfaceType env ty) (go tys)
-    go (ITC_Kind ty tys) = ITC_Kind (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
 
+
 {-
 ************************************************************************
 *                                                                      *
-                Functions over IFaceTcArgs
+                Functions over IfaceAppArgs
 *                                                                      *
 ************************************************************************
 -}
 
-stripKindArgs :: DynFlags -> IfaceTcArgs -> IfaceTcArgs
-stripKindArgs dflags tys
+stripInvisArgs :: DynFlags -> IfaceAppArgs -> IfaceAppArgs
+stripInvisArgs dflags tys
   | gopt Opt_PrintExplicitKinds dflags = tys
-  | otherwise = suppressKinds tys
+  | otherwise = suppress_invis tys
     where
-      suppressKinds c
+      suppress_invis c
         = case c of
-            ITC_Kind _ ts -> suppressKinds ts
-            _ -> c
-
-toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
--- See Note [Suppressing kinds]
-toIfaceTcArgs tc ty_args
-  = go (tyConKind tc) ty_args
+            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
-    go _                []     = ITC_Nil
-    go (ForAllTy _ res) (t:ts) = ITC_Kind (toIfaceKind t) (go res ts)
-    go (FunTy _ res)    (t:ts) = ITC_Type (toIfaceType t) (go res ts)
-    go kind             (t:ts) = WARN( True, ppr tc $$ ppr (tyConKind tc) $$ ppr ty_args )
-                                 ITC_Type (toIfaceType t) (go kind ts) -- Ill-kinded
-
-tcArgsIfaceTypes :: IfaceTcArgs -> [IfaceType]
-tcArgsIfaceTypes ITC_Nil = []
-tcArgsIfaceTypes (ITC_Kind t ts) = t : tcArgsIfaceTypes ts
-tcArgsIfaceTypes (ITC_Type t ts) = t : tcArgsIfaceTypes ts
+    go !n IA_Nil = n
+    go n  (IA_Arg _ argf rest)
+      | isVisibleArgFlag argf = go (n+1) rest
+      | otherwise             = go n rest
 
 {-
-Note [Suppressing kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We use the IfaceTcArgs to specify which of the arguments to a type
-constructor instantiate a for-all, and which are regular kind args.
-This in turn used to control kind-suppression when printing types,
-under the control of -fprint-explicit-kinds.  See also TypeRep.suppressKinds.
+Note [Suppressing invisible arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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
+
     T :: forall k. (k->*) -> k -> *    -- Ordinary kind polymorphism
     'Just :: forall k. k -> 'Maybe k   -- Promoted
+
 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 *
 
-************************************************************************
-*                                                                      *
-                Functions over IFaceTyCon
-*                                                                      *
-************************************************************************
--}
+For type constructors (IfaceTyConApp), IfaceAppArgs is a quite natural fit,
+since the corresponding Core constructor:
 
---isPromotedIfaceTyCon :: IfaceTyCon -> Bool
---isPromotedIfaceTyCon (IfacePromotedTyCon _) = True
---isPromotedIfaceTyCon _ = False
+    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.)
 
-{-
 ************************************************************************
 *                                                                      *
                 Pretty-printing
@@ -321,22 +666,33 @@ we want
 ************************************************************************
 -}
 
-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]
-
-pprIfacePrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
-pprIfacePrefixApp p pp_fun pp_tys
+if_print_coercions :: SDoc  -- ^ if printing coercions
+                   -> SDoc  -- ^ otherwise
+                   -> SDoc
+if_print_coercions yes no
+  = sdocWithDynFlags $ \dflags ->
+    getPprStyle $ \style ->
+    if gopt Opt_PrintExplicitCoercions dflags
+         || dumpStyle style || debugStyle style
+    then yes
+    else no
+
+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 :: PprPrec -> SDoc -> [SDoc] -> SDoc
+pprIfacePrefixApp ctxt_prec pp_fun pp_tys
   | null pp_tys = pp_fun
-  | otherwise   = maybeParen p TyConPrec $
+  | otherwise   = maybeParen ctxt_prec appPrec $
                   hang pp_fun 2 (sep pp_tys)
 
 -- ----------------------------- Printing binders ------------------------------------
 
 instance Outputable IfaceBndr where
     ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
-    ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr bndr
+    ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr False bndr
 
 pprIfaceBndrs :: [IfaceBndr] -> SDoc
 pprIfaceBndrs bs = sep (map ppr bs)
@@ -345,16 +701,31 @@ pprIfaceLamBndr :: IfaceLamBndr -> SDoc
 pprIfaceLamBndr (b, IfaceNoOneShot) = ppr b
 pprIfaceLamBndr (b, IfaceOneShot)   = ppr b <> text "[OneShot]"
 
-pprIfaceIdBndr :: (IfLclName, IfaceType) -> SDoc
-pprIfaceIdBndr (name, ty) = hsep [ppr name, dcolon, ppr ty]
+pprIfaceIdBndr :: IfaceIdBndr -> SDoc
+pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty)
 
-pprIfaceTvBndr :: IfaceTvBndr -> SDoc
-pprIfaceTvBndr (tv, IfaceTyConApp tc ITC_Nil)
-  | ifaceTyConName tc == liftedTypeKindTyConName = ppr tv
-pprIfaceTvBndr (tv, kind) = parens (ppr tv <+> dcolon <+> ppr kind)
+pprIfaceTvBndr :: Bool -> IfaceTvBndr -> SDoc
+pprIfaceTvBndr use_parens (tv, ki)
+  | isIfaceLiftedTypeKind ki = ppr tv
+  | otherwise                = maybe_parens (ppr tv <+> dcolon <+> ppr ki)
+  where
+    maybe_parens | use_parens = parens
+                 | otherwise  = id
 
-pprIfaceTvBndrs :: [IfaceTvBndr] -> SDoc
-pprIfaceTvBndrs tyvars = sep (map pprIfaceTvBndr tyvars)
+pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
+pprIfaceTyConBinders = sep . map go
+  where
+    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
@@ -388,239 +759,759 @@ instance Binary IfaceOneShot where
 instance Outputable IfaceType where
   ppr ty = pprIfaceType ty
 
-pprIfaceType, pprParendIfaceType ::IfaceType -> SDoc
-pprIfaceType       = ppr_ty TopPrec
-pprParendIfaceType = ppr_ty TyConPrec
-
-ppr_ty :: TyPrec -> IfaceType -> SDoc
-ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar
-ppr_ty ctxt_prec (IfaceTyConApp tc tys) = sdocWithDynFlags (pprTyTcApp ctxt_prec tc tys)
-ppr_ty _         (IfaceLitTy n)         = ppr_tylit n
+pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
+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 :: 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 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.
-    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)
-      = (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_ty ctxt_prec (IfaceAppTy ty1 ty2)
-  = maybeParen ctxt_prec TyConPrec $
-    ppr_ty FunPrec ty1 <+> pprParendIfaceType ty2
-
-ppr_ty ctxt_prec ty
-  = maybeParen ctxt_prec FunPrec (ppr_iface_sigma_type True 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_Type t ts -> pprTys t ts
-        ITC_Kind t ts -> pprTys t ts
-
--------------------
-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)
+ppr_ty ctxt_prec (IfaceAppTy t ts)
+  = if_print_coercions
+      ppr_app_ty
+      ppr_app_ty_no_casts
   where
-    (tvs, theta, tau) = splitIfaceSigmaTy ty
+    ppr_app_ty =
+        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 =
+        case t of
+          IfaceCastTy head _ -> ppr_ty ctxt_prec (mk_app_tys head ts)
+          _                  -> ppr_app_ty
+
+    mk_app_tys :: IfaceType -> IfaceAppArgs -> IfaceType
+    mk_app_tys (IfaceTyConApp tc tys1) tys2 =
+        IfaceTyConApp tc (tys1 `mappend` tys2)
+    mk_app_tys t1 tys2 = IfaceAppTy t1 tys2
+
+ppr_ty ctxt_prec (IfaceCastTy ty co)
+  = if_print_coercions
+      (parens (ppr_ty topPrec ty <+> text "|>" <+> ppr co))
+      (ppr_ty ctxt_prec ty)
+
+ppr_ty ctxt_prec (IfaceCoercionTy co)
+  = if_print_coercions
+      (ppr_co ctxt_prec co)
+      (text "<>")
+
+ppr_ty ctxt_prec ty -- IfaceForAllTy
+  = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
+
+{- 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
+
+which is significantly less readable than its non RuntimeRep-polymorphic type of
+
+    ($) :: (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 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.
+-}
 
-pprIfaceForAllPart :: Outputable a => [IfaceTvBndr] -> [a] -> SDoc -> SDoc
-pprIfaceForAllPart tvs ctxt sdoc = ppr_iface_forall_part False tvs ctxt sdoc
+-- | Default 'RuntimeRep' variables to 'LiftedPtr'. e.g.
+--
+-- @
+-- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+--        (a -> b) -> a -> b
+-- @
+--
+-- turns in to,
+--
+-- @ ($) :: forall a (b :: *). (a -> b) -> a -> b @
+--
+-- We do this to prevent RuntimeRep variables from incurring a significant
+-- syntactic overhead in otherwise simple type signatures (e.g. ($)). See
+-- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
+--
+defaultRuntimeRepVars :: IfaceType -> IfaceType
+defaultRuntimeRepVars ty = go False emptyFsEnv ty
+  where
+    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 ()
+            -- Record that we should replace it with LiftedRep,
+            -- and recurse, discarding the forall
+        in go ink subs' ty
+
+    go ink subs (IfaceForAllTy bndr ty)
+      = IfaceForAllTy (go_ifacebndr subs bndr) (go ink subs ty)
+
+    go _ subs ty@(IfaceTyVar tv)
+      | tv `elemFsEnv` subs
+      = 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 ink subs (IfaceTupleTy sort is_prom tc_args)
+      = IfaceTupleTy sort is_prom (go_args ink subs tc_args)
+
+    go ink subs (IfaceFunTy arg res)
+      = IfaceFunTy (go ink subs arg) (go ink subs res)
+
+    go ink subs (IfaceAppTy t ts)
+      = IfaceAppTy (go ink subs t) (go_args ink subs ts)
+
+    go ink subs (IfaceDFunTy x y)
+      = IfaceDFunTy (go ink subs x) (go ink subs y)
+
+    go ink subs (IfaceCastTy x co)
+      = IfaceCastTy (go ink subs x) co
+
+    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 _) =
+        tc `ifaceTyConHasKey` runtimeRepTyConKey
+    isRuntimeRep _ = False
+
+eliminateRuntimeRep :: (IfaceType -> SDoc) -> IfaceType -> SDoc
+eliminateRuntimeRep f ty
+  = sdocWithDynFlags $ \dflags ->
+    getPprStyle      $ \sty    ->
+    if userStyle sty && not (gopt Opt_PrintExplicitRuntimeReps dflags)
+      then f (defaultRuntimeRepVars ty)
+      else f ty
+
+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
+    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
 
-ppr_iface_forall_part :: Outputable a
-                      => Bool -> [IfaceTvBndr] -> [a] -> SDoc -> SDoc
-ppr_iface_forall_part show_foralls_unconditionally tvs ctxt sdoc
-  = sep [ if show_foralls_unconditionally
-          then pprIfaceForAll tvs
-          else pprUserIfaceForAll tvs
+-------------------
+pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> 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 tvs sdoc
+  = sep [ pprIfaceForAllCo tvs, sdoc ]
+
+ppr_iface_forall_part :: ShowForAllFlag
+                      -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
+ppr_iface_forall_part show_forall tvs ctxt sdoc
+  = sep [ case show_forall of
+            ShowForAllMust -> pprIfaceForAll tvs
+            ShowForAllWhen -> pprUserIfaceForAll tvs
         , pprIfaceContextArr ctxt
         , sdoc]
 
-pprIfaceForAll :: [IfaceTvBndr] -> SDoc
-pprIfaceForAll []  = empty
-pprIfaceForAll tvs = ptext (sLit "forall") <+> pprIfaceTvBndrs tvs <> dot
-
-pprIfaceSigmaType :: IfaceType -> SDoc
-pprIfaceSigmaType ty = ppr_iface_sigma_type False ty
+-- | Render the "forall ... ." or "forall ... ->" bit of a type.
+pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
+pprIfaceForAll [] = empty
+pprIfaceForAll bndrs@(Bndr _ vis : _)
+  = sep [ add_separator (forAllLit <+> fsep docs)
+        , pprIfaceForAll bndrs' ]
+  where
+    (bndrs', docs) = ppr_itv_bndrs bndrs vis
+
+    add_separator stuff = case vis of
+                            Required -> stuff <+> arrow
+                            _inv     -> stuff <>  dot
+
+
+-- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
+-- Returns both the list of not-yet-rendered binders and the doc.
+-- 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@(Bndr _ vis) : bndrs) vis1
+  | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
+                         (bndrs', pprIfaceForAllBndr bndr : doc)
+  | otherwise   = (all_bndrs, [])
+ppr_itv_bndrs [] _ = ([], [])
+
+pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
+pprIfaceForAllCo []  = empty
+pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
+
+pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
+pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
+
+pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
+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)
+
+-- | 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 :: [IfaceTvBndr] -> SDoc
+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
-     tv_has_kind_var (_,t) = not (isEmptyUniqSet (ifTyVarsOfType t))
+     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.
+-}
+
+
 -------------------
 
--- See equivalent function in TypeRep.hs
-pprIfaceTyList :: TyPrec -> IfaceType -> IfaceType -> SDoc
+-- | 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
+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)
-        -> 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)
-        -> 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)
-      | tcname == consDataConName
-      , (ITC_Kind _ (ITC_Type ty1 (ITC_Type ty2 ITC_Nil))) <- tys
+      | tc `ifaceTyConHasKey` consDataConKey
+      , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
+      , isInvisibleArgFlag argf
       , (args, tl) <- gather ty2
       = (ty1:args, tl)
-      | tcname == nilDataConName
+      | tc `ifaceTyConHasKey` nilDataConKey
       = ([], Nothing)
-      where tcname = ifaceTyConName tc
     gather ty = ([], Just ty)
 
-pprIfaceTypeApp :: IfaceTyCon -> IfaceTcArgs -> SDoc
-pprIfaceTypeApp tc args = sdocWithDynFlags (pprTyTcApp TopPrec tc args)
-
-pprTyTcApp :: TyPrec -> IfaceTyCon -> IfaceTcArgs -> DynFlags -> SDoc
-pprTyTcApp ctxt_prec tc tys dflags
-  | ifaceTyConName tc == ipClassName
-  , ITC_Type (IfaceLitTy (IfaceStrTyLit n)) (ITC_Type ty ITC_Nil) <- tys
-  = char '?' <> ftext n <> ptext (sLit "::") <> ppr_ty TopPrec ty
-
-  | ifaceTyConName tc == consDataConName
+pprIfaceTypeApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
+pprIfaceTypeApp prec tc args = pprTyTcApp prec tc args
+
+pprTyTcApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
+pprTyTcApp ctxt_prec tc tys =
+    sdocWithDynFlags $ \dflags ->
+    getPprStyle $ \style ->
+    pprTyTcApp' ctxt_prec tc tys dflags style
+
+pprTyTcApp' :: PprPrec -> IfaceTyCon -> IfaceAppArgs
+            -> DynFlags -> PprStyle -> SDoc
+pprTyTcApp' ctxt_prec tc tys dflags style
+  | ifaceTyConName tc `hasKey` ipClassKey
+  , 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)
+  , 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)
-  , ITC_Kind _ (ITC_Type ty1 (ITC_Type 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
+  , IA_Arg (IfaceTyConApp rep IA_Nil) Required IA_Nil <- tys
+  , rep `ifaceTyConHasKey` liftedRepDataConKey
+  = kindType
+
   | otherwise
-  = ppr_iface_tc_app ppr_ty ctxt_prec tc tys_wo_kinds
-  where
-    tys_wo_kinds = tcArgsIfaceTypes $ stripKindArgs dflags tys
+  = getPprDebug $ \dbg ->
+    if | not dbg && tc `ifaceTyConHasKey` errorMessageTypeErrorFamKey
+         -- Suppress detail unles you _really_ want to see
+         -> text "(TypeError ...)"
 
-pprIfaceCoTcApp :: TyPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
-pprIfaceCoTcApp ctxt_prec tc tys = ppr_iface_tc_app ppr_co ctxt_prec tc tys
+       | Just doc <- ppr_equality ctxt_prec tc (appArgsIfaceTypes tys)
+         -> doc
 
-ppr_iface_tc_app :: (TyPrec -> a -> SDoc) -> TyPrec -> IfaceTyCon -> [a] -> SDoc
-ppr_iface_tc_app pp _ tc [ty]
-  | n == listTyConName = pprPromotionQuote tc <> brackets (pp TopPrec ty)
-  | n == parrTyConName = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
+       | otherwise
+         -> ppr_iface_tc_app ppr_app_arg ctxt_prec tc tys_wo_kinds
   where
-    n = ifaceTyConName tc
-
-ppr_iface_tc_app pp ctxt_prec tc tys
-  | Just (tup_sort, tup_args) <- is_tuple
-  = pprPromotionQuote tc <>
-    tupleParens tup_sort (sep (punctuate comma (map (pp TopPrec) tup_args)))
-
-  | not (isSymOcc (nameOccName tc_name))
-  = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp TyConPrec) tys)
-
-  | [ty1,ty2] <- tys  -- Infix, two arguments;
-                      -- we know nothing of precedence though
-  = pprIfaceInfixApp pp ctxt_prec (ppr tc) ty1 ty2
-
-  | tc_name == liftedTypeKindTyConName || tc_name == unliftedTypeKindTyConName
-  = ppr tc   -- Do not wrap *, # in parens
+    info = ifaceTyConInfo tc
+    tys_wo_kinds = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags tys
+
+-- | 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]
+-- 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)
+
+  | hom_eq_tc
+  , [k, t1, t2] <- args
+  = Just $ print_equality (k, k, t1, t2)
 
   | otherwise
-  = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp TyConPrec) tys)
+  = Nothing
   where
-    tc_name = ifaceTyConName 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
 
-    is_tuple = case wiredInNameTyThing_maybe tc_name of
-                 Just (ATyCon tc)
-                   | Just sort <- tyConTuple_maybe tc
-                   , tyConArity tc == length tys
-                   -> Just (sort, tys)
+    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 =
+        sdocWithDynFlags $ \dflags ->
+        getPprStyle      $ \style  ->
+        print_equality' args style dflags
+
+    print_equality' (ki1, ki2, ty1, ty2) style dflags
+      | -- If -fprint-equality-relations is on, just print the original TyCon
+        print_eqs
+      = ppr_infix_eq (ppr tc)
+
+      | -- 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
+      = ppr_infix_eq (ppr tc)
+      where
+        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
+
+
+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.
+
+-- | 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]
+  | tc `ifaceTyConHasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp topPrec ty)
 
-                   | Just dc <- isPromotedDataCon_maybe tc
-                   , let dc_tc = dataConTyCon dc
-                   , isTupleTyCon dc_tc
-                   , let arity = tyConArity dc_tc
-                         ty_args = drop arity tys
-                   , ty_args `lengthIs` arity
-                   -> Just (tupleTyConSort tc, ty_args)
+ppr_iface_tc_app pp ctxt_prec tc tys
+  | tc `ifaceTyConHasKey` liftedTypeKindTyConKey
+  = kindType
 
-                 _ -> Nothing
+  | not (isSymOcc (nameOccName (ifaceTyConName tc)))
+  = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp appPrec) tys)
 
+  | [ 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)
 
-ppr_tylit :: IfaceTyLit -> SDoc
-ppr_tylit (IfaceNumTyLit n) = integer n
-ppr_tylit (IfaceStrTyLit n) = text (show n)
+  | otherwise
+  = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp appPrec) tys)
+
+pprSum :: Arity -> PromotionFlag -> IfaceAppArgs -> SDoc
+pprSum _arity is_promoted args
+  =   -- drop the RuntimeRep vars.
+      -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
+    let tys   = appArgsIfaceTypes args
+        args' = drop (length tys `div` 2) tys
+    in pprPromotionQuoteI is_promoted
+       <> sumParens (pprWithBars (ppr_ty topPrec) args')
+
+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
+pprTuple _ sort IsPromoted args
+  = let tys = appArgsIfaceTypes args
+        args' = drop (length tys `div` 2) tys
+        spaceIfPromoted = case args' of
+          arg0:_ -> pprSpaceIfPromotedTyCon arg0
+          _ -> id
+    in pprPromotionQuoteI IsPromoted <>
+       tupleParens sort (spaceIfPromoted (pprWithCommas pprIfaceType args'))
+
+pprTuple _ sort promoted args
+  =   -- drop the RuntimeRep vars.
+      -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
+    let tys   = appArgsIfaceTypes args
+        args' = case sort of
+                  UnboxedTuple -> drop (length tys `div` 2) tys
+                  _            -> tys
+    in
+    pprPromotionQuoteI promoted <>
+    tupleParens sort (pprWithCommas pprIfaceType args')
+
+pprIfaceTyLit :: IfaceTyLit -> SDoc
+pprIfaceTyLit (IfaceNumTyLit n) = integer n
+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)
-  = 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)
-      = (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)
-  = parens (pprIfaceCoTcApp TopPrec tc cos) <> ppr_role r
+  = parens (pprIfaceCoTcApp topPrec tc cos) <> ppr_role r
 ppr_co ctxt_prec (IfaceAppCo co1 co2)
-  = maybeParen ctxt_prec TyConPrec $
-    ppr_co FunPrec co1 <+> pprParendIfaceCoercion co2
-ppr_co ctxt_prec co@(IfaceForAllCo _ _)
-  = maybeParen ctxt_prec FunPrec (sep [ppr_tvs, pprIfaceCoercion inner_co])
+  = maybeParen ctxt_prec appPrec $
+    ppr_co funPrec co1 <+> pprParendIfaceCoercion co2
+ppr_co ctxt_prec co@(IfaceForAllCo {})
+  = maybeParen ctxt_prec funPrec $
+    pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co)
   where
     (tvs, inner_co) = split_co co
-    ppr_tvs = ptext (sLit "forall") <+> pprIfaceTvBndrs tvs <> dot
 
-    split_co (IfaceForAllCo tv co')
-      = let (tvs, co'') = split_co co' in (tv:tvs,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')
 
-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 s r ty1 ty2)
-  = maybeParen ctxt_prec TyConPrec $
-    ptext (sLit "UnivCo") <+> ftext s <+> ppr r <+>
+ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
+  = maybeParen ctxt_prec appPrec $
+    text "UnsafeCo" <+> ppr r <+>
     pprParendIfaceType ty1 <+> pprParendIfaceType 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)
-  = maybeParen ctxt_prec TyConPrec $
-    ptext (sLit "Inst") <+> pprParendIfaceCoercion co <+> pprParendIfaceType ty
-
-ppr_co ctxt_prec (IfaceAxiomRuleCo tc tys cos)
-  = maybeParen ctxt_prec TyConPrec
-               (sep [ppr tc, nest 4 (sep (map pprParendIfaceType tys ++ map pprParendIfaceCoercion cos))])
-
-ppr_co ctxt_prec co
-  = ppr_special_co ctxt_prec doc cos
-  where (doc, cos) = case co of
-                     { IfaceAxiomInstCo n i cos -> (ppr n <> brackets (ppr i), cos)
-                     ; IfaceSymCo co            -> (ptext (sLit "Sym"), [co])
-                     ; IfaceTransCo co1 co2     -> (ptext (sLit "Trans"), [co1,co2])
-                     ; IfaceNthCo d co          -> (ptext (sLit "Nth:") <> int d,
-                                                    [co])
-                     ; IfaceLRCo lr co          -> (ppr lr, [co])
-                     ; IfaceSubCo co            -> (ptext (sLit "Sub"), [co])
-                     ; _                        -> panic "pprIfaceCo" }
-
-ppr_special_co :: TyPrec -> SDoc -> [IfaceCoercion] -> SDoc
+  = maybeParen ctxt_prec appPrec $
+    text "Inst" <+> pprParendIfaceCoercion co
+                        <+> pprParendIfaceCoercion ty
+
+ppr_co ctxt_prec (IfaceAxiomRuleCo tc 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)
+  = 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 (IfaceKindCo co)
+  = ppr_special_co ctxt_prec (text "Kind") [co]
+
+ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
 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
@@ -630,35 +1521,60 @@ ppr_role r = underscore <> pp_role
                     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)
 
 pprPromotionQuote :: IfaceTyCon -> SDoc
-pprPromotionQuote (IfacePromotedDataCon _ ) = char '\''
-pprPromotionQuote (IfacePromotedTyCon _)    = ifPprDebug (char '\'')
-pprPromotionQuote _                         = empty
+pprPromotionQuote tc =
+    pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
+
+pprPromotionQuoteI  :: PromotionFlag -> SDoc
+pprPromotionQuoteI NotPromoted = empty
+pprPromotionQuoteI IsPromoted    = char '\''
 
 instance Outputable IfaceCoercion where
   ppr = pprIfaceCoercion
 
 instance Binary IfaceTyCon where
-   put_ bh tc =
-     case tc of
-       IfaceTc n              -> putByte bh 0 >> put_ bh n
-       IfacePromotedDataCon n -> putByte bh 1 >> put_ bh n
-       IfacePromotedTyCon   n -> putByte bh 2 >> put_ bh n
-
-   get bh =
-     do tc <- getByte bh
-        case tc of
-          0 -> get bh >>= return . IfaceTc
-          1 -> get bh >>= return . IfacePromotedDataCon
-          2 -> get bh >>= return . IfacePromotedTyCon
-          _ -> panic ("get IfaceTyCon " ++ show tc)
+   put_ bh (IfaceTyCon n i) = put_ bh n >> put_ bh i
+
+   get bh = do n <- get bh
+               i <- get bh
+               return (IfaceTyCon n i)
+
+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           = putByte bh 3
+
+   get bh = do
+       n <- getByte bh
+       case n of
+         0 -> return IfaceNormalTyCon
+         1 -> IfaceTupleTyCon <$> get bh <*> get bh
+         2 -> IfaceSumTyCon <$> get bh
+         _ -> return IfaceEqualityTyCon
+
+instance Binary IfaceTyConInfo where
+   put_ bh (IfaceTyConInfo i s) = put_ bh i >> put_ bh s
+
+   get bh = IfaceTyConInfo <$> get bh <*> get bh
 
 instance Outputable IfaceTyLit where
-  ppr = ppr_tylit
+  ppr = pprIfaceTyLit
 
 instance Binary IfaceTyLit where
   put_ bh (IfaceNumTyLit n)  = putByte bh 1 >> put_ bh n
@@ -673,41 +1589,79 @@ instance Binary IfaceTyLit where
                  ; return (IfaceStrTyLit n) }
          _ -> panic ("get IfaceTyLit " ++ show tag)
 
-instance Binary IfaceTcArgs where
+instance Binary IfaceAppArgs where
   put_ bh tk =
     case tk of
-      ITC_Type t ts -> putByte bh 0 >> put_ bh t >> put_ bh ts
-      ITC_Kind 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
+           a  <- get bh
            ts <- get bh
-           return $! ITC_Type t ts
-         1 -> do
-           t  <- get bh
-           ts <- get bh
-           return $! ITC_Kind 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)
 
 -------------------
-pprIfaceContextArr :: Outputable a => [a] -> SDoc
--- Prints "(C a, D b) =>", including the arrow
-pprIfaceContextArr = maybe empty (<+> darrow) . pprIfaceContextMaybe
-
-pprIfaceContext :: Outputable a => [a] -> SDoc
-pprIfaceContext = fromMaybe (parens empty) . pprIfaceContextMaybe
 
-pprIfaceContextMaybe :: Outputable a => [a] -> Maybe SDoc
-pprIfaceContextMaybe [] = Nothing
-pprIfaceContextMaybe [pred] = Just $ ppr pred -- No parens
-pprIfaceContextMaybe preds  = Just $ parens (fsep (punctuate comma (map ppr preds)))
+-- Some notes about printing contexts
+--
+-- 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 opPrec, since something like @a :~: b@ must be parenthesized (see
+-- #9658).
+--
+-- When printing a larger context we use 'fsep' instead of 'sep' so that
+-- the context doesn't get displayed as a giant column. Rather than,
+--  instance (Eq a,
+--            Eq b,
+--            Eq c,
+--            Eq d,
+--            Eq e,
+--            Eq f,
+--            Eq g,
+--            Eq h,
+--            Eq i,
+--            Eq j,
+--            Eq k,
+--            Eq l) =>
+--           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
+--
+-- we want
+--
+--  instance (Eq a, Eq b, Eq c, Eq d, Eq e, Eq f, Eq g, Eq h, Eq i,
+--            Eq j, Eq k, Eq l) =>
+--           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
+
+
+
+-- | 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 [pred] = ppr_ty funPrec pred <+> darrow
+pprIfaceContextArr preds  = ppr_parend_preds preds <+> darrow
+
+-- | 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
+    put_ _ (IfaceFreeTyVar tv)
+       = pprPanic "Can't serialise IfaceFreeTyVar" (ppr tv)
+
     put_ bh (IfaceForAllTy aa ab) = do
             putByte bh 0
             put_ bh aa
@@ -729,9 +1683,14 @@ instance Binary IfaceType where
             put_ bh ah
     put_ bh (IfaceTyConApp tc tys)
       = do { putByte bh 5; put_ bh tc; put_ bh tys }
-
+    put_ bh (IfaceCastTy a b)
+      = do { putByte bh 6; put_ bh a; put_ bh b }
+    put_ bh (IfaceCoercionTy a)
+      = do { putByte bh 7; put_ bh a }
+    put_ bh (IfaceTupleTy s i tys)
+      = do { putByte bh 8; put_ bh s; put_ bh i; put_ bh tys }
     put_ bh (IfaceLitTy n)
-      = do { putByte bh 30; put_ bh n }
+      = do { putByte bh 9; put_ bh n }
 
     get bh = do
             h <- getByte bh
@@ -752,222 +1711,196 @@ instance Binary IfaceType where
                       return (IfaceDFunTy ag ah)
               5 -> do { tc <- get bh; tys <- get bh
                       ; return (IfaceTyConApp tc tys) }
-              30 -> do n <- get bh
+              6 -> do { a <- get bh; b <- get bh
+                      ; return (IfaceCastTy a b) }
+              7 -> do { a <- get bh
+                      ; return (IfaceCoercionTy a) }
+
+              8 -> do { s <- get bh; i <- get bh; tys <- get bh
+                      ; return (IfaceTupleTy s i tys) }
+              _  -> do n <- get bh
                        return (IfaceLitTy n)
 
-              _  -> panic ("get IfaceType " ++ show h)
+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
-  put_ bh (IfaceReflCo a b) = do
+  put_ bh (IfaceReflCo a) = do
           putByte bh 1
           put_ bh a
-          put_ bh b
-  put_ bh (IfaceFunCo a b c) = do
+  put_ bh (IfaceGReflCo a b c) = do
           putByte bh 2
           put_ bh a
           put_ bh b
           put_ bh c
-  put_ bh (IfaceTyConAppCo a b c) = do
+  put_ bh (IfaceFunCo a b c) = do
           putByte bh 3
           put_ bh a
           put_ bh b
           put_ bh c
-  put_ bh (IfaceAppCo a b) = do
+  put_ bh (IfaceTyConAppCo a b c) = do
           putByte bh 4
           put_ bh a
           put_ bh b
-  put_ bh (IfaceForAllCo a b) = do
+          put_ bh c
+  put_ bh (IfaceAppCo a b) = do
           putByte bh 5
           put_ bh a
           put_ bh b
-  put_ bh (IfaceCoVarCo a) = do
+  put_ bh (IfaceForAllCo a b c) = do
           putByte bh 6
           put_ bh a
-  put_ bh (IfaceAxiomInstCo a b c) = do
+          put_ bh b
+          put_ bh c
+  put_ bh (IfaceCoVarCo a) = do
           putByte bh 7
           put_ bh a
+  put_ bh (IfaceAxiomInstCo a b c) = do
+          putByte bh 8
+          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
-          putByte bh 9
+          putByte bh 10
           put_ bh a
   put_ bh (IfaceTransCo a b) = do
-          putByte bh 10
+          putByte bh 11
           put_ bh a
           put_ bh b
   put_ bh (IfaceNthCo a b) = do
-          putByte bh 11
+          putByte bh 12
           put_ bh a
           put_ bh b
   put_ bh (IfaceLRCo a b) = do
-          putByte bh 12
+          putByte bh 13
           put_ bh a
           put_ bh b
   put_ bh (IfaceInstCo a b) = do
-          putByte bh 13
+          putByte bh 14
           put_ bh a
           put_ bh b
+  put_ bh (IfaceKindCo a) = do
+          putByte bh 15
+          put_ bh a
   put_ bh (IfaceSubCo a) = do
-          putByte bh 14
+          putByte bh 16
           put_ bh a
-  put_ bh (IfaceAxiomRuleCo a b c) = do
-          putByte bh 15
+  put_ bh (IfaceAxiomRuleCo a b) = do
+          putByte bh 17
           put_ bh a
           put_ bh b
-          put_ bh c
+  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
-                   b <- get bh
-                   return $ IfaceReflCo a b
+                   return $ IfaceReflCo a
            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
-                   return $ IfaceTyConAppCo a b c
+                   return $ IfaceFunCo a b c
            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
-                   return $ IfaceForAllCo a b
+                   return $ IfaceAppCo a b
            6 -> do a <- get bh
-                   return $ IfaceCoVarCo a
+                   b <- get bh
+                   c <- get bh
+                   return $ IfaceForAllCo a b c
            7 -> do a <- get bh
+                   return $ IfaceCoVarCo a
+           8 -> do a <- get bh
                    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
-           9 -> do a <- get bh
-                   return $ IfaceSymCo a
            10-> do a <- get bh
+                   return $ IfaceSymCo a
+           11-> do a <- get bh
                    b <- get bh
                    return $ IfaceTransCo a b
-           11-> do a <- get bh
+           12-> do a <- get bh
                    b <- get bh
                    return $ IfaceNthCo a b
-           12-> do a <- get bh
+           13-> do a <- get bh
                    b <- get bh
                    return $ IfaceLRCo a b
-           13-> do a <- get bh
+           14-> do a <- get bh
                    b <- get bh
                    return $ IfaceInstCo a b
-           14-> do a <- get bh
-                   return $ IfaceSubCo a
            15-> do a <- get bh
+                   return $ IfaceKindCo a
+           16-> do a <- get bh
+                   return $ IfaceSubCo a
+           17-> do a <- get bh
                    b <- get bh
-                   c <- get bh
-                   return $ IfaceAxiomRuleCo a b c
+                   return $ IfaceAxiomRuleCo a b
            _ -> panic ("get IfaceCoercion " ++ show tag)
 
-{-
-************************************************************************
-*                                                                      *
-        Conversion from Type to IfaceType
-*                                                                      *
-************************************************************************
--}
+instance Binary IfaceUnivCoProv where
+  put_ bh IfaceUnsafeCoerceProv = putByte bh 1
+  put_ bh (IfacePhantomProv a) = do
+          putByte bh 2
+          put_ bh a
+  put_ bh (IfaceProofIrrelProv a) = do
+          putByte bh 3
+          put_ bh a
+  put_ bh (IfacePluginProv a) = do
+          putByte bh 4
+          put_ bh a
+
+  get bh = do
+      tag <- getByte bh
+      case tag of
+           1 -> return $ IfaceUnsafeCoerceProv
+           2 -> do a <- get bh
+                   return $ IfacePhantomProv a
+           3 -> do a <- get bh
+                   return $ IfaceProofIrrelProv a
+           4 -> do a <- get bh
+                   return $ IfacePluginProv a
+           _ -> panic ("get IfaceUnivCoProv " ++ show tag)
+
 
-----------------
-toIfaceTvBndr :: TyVar -> (IfLclName, IfaceType)
-toIfaceTvBndr tyvar   = (occNameFS (getOccName tyvar), toIfaceKind (tyVarKind tyvar))
-toIfaceIdBndr :: Id -> (IfLclName, IfaceType)
-toIfaceIdBndr id      = (occNameFS (getOccName id),    toIfaceType (idType id))
-toIfaceTvBndrs :: [TyVar] -> [(IfLclName, IfaceType)]
-toIfaceTvBndrs tyvars = map toIfaceTvBndr tyvars
-
-toIfaceBndr :: Var -> IfaceBndr
-toIfaceBndr var
-  | isId var  = IfaceIdBndr (toIfaceIdBndr var)
-  | otherwise = IfaceTvBndr (toIfaceTvBndr var)
-
-toIfaceKind :: Type -> IfaceType
-toIfaceKind = toIfaceType
-
----------------------
-toIfaceType :: Type -> IfaceType
--- Synonyms are retained in the interface type
-toIfaceType (TyVarTy tv)      = IfaceTyVar (toIfaceTyVar tv)
-toIfaceType (AppTy t1 t2)     = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
-toIfaceType (FunTy t1 t2)
-  | isPredTy t1 = IfaceDFunTy (toIfaceType t1) (toIfaceType t2)
-  | otherwise   = IfaceFunTy  (toIfaceType t1) (toIfaceType t2)
-toIfaceType (TyConApp tc tys) = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTcArgs tc tys)
-toIfaceType (LitTy n)         = IfaceLitTy (toIfaceTyLit n)
-toIfaceType (ForAllTy tv t)   = IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
-
-toIfaceTyVar :: TyVar -> FastString
-toIfaceTyVar = occNameFS . getOccName
-
-toIfaceCoVar :: CoVar -> FastString
-toIfaceCoVar = occNameFS . getOccName
-
-----------------
-toIfaceTyCon :: TyCon -> IfaceTyCon
-toIfaceTyCon tc
-  | isPromotedDataCon tc = IfacePromotedDataCon tc_name
-  | isPromotedTyCon tc   = IfacePromotedTyCon tc_name
-  | otherwise            = IfaceTc tc_name
-    where tc_name = tyConName tc
-
-toIfaceTyCon_name :: Name -> IfaceTyCon
-toIfaceTyCon_name = IfaceTc
-
-toIfaceTyLit :: TyLit -> IfaceTyLit
-toIfaceTyLit (NumTyLit x) = IfaceNumTyLit x
-toIfaceTyLit (StrTyLit x) = IfaceStrTyLit x
-
-----------------
-toIfaceTypes :: [Type] -> [IfaceType]
-toIfaceTypes ts = map toIfaceType ts
-
-----------------
-toIfaceContext :: ThetaType -> IfaceContext
-toIfaceContext = toIfaceTypes
-
-----------------
-toIfaceCoercion :: Coercion -> IfaceCoercion
-toIfaceCoercion (Refl r ty)         = IfaceReflCo r (toIfaceType ty)
-toIfaceCoercion (TyConAppCo r tc cos)
-  | tc `hasKey` funTyConKey
-  , [arg,res] <- cos                = IfaceFunCo r (toIfaceCoercion arg) (toIfaceCoercion res)
-  | otherwise                       = IfaceTyConAppCo r (toIfaceTyCon tc)
-                                                      (map toIfaceCoercion cos)
-toIfaceCoercion (AppCo co1 co2)     = IfaceAppCo  (toIfaceCoercion co1)
-                                                  (toIfaceCoercion co2)
-toIfaceCoercion (ForAllCo v co)     = IfaceForAllCo (toIfaceTvBndr v)
-                                                    (toIfaceCoercion co)
-toIfaceCoercion (CoVarCo cv)        = IfaceCoVarCo  (toIfaceCoVar cv)
-toIfaceCoercion (AxiomInstCo con ind cos)
-                                    = IfaceAxiomInstCo (coAxiomName con) ind
-                                                       (map toIfaceCoercion cos)
-toIfaceCoercion (UnivCo s r ty1 ty2)= IfaceUnivCo s r (toIfaceType ty1)
-                                                  (toIfaceType ty2)
-toIfaceCoercion (SymCo co)          = IfaceSymCo (toIfaceCoercion co)
-toIfaceCoercion (TransCo co1 co2)   = IfaceTransCo (toIfaceCoercion co1)
-                                                   (toIfaceCoercion co2)
-toIfaceCoercion (NthCo d co)        = IfaceNthCo d (toIfaceCoercion co)
-toIfaceCoercion (LRCo lr co)        = IfaceLRCo lr (toIfaceCoercion co)
-toIfaceCoercion (InstCo co ty)      = IfaceInstCo (toIfaceCoercion co)
-                                                  (toIfaceType ty)
-toIfaceCoercion (SubCo co)          = IfaceSubCo (toIfaceCoercion co)
-
-toIfaceCoercion (AxiomRuleCo co ts cs) = IfaceAxiomRuleCo
-                                          (coaxrName co)
-                                          (map toIfaceType ts)
-                                          (map toIfaceCoercion cs)
+instance Binary (DefMethSpec IfaceType) where
+    put_ bh VanillaDM     = putByte bh 0
+    put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
+    get bh = do
+            h <- getByte bh
+            case h of
+              0 -> return VanillaDM
+              _ -> do { t <- get bh; return (GenericDM t) }