never executed always true always false
    1 {-
    2 (c) The University of Glasgow 2006
    3 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
    4 
    5 
    6 This module defines interface types and binders
    7 -}
    8 
    9 
   10 {-# LANGUAGE FlexibleInstances #-}
   11   -- FlexibleInstances for Binary (DefMethSpec IfaceType)
   12 {-# LANGUAGE BangPatterns #-}
   13 {-# LANGUAGE MultiWayIf #-}
   14 {-# LANGUAGE TupleSections #-}
   15 {-# LANGUAGE LambdaCase #-}
   16 
   17 module GHC.Iface.Type (
   18         IfExtName, IfLclName,
   19 
   20         IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
   21         IfaceMCoercion(..),
   22         IfaceUnivCoProv(..),
   23         IfaceMult,
   24         IfaceTyCon(..),
   25         IfaceTyConInfo(..), mkIfaceTyConInfo,
   26         IfaceTyConSort(..),
   27         IfaceTyLit(..), IfaceAppArgs(..),
   28         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
   29         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
   30         IfaceForAllSpecBndr,
   31         IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ShowForAllFlag(..),
   32         mkIfaceForAllTvBndr,
   33         mkIfaceTyConKind,
   34         ifaceForAllSpecToBndrs, ifaceForAllSpecToBndr,
   35 
   36         ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
   37         ifTyConBinderVar, ifTyConBinderName,
   38 
   39         -- Equality testing
   40         isIfaceLiftedTypeKind,
   41 
   42         -- Conversion from IfaceAppArgs to IfaceTypes/ArgFlags
   43         appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
   44 
   45         -- Printing
   46         SuppressBndrSig(..),
   47         UseBndrParens(..),
   48         PrintExplicitKinds(..),
   49         pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
   50         pprIfaceContext, pprIfaceContextArr,
   51         pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
   52         pprIfaceBndrs, pprIfaceAppArgs, pprParendIfaceAppArgs,
   53         pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
   54         pprIfaceSigmaType, pprIfaceTyLit,
   55         pprIfaceCoercion, pprParendIfaceCoercion,
   56         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
   57         pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
   58         ppr_fun_arrow,
   59         isIfaceTauType,
   60 
   61         suppressIfaceInvisibles,
   62         stripIfaceInvisVars,
   63         stripInvisArgs,
   64 
   65         mkIfaceTySubst, substIfaceTyVar, substIfaceAppArgs, inDomIfaceTySubst,
   66 
   67         many_ty
   68     ) where
   69 
   70 import GHC.Prelude
   71 
   72 import {-# SOURCE #-} GHC.Builtin.Types
   73                                  ( coercibleTyCon, heqTyCon
   74                                  , tupleTyConName
   75                                  , manyDataConTyCon, oneDataConTyCon
   76                                  , liftedRepTyCon, liftedDataConTyCon )
   77 import {-# SOURCE #-} GHC.Core.Type ( isRuntimeRepTy, isMultiplicityTy, isLevityTy )
   78 
   79 import GHC.Core.TyCon hiding ( pprPromotionQuote )
   80 import GHC.Core.Coercion.Axiom
   81 import GHC.Types.Var
   82 import GHC.Builtin.Names
   83 import GHC.Types.Name
   84 import GHC.Types.Basic
   85 import GHC.Utils.Binary
   86 import GHC.Utils.Outputable
   87 import GHC.Data.FastString
   88 import GHC.Utils.Misc
   89 import GHC.Utils.Panic
   90 import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isMetaTyVar, isTyConableTyVar )
   91 
   92 import Data.Maybe( isJust )
   93 import qualified Data.Semigroup as Semi
   94 import Control.DeepSeq
   95 
   96 {-
   97 ************************************************************************
   98 *                                                                      *
   99                 Local (nested) binders
  100 *                                                                      *
  101 ************************************************************************
  102 -}
  103 
  104 type IfLclName = FastString     -- A local name in iface syntax
  105 
  106 type IfExtName = Name   -- An External or WiredIn Name can appear in Iface syntax
  107                         -- (However Internal or System Names never should)
  108 
  109 data IfaceBndr          -- Local (non-top-level) binders
  110   = IfaceIdBndr {-# UNPACK #-} !IfaceIdBndr
  111   | IfaceTvBndr {-# UNPACK #-} !IfaceTvBndr
  112 
  113 type IfaceIdBndr  = (IfaceType, IfLclName, IfaceType)
  114 type IfaceTvBndr  = (IfLclName, IfaceKind)
  115 
  116 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
  117 ifaceTvBndrName (n,_) = n
  118 
  119 ifaceIdBndrName :: IfaceIdBndr -> IfLclName
  120 ifaceIdBndrName (_,n,_) = n
  121 
  122 ifaceBndrName :: IfaceBndr -> IfLclName
  123 ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr
  124 ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr
  125 
  126 ifaceBndrType :: IfaceBndr -> IfaceType
  127 ifaceBndrType (IfaceIdBndr (_, _, t)) = t
  128 ifaceBndrType (IfaceTvBndr (_, t)) = t
  129 
  130 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
  131 
  132 data IfaceOneShot    -- See Note [Preserve OneShotInfo] in "GHC.Core.Tidy"
  133   = IfaceNoOneShot   -- and Note [The oneShot function] in "GHC.Types.Id.Make"
  134   | IfaceOneShot
  135 
  136 instance Outputable IfaceOneShot where
  137   ppr IfaceNoOneShot = text "NoOneShotInfo"
  138   ppr IfaceOneShot = text "OneShot"
  139 
  140 {-
  141 %************************************************************************
  142 %*                                                                      *
  143                 IfaceType
  144 %*                                                                      *
  145 %************************************************************************
  146 -}
  147 
  148 -------------------------------
  149 type IfaceKind     = IfaceType
  150 
  151 -- | A kind of universal type, used for types and kinds.
  152 --
  153 -- Any time a 'Type' is pretty-printed, it is first converted to an 'IfaceType'
  154 -- before being printed. See Note [Pretty printing via Iface syntax] in "GHC.Types.TyThing.Ppr"
  155 data IfaceType
  156   = IfaceFreeTyVar TyVar                -- See Note [Free tyvars in IfaceType]
  157   | IfaceTyVar     IfLclName            -- Type/coercion variable only, not tycon
  158   | IfaceLitTy     IfaceTyLit
  159   | IfaceAppTy     IfaceType IfaceAppArgs
  160                              -- See Note [Suppressing invisible arguments] for
  161                              -- an explanation of why the second field isn't
  162                              -- IfaceType, analogous to AppTy.
  163   | IfaceFunTy     AnonArgFlag IfaceMult IfaceType IfaceType
  164   | IfaceForAllTy  IfaceForAllBndr IfaceType
  165   | IfaceTyConApp  IfaceTyCon IfaceAppArgs  -- Not necessarily saturated
  166                                             -- Includes newtypes, synonyms, tuples
  167   | IfaceCastTy     IfaceType IfaceCoercion
  168   | IfaceCoercionTy IfaceCoercion
  169 
  170   | IfaceTupleTy                  -- Saturated tuples (unsaturated ones use IfaceTyConApp)
  171        TupleSort                  -- What sort of tuple?
  172        PromotionFlag                 -- A bit like IfaceTyCon
  173        IfaceAppArgs               -- arity = length args
  174           -- For promoted data cons, the kind args are omitted
  175           -- Why have this? Only for efficiency: IfaceTupleTy can omit the
  176           -- type arguments, as they can be recreated when deserializing.
  177           -- In an experiment, removing IfaceTupleTy resulted in a 0.75% regression
  178           -- in interface file size (in GHC's boot libraries).
  179           -- See !3987.
  180 
  181 type IfaceMult = IfaceType
  182 
  183 type IfacePredType = IfaceType
  184 type IfaceContext = [IfacePredType]
  185 
  186 data IfaceTyLit
  187   = IfaceNumTyLit Integer
  188   | IfaceStrTyLit FastString
  189   | IfaceCharTyLit Char
  190   deriving (Eq)
  191 
  192 type IfaceTyConBinder    = VarBndr IfaceBndr TyConBndrVis
  193 type IfaceForAllBndr     = VarBndr IfaceBndr ArgFlag
  194 type IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity
  195 
  196 -- | Make an 'IfaceForAllBndr' from an 'IfaceTvBndr'.
  197 mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr
  198 mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis
  199 
  200 -- | Build the 'tyConKind' from the binders and the result kind.
  201 -- Keep in sync with 'mkTyConKind' in "GHC.Core.TyCon".
  202 mkIfaceTyConKind :: [IfaceTyConBinder] -> IfaceKind -> IfaceKind
  203 mkIfaceTyConKind bndrs res_kind = foldr mk res_kind bndrs
  204   where
  205     mk :: IfaceTyConBinder -> IfaceKind -> IfaceKind
  206     mk (Bndr tv (AnonTCB af))   k = IfaceFunTy af many_ty (ifaceBndrType tv) k
  207     mk (Bndr tv (NamedTCB vis)) k = IfaceForAllTy (Bndr tv vis) k
  208 
  209 ifaceForAllSpecToBndrs :: [IfaceForAllSpecBndr] -> [IfaceForAllBndr]
  210 ifaceForAllSpecToBndrs = map ifaceForAllSpecToBndr
  211 
  212 ifaceForAllSpecToBndr :: IfaceForAllSpecBndr -> IfaceForAllBndr
  213 ifaceForAllSpecToBndr (Bndr tv spec) = Bndr tv (Invisible spec)
  214 
  215 -- | Stores the arguments in a type application as a list.
  216 -- See @Note [Suppressing invisible arguments]@.
  217 data IfaceAppArgs
  218   = IA_Nil
  219   | IA_Arg IfaceType    -- The type argument
  220 
  221            ArgFlag      -- The argument's visibility. We store this here so
  222                         -- that we can:
  223                         --
  224                         -- 1. Avoid pretty-printing invisible (i.e., specified
  225                         --    or inferred) arguments when
  226                         --    -fprint-explicit-kinds isn't enabled, or
  227                         -- 2. When -fprint-explicit-kinds *is*, enabled, print
  228                         --    specified arguments in @(...) and inferred
  229                         --    arguments in @{...}.
  230 
  231            IfaceAppArgs -- The rest of the arguments
  232 
  233 instance Semi.Semigroup IfaceAppArgs where
  234   IA_Nil <> xs              = xs
  235   IA_Arg ty argf rest <> xs = IA_Arg ty argf (rest Semi.<> xs)
  236 
  237 instance Monoid IfaceAppArgs where
  238   mempty = IA_Nil
  239   mappend = (Semi.<>)
  240 
  241 -- Encodes type constructors, kind constructors,
  242 -- coercion constructors, the lot.
  243 -- We have to tag them in order to pretty print them
  244 -- properly.
  245 data IfaceTyCon = IfaceTyCon { ifaceTyConName :: IfExtName
  246                              , ifaceTyConInfo :: IfaceTyConInfo }
  247     deriving (Eq)
  248 
  249 -- | The various types of TyCons which have special, built-in syntax.
  250 data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon
  251 
  252                     | IfaceTupleTyCon !Arity !TupleSort
  253                       -- ^ e.g. @(a, b, c)@ or @(#a, b, c#)@.
  254                       -- The arity is the tuple width, not the tycon arity
  255                       -- (which is twice the width in the case of unboxed
  256                       -- tuples).
  257 
  258                     | IfaceSumTyCon !Arity
  259                       -- ^ e.g. @(a | b | c)@
  260 
  261                     | IfaceEqualityTyCon
  262                       -- ^ A heterogeneous equality TyCon
  263                       --   (i.e. eqPrimTyCon, eqReprPrimTyCon, heqTyCon)
  264                       -- that is actually being applied to two types
  265                       -- of the same kind.  This affects pretty-printing
  266                       -- only: see Note [Equality predicates in IfaceType]
  267                     deriving (Eq)
  268 
  269 instance Outputable IfaceTyConSort where
  270   ppr IfaceNormalTyCon         = text "normal"
  271   ppr (IfaceTupleTyCon n sort) = ppr sort <> colon <> ppr n
  272   ppr (IfaceSumTyCon n)        = text "sum:" <> ppr n
  273   ppr IfaceEqualityTyCon       = text "equality"
  274 
  275 {- Note [Free tyvars in IfaceType]
  276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  277 Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
  278 an IfaceType and pretty printing that.  This eliminates a lot of
  279 pretty-print duplication, and it matches what we do with pretty-
  280 printing TyThings. See Note [Pretty printing via Iface syntax] in GHC.Types.TyThing.Ppr.
  281 
  282 It works fine for closed types, but when printing debug traces (e.g.
  283 when using -ddump-tc-trace) we print a lot of /open/ types.  These
  284 types are full of TcTyVars, and it's absolutely crucial to print them
  285 in their full glory, with their unique, TcTyVarDetails etc.
  286 
  287 So we simply embed a TyVar in IfaceType with the IfaceFreeTyVar constructor.
  288 Note that:
  289 
  290 * We never expect to serialise an IfaceFreeTyVar into an interface file, nor
  291   to deserialise one.  IfaceFreeTyVar is used only in the "convert to IfaceType
  292   and then pretty-print" pipeline.
  293 
  294 We do the same for covars, naturally.
  295 
  296 Note [Equality predicates in IfaceType]
  297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  298 GHC has several varieties of type equality (see Note [The equality types story]
  299 in GHC.Builtin.Types.Prim for details).  In an effort to avoid confusing users, we suppress
  300 the differences during pretty printing unless certain flags are enabled.
  301 Here is how each equality predicate* is printed in homogeneous and
  302 heterogeneous contexts, depending on which combination of the
  303 -fprint-explicit-kinds and -fprint-equality-relations flags is used:
  304 
  305 --------------------------------------------------------------------------------------------
  306 |         Predicate             |        Neither flag        |    -fprint-explicit-kinds   |
  307 |-------------------------------|----------------------------|-----------------------------|
  308 | a ~ b         (homogeneous)   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
  309 | a ~~ b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
  310 | a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
  311 | a ~# b,       homogeneously   |        a ~ b               | (a :: Type) ~  (b :: Type)  |
  312 | a ~# b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
  313 | Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
  314 | a ~R# b,      homogeneously   |        Coercible a b       | Coercible @Type a b         |
  315 | a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
  316 |-------------------------------|----------------------------|-----------------------------|
  317 |         Predicate             | -fprint-equality-relations |          Both flags         |
  318 |-------------------------------|----------------------------|-----------------------------|
  319 | a ~ b         (homogeneous)   |        a ~  b              | (a :: Type) ~  (b :: Type)  |
  320 | a ~~ b,       homogeneously   |        a ~~ b              | (a :: Type) ~~ (b :: Type)  |
  321 | a ~~ b,       heterogeneously |        a ~~ c              | (a :: Type) ~~ (c :: k)     |
  322 | a ~# b,       homogeneously   |        a ~# b              | (a :: Type) ~# (b :: Type)  |
  323 | a ~# b,       heterogeneously |        a ~# c              | (a :: Type) ~# (c :: k)     |
  324 | Coercible a b (homogeneous)   |        Coercible a b       | Coercible @Type a b         |
  325 | a ~R# b,      homogeneously   |        a ~R# b             | (a :: Type) ~R# (b :: Type) |
  326 | a ~R# b,      heterogeneously |        a ~R# b             | (a :: Type) ~R# (c :: k)    |
  327 --------------------------------------------------------------------------------------------
  328 
  329 (* There is no heterogeneous, representational, lifted equality counterpart
  330 to (~~). There could be, but there seems to be no use for it.)
  331 
  332 This table adheres to the following rules:
  333 
  334 A. With -fprint-equality-relations, print the true equality relation.
  335 B. Without -fprint-equality-relations:
  336      i. If the equality is representational and homogeneous, use Coercible.
  337     ii. Otherwise, if the equality is representational, use ~R#.
  338    iii. If the equality is nominal and homogeneous, use ~.
  339     iv. Otherwise, if the equality is nominal, use ~~.
  340 C. With -fprint-explicit-kinds, print kinds on both sides of an infix operator,
  341    as above; or print the kind with Coercible.
  342 D. Without -fprint-explicit-kinds, don't print kinds.
  343 
  344 A hetero-kinded equality is used homogeneously when it is applied to two
  345 identical kinds. Unfortunately, determining this from an IfaceType isn't
  346 possible since we can't see through type synonyms. Consequently, we need to
  347 record whether this particular application is homogeneous in IfaceTyConSort
  348 for the purposes of pretty-printing.
  349 
  350 See Note [The equality types story] in GHC.Builtin.Types.Prim.
  351 -}
  352 
  353 data IfaceTyConInfo   -- Used to guide pretty-printing
  354                       -- and to disambiguate D from 'D (they share a name)
  355   = IfaceTyConInfo { ifaceTyConIsPromoted :: PromotionFlag
  356                    , ifaceTyConSort       :: IfaceTyConSort }
  357     deriving (Eq)
  358 
  359 -- This smart constructor allows sharing of the two most common
  360 -- cases. See #19194
  361 mkIfaceTyConInfo :: PromotionFlag -> IfaceTyConSort -> IfaceTyConInfo
  362 mkIfaceTyConInfo IsPromoted  IfaceNormalTyCon = IfaceTyConInfo IsPromoted  IfaceNormalTyCon
  363 mkIfaceTyConInfo NotPromoted IfaceNormalTyCon = IfaceTyConInfo NotPromoted IfaceNormalTyCon
  364 mkIfaceTyConInfo prom        sort             = IfaceTyConInfo prom        sort
  365 
  366 data IfaceMCoercion
  367   = IfaceMRefl
  368   | IfaceMCo IfaceCoercion
  369 
  370 data IfaceCoercion
  371   = IfaceReflCo       IfaceType
  372   | IfaceGReflCo      Role IfaceType (IfaceMCoercion)
  373   | IfaceFunCo        Role IfaceCoercion IfaceCoercion IfaceCoercion
  374   | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
  375   | IfaceAppCo        IfaceCoercion IfaceCoercion
  376   | IfaceForAllCo     IfaceBndr IfaceCoercion IfaceCoercion
  377   | IfaceCoVarCo      IfLclName
  378   | IfaceAxiomInstCo  IfExtName BranchIndex [IfaceCoercion]
  379   | IfaceAxiomRuleCo  IfLclName [IfaceCoercion]
  380        -- There are only a fixed number of CoAxiomRules, so it suffices
  381        -- to use an IfaceLclName to distinguish them.
  382        -- See Note [Adding built-in type families] in GHC.Builtin.Types.Literals
  383   | IfaceUnivCo       IfaceUnivCoProv Role IfaceType IfaceType
  384   | IfaceSymCo        IfaceCoercion
  385   | IfaceTransCo      IfaceCoercion IfaceCoercion
  386   | IfaceNthCo        Int IfaceCoercion
  387   | IfaceLRCo         LeftOrRight IfaceCoercion
  388   | IfaceInstCo       IfaceCoercion IfaceCoercion
  389   | IfaceKindCo       IfaceCoercion
  390   | IfaceSubCo        IfaceCoercion
  391   | IfaceFreeCoVar    CoVar    -- See Note [Free tyvars in IfaceType]
  392   | IfaceHoleCo       CoVar    -- ^ See Note [Holes in IfaceCoercion]
  393 
  394 data IfaceUnivCoProv
  395   = IfacePhantomProv IfaceCoercion
  396   | IfaceProofIrrelProv IfaceCoercion
  397   | IfacePluginProv String
  398   | IfaceCorePrepProv Bool  -- See defn of CorePrepProv
  399 
  400 {- Note [Holes in IfaceCoercion]
  401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  402 When typechecking fails the typechecker will produce a HoleCo to stand
  403 in place of the unproven assertion. While we generally don't want to
  404 let these unproven assertions leak into interface files, we still need
  405 to be able to pretty-print them as we use IfaceType's pretty-printer
  406 to render Types. For this reason IfaceCoercion has a IfaceHoleCo
  407 constructor; however, we fails when asked to serialize to a
  408 IfaceHoleCo to ensure that they don't end up in an interface file.
  409 
  410 
  411 %************************************************************************
  412 %*                                                                      *
  413                 Functions over IFaceTypes
  414 *                                                                      *
  415 ************************************************************************
  416 -}
  417 
  418 ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
  419 ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
  420 
  421 -- | Given a kind K, is K of the form (TYPE ('BoxedRep 'LiftedRep))?
  422 isIfaceLiftedTypeKind :: IfaceKind -> Bool
  423 isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
  424   = isLiftedTypeKindTyConName (ifaceTyConName tc)
  425 isIfaceLiftedTypeKind (IfaceTyConApp tc1 args1)
  426   = isIfaceTyConAppLiftedTypeKind tc1 args1
  427 isIfaceLiftedTypeKind _ = False
  428 
  429 -- | Given a kind constructor K and arguments A, returns true if
  430 -- both of the following statements are true:
  431 --
  432 -- * K is TYPE
  433 -- * A is a singleton IfaceAppArgs of the form ('BoxedRep 'Lifted)
  434 --
  435 -- For the second condition, we must also check for the type
  436 -- synonym LiftedRep.
  437 isIfaceTyConAppLiftedTypeKind :: IfaceTyCon -> IfaceAppArgs -> Bool
  438 isIfaceTyConAppLiftedTypeKind tc1 args1
  439   | tc1 `ifaceTyConHasKey` tYPETyConKey
  440   , IA_Arg soleArg1 Required IA_Nil <- args1
  441   , IfaceTyConApp rep args2 <- soleArg1 =
  442     if | rep `ifaceTyConHasKey` boxedRepDataConKey
  443        , IA_Arg soleArg2 Required IA_Nil <- args2
  444        , IfaceTyConApp lev IA_Nil <- soleArg2
  445        , lev `ifaceTyConHasKey` liftedDataConKey -> True
  446        | rep `ifaceTyConHasKey` liftedRepTyConKey
  447        , IA_Nil <- args2 -> True
  448        | otherwise -> False
  449   | otherwise = False
  450 
  451 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
  452 -- Mainly for printing purposes
  453 --
  454 -- Here we split nested IfaceSigmaTy properly.
  455 --
  456 -- @
  457 -- forall t. T t => forall m a b. M m => (a -> m b) -> t a -> m (t b)
  458 -- @
  459 --
  460 -- If you called @splitIfaceSigmaTy@ on this type:
  461 --
  462 -- @
  463 -- ([t, m, a, b], [T t, M m], (a -> m b) -> t a -> m (t b))
  464 -- @
  465 splitIfaceSigmaTy ty
  466   = case (bndrs, theta) of
  467       ([], []) -> (bndrs, theta, tau)
  468       _        -> let (bndrs', theta', tau') = splitIfaceSigmaTy tau
  469                    in (bndrs ++ bndrs', theta ++ theta', tau')
  470   where
  471     (bndrs, rho)   = split_foralls ty
  472     (theta, tau)   = split_rho rho
  473 
  474     split_foralls (IfaceForAllTy bndr ty)
  475         | isInvisibleArgFlag (binderArgFlag bndr)
  476         = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
  477     split_foralls rho = ([], rho)
  478 
  479     split_rho (IfaceFunTy InvisArg _ ty1 ty2)
  480         = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
  481     split_rho tau = ([], tau)
  482 
  483 splitIfaceReqForallTy :: IfaceType -> ([IfaceForAllBndr], IfaceType)
  484 splitIfaceReqForallTy (IfaceForAllTy bndr ty)
  485   | isVisibleArgFlag (binderArgFlag bndr)
  486   = case splitIfaceReqForallTy ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
  487 splitIfaceReqForallTy rho = ([], rho)
  488 
  489 suppressIfaceInvisibles :: PrintExplicitKinds -> [IfaceTyConBinder] -> [a] -> [a]
  490 suppressIfaceInvisibles (PrintExplicitKinds True) _tys xs = xs
  491 suppressIfaceInvisibles (PrintExplicitKinds False) tys xs = suppress tys xs
  492     where
  493       suppress _       []      = []
  494       suppress []      a       = a
  495       suppress (k:ks) (x:xs)
  496         | isInvisibleTyConBinder k =     suppress ks xs
  497         | otherwise                = x : suppress ks xs
  498 
  499 stripIfaceInvisVars :: PrintExplicitKinds -> [IfaceTyConBinder] -> [IfaceTyConBinder]
  500 stripIfaceInvisVars (PrintExplicitKinds True)  tyvars = tyvars
  501 stripIfaceInvisVars (PrintExplicitKinds False) tyvars
  502   = filterOut isInvisibleTyConBinder tyvars
  503 
  504 -- | Extract an 'IfaceBndr' from an 'IfaceForAllBndr'.
  505 ifForAllBndrVar :: IfaceForAllBndr -> IfaceBndr
  506 ifForAllBndrVar = binderVar
  507 
  508 -- | Extract the variable name from an 'IfaceForAllBndr'.
  509 ifForAllBndrName :: IfaceForAllBndr -> IfLclName
  510 ifForAllBndrName fab = ifaceBndrName (ifForAllBndrVar fab)
  511 
  512 -- | Extract an 'IfaceBndr' from an 'IfaceTyConBinder'.
  513 ifTyConBinderVar :: IfaceTyConBinder -> IfaceBndr
  514 ifTyConBinderVar = binderVar
  515 
  516 -- | Extract the variable name from an 'IfaceTyConBinder'.
  517 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
  518 ifTyConBinderName tcb = ifaceBndrName (ifTyConBinderVar tcb)
  519 
  520 ifTypeIsVarFree :: IfaceType -> Bool
  521 -- Returns True if the type definitely has no variables at all
  522 -- Just used to control pretty printing
  523 ifTypeIsVarFree ty = go ty
  524   where
  525     go (IfaceTyVar {})         = False
  526     go (IfaceFreeTyVar {})     = False
  527     go (IfaceAppTy fun args)   = go fun && go_args args
  528     go (IfaceFunTy _ w arg res) = go w && go arg && go res
  529     go (IfaceForAllTy {})      = False
  530     go (IfaceTyConApp _ args)  = go_args args
  531     go (IfaceTupleTy _ _ args) = go_args args
  532     go (IfaceLitTy _)          = True
  533     go (IfaceCastTy {})        = False -- Safe
  534     go (IfaceCoercionTy {})    = False -- Safe
  535 
  536     go_args IA_Nil = True
  537     go_args (IA_Arg arg _ args) = go arg && go_args args
  538 
  539 {- Note [Substitution on IfaceType]
  540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  541 Substitutions on IfaceType are done only during pretty-printing to
  542 construct the result type of a GADT, and does not deal with binders
  543 (eg IfaceForAll), so it doesn't need fancy capture stuff.  -}
  544 
  545 type IfaceTySubst = FastStringEnv IfaceType -- Note [Substitution on IfaceType]
  546 
  547 mkIfaceTySubst :: [(IfLclName,IfaceType)] -> IfaceTySubst
  548 -- See Note [Substitution on IfaceType]
  549 mkIfaceTySubst eq_spec = mkFsEnv eq_spec
  550 
  551 inDomIfaceTySubst :: IfaceTySubst -> IfaceTvBndr -> Bool
  552 -- See Note [Substitution on IfaceType]
  553 inDomIfaceTySubst subst (fs, _) = isJust (lookupFsEnv subst fs)
  554 
  555 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
  556 -- See Note [Substitution on IfaceType]
  557 substIfaceType env ty
  558   = go ty
  559   where
  560     go (IfaceFreeTyVar tv)    = IfaceFreeTyVar tv
  561     go (IfaceTyVar tv)        = substIfaceTyVar env tv
  562     go (IfaceAppTy  t ts)     = IfaceAppTy  (go t) (substIfaceAppArgs env ts)
  563     go (IfaceFunTy af w t1 t2)  = IfaceFunTy af (go w) (go t1) (go t2)
  564     go ty@(IfaceLitTy {})     = ty
  565     go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceAppArgs env tys)
  566     go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceAppArgs env tys)
  567     go (IfaceForAllTy {})     = pprPanic "substIfaceType" (ppr ty)
  568     go (IfaceCastTy ty co)    = IfaceCastTy (go ty) (go_co co)
  569     go (IfaceCoercionTy co)   = IfaceCoercionTy (go_co co)
  570 
  571     go_mco IfaceMRefl    = IfaceMRefl
  572     go_mco (IfaceMCo co) = IfaceMCo $ go_co co
  573 
  574     go_co (IfaceReflCo ty)           = IfaceReflCo (go ty)
  575     go_co (IfaceGReflCo r ty mco)    = IfaceGReflCo r (go ty) (go_mco mco)
  576     go_co (IfaceFunCo r w c1 c2)     = IfaceFunCo r (go_co w) (go_co c1) (go_co c2)
  577     go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
  578     go_co (IfaceAppCo c1 c2)         = IfaceAppCo (go_co c1) (go_co c2)
  579     go_co (IfaceForAllCo {})         = pprPanic "substIfaceCoercion" (ppr ty)
  580     go_co (IfaceFreeCoVar cv)        = IfaceFreeCoVar cv
  581     go_co (IfaceCoVarCo cv)          = IfaceCoVarCo cv
  582     go_co (IfaceHoleCo cv)           = IfaceHoleCo cv
  583     go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
  584     go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
  585     go_co (IfaceSymCo co)            = IfaceSymCo (go_co co)
  586     go_co (IfaceTransCo co1 co2)     = IfaceTransCo (go_co co1) (go_co co2)
  587     go_co (IfaceNthCo n co)          = IfaceNthCo n (go_co co)
  588     go_co (IfaceLRCo lr co)          = IfaceLRCo lr (go_co co)
  589     go_co (IfaceInstCo c1 c2)        = IfaceInstCo (go_co c1) (go_co c2)
  590     go_co (IfaceKindCo co)           = IfaceKindCo (go_co co)
  591     go_co (IfaceSubCo co)            = IfaceSubCo (go_co co)
  592     go_co (IfaceAxiomRuleCo n cos)   = IfaceAxiomRuleCo n (go_cos cos)
  593 
  594     go_cos = map go_co
  595 
  596     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
  597     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
  598     go_prov co@(IfacePluginProv _)   = co
  599     go_prov co@(IfaceCorePrepProv _) = co
  600 
  601 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
  602 substIfaceAppArgs env args
  603   = go args
  604   where
  605     go IA_Nil              = IA_Nil
  606     go (IA_Arg ty arg tys) = IA_Arg (substIfaceType env ty) arg (go tys)
  607 
  608 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
  609 substIfaceTyVar env tv
  610   | Just ty <- lookupFsEnv env tv = ty
  611   | otherwise                     = IfaceTyVar tv
  612 
  613 
  614 {-
  615 ************************************************************************
  616 *                                                                      *
  617                 Functions over IfaceAppArgs
  618 *                                                                      *
  619 ************************************************************************
  620 -}
  621 
  622 stripInvisArgs :: PrintExplicitKinds -> IfaceAppArgs -> IfaceAppArgs
  623 stripInvisArgs (PrintExplicitKinds True)  tys = tys
  624 stripInvisArgs (PrintExplicitKinds False) tys = suppress_invis tys
  625     where
  626       suppress_invis c
  627         = case c of
  628             IA_Nil -> IA_Nil
  629             IA_Arg t argf ts
  630               |  isVisibleArgFlag argf
  631               -> IA_Arg t argf $ suppress_invis ts
  632               -- Keep recursing through the remainder of the arguments, as it's
  633               -- possible that there are remaining invisible ones.
  634               -- See the "In type declarations" section of Note [VarBndrs,
  635               -- TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep.
  636               |  otherwise
  637               -> suppress_invis ts
  638 
  639 appArgsIfaceTypes :: IfaceAppArgs -> [IfaceType]
  640 appArgsIfaceTypes IA_Nil = []
  641 appArgsIfaceTypes (IA_Arg t _ ts) = t : appArgsIfaceTypes ts
  642 
  643 appArgsIfaceTypesArgFlags :: IfaceAppArgs -> [(IfaceType, ArgFlag)]
  644 appArgsIfaceTypesArgFlags IA_Nil = []
  645 appArgsIfaceTypesArgFlags (IA_Arg t a ts)
  646                                  = (t, a) : appArgsIfaceTypesArgFlags ts
  647 
  648 ifaceVisAppArgsLength :: IfaceAppArgs -> Int
  649 ifaceVisAppArgsLength = go 0
  650   where
  651     go !n IA_Nil = n
  652     go n  (IA_Arg _ argf rest)
  653       | isVisibleArgFlag argf = go (n+1) rest
  654       | otherwise             = go n rest
  655 
  656 {-
  657 Note [Suppressing invisible arguments]
  658 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  659 We use the IfaceAppArgs data type to specify which of the arguments to a type
  660 should be displayed when pretty-printing, under the control of
  661 -fprint-explicit-kinds.
  662 See also Type.filterOutInvisibleTypes.
  663 For example, given
  664 
  665     T :: forall k. (k->*) -> k -> *    -- Ordinary kind polymorphism
  666     'Just :: forall k. k -> 'Maybe k   -- Promoted
  667 
  668 we want
  669 
  670     T * Tree Int    prints as    T Tree Int
  671     'Just *         prints as    Just *
  672 
  673 For type constructors (IfaceTyConApp), IfaceAppArgs is a quite natural fit,
  674 since the corresponding Core constructor:
  675 
  676     data Type
  677       = ...
  678       | TyConApp TyCon [Type]
  679 
  680 Already puts all of its arguments into a list. So when converting a Type to an
  681 IfaceType (see toIfaceAppArgsX in GHC.Core.ToIface), we simply use the kind of
  682 the TyCon (which is cached) to guide the process of converting the argument
  683 Types into an IfaceAppArgs list.
  684 
  685 We also want this behavior for IfaceAppTy, since given:
  686 
  687     data Proxy (a :: k)
  688     f :: forall (t :: forall a. a -> Type). Proxy Type (t Bool True)
  689 
  690 We want to print the return type as `Proxy (t True)` without the use of
  691 -fprint-explicit-kinds (#15330). Accomplishing this is trickier than in the
  692 tycon case, because the corresponding Core constructor for IfaceAppTy:
  693 
  694     data Type
  695       = ...
  696       | AppTy Type Type
  697 
  698 Only stores one argument at a time. Therefore, when converting an AppTy to an
  699 IfaceAppTy (in toIfaceTypeX in GHC.CoreToIface), we:
  700 
  701 1. Flatten the chain of AppTys down as much as possible
  702 2. Use typeKind to determine the function Type's kind
  703 3. Use this kind to guide the process of converting the argument Types into an
  704    IfaceAppArgs list.
  705 
  706 By flattening the arguments like this, we obtain two benefits:
  707 
  708 (a) We can reuse the same machinery to pretty-print IfaceTyConApp arguments as
  709     we do IfaceTyApp arguments, which means that we only need to implement the
  710     logic to filter out invisible arguments once.
  711 (b) Unlike for tycons, finding the kind of a type in general (through typeKind)
  712     is not a constant-time operation, so by flattening the arguments first, we
  713     decrease the number of times we have to call typeKind.
  714 
  715 Note [Pretty-printing invisible arguments]
  716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  717 Note [Suppressing invisible arguments] is all about how to avoid printing
  718 invisible arguments when the -fprint-explicit-kinds flag is disables. Well,
  719 what about when it's enabled? Then we can and should print invisible kind
  720 arguments, and this Note explains how we do it.
  721 
  722 As two running examples, consider the following code:
  723 
  724   {-# LANGUAGE PolyKinds #-}
  725   data T1 a
  726   data T2 (a :: k)
  727 
  728 When displaying these types (with -fprint-explicit-kinds on), we could just
  729 do the following:
  730 
  731   T1 k a
  732   T2 k a
  733 
  734 That certainly gets the job done. But it lacks a crucial piece of information:
  735 is the `k` argument inferred or specified? To communicate this, we use visible
  736 kind application syntax to distinguish the two cases:
  737 
  738   T1 @{k} a
  739   T2 @k   a
  740 
  741 Here, @{k} indicates that `k` is an inferred argument, and @k indicates that
  742 `k` is a specified argument. (See
  743 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep for
  744 a lengthier explanation on what "inferred" and "specified" mean.)
  745 
  746 ************************************************************************
  747 *                                                                      *
  748                 Pretty-printing
  749 *                                                                      *
  750 ************************************************************************
  751 -}
  752 
  753 if_print_coercions :: SDoc  -- ^ if printing coercions
  754                    -> SDoc  -- ^ otherwise
  755                    -> SDoc
  756 if_print_coercions yes no
  757   = sdocOption sdocPrintExplicitCoercions $ \print_co ->
  758     getPprStyle $ \style ->
  759     getPprDebug $ \debug ->
  760     if print_co || dumpStyle style || debug
  761     then yes
  762     else no
  763 
  764 pprIfaceInfixApp :: PprPrec -> SDoc -> SDoc -> SDoc -> SDoc
  765 pprIfaceInfixApp ctxt_prec pp_tc pp_ty1 pp_ty2
  766   = maybeParen ctxt_prec opPrec $
  767     sep [pp_ty1, pp_tc <+> pp_ty2]
  768 
  769 pprIfacePrefixApp :: PprPrec -> SDoc -> [SDoc] -> SDoc
  770 pprIfacePrefixApp ctxt_prec pp_fun pp_tys
  771   | null pp_tys = pp_fun
  772   | otherwise   = maybeParen ctxt_prec appPrec $
  773                   hang pp_fun 2 (sep pp_tys)
  774 
  775 isIfaceTauType :: IfaceType -> Bool
  776 isIfaceTauType (IfaceForAllTy _ _) = False
  777 isIfaceTauType (IfaceFunTy InvisArg _ _ _) = False
  778 isIfaceTauType _ = True
  779 
  780 -- ----------------------------- Printing binders ------------------------------------
  781 
  782 instance Outputable IfaceBndr where
  783     ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
  784     ppr (IfaceTvBndr bndr) = char '@' <> pprIfaceTvBndr bndr (SuppressBndrSig False)
  785                                                              (UseBndrParens False)
  786 
  787 pprIfaceBndrs :: [IfaceBndr] -> SDoc
  788 pprIfaceBndrs bs = sep (map ppr bs)
  789 
  790 pprIfaceLamBndr :: IfaceLamBndr -> SDoc
  791 pprIfaceLamBndr (b, IfaceNoOneShot) = ppr b
  792 pprIfaceLamBndr (b, IfaceOneShot)   = ppr b <> text "[OneShot]"
  793 
  794 pprIfaceIdBndr :: IfaceIdBndr -> SDoc
  795 pprIfaceIdBndr (w, name, ty) = parens (ppr name <> brackets (ppr w) <+> dcolon <+> ppr ty)
  796 
  797 {- Note [Suppressing binder signatures]
  798 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  799 When printing the binders in a 'forall', we want to keep the kind annotations:
  800 
  801     forall (a :: k). blah
  802               ^^^^
  803               good
  804 
  805 On the other hand, when we print the binders of a data declaration in :info,
  806 the kind information would be redundant due to the standalone kind signature:
  807 
  808    type F :: Symbol -> Type
  809    type F (s :: Symbol) = blah
  810              ^^^^^^^^^
  811              redundant
  812 
  813 Here we'd like to omit the kind annotation:
  814 
  815    type F :: Symbol -> Type
  816    type F s = blah
  817 
  818 Note [Printing type abbreviations]
  819 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  820 Normally, we pretty-print `TYPE 'LiftedRep` as `Type` (or `*`) and
  821 `FUN 'Many` as `(->)`.
  822 This way, error messages don't refer to representation polymorphism
  823 or linearity if it is not necessary.
  824 
  825 However, when printing the definition of Type or (->) with :info,
  826 this would give confusing output: `type (->) = (->)` (#18594).
  827 Solution: detect when we are in :info and disable displaying the synonym
  828 with the SDoc option sdocPrintTypeAbbreviations.
  829 
  830 If there will be a need, in the future we could expose it as a flag
  831 -fprint-type-abbreviations or even two separate flags controlling
  832 TYPE 'LiftedRep and FUN 'Many.
  833 -}
  834 
  835 -- | Do we want to suppress kind annotations on binders?
  836 -- See Note [Suppressing binder signatures]
  837 newtype SuppressBndrSig = SuppressBndrSig Bool
  838 
  839 newtype UseBndrParens      = UseBndrParens Bool
  840 newtype PrintExplicitKinds = PrintExplicitKinds Bool
  841 
  842 pprIfaceTvBndr :: IfaceTvBndr -> SuppressBndrSig -> UseBndrParens -> SDoc
  843 pprIfaceTvBndr (tv, ki) (SuppressBndrSig suppress_sig) (UseBndrParens use_parens)
  844   | suppress_sig             = ppr tv
  845   | isIfaceLiftedTypeKind ki = ppr tv
  846   | otherwise                = maybe_parens (ppr tv <+> dcolon <+> ppr ki)
  847   where
  848     maybe_parens | use_parens = parens
  849                  | otherwise  = id
  850 
  851 pprIfaceTyConBinders :: SuppressBndrSig -> [IfaceTyConBinder] -> SDoc
  852 pprIfaceTyConBinders suppress_sig = sep . map go
  853   where
  854     go :: IfaceTyConBinder -> SDoc
  855     go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr
  856     go (Bndr (IfaceTvBndr bndr) vis) =
  857       -- See Note [Pretty-printing invisible arguments]
  858       case vis of
  859         AnonTCB  VisArg    -> ppr_bndr (UseBndrParens True)
  860         AnonTCB  InvisArg  -> char '@' <> braces (ppr_bndr (UseBndrParens False))
  861           -- The above case is rare. (See Note [AnonTCB InvisArg] in GHC.Core.TyCon.)
  862           -- Should we print these differently?
  863         NamedTCB Required  -> ppr_bndr (UseBndrParens True)
  864         -- See Note [Explicit Case Statement for Specificity]
  865         NamedTCB (Invisible spec) -> case spec of
  866           SpecifiedSpec    -> char '@' <> ppr_bndr (UseBndrParens True)
  867           InferredSpec     -> char '@' <> braces (ppr_bndr (UseBndrParens False))
  868       where
  869         ppr_bndr = pprIfaceTvBndr bndr suppress_sig
  870 
  871 instance Binary IfaceBndr where
  872     put_ bh (IfaceIdBndr aa) = do
  873             putByte bh 0
  874             put_ bh aa
  875     put_ bh (IfaceTvBndr ab) = do
  876             putByte bh 1
  877             put_ bh ab
  878     get bh = do
  879             h <- getByte bh
  880             case h of
  881               0 -> do aa <- get bh
  882                       return (IfaceIdBndr aa)
  883               _ -> do ab <- get bh
  884                       return (IfaceTvBndr ab)
  885 
  886 instance Binary IfaceOneShot where
  887     put_ bh IfaceNoOneShot =
  888             putByte bh 0
  889     put_ bh IfaceOneShot =
  890             putByte bh 1
  891     get bh = do
  892             h <- getByte bh
  893             case h of
  894               0 -> return IfaceNoOneShot
  895               _ -> return IfaceOneShot
  896 
  897 -- ----------------------------- Printing IfaceType ------------------------------------
  898 
  899 ---------------------------------
  900 instance Outputable IfaceType where
  901   ppr ty = pprIfaceType ty
  902 
  903 pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
  904 pprIfaceType       = pprPrecIfaceType topPrec
  905 pprParendIfaceType = pprPrecIfaceType appPrec
  906 
  907 pprPrecIfaceType :: PprPrec -> IfaceType -> SDoc
  908 -- We still need `hideNonStandardTypes`, since the `pprPrecIfaceType` may be
  909 -- called from other places, besides `:type` and `:info`.
  910 pprPrecIfaceType prec ty =
  911   hideNonStandardTypes (ppr_ty prec) ty
  912 
  913 ppr_fun_arrow :: IfaceMult -> SDoc
  914 ppr_fun_arrow w
  915   | (IfaceTyConApp tc _) <- w
  916   , tc `ifaceTyConHasKey` (getUnique manyDataConTyCon) = arrow
  917   | (IfaceTyConApp tc _) <- w
  918   , tc `ifaceTyConHasKey` (getUnique oneDataConTyCon) = lollipop
  919   | otherwise = mulArrow (pprIfaceType w)
  920 
  921 ppr_sigma :: PprPrec -> IfaceType -> SDoc
  922 ppr_sigma ctxt_prec ty
  923   = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
  924 
  925 ppr_ty :: PprPrec -> IfaceType -> SDoc
  926 ppr_ty ctxt_prec ty@(IfaceForAllTy {})          = ppr_sigma ctxt_prec ty
  927 ppr_ty ctxt_prec ty@(IfaceFunTy InvisArg _ _ _) = ppr_sigma ctxt_prec ty
  928 
  929 ppr_ty _         (IfaceFreeTyVar tyvar) = ppr tyvar  -- This is the main reason for IfaceFreeTyVar!
  930 ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar  -- See Note [TcTyVars in IfaceType]
  931 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = pprTyTcApp ctxt_prec tc tys
  932 ppr_ty ctxt_prec (IfaceTupleTy i p tys) = pprTuple ctxt_prec i p tys
  933 ppr_ty _         (IfaceLitTy n)         = pprIfaceTyLit n
  934         -- Function types
  935 ppr_ty ctxt_prec (IfaceFunTy _ w ty1 ty2)  -- Should be VisArg
  936   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
  937     maybeParen ctxt_prec funPrec $
  938     sep [ppr_ty funPrec ty1, sep (ppr_fun_tail w ty2)]
  939   where
  940     ppr_fun_tail wthis (IfaceFunTy VisArg wnext ty1 ty2)
  941       = (ppr_fun_arrow wthis <+> ppr_ty funPrec ty1) : ppr_fun_tail wnext ty2
  942     ppr_fun_tail wthis other_ty
  943       = [ppr_fun_arrow wthis <+> pprIfaceType other_ty]
  944 
  945 ppr_ty ctxt_prec (IfaceAppTy t ts)
  946   = if_print_coercions
  947       ppr_app_ty
  948       ppr_app_ty_no_casts
  949   where
  950     ppr_app_ty =
  951         sdocOption sdocPrintExplicitKinds $ \print_kinds ->
  952         let tys_wo_kinds = appArgsIfaceTypesArgFlags $ stripInvisArgs
  953                               (PrintExplicitKinds print_kinds) ts
  954         in pprIfacePrefixApp ctxt_prec
  955                              (ppr_ty funPrec t)
  956                              (map (ppr_app_arg appPrec) tys_wo_kinds)
  957 
  958 
  959     -- Strip any casts from the head of the application
  960     ppr_app_ty_no_casts =
  961         case t of
  962           IfaceCastTy head _ -> ppr_ty ctxt_prec (mk_app_tys head ts)
  963           _                  -> ppr_app_ty
  964 
  965     mk_app_tys :: IfaceType -> IfaceAppArgs -> IfaceType
  966     mk_app_tys (IfaceTyConApp tc tys1) tys2 =
  967         IfaceTyConApp tc (tys1 `mappend` tys2)
  968     mk_app_tys t1 tys2 = IfaceAppTy t1 tys2
  969 
  970 ppr_ty ctxt_prec (IfaceCastTy ty co)
  971   = if_print_coercions
  972       (parens (ppr_ty topPrec ty <+> text "|>" <+> ppr co))
  973       (ppr_ty ctxt_prec ty)
  974 
  975 ppr_ty ctxt_prec (IfaceCoercionTy co)
  976   = if_print_coercions
  977       (ppr_co ctxt_prec co)
  978       (text "<>")
  979 
  980 {- Note [Defaulting RuntimeRep variables]
  981 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  982 RuntimeRep variables are considered by many (most?) users to be little
  983 more than syntactic noise. When the notion was introduced there was a
  984 significant and understandable push-back from those with pedagogy in
  985 mind, which argued that RuntimeRep variables would throw a wrench into
  986 nearly any teach approach since they appear in even the lowly ($)
  987 function's type,
  988 
  989     ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
  990 
  991 which is significantly less readable than its non RuntimeRep-polymorphic type of
  992 
  993     ($) :: (a -> b) -> a -> b
  994 
  995 Moreover, unboxed types don't appear all that often in run-of-the-mill
  996 Haskell programs, so it makes little sense to make all users pay this
  997 syntactic overhead.
  998 
  999 For this reason it was decided that we would hide RuntimeRep variables
 1000 for now (see #11549). We do this by defaulting all type variables of
 1001 kind RuntimeRep to LiftedRep.
 1002 Likewise, we default all Multiplicity variables to Many.
 1003 
 1004 This is done in a pass right before pretty-printing
 1005 (defaultIfaceTyVarsOfKind, controlled by
 1006 -fprint-explicit-runtime-reps and -XLinearTypes)
 1007 
 1008 This applies to /quantified/ variables like 'w' above.  What about
 1009 variables that are /free/ in the type being printed, which certainly
 1010 happens in error messages.  Suppose (#16074, #19361) we are reporting a
 1011 mismatch between skolems
 1012           (a :: RuntimeRep) ~ (b :: RuntimeRep)
 1013         or
 1014           (m :: Multiplicity) ~ Many
 1015 We certainly don't want to say "Can't match LiftedRep with LiftedRep" or
 1016 "Can't match Many with Many"!
 1017 
 1018 But if we are printing the type
 1019     (forall (a :: TYPE r). blah)
 1020 we do want to turn that (free) r into LiftedRep, so it prints as
 1021     (forall a. blah)
 1022 
 1023 We use isMetaTyVar to distinguish between those two situations:
 1024 metavariables are converted, skolem variables are not.
 1025 
 1026 There's one exception though: TyVarTv metavariables should not be defaulted,
 1027 as they appear during kind-checking of "newtype T :: TYPE r where..."
 1028 (test T18357a). Therefore, we additionally test for isTyConableTyVar.
 1029 -}
 1030 
 1031 -- | Default 'RuntimeRep' variables to 'LiftedRep',
 1032 --   'Levity' variables to 'Lifted', and 'Multiplicity'
 1033 --   variables to 'Many'. For example:
 1034 --
 1035 -- @
 1036 -- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
 1037 --        (a -> b) -> a -> b
 1038 -- Just :: forall (k :: Multiplicity) a. a # k -> Maybe a
 1039 -- @
 1040 --
 1041 -- turns in to,
 1042 --
 1043 -- @ ($) :: forall a (b :: *). (a -> b) -> a -> b @
 1044 -- @ Just :: forall a . a -> Maybe a @
 1045 --
 1046 -- We do this to prevent RuntimeRep, Levity and Multiplicity variables from
 1047 -- incurring a significant syntactic overhead in otherwise simple
 1048 -- type signatures (e.g. ($)). See Note [Defaulting RuntimeRep variables]
 1049 -- and #11549 for further discussion.
 1050 defaultIfaceTyVarsOfKind :: DefaultVarsOfKind
 1051                          -> IfaceType -> IfaceType
 1052 defaultIfaceTyVarsOfKind def_ns_vars ty = go emptyFsEnv ty
 1053   where
 1054     go :: FastStringEnv IfaceType -- Set of enclosing forall-ed RuntimeRep/Levity/Multiplicity variables
 1055        -> IfaceType
 1056        -> IfaceType
 1057     go subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
 1058      | isInvisibleArgFlag argf  -- Don't default *visible* quantification
 1059                                 -- or we get the mess in #13963
 1060      , Just substituted_ty <- check_substitution var_kind
 1061       = let subs' = extendFsEnv subs var substituted_ty
 1062             -- Record that we should replace it with LiftedRep/Lifted/Many,
 1063             -- and recurse, discarding the forall
 1064         in go subs' ty
 1065 
 1066     go subs (IfaceForAllTy bndr ty)
 1067       = IfaceForAllTy (go_ifacebndr subs bndr) (go subs ty)
 1068 
 1069     go subs ty@(IfaceTyVar tv) = case lookupFsEnv subs tv of
 1070       Just s -> s
 1071       Nothing -> ty
 1072 
 1073     go _ ty@(IfaceFreeTyVar tv)
 1074       -- See Note [Defaulting RuntimeRep variables], about free vars
 1075       | def_runtimeRep def_ns_vars
 1076       , GHC.Core.Type.isRuntimeRepTy (tyVarKind tv)
 1077       , isMetaTyVar tv
 1078       , isTyConableTyVar tv
 1079       = liftedRep_ty
 1080       | def_levity def_ns_vars
 1081       , GHC.Core.Type.isLevityTy (tyVarKind tv)
 1082       , isMetaTyVar tv
 1083       , isTyConableTyVar tv
 1084       = lifted_ty
 1085       | def_multiplicity def_ns_vars
 1086       , GHC.Core.Type.isMultiplicityTy (tyVarKind tv)
 1087       , isMetaTyVar tv
 1088       , isTyConableTyVar tv
 1089       = many_ty
 1090       | otherwise
 1091       = ty
 1092 
 1093     go subs (IfaceTyConApp tc tc_args)
 1094       = IfaceTyConApp tc (go_args subs tc_args)
 1095 
 1096     go subs (IfaceTupleTy sort is_prom tc_args)
 1097       = IfaceTupleTy sort is_prom (go_args subs tc_args)
 1098 
 1099     go subs (IfaceFunTy af w arg res)
 1100       = IfaceFunTy af (go subs w) (go subs arg) (go subs res)
 1101 
 1102     go subs (IfaceAppTy t ts)
 1103       = IfaceAppTy (go subs t) (go_args subs ts)
 1104 
 1105     go subs (IfaceCastTy x co)
 1106       = IfaceCastTy (go subs x) co
 1107 
 1108     go _ ty@(IfaceLitTy {}) = ty
 1109     go _ ty@(IfaceCoercionTy {}) = ty
 1110 
 1111     go_ifacebndr :: FastStringEnv IfaceType -> IfaceForAllBndr -> IfaceForAllBndr
 1112     go_ifacebndr subs (Bndr (IfaceIdBndr (w, n, t)) argf)
 1113       = Bndr (IfaceIdBndr (w, n, go subs t)) argf
 1114     go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
 1115       = Bndr (IfaceTvBndr (n, go subs t)) argf
 1116 
 1117     go_args :: FastStringEnv IfaceType -> IfaceAppArgs -> IfaceAppArgs
 1118     go_args _ IA_Nil = IA_Nil
 1119     go_args subs (IA_Arg ty argf args)
 1120       = IA_Arg (go subs ty) argf (go_args subs args)
 1121 
 1122     check_substitution :: IfaceType -> Maybe IfaceType
 1123     check_substitution (IfaceTyConApp tc _)
 1124         | def_runtimeRep def_ns_vars
 1125         , tc `ifaceTyConHasKey` runtimeRepTyConKey
 1126         = Just liftedRep_ty
 1127         | def_levity def_ns_vars
 1128         , tc `ifaceTyConHasKey` levityTyConKey
 1129         = Just lifted_ty
 1130         | def_multiplicity def_ns_vars
 1131         , tc `ifaceTyConHasKey` multiplicityTyConKey
 1132         = Just many_ty
 1133     check_substitution _ = Nothing
 1134 
 1135 -- | The type ('BoxedRep 'Lifted), also known as LiftedRep.
 1136 liftedRep_ty :: IfaceType
 1137 liftedRep_ty =
 1138   IfaceTyConApp liftedRep IA_Nil
 1139   where
 1140     liftedRep :: IfaceTyCon
 1141     liftedRep = IfaceTyCon tc_name (mkIfaceTyConInfo NotPromoted IfaceNormalTyCon)
 1142       where tc_name = getName liftedRepTyCon
 1143 
 1144 -- | The type 'Lifted :: Levity'.
 1145 lifted_ty :: IfaceType
 1146 lifted_ty =
 1147     IfaceTyConApp (IfaceTyCon dc_name (mkIfaceTyConInfo IsPromoted IfaceNormalTyCon))
 1148                   IA_Nil
 1149   where dc_name = getName liftedDataConTyCon
 1150 
 1151 -- | The type 'Many :: Multiplicity'.
 1152 many_ty :: IfaceType
 1153 many_ty =
 1154     IfaceTyConApp (IfaceTyCon dc_name (mkIfaceTyConInfo IsPromoted IfaceNormalTyCon))
 1155                   IA_Nil
 1156   where dc_name = getName manyDataConTyCon
 1157 
 1158 hideNonStandardTypes :: (IfaceType -> SDoc) -> IfaceType -> SDoc
 1159 hideNonStandardTypes f ty
 1160   = sdocOption sdocPrintExplicitRuntimeReps $ \printExplicitRuntimeReps ->
 1161     sdocOption sdocLinearTypes $ \linearTypes ->
 1162     getPprStyle      $ \sty    ->
 1163     let def_opts =
 1164           DefaultVarsOfKind
 1165             { def_runtimeRep   = not printExplicitRuntimeReps
 1166             , def_levity       = not printExplicitRuntimeReps
 1167             , def_multiplicity = not linearTypes }
 1168     in if userStyle sty
 1169        then f (defaultIfaceTyVarsOfKind def_opts ty)
 1170        else f ty
 1171 
 1172 instance Outputable IfaceAppArgs where
 1173   ppr tca = pprIfaceAppArgs tca
 1174 
 1175 pprIfaceAppArgs, pprParendIfaceAppArgs :: IfaceAppArgs -> SDoc
 1176 pprIfaceAppArgs  = ppr_app_args topPrec
 1177 pprParendIfaceAppArgs = ppr_app_args appPrec
 1178 
 1179 ppr_app_args :: PprPrec -> IfaceAppArgs -> SDoc
 1180 ppr_app_args ctx_prec = go
 1181   where
 1182     go :: IfaceAppArgs -> SDoc
 1183     go IA_Nil             = empty
 1184     go (IA_Arg t argf ts) = ppr_app_arg ctx_prec (t, argf) <+> go ts
 1185 
 1186 -- See Note [Pretty-printing invisible arguments]
 1187 ppr_app_arg :: PprPrec -> (IfaceType, ArgFlag) -> SDoc
 1188 ppr_app_arg ctx_prec (t, argf) =
 1189   sdocOption sdocPrintExplicitKinds $ \print_kinds ->
 1190   case argf of
 1191        Required  -> ppr_ty ctx_prec t
 1192        Specified |  print_kinds
 1193                  -> char '@' <> ppr_ty appPrec t
 1194        Inferred  |  print_kinds
 1195                  -> char '@' <> braces (ppr_ty topPrec t)
 1196        _         -> empty
 1197 
 1198 -------------------
 1199 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
 1200 pprIfaceForAllPart tvs ctxt sdoc
 1201   = ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc
 1202 
 1203 -- | Like 'pprIfaceForAllPart', but always uses an explicit @forall@.
 1204 pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
 1205 pprIfaceForAllPartMust tvs ctxt sdoc
 1206   = ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
 1207 
 1208 pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
 1209 pprIfaceForAllCoPart tvs sdoc
 1210   = sep [ pprIfaceForAllCo tvs, sdoc ]
 1211 
 1212 ppr_iface_forall_part :: ShowForAllFlag
 1213                       -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
 1214 ppr_iface_forall_part show_forall tvs ctxt sdoc
 1215   = sep [ case show_forall of
 1216             ShowForAllMust -> pprIfaceForAll tvs
 1217             ShowForAllWhen -> pprUserIfaceForAll tvs
 1218         , pprIfaceContextArr ctxt
 1219         , sdoc]
 1220 
 1221 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
 1222 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
 1223 pprIfaceForAll [] = empty
 1224 pprIfaceForAll bndrs@(Bndr _ vis : _)
 1225   = sep [ add_separator (forAllLit <+> fsep docs)
 1226         , pprIfaceForAll bndrs' ]
 1227   where
 1228     (bndrs', docs) = ppr_itv_bndrs bndrs vis
 1229 
 1230     add_separator stuff = case vis of
 1231                             Required -> stuff <+> arrow
 1232                             _inv     -> stuff <>  dot
 1233 
 1234 
 1235 -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
 1236 -- Returns both the list of not-yet-rendered binders and the doc.
 1237 -- No anonymous binders here!
 1238 ppr_itv_bndrs :: [IfaceForAllBndr]
 1239              -> ArgFlag  -- ^ visibility of the first binder in the list
 1240              -> ([IfaceForAllBndr], [SDoc])
 1241 ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
 1242   | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
 1243                          (bndrs', pprIfaceForAllBndr bndr : doc)
 1244   | otherwise   = (all_bndrs, [])
 1245 ppr_itv_bndrs [] _ = ([], [])
 1246 
 1247 pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
 1248 pprIfaceForAllCo []  = empty
 1249 pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
 1250 
 1251 pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
 1252 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 1253 
 1254 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
 1255 pprIfaceForAllBndr bndr =
 1256   case bndr of
 1257     Bndr (IfaceTvBndr tv) Inferred ->
 1258       braces $ pprIfaceTvBndr tv suppress_sig (UseBndrParens False)
 1259     Bndr (IfaceTvBndr tv) _ ->
 1260       pprIfaceTvBndr tv suppress_sig (UseBndrParens True)
 1261     Bndr (IfaceIdBndr idv) _ -> pprIfaceIdBndr idv
 1262   where
 1263     -- See Note [Suppressing binder signatures]
 1264     suppress_sig = SuppressBndrSig False
 1265 
 1266 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 1267 pprIfaceForAllCoBndr (tv, kind_co)
 1268   = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
 1269 
 1270 -- | Show forall flag
 1271 --
 1272 -- Unconditionally show the forall quantifier with ('ShowForAllMust')
 1273 -- or when ('ShowForAllWhen') the names used are free in the binder
 1274 -- or when compiling with -fprint-explicit-foralls.
 1275 data ShowForAllFlag = ShowForAllMust | ShowForAllWhen
 1276 
 1277 pprIfaceSigmaType :: ShowForAllFlag -> IfaceType -> SDoc
 1278 pprIfaceSigmaType show_forall ty
 1279   = hideNonStandardTypes ppr_fn ty
 1280   where
 1281     ppr_fn iface_ty =
 1282       let (invis_tvs, theta, tau) = splitIfaceSigmaTy iface_ty
 1283           (req_tvs, tau') = splitIfaceReqForallTy tau
 1284           -- splitIfaceSigmaTy is recursive, so it will gather the binders after
 1285           -- the theta, i.e.  forall a. theta => forall b. tau
 1286           -- will give you    ([a,b], theta, tau).
 1287           --
 1288           -- This isn't right when it comes to visible forall (see
 1289           --  testsuite/tests/polykinds/T18522-ppr),
 1290           -- so we split off required binders separately,
 1291           -- using splitIfaceReqForallTy.
 1292           --
 1293           -- An alternative solution would be to make splitIfaceSigmaTy
 1294           -- non-recursive (see #18458).
 1295           -- Then it could handle both invisible and required binders, and
 1296           -- splitIfaceReqForallTy wouldn't be necessary here.
 1297        in ppr_iface_forall_part show_forall invis_tvs theta $
 1298           sep [pprIfaceForAll req_tvs, ppr tau']
 1299 
 1300 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
 1301 pprUserIfaceForAll tvs
 1302    = sdocOption sdocPrintExplicitForalls $ \print_foralls ->
 1303      -- See Note [When to print foralls] in this module.
 1304      ppWhen (any tv_has_kind_var tvs
 1305              || any tv_is_required tvs
 1306              || print_foralls) $
 1307      pprIfaceForAll tvs
 1308    where
 1309      tv_has_kind_var (Bndr (IfaceTvBndr (_,kind)) _)
 1310        = not (ifTypeIsVarFree kind)
 1311      tv_has_kind_var _ = False
 1312 
 1313      tv_is_required = isVisibleArgFlag . binderArgFlag
 1314 
 1315 {-
 1316 Note [When to print foralls]
 1317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1318 We opt to explicitly pretty-print `forall`s if any of the following
 1319 criteria are met:
 1320 
 1321 1. -fprint-explicit-foralls is on.
 1322 
 1323 2. A bound type variable has a polymorphic kind. E.g.,
 1324 
 1325      forall k (a::k). Proxy a -> Proxy a
 1326 
 1327    Since a's kind mentions a variable k, we print the foralls.
 1328 
 1329 3. A bound type variable is a visible argument (#14238).
 1330    Suppose we are printing the kind of:
 1331 
 1332      T :: forall k -> k -> Type
 1333 
 1334    The "forall k ->" notation means that this kind argument is required.
 1335    That is, it must be supplied at uses of T. E.g.,
 1336 
 1337      f :: T (Type->Type)  Monad -> Int
 1338 
 1339    So we print an explicit "T :: forall k -> k -> Type",
 1340    because omitting it and printing "T :: k -> Type" would be
 1341    utterly misleading.
 1342 
 1343    See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
 1344    in GHC.Core.TyCo.Rep.
 1345 
 1346 N.B. Until now (Aug 2018) we didn't check anything for coercion variables.
 1347 
 1348 Note [Printing foralls in type family instances]
 1349 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1350 We use the same criteria as in Note [When to print foralls] to determine
 1351 whether a type family instance should be pretty-printed with an explicit
 1352 `forall`. Example:
 1353 
 1354   type family Foo (a :: k) :: k where
 1355     Foo Maybe       = []
 1356     Foo (a :: Type) = Int
 1357     Foo a           = a
 1358 
 1359 Without -fprint-explicit-foralls enabled, this will be pretty-printed as:
 1360 
 1361 type family Foo (a :: k) :: k where
 1362   Foo Maybe = []
 1363   Foo a = Int
 1364   forall k (a :: k). Foo a = a
 1365 
 1366 Note that only the third equation has an explicit forall, since it has a type
 1367 variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then
 1368 the second equation would be preceded with `forall a.`.)
 1369 
 1370 There is one tricky point in the implementation: what visibility
 1371 do we give the type variables in a type family instance? Type family instances
 1372 only store type *variables*, not type variable *binders*, and only the latter
 1373 has visibility information. We opt to default the visibility of each of these
 1374 type variables to Specified because users can't ever instantiate these
 1375 variables manually, so the choice of visibility is only relevant to
 1376 pretty-printing. (This is why the `k` in `forall k (a :: k). ...` above is
 1377 printed the way it is, even though it wasn't written explicitly in the
 1378 original source code.)
 1379 
 1380 We adopt the same strategy for data family instances. Example:
 1381 
 1382   data family DF (a :: k)
 1383   data instance DF '[a, b] = DFList
 1384 
 1385 That data family instance is pretty-printed as:
 1386 
 1387   data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList
 1388 
 1389 This is despite that the representation tycon for this data instance (call it
 1390 $DF:List) actually has different visibilities for its binders.
 1391 However, the visibilities of these binders are utterly irrelevant to the
 1392 programmer, who cares only about the specificity of variables in `DF`'s type,
 1393 not $DF:List's type. Therefore, we opt to pretty-print all variables in data
 1394 family instances as Specified.
 1395 
 1396 Note [Printing promoted type constructors]
 1397 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1398 Consider this GHCi session (#14343)
 1399     > _ :: Proxy '[ 'True ]
 1400     error:
 1401       Found hole: _ :: Proxy '['True]
 1402 
 1403 This would be bad, because the '[' looks like a character literal.
 1404 Solution: in type-level lists and tuples, add a leading space
 1405 if the first type is itself promoted.  See pprSpaceIfPromotedTyCon.
 1406 -}
 1407 
 1408 
 1409 -------------------
 1410 
 1411 -- | Prefix a space if the given 'IfaceType' is a promoted 'TyCon'.
 1412 -- See Note [Printing promoted type constructors]
 1413 pprSpaceIfPromotedTyCon :: IfaceType -> SDoc -> SDoc
 1414 pprSpaceIfPromotedTyCon (IfaceTyConApp tyCon _)
 1415   = case ifaceTyConIsPromoted (ifaceTyConInfo tyCon) of
 1416       IsPromoted -> (space <>)
 1417       _ -> id
 1418 pprSpaceIfPromotedTyCon _
 1419   = id
 1420 
 1421 -- See equivalent function in "GHC.Core.TyCo.Rep"
 1422 pprIfaceTyList :: PprPrec -> IfaceType -> IfaceType -> SDoc
 1423 -- Given a type-level list (t1 ': t2), see if we can print
 1424 -- it in list notation [t1, ...].
 1425 -- Precondition: Opt_PrintExplicitKinds is off
 1426 pprIfaceTyList ctxt_prec ty1 ty2
 1427   = case gather ty2 of
 1428       (arg_tys, Nothing)
 1429         -> char '\'' <> brackets (pprSpaceIfPromotedTyCon ty1 (fsep
 1430                         (punctuate comma (map (ppr_ty topPrec) (ty1:arg_tys)))))
 1431       (arg_tys, Just tl)
 1432         -> maybeParen ctxt_prec funPrec $ hang (ppr_ty funPrec ty1)
 1433            2 (fsep [ colon <+> ppr_ty funPrec ty | ty <- arg_tys ++ [tl]])
 1434   where
 1435     gather :: IfaceType -> ([IfaceType], Maybe IfaceType)
 1436      -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
 1437      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
 1438     gather (IfaceTyConApp tc tys)
 1439       | tc `ifaceTyConHasKey` consDataConKey
 1440       , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
 1441       , isInvisibleArgFlag argf
 1442       , (args, tl) <- gather ty2
 1443       = (ty1:args, tl)
 1444       | tc `ifaceTyConHasKey` nilDataConKey
 1445       = ([], Nothing)
 1446     gather ty = ([], Just ty)
 1447 
 1448 pprIfaceTypeApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
 1449 pprIfaceTypeApp prec tc args = pprTyTcApp prec tc args
 1450 
 1451 pprTyTcApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
 1452 pprTyTcApp ctxt_prec tc tys =
 1453     sdocOption sdocPrintExplicitKinds $ \print_kinds ->
 1454     sdocOption sdocPrintTypeAbbreviations $ \print_type_abbreviations ->
 1455     getPprDebug $ \debug ->
 1456 
 1457     if | ifaceTyConName tc `hasKey` ipClassKey
 1458        , IA_Arg (IfaceLitTy (IfaceStrTyLit n))
 1459                 Required (IA_Arg ty Required IA_Nil) <- tys
 1460        -> maybeParen ctxt_prec funPrec
 1461          $ char '?' <> ftext n <> text "::" <> ppr_ty topPrec ty
 1462 
 1463        | IfaceTupleTyCon arity sort <- ifaceTyConSort info
 1464        , not debug
 1465        , arity == ifaceVisAppArgsLength tys
 1466        -> pprTuple ctxt_prec sort (ifaceTyConIsPromoted info) tys
 1467 
 1468        | IfaceSumTyCon arity <- ifaceTyConSort info
 1469        -> pprSum arity (ifaceTyConIsPromoted info) tys
 1470 
 1471        | tc `ifaceTyConHasKey` consDataConKey
 1472        , False <- print_kinds
 1473        , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
 1474        , isInvisibleArgFlag argf
 1475        -> pprIfaceTyList ctxt_prec ty1 ty2
 1476 
 1477        | isIfaceTyConAppLiftedTypeKind tc tys
 1478        , print_type_abbreviations  -- See Note [Printing type abbreviations]
 1479        -> ppr_kind_type ctxt_prec
 1480 
 1481        | tc `ifaceTyConHasKey` funTyConKey
 1482        , IA_Arg (IfaceTyConApp rep IA_Nil) Required args <- tys
 1483        , rep `ifaceTyConHasKey` manyDataConKey
 1484        , print_type_abbreviations  -- See Note [Printing type abbreviations]
 1485        -> pprIfacePrefixApp ctxt_prec (parens arrow) (map (ppr_app_arg appPrec) $
 1486           appArgsIfaceTypesArgFlags $ stripInvisArgs (PrintExplicitKinds print_kinds) args)
 1487           -- Use appArgsIfaceTypesArgFlags to print invisible arguments
 1488           -- correctly (#19310)
 1489 
 1490        | tc `ifaceTyConHasKey` errorMessageTypeErrorFamKey
 1491        , not debug
 1492          -- Suppress detail unless you _really_ want to see
 1493        -> text "(TypeError ...)"
 1494 
 1495        | Just doc <- ppr_equality ctxt_prec tc (appArgsIfaceTypes tys)
 1496        -> doc
 1497 
 1498        | otherwise
 1499        -> ppr_iface_tc_app ppr_app_arg ctxt_prec tc $
 1500           appArgsIfaceTypesArgFlags $ stripInvisArgs (PrintExplicitKinds print_kinds) tys
 1501   where
 1502     info = ifaceTyConInfo tc
 1503 
 1504 ppr_kind_type :: PprPrec -> SDoc
 1505 ppr_kind_type ctxt_prec = sdocOption sdocStarIsType $ \case
 1506    False -> text "Type"
 1507    True  -> maybeParen ctxt_prec starPrec $
 1508               unicodeSyntax (char '★') (char '*')
 1509 
 1510 -- | Pretty-print a type-level equality.
 1511 -- Returns (Just doc) if the argument is a /saturated/ application
 1512 -- of   eqTyCon          (~)
 1513 --      eqPrimTyCon      (~#)
 1514 --      eqReprPrimTyCon  (~R#)
 1515 --      heqTyCon         (~~)
 1516 --
 1517 -- See Note [Equality predicates in IfaceType]
 1518 -- and Note [The equality types story] in GHC.Builtin.Types.Prim
 1519 ppr_equality :: PprPrec -> IfaceTyCon -> [IfaceType] -> Maybe SDoc
 1520 ppr_equality ctxt_prec tc args
 1521   | hetero_eq_tc
 1522   , [k1, k2, t1, t2] <- args
 1523   = Just $ print_equality (k1, k2, t1, t2)
 1524 
 1525   | hom_eq_tc
 1526   , [k, t1, t2] <- args
 1527   = Just $ print_equality (k, k, t1, t2)
 1528 
 1529   | otherwise
 1530   = Nothing
 1531   where
 1532     homogeneous = tc_name `hasKey` eqTyConKey -- (~)
 1533                || hetero_tc_used_homogeneously
 1534       where
 1535         hetero_tc_used_homogeneously
 1536           = case ifaceTyConSort $ ifaceTyConInfo tc of
 1537                           IfaceEqualityTyCon -> True
 1538                           _other             -> False
 1539              -- True <=> a heterogeneous equality whose arguments
 1540              --          are (in this case) of the same kind
 1541 
 1542     tc_name = ifaceTyConName tc
 1543     pp = ppr_ty
 1544     hom_eq_tc = tc_name `hasKey` eqTyConKey            -- (~)
 1545     hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey     -- (~#)
 1546                 || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
 1547                 || tc_name `hasKey` heqTyConKey        -- (~~)
 1548     nominal_eq_tc = tc_name `hasKey` heqTyConKey       -- (~~)
 1549                  || tc_name `hasKey` eqPrimTyConKey    -- (~#)
 1550     print_equality args =
 1551         sdocOption sdocPrintExplicitKinds $ \print_kinds ->
 1552         sdocOption sdocPrintEqualityRelations $ \print_eqs ->
 1553         getPprStyle      $ \style  ->
 1554         getPprDebug      $ \debug  ->
 1555         print_equality' args print_kinds
 1556           (print_eqs || dumpStyle style || debug)
 1557 
 1558     print_equality' (ki1, ki2, ty1, ty2) print_kinds print_eqs
 1559       | -- If -fprint-equality-relations is on, just print the original TyCon
 1560         print_eqs
 1561       = ppr_infix_eq (ppr tc)
 1562 
 1563       | -- Homogeneous use of heterogeneous equality (ty1 ~~ ty2)
 1564         --                 or unlifted equality      (ty1 ~# ty2)
 1565         nominal_eq_tc, homogeneous
 1566       = ppr_infix_eq (text "~")
 1567 
 1568       | -- Heterogeneous use of unlifted equality (ty1 ~# ty2)
 1569         not homogeneous
 1570       = ppr_infix_eq (ppr heqTyCon)
 1571 
 1572       | -- Homogeneous use of representational unlifted equality (ty1 ~R# ty2)
 1573         tc_name `hasKey` eqReprPrimTyConKey, homogeneous
 1574       = let ki | print_kinds = [pp appPrec ki1]
 1575                | otherwise   = []
 1576         in pprIfacePrefixApp ctxt_prec (ppr coercibleTyCon)
 1577                             (ki ++ [pp appPrec ty1, pp appPrec ty2])
 1578 
 1579         -- The other cases work as you'd expect
 1580       | otherwise
 1581       = ppr_infix_eq (ppr tc)
 1582       where
 1583         ppr_infix_eq :: SDoc -> SDoc
 1584         ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op
 1585                                (pp_ty_ki ty1 ki1) (pp_ty_ki ty2 ki2)
 1586           where
 1587             pp_ty_ki ty ki
 1588               | print_kinds
 1589               = parens (pp topPrec ty <+> dcolon <+> pp opPrec ki)
 1590               | otherwise
 1591               = pp opPrec ty
 1592 
 1593 
 1594 pprIfaceCoTcApp :: PprPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
 1595 pprIfaceCoTcApp ctxt_prec tc tys =
 1596   ppr_iface_tc_app (\prec (co, _) -> ppr_co prec co) ctxt_prec tc
 1597     (map (, Required) tys)
 1598     -- We are trying to re-use ppr_iface_tc_app here, which requires its
 1599     -- arguments to be accompanied by visibilities. But visibility is
 1600     -- irrelevant when printing coercions, so just default everything to
 1601     -- Required.
 1602 
 1603 -- | Pretty-prints an application of a type constructor to some arguments
 1604 -- (whose visibilities are known). This is polymorphic (over @a@) since we use
 1605 -- this function to pretty-print two different things:
 1606 --
 1607 -- 1. Types (from `pprTyTcApp'`)
 1608 --
 1609 -- 2. Coercions (from 'pprIfaceCoTcApp')
 1610 ppr_iface_tc_app :: (PprPrec -> (a, ArgFlag) -> SDoc)
 1611                  -> PprPrec -> IfaceTyCon -> [(a, ArgFlag)] -> SDoc
 1612 ppr_iface_tc_app pp _ tc [ty]
 1613   | tc `ifaceTyConHasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp topPrec ty)
 1614 
 1615 ppr_iface_tc_app pp ctxt_prec tc tys
 1616   | tc `ifaceTyConHasKey` liftedTypeKindTyConKey
 1617   = ppr_kind_type ctxt_prec
 1618 
 1619   | not (isSymOcc (nameOccName (ifaceTyConName tc)))
 1620   = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp appPrec) tys)
 1621 
 1622   | [ ty1@(_, Required)
 1623     , ty2@(_, Required) ] <- tys
 1624       -- Infix, two visible arguments (we know nothing of precedence though).
 1625       -- Don't apply this special case if one of the arguments is invisible,
 1626       -- lest we print something like (@LiftedRep -> @LiftedRep) (#15941).
 1627   = pprIfaceInfixApp ctxt_prec (ppr tc)
 1628                      (pp opPrec ty1) (pp opPrec ty2)
 1629 
 1630   | otherwise
 1631   = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp appPrec) tys)
 1632 
 1633 pprSum :: Arity -> PromotionFlag -> IfaceAppArgs -> SDoc
 1634 pprSum _arity is_promoted args
 1635   =   -- drop the RuntimeRep vars.
 1636       -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
 1637     let tys   = appArgsIfaceTypes args
 1638         args' = drop (length tys `div` 2) tys
 1639     in pprPromotionQuoteI is_promoted
 1640        <> sumParens (pprWithBars (ppr_ty topPrec) args')
 1641 
 1642 pprTuple :: PprPrec -> TupleSort -> PromotionFlag -> IfaceAppArgs -> SDoc
 1643 pprTuple ctxt_prec sort promoted args =
 1644   case promoted of
 1645     IsPromoted
 1646       -> let tys = appArgsIfaceTypes args
 1647              args' = drop (length tys `div` 2) tys
 1648              spaceIfPromoted = case args' of
 1649                arg0:_ -> pprSpaceIfPromotedTyCon arg0
 1650                _ -> id
 1651          in ppr_tuple_app args' $
 1652             pprPromotionQuoteI IsPromoted <>
 1653             tupleParens sort (spaceIfPromoted (pprWithCommas pprIfaceType args'))
 1654 
 1655     NotPromoted
 1656       |  ConstraintTuple <- sort
 1657       ,  IA_Nil <- args
 1658       -> maybeParen ctxt_prec sigPrec $
 1659          text "() :: Constraint"
 1660 
 1661       | otherwise
 1662       ->   -- drop the RuntimeRep vars.
 1663            -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
 1664          let tys   = appArgsIfaceTypes args
 1665              args' = case sort of
 1666                        UnboxedTuple -> drop (length tys `div` 2) tys
 1667                        _            -> tys
 1668          in
 1669          ppr_tuple_app args' $
 1670          pprPromotionQuoteI promoted <>
 1671          tupleParens sort (pprWithCommas pprIfaceType args')
 1672   where
 1673     ppr_tuple_app :: [IfaceType] -> SDoc -> SDoc
 1674     ppr_tuple_app args_wo_runtime_reps ppr_args_w_parens
 1675         -- Special-case unary boxed tuples so that they are pretty-printed as
 1676         -- `Solo x`, not `(x)`
 1677       | [_] <- args_wo_runtime_reps
 1678       , BoxedTuple <- sort
 1679       = let unit_tc_info = mkIfaceTyConInfo promoted IfaceNormalTyCon
 1680             unit_tc = IfaceTyCon (tupleTyConName sort 1) unit_tc_info in
 1681         pprPrecIfaceType ctxt_prec $ IfaceTyConApp unit_tc args
 1682       | otherwise
 1683       = ppr_args_w_parens
 1684 
 1685 pprIfaceTyLit :: IfaceTyLit -> SDoc
 1686 pprIfaceTyLit (IfaceNumTyLit n) = integer n
 1687 pprIfaceTyLit (IfaceStrTyLit n) = text (show n)
 1688 pprIfaceTyLit (IfaceCharTyLit c) = text (show c)
 1689 
 1690 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc
 1691 pprIfaceCoercion = ppr_co topPrec
 1692 pprParendIfaceCoercion = ppr_co appPrec
 1693 
 1694 ppr_co :: PprPrec -> IfaceCoercion -> SDoc
 1695 ppr_co _         (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal
 1696 ppr_co _         (IfaceGReflCo r ty IfaceMRefl)
 1697   = angleBrackets (ppr ty) <> ppr_role r
 1698 ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co))
 1699   = ppr_special_co ctxt_prec
 1700     (text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co]
 1701 ppr_co ctxt_prec (IfaceFunCo r cow co1 co2)
 1702   = maybeParen ctxt_prec funPrec $
 1703     sep (ppr_co funPrec co1 : ppr_fun_tail cow co2)
 1704   where
 1705     ppr_fun_tail cow' (IfaceFunCo r cow co1 co2)
 1706       = (coercionArrow cow' <> ppr_role r <+> ppr_co funPrec co1) : ppr_fun_tail cow co2
 1707     ppr_fun_tail cow' other_co
 1708       = [coercionArrow cow' <> ppr_role r <+> pprIfaceCoercion other_co]
 1709     coercionArrow w = mulArrow (ppr_co topPrec w)
 1710 
 1711 ppr_co _         (IfaceTyConAppCo r tc cos)
 1712   = parens (pprIfaceCoTcApp topPrec tc cos) <> ppr_role r
 1713 ppr_co ctxt_prec (IfaceAppCo co1 co2)
 1714   = maybeParen ctxt_prec appPrec $
 1715     ppr_co funPrec co1 <+> pprParendIfaceCoercion co2
 1716 ppr_co ctxt_prec co@(IfaceForAllCo {})
 1717   = maybeParen ctxt_prec funPrec $
 1718     pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co)
 1719   where
 1720     (tvs, inner_co) = split_co co
 1721 
 1722     split_co (IfaceForAllCo (IfaceTvBndr (name, _)) kind_co co')
 1723       = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
 1724     split_co (IfaceForAllCo (IfaceIdBndr (_, name, _)) kind_co co')
 1725       = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
 1726     split_co co' = ([], co')
 1727 
 1728 -- Why these three? See Note [TcTyVars in IfaceType]
 1729 ppr_co _ (IfaceFreeCoVar covar) = ppr covar
 1730 ppr_co _ (IfaceCoVarCo covar)   = ppr covar
 1731 ppr_co _ (IfaceHoleCo covar)    = braces (ppr covar)
 1732 
 1733 ppr_co _ (IfaceUnivCo prov role ty1 ty2)
 1734   = text "Univ" <> (parens $
 1735       sep [ ppr role <+> pprIfaceUnivCoProv prov
 1736           , dcolon <+>  ppr ty1 <> comma <+> ppr ty2 ])
 1737 
 1738 ppr_co ctxt_prec (IfaceInstCo co ty)
 1739   = maybeParen ctxt_prec appPrec $
 1740     text "Inst" <+> pprParendIfaceCoercion co
 1741                         <+> pprParendIfaceCoercion ty
 1742 
 1743 ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
 1744   = maybeParen ctxt_prec appPrec $ ppr tc <+> parens (interpp'SP cos)
 1745 
 1746 ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
 1747   = ppr_special_co ctxt_prec (ppr n <> brackets (ppr i)) cos
 1748 ppr_co ctxt_prec (IfaceSymCo co)
 1749   = ppr_special_co ctxt_prec (text "Sym") [co]
 1750 ppr_co ctxt_prec (IfaceTransCo co1 co2)
 1751     -- chain nested TransCo
 1752   = let ppr_trans (IfaceTransCo c1 c2) = semi <+> ppr_co topPrec c1 : ppr_trans c2
 1753         ppr_trans c                    = [semi <+> ppr_co opPrec c]
 1754     in maybeParen ctxt_prec opPrec $
 1755         vcat (ppr_co topPrec co1 : ppr_trans co2)
 1756 ppr_co ctxt_prec (IfaceNthCo d co)
 1757   = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
 1758 ppr_co ctxt_prec (IfaceLRCo lr co)
 1759   = ppr_special_co ctxt_prec (ppr lr) [co]
 1760 ppr_co ctxt_prec (IfaceSubCo co)
 1761   = ppr_special_co ctxt_prec (text "Sub") [co]
 1762 ppr_co ctxt_prec (IfaceKindCo co)
 1763   = ppr_special_co ctxt_prec (text "Kind") [co]
 1764 
 1765 ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
 1766 ppr_special_co ctxt_prec doc cos
 1767   = maybeParen ctxt_prec appPrec
 1768                (sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
 1769 
 1770 ppr_role :: Role -> SDoc
 1771 ppr_role r = underscore <> pp_role
 1772   where pp_role = case r of
 1773                     Nominal          -> char 'N'
 1774                     Representational -> char 'R'
 1775                     Phantom          -> char 'P'
 1776 
 1777 ------------------
 1778 pprIfaceUnivCoProv :: IfaceUnivCoProv -> SDoc
 1779 pprIfaceUnivCoProv (IfacePhantomProv co)
 1780   = text "phantom" <+> pprParendIfaceCoercion co
 1781 pprIfaceUnivCoProv (IfaceProofIrrelProv co)
 1782   = text "irrel" <+> pprParendIfaceCoercion co
 1783 pprIfaceUnivCoProv (IfacePluginProv s)
 1784   = text "plugin" <+> doubleQuotes (text s)
 1785 pprIfaceUnivCoProv (IfaceCorePrepProv _)
 1786   = text "CorePrep"
 1787 
 1788 -------------------
 1789 instance Outputable IfaceTyCon where
 1790   ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
 1791 
 1792 instance Outputable IfaceTyConInfo where
 1793   ppr (IfaceTyConInfo { ifaceTyConIsPromoted = prom
 1794                       , ifaceTyConSort       = sort })
 1795     = angleBrackets $ ppr prom <> comma <+> ppr sort
 1796 
 1797 pprPromotionQuote :: IfaceTyCon -> SDoc
 1798 pprPromotionQuote tc =
 1799     pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
 1800 
 1801 pprPromotionQuoteI  :: PromotionFlag -> SDoc
 1802 pprPromotionQuoteI NotPromoted = empty
 1803 pprPromotionQuoteI IsPromoted    = char '\''
 1804 
 1805 instance Outputable IfaceCoercion where
 1806   ppr = pprIfaceCoercion
 1807 
 1808 instance Binary IfaceTyCon where
 1809    put_ bh (IfaceTyCon n i) = put_ bh n >> put_ bh i
 1810 
 1811    get bh = do n <- get bh
 1812                i <- get bh
 1813                return (IfaceTyCon n i)
 1814 
 1815 instance Binary IfaceTyConSort where
 1816    put_ bh IfaceNormalTyCon             = putByte bh 0
 1817    put_ bh (IfaceTupleTyCon arity sort) = putByte bh 1 >> put_ bh arity >> put_ bh sort
 1818    put_ bh (IfaceSumTyCon arity)        = putByte bh 2 >> put_ bh arity
 1819    put_ bh IfaceEqualityTyCon           = putByte bh 3
 1820 
 1821    get bh = do
 1822        n <- getByte bh
 1823        case n of
 1824          0 -> return IfaceNormalTyCon
 1825          1 -> IfaceTupleTyCon <$> get bh <*> get bh
 1826          2 -> IfaceSumTyCon <$> get bh
 1827          _ -> return IfaceEqualityTyCon
 1828 
 1829 instance Binary IfaceTyConInfo where
 1830    put_ bh (IfaceTyConInfo i s) = put_ bh i >> put_ bh s
 1831 
 1832    get bh = mkIfaceTyConInfo <$> get bh <*> get bh
 1833 
 1834 instance Outputable IfaceTyLit where
 1835   ppr = pprIfaceTyLit
 1836 
 1837 instance Binary IfaceTyLit where
 1838   put_ bh (IfaceNumTyLit n)   = putByte bh 1 >> put_ bh n
 1839   put_ bh (IfaceStrTyLit n)   = putByte bh 2 >> put_ bh n
 1840   put_ bh (IfaceCharTyLit n)  = putByte bh 3 >> put_ bh n
 1841 
 1842   get bh =
 1843     do tag <- getByte bh
 1844        case tag of
 1845          1 -> do { n <- get bh
 1846                  ; return (IfaceNumTyLit n) }
 1847          2 -> do { n <- get bh
 1848                  ; return (IfaceStrTyLit n) }
 1849          3 -> do { n <- get bh
 1850                  ; return (IfaceCharTyLit n) }
 1851          _ -> panic ("get IfaceTyLit " ++ show tag)
 1852 
 1853 instance Binary IfaceAppArgs where
 1854   put_ bh tk =
 1855     case tk of
 1856       IA_Arg t a ts -> putByte bh 0 >> put_ bh t >> put_ bh a >> put_ bh ts
 1857       IA_Nil        -> putByte bh 1
 1858 
 1859   get bh =
 1860     do c <- getByte bh
 1861        case c of
 1862          0 -> do
 1863            t  <- get bh
 1864            a  <- get bh
 1865            ts <- get bh
 1866            return $! IA_Arg t a ts
 1867          1 -> return IA_Nil
 1868          _ -> panic ("get IfaceAppArgs " ++ show c)
 1869 
 1870 -------------------
 1871 
 1872 -- Some notes about printing contexts
 1873 --
 1874 -- In the event that we are printing a singleton context (e.g. @Eq a@) we can
 1875 -- omit parentheses. However, we must take care to set the precedence correctly
 1876 -- to opPrec, since something like @a :~: b@ must be parenthesized (see
 1877 -- #9658).
 1878 --
 1879 -- When printing a larger context we use 'fsep' instead of 'sep' so that
 1880 -- the context doesn't get displayed as a giant column. Rather than,
 1881 --  instance (Eq a,
 1882 --            Eq b,
 1883 --            Eq c,
 1884 --            Eq d,
 1885 --            Eq e,
 1886 --            Eq f,
 1887 --            Eq g,
 1888 --            Eq h,
 1889 --            Eq i,
 1890 --            Eq j,
 1891 --            Eq k,
 1892 --            Eq l) =>
 1893 --           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
 1894 --
 1895 -- we want
 1896 --
 1897 --  instance (Eq a, Eq b, Eq c, Eq d, Eq e, Eq f, Eq g, Eq h, Eq i,
 1898 --            Eq j, Eq k, Eq l) =>
 1899 --           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
 1900 
 1901 
 1902 
 1903 -- | Prints "(C a, D b) =>", including the arrow.
 1904 -- Used when we want to print a context in a type, so we
 1905 -- use 'funPrec' to decide whether to parenthesise a singleton
 1906 -- predicate; e.g.   Num a => a -> a
 1907 pprIfaceContextArr :: [IfacePredType] -> SDoc
 1908 pprIfaceContextArr []     = empty
 1909 pprIfaceContextArr [pred] = ppr_ty funPrec pred <+> darrow
 1910 pprIfaceContextArr preds  = ppr_parend_preds preds <+> darrow
 1911 
 1912 -- | Prints a context or @()@ if empty
 1913 -- You give it the context precedence
 1914 pprIfaceContext :: PprPrec -> [IfacePredType] -> SDoc
 1915 pprIfaceContext _    []     = text "()"
 1916 pprIfaceContext prec [pred] = ppr_ty prec pred
 1917 pprIfaceContext _    preds  = ppr_parend_preds preds
 1918 
 1919 ppr_parend_preds :: [IfacePredType] -> SDoc
 1920 ppr_parend_preds preds = parens (fsep (punctuate comma (map ppr preds)))
 1921 
 1922 instance Binary IfaceType where
 1923     put_ _ (IfaceFreeTyVar tv)
 1924        = pprPanic "Can't serialise IfaceFreeTyVar" (ppr tv)
 1925 
 1926     put_ bh (IfaceForAllTy aa ab) = do
 1927             putByte bh 0
 1928             put_ bh aa
 1929             put_ bh ab
 1930     put_ bh (IfaceTyVar ad) = do
 1931             putByte bh 1
 1932             put_ bh ad
 1933     put_ bh (IfaceAppTy ae af) = do
 1934             putByte bh 2
 1935             put_ bh ae
 1936             put_ bh af
 1937     put_ bh (IfaceFunTy af aw ag ah) = do
 1938             putByte bh 3
 1939             put_ bh af
 1940             put_ bh aw
 1941             put_ bh ag
 1942             put_ bh ah
 1943     put_ bh (IfaceTyConApp tc tys)
 1944       = do { putByte bh 5; put_ bh tc; put_ bh tys }
 1945     put_ bh (IfaceCastTy a b)
 1946       = do { putByte bh 6; put_ bh a; put_ bh b }
 1947     put_ bh (IfaceCoercionTy a)
 1948       = do { putByte bh 7; put_ bh a }
 1949     put_ bh (IfaceTupleTy s i tys)
 1950       = do { putByte bh 8; put_ bh s; put_ bh i; put_ bh tys }
 1951     put_ bh (IfaceLitTy n)
 1952       = do { putByte bh 9; put_ bh n }
 1953 
 1954     get bh = do
 1955             h <- getByte bh
 1956             case h of
 1957               0 -> do aa <- get bh
 1958                       ab <- get bh
 1959                       return (IfaceForAllTy aa ab)
 1960               1 -> do ad <- get bh
 1961                       return (IfaceTyVar ad)
 1962               2 -> do ae <- get bh
 1963                       af <- get bh
 1964                       return (IfaceAppTy ae af)
 1965               3 -> do af <- get bh
 1966                       aw <- get bh
 1967                       ag <- get bh
 1968                       ah <- get bh
 1969                       return (IfaceFunTy af aw ag ah)
 1970               5 -> do { tc <- get bh; tys <- get bh
 1971                       ; return (IfaceTyConApp tc tys) }
 1972               6 -> do { a <- get bh; b <- get bh
 1973                       ; return (IfaceCastTy a b) }
 1974               7 -> do { a <- get bh
 1975                       ; return (IfaceCoercionTy a) }
 1976 
 1977               8 -> do { s <- get bh; i <- get bh; tys <- get bh
 1978                       ; return (IfaceTupleTy s i tys) }
 1979               _  -> do n <- get bh
 1980                        return (IfaceLitTy n)
 1981 
 1982 instance Binary IfaceMCoercion where
 1983   put_ bh IfaceMRefl =
 1984           putByte bh 1
 1985   put_ bh (IfaceMCo co) = do
 1986           putByte bh 2
 1987           put_ bh co
 1988 
 1989   get bh = do
 1990     tag <- getByte bh
 1991     case tag of
 1992          1 -> return IfaceMRefl
 1993          2 -> do a <- get bh
 1994                  return $ IfaceMCo a
 1995          _ -> panic ("get IfaceMCoercion " ++ show tag)
 1996 
 1997 instance Binary IfaceCoercion where
 1998   put_ bh (IfaceReflCo a) = do
 1999           putByte bh 1
 2000           put_ bh a
 2001   put_ bh (IfaceGReflCo a b c) = do
 2002           putByte bh 2
 2003           put_ bh a
 2004           put_ bh b
 2005           put_ bh c
 2006   put_ bh (IfaceFunCo a w b c) = do
 2007           putByte bh 3
 2008           put_ bh a
 2009           put_ bh w
 2010           put_ bh b
 2011           put_ bh c
 2012   put_ bh (IfaceTyConAppCo a b c) = do
 2013           putByte bh 4
 2014           put_ bh a
 2015           put_ bh b
 2016           put_ bh c
 2017   put_ bh (IfaceAppCo a b) = do
 2018           putByte bh 5
 2019           put_ bh a
 2020           put_ bh b
 2021   put_ bh (IfaceForAllCo a b c) = do
 2022           putByte bh 6
 2023           put_ bh a
 2024           put_ bh b
 2025           put_ bh c
 2026   put_ bh (IfaceCoVarCo a) = do
 2027           putByte bh 7
 2028           put_ bh a
 2029   put_ bh (IfaceAxiomInstCo a b c) = do
 2030           putByte bh 8
 2031           put_ bh a
 2032           put_ bh b
 2033           put_ bh c
 2034   put_ bh (IfaceUnivCo a b c d) = do
 2035           putByte bh 9
 2036           put_ bh a
 2037           put_ bh b
 2038           put_ bh c
 2039           put_ bh d
 2040   put_ bh (IfaceSymCo a) = do
 2041           putByte bh 10
 2042           put_ bh a
 2043   put_ bh (IfaceTransCo a b) = do
 2044           putByte bh 11
 2045           put_ bh a
 2046           put_ bh b
 2047   put_ bh (IfaceNthCo a b) = do
 2048           putByte bh 12
 2049           put_ bh a
 2050           put_ bh b
 2051   put_ bh (IfaceLRCo a b) = do
 2052           putByte bh 13
 2053           put_ bh a
 2054           put_ bh b
 2055   put_ bh (IfaceInstCo a b) = do
 2056           putByte bh 14
 2057           put_ bh a
 2058           put_ bh b
 2059   put_ bh (IfaceKindCo a) = do
 2060           putByte bh 15
 2061           put_ bh a
 2062   put_ bh (IfaceSubCo a) = do
 2063           putByte bh 16
 2064           put_ bh a
 2065   put_ bh (IfaceAxiomRuleCo a b) = do
 2066           putByte bh 17
 2067           put_ bh a
 2068           put_ bh b
 2069   put_ _ (IfaceFreeCoVar cv)
 2070        = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
 2071   put_ _  (IfaceHoleCo cv)
 2072        = pprPanic "Can't serialise IfaceHoleCo" (ppr cv)
 2073           -- See Note [Holes in IfaceCoercion]
 2074 
 2075   get bh = do
 2076       tag <- getByte bh
 2077       case tag of
 2078            1 -> do a <- get bh
 2079                    return $ IfaceReflCo a
 2080            2 -> do a <- get bh
 2081                    b <- get bh
 2082                    c <- get bh
 2083                    return $ IfaceGReflCo a b c
 2084            3 -> do a <- get bh
 2085                    w <- get bh
 2086                    b <- get bh
 2087                    c <- get bh
 2088                    return $ IfaceFunCo a w b c
 2089            4 -> do a <- get bh
 2090                    b <- get bh
 2091                    c <- get bh
 2092                    return $ IfaceTyConAppCo a b c
 2093            5 -> do a <- get bh
 2094                    b <- get bh
 2095                    return $ IfaceAppCo a b
 2096            6 -> do a <- get bh
 2097                    b <- get bh
 2098                    c <- get bh
 2099                    return $ IfaceForAllCo a b c
 2100            7 -> do a <- get bh
 2101                    return $ IfaceCoVarCo a
 2102            8 -> do a <- get bh
 2103                    b <- get bh
 2104                    c <- get bh
 2105                    return $ IfaceAxiomInstCo a b c
 2106            9 -> do a <- get bh
 2107                    b <- get bh
 2108                    c <- get bh
 2109                    d <- get bh
 2110                    return $ IfaceUnivCo a b c d
 2111            10-> do a <- get bh
 2112                    return $ IfaceSymCo a
 2113            11-> do a <- get bh
 2114                    b <- get bh
 2115                    return $ IfaceTransCo a b
 2116            12-> do a <- get bh
 2117                    b <- get bh
 2118                    return $ IfaceNthCo a b
 2119            13-> do a <- get bh
 2120                    b <- get bh
 2121                    return $ IfaceLRCo a b
 2122            14-> do a <- get bh
 2123                    b <- get bh
 2124                    return $ IfaceInstCo a b
 2125            15-> do a <- get bh
 2126                    return $ IfaceKindCo a
 2127            16-> do a <- get bh
 2128                    return $ IfaceSubCo a
 2129            17-> do a <- get bh
 2130                    b <- get bh
 2131                    return $ IfaceAxiomRuleCo a b
 2132            _ -> panic ("get IfaceCoercion " ++ show tag)
 2133 
 2134 instance Binary IfaceUnivCoProv where
 2135   put_ bh (IfacePhantomProv a) = do
 2136           putByte bh 1
 2137           put_ bh a
 2138   put_ bh (IfaceProofIrrelProv a) = do
 2139           putByte bh 2
 2140           put_ bh a
 2141   put_ bh (IfacePluginProv a) = do
 2142           putByte bh 3
 2143           put_ bh a
 2144   put_ bh (IfaceCorePrepProv a) = do
 2145           putByte bh 4
 2146           put_ bh a
 2147 
 2148   get bh = do
 2149       tag <- getByte bh
 2150       case tag of
 2151            1 -> do a <- get bh
 2152                    return $ IfacePhantomProv a
 2153            2 -> do a <- get bh
 2154                    return $ IfaceProofIrrelProv a
 2155            3 -> do a <- get bh
 2156                    return $ IfacePluginProv a
 2157            4 -> do a <- get bh
 2158                    return (IfaceCorePrepProv a)
 2159            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 2160 
 2161 
 2162 instance Binary (DefMethSpec IfaceType) where
 2163     put_ bh VanillaDM     = putByte bh 0
 2164     put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
 2165     get bh = do
 2166             h <- getByte bh
 2167             case h of
 2168               0 -> return VanillaDM
 2169               _ -> do { t <- get bh; return (GenericDM t) }
 2170 
 2171 instance NFData IfaceType where
 2172   rnf = \case
 2173     IfaceFreeTyVar f1 -> f1 `seq` ()
 2174     IfaceTyVar f1 -> rnf f1
 2175     IfaceLitTy f1 -> rnf f1
 2176     IfaceAppTy f1 f2 -> rnf f1 `seq` rnf f2
 2177     IfaceFunTy f1 f2 f3 f4 -> f1 `seq` rnf f2 `seq` rnf f3 `seq` rnf f4
 2178     IfaceForAllTy f1 f2 -> f1 `seq` rnf f2
 2179     IfaceTyConApp f1 f2 -> rnf f1 `seq` rnf f2
 2180     IfaceCastTy f1 f2 -> rnf f1 `seq` rnf f2
 2181     IfaceCoercionTy f1 -> rnf f1
 2182     IfaceTupleTy f1 f2 f3 -> f1 `seq` f2 `seq` rnf f3
 2183 
 2184 instance NFData IfaceTyLit where
 2185   rnf = \case
 2186     IfaceNumTyLit f1 -> rnf f1
 2187     IfaceStrTyLit f1 -> rnf f1
 2188     IfaceCharTyLit f1 -> rnf f1
 2189 
 2190 instance NFData IfaceCoercion where
 2191   rnf = \case
 2192     IfaceReflCo f1 -> rnf f1
 2193     IfaceGReflCo f1 f2 f3 -> f1 `seq` rnf f2 `seq` rnf f3
 2194     IfaceFunCo f1 f2 f3 f4 -> f1 `seq` rnf f2 `seq` rnf f3 `seq` rnf f4
 2195     IfaceTyConAppCo f1 f2 f3 -> f1 `seq` rnf f2 `seq` rnf f3
 2196     IfaceAppCo f1 f2 -> rnf f1 `seq` rnf f2
 2197     IfaceForAllCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
 2198     IfaceCoVarCo f1 -> rnf f1
 2199     IfaceAxiomInstCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
 2200     IfaceAxiomRuleCo f1 f2 -> rnf f1 `seq` rnf f2
 2201     IfaceUnivCo f1 f2 f3 f4 -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4
 2202     IfaceSymCo f1 -> rnf f1
 2203     IfaceTransCo f1 f2 -> rnf f1 `seq` rnf f2
 2204     IfaceNthCo f1 f2 -> rnf f1 `seq` rnf f2
 2205     IfaceLRCo f1 f2 -> f1 `seq` rnf f2
 2206     IfaceInstCo f1 f2 -> rnf f1 `seq` rnf f2
 2207     IfaceKindCo f1 -> rnf f1
 2208     IfaceSubCo f1 -> rnf f1
 2209     IfaceFreeCoVar f1 -> f1 `seq` ()
 2210     IfaceHoleCo f1 -> f1 `seq` ()
 2211 
 2212 instance NFData IfaceUnivCoProv where
 2213   rnf x = seq x ()
 2214 
 2215 instance NFData IfaceMCoercion where
 2216   rnf x = seq x ()
 2217 
 2218 instance NFData IfaceOneShot where
 2219   rnf x = seq x ()
 2220 
 2221 instance NFData IfaceTyConSort where
 2222   rnf = \case
 2223     IfaceNormalTyCon -> ()
 2224     IfaceTupleTyCon arity sort -> rnf arity `seq` sort `seq` ()
 2225     IfaceSumTyCon arity -> rnf arity
 2226     IfaceEqualityTyCon -> ()
 2227 
 2228 instance NFData IfaceTyConInfo where
 2229   rnf (IfaceTyConInfo f s) = f `seq` rnf s
 2230 
 2231 instance NFData IfaceTyCon where
 2232   rnf (IfaceTyCon nm info) = rnf nm `seq` rnf info
 2233 
 2234 instance NFData IfaceBndr where
 2235   rnf = \case
 2236     IfaceIdBndr id_bndr -> rnf id_bndr
 2237     IfaceTvBndr tv_bndr -> rnf tv_bndr
 2238 
 2239 instance NFData IfaceAppArgs where
 2240   rnf = \case
 2241     IA_Nil -> ()
 2242     IA_Arg f1 f2 f3 -> rnf f1 `seq` f2 `seq` rnf f3