never executed always true always false
    1 {-
    2 (c) The University of Glasgow 2006
    3 (c) The GRASP/AQUA Project, Glasgow University, 1998
    4 Type and Coercion - friends' interface
    5 -}
    6 
    7 
    8 {-# LANGUAGE BangPatterns #-}
    9 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
   10 
   11 -- | Substitution into types and coercions.
   12 module GHC.Core.TyCo.Subst
   13   (
   14         -- * Substitutions
   15         TCvSubst(..), TvSubstEnv, CvSubstEnv,
   16         emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
   17         emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
   18         mkTCvSubst, mkTvSubst, mkCvSubst,
   19         getTvSubstEnv,
   20         getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
   21         isInScope, elemTCvSubst, notElemTCvSubst,
   22         setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
   23         extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
   24         extendTCvSubst, extendTCvSubstWithClone,
   25         extendCvSubst, extendCvSubstWithClone,
   26         extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
   27         extendTvSubstList, extendTvSubstAndInScope,
   28         extendTCvSubstList,
   29         unionTCvSubst, zipTyEnv, zipCoEnv,
   30         zipTvSubst, zipCvSubst,
   31         zipTCvSubst,
   32         mkTvSubstPrs,
   33 
   34         substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
   35         substCoWith,
   36         substTy, substTyAddInScope, substScaledTy,
   37         substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked,
   38         substTyWithUnchecked, substScaledTyUnchecked,
   39         substCoUnchecked, substCoWithUnchecked,
   40         substTyWithInScope,
   41         substTys, substScaledTys, substTheta,
   42         lookupTyVar,
   43         substCo, substCos, substCoVar, substCoVars, lookupCoVar,
   44         cloneTyVarBndr, cloneTyVarBndrs,
   45         substVarBndr, substVarBndrs,
   46         substTyVarBndr, substTyVarBndrs,
   47         substCoVarBndr,
   48         substTyVar, substTyVars, substTyCoVars,
   49         substTyCoBndr,
   50         substForAllCoBndr,
   51         substVarBndrUsing, substForAllCoBndrUsing,
   52         checkValidSubst, isValidTCvSubst,
   53   ) where
   54 
   55 import GHC.Prelude
   56 
   57 import {-# SOURCE #-} GHC.Core.Type
   58    ( mkCastTy, mkAppTy, isCoercionTy, mkTyConApp )
   59 import {-# SOURCE #-} GHC.Core.Coercion
   60    ( mkCoVarCo, mkKindCo, mkNthCo, mkTransCo
   61    , mkNomReflCo, mkSubCo, mkSymCo
   62    , mkFunCo, mkForAllCo, mkUnivCo
   63    , mkAxiomInstCo, mkAppCo, mkGReflCo
   64    , mkInstCo, mkLRCo, mkTyConAppCo
   65    , mkCoercionType
   66    , coercionKind, coercionLKind, coVarKindsTypesRole )
   67 import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
   68 
   69 import GHC.Core.TyCo.Rep
   70 import GHC.Core.TyCo.FVs
   71 
   72 import GHC.Types.Var
   73 import GHC.Types.Var.Set
   74 import GHC.Types.Var.Env
   75 
   76 import GHC.Data.Pair
   77 import GHC.Utils.Constants (debugIsOn)
   78 import GHC.Utils.Misc
   79 import GHC.Types.Unique.Supply
   80 import GHC.Types.Unique
   81 import GHC.Types.Unique.FM
   82 import GHC.Types.Unique.Set
   83 import GHC.Utils.Outputable
   84 import GHC.Utils.Panic
   85 import GHC.Utils.Panic.Plain
   86 
   87 import Data.List (mapAccumL)
   88 
   89 {-
   90 %************************************************************************
   91 %*                                                                      *
   92                         Substitutions
   93       Data type defined here to avoid unnecessary mutual recursion
   94 %*                                                                      *
   95 %************************************************************************
   96 -}
   97 
   98 -- | Type & coercion substitution
   99 --
  100 -- #tcvsubst_invariant#
  101 -- The following invariants must hold of a 'TCvSubst':
  102 --
  103 -- 1. The in-scope set is needed /only/ to
  104 -- guide the generation of fresh uniques
  105 --
  106 -- 2. In particular, the /kind/ of the type variables in
  107 -- the in-scope set is not relevant
  108 --
  109 -- 3. The substitution is only applied ONCE! This is because
  110 -- in general such application will not reach a fixed point.
  111 data TCvSubst
  112   = TCvSubst InScopeSet -- The in-scope type and kind variables
  113              TvSubstEnv -- Substitutes both type and kind variables
  114              CvSubstEnv -- Substitutes coercion variables
  115         -- See Note [Substitutions apply only once]
  116         -- and Note [Extending the TvSubstEnv]
  117         -- and Note [Substituting types and coercions]
  118         -- and Note [The substitution invariant]
  119 
  120 -- | A substitution of 'Type's for 'TyVar's
  121 --                 and 'Kind's for 'KindVar's
  122 type TvSubstEnv = TyVarEnv Type
  123   -- NB: A TvSubstEnv is used
  124   --   both inside a TCvSubst (with the apply-once invariant
  125   --        discussed in Note [Substitutions apply only once],
  126   --   and  also independently in the middle of matching,
  127   --        and unification (see Types.Unify).
  128   -- So you have to look at the context to know if it's idempotent or
  129   -- apply-once or whatever
  130 
  131 -- | A substitution of 'Coercion's for 'CoVar's
  132 type CvSubstEnv = CoVarEnv Coercion
  133 
  134 {- Note [The substitution invariant]
  135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  136 When calling (substTy subst ty) it should be the case that
  137 the in-scope set in the substitution is a superset of both:
  138 
  139   (SIa) The free vars of the range of the substitution
  140   (SIb) The free vars of ty minus the domain of the substitution
  141 
  142 The same rules apply to other substitutions (notably GHC.Core.Subst.Subst)
  143 
  144 * Reason for (SIa). Consider
  145       substTy [a :-> Maybe b] (forall b. b->a)
  146   we must rename the forall b, to get
  147       forall b2. b2 -> Maybe b
  148   Making 'b' part of the in-scope set forces this renaming to
  149   take place.
  150 
  151 * Reason for (SIb). Consider
  152      substTy [a :-> Maybe b] (forall b. (a,b,x))
  153   Then if we use the in-scope set {b}, satisfying (SIa), there is
  154   a danger we will rename the forall'd variable to 'x' by mistake,
  155   getting this:
  156       forall x. (Maybe b, x, x)
  157   Breaking (SIb) caused the bug from #11371.
  158 
  159 Note: if the free vars of the range of the substitution are freshly created,
  160 then the problems of (SIa) can't happen, and so it would be sound to
  161 ignore (SIa).
  162 
  163 Note [Substitutions apply only once]
  164 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  165 We use TCvSubsts to instantiate things, and we might instantiate
  166         forall a b. ty
  167 with the types
  168         [a, b], or [b, a].
  169 So the substitution might go [a->b, b->a].  A similar situation arises in Core
  170 when we find a beta redex like
  171         (/\ a /\ b -> e) b a
  172 Then we also end up with a substitution that permutes type variables. Other
  173 variations happen to; for example [a -> (a, b)].
  174 
  175         ********************************************************
  176         *** So a substitution must be applied precisely once ***
  177         ********************************************************
  178 
  179 A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
  180 we use during unifications, it must not be repeatedly applied.
  181 
  182 Note [Extending the TvSubstEnv]
  183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  184 See #tcvsubst_invariant# for the invariants that must hold.
  185 
  186 This invariant allows a short-cut when the subst envs are empty:
  187 if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst)
  188 holds --- then (substTy subst ty) does nothing.
  189 
  190 For example, consider:
  191         (/\a. /\b:(a~Int). ...b..) Int
  192 We substitute Int for 'a'.  The Unique of 'b' does not change, but
  193 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
  194 
  195 This invariant has several crucial consequences:
  196 
  197 * In substVarBndr, we need extend the TvSubstEnv
  198         - if the unique has changed
  199         - or if the kind has changed
  200 
  201 * In substTyVar, we do not need to consult the in-scope set;
  202   the TvSubstEnv is enough
  203 
  204 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
  205 
  206 Note [Substituting types and coercions]
  207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  208 Types and coercions are mutually recursive, and either may have variables
  209 "belonging" to the other. Thus, every time we wish to substitute in a
  210 type, we may also need to substitute in a coercion, and vice versa.
  211 However, the constructor used to create type variables is distinct from
  212 that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note
  213 that it would be possible to use the CoercionTy constructor to combine
  214 these environments, but that seems like a false economy.
  215 
  216 Note that the TvSubstEnv should *never* map a CoVar (built with the Id
  217 constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
  218 the range of the TvSubstEnv should *never* include a type headed with
  219 CoercionTy.
  220 -}
  221 
  222 emptyTvSubstEnv :: TvSubstEnv
  223 emptyTvSubstEnv = emptyVarEnv
  224 
  225 emptyCvSubstEnv :: CvSubstEnv
  226 emptyCvSubstEnv = emptyVarEnv
  227 
  228 composeTCvSubstEnv :: InScopeSet
  229                    -> (TvSubstEnv, CvSubstEnv)
  230                    -> (TvSubstEnv, CvSubstEnv)
  231                    -> (TvSubstEnv, CvSubstEnv)
  232 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
  233 -- It assumes that both are idempotent.
  234 -- Typically, @env1@ is the refinement to a base substitution @env2@
  235 composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2)
  236   = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
  237     , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 )
  238         -- First apply env1 to the range of env2
  239         -- Then combine the two, making sure that env1 loses if
  240         -- both bind the same variable; that's why env1 is the
  241         --  *left* argument to plusVarEnv, because the right arg wins
  242   where
  243     subst1 = TCvSubst in_scope tenv1 cenv1
  244 
  245 -- | Composes two substitutions, applying the second one provided first,
  246 -- like in function composition.
  247 composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
  248 composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2)
  249   = TCvSubst is3 tenv3 cenv3
  250   where
  251     is3 = is1 `unionInScope` is2
  252     (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2)
  253 
  254 emptyTCvSubst :: TCvSubst
  255 emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv
  256 
  257 mkEmptyTCvSubst :: InScopeSet -> TCvSubst
  258 mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv
  259 
  260 isEmptyTCvSubst :: TCvSubst -> Bool
  261          -- See Note [Extending the TvSubstEnv]
  262 isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
  263 
  264 mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
  265 mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv
  266 
  267 mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
  268 -- ^ Make a TCvSubst with specified tyvar subst and empty covar subst
  269 mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv
  270 
  271 mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
  272 -- ^ Make a TCvSubst with specified covar subst and empty tyvar subst
  273 mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv
  274 
  275 getTvSubstEnv :: TCvSubst -> TvSubstEnv
  276 getTvSubstEnv (TCvSubst _ env _) = env
  277 
  278 getCvSubstEnv :: TCvSubst -> CvSubstEnv
  279 getCvSubstEnv (TCvSubst _ _ env) = env
  280 
  281 getTCvInScope :: TCvSubst -> InScopeSet
  282 getTCvInScope (TCvSubst in_scope _ _) = in_scope
  283 
  284 -- | Returns the free variables of the types in the range of a substitution as
  285 -- a non-deterministic set.
  286 getTCvSubstRangeFVs :: TCvSubst -> VarSet
  287 getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
  288     = unionVarSet tenvFVs cenvFVs
  289   where
  290     tenvFVs = shallowTyCoVarsOfTyVarEnv tenv
  291     cenvFVs = shallowTyCoVarsOfCoVarEnv cenv
  292 
  293 isInScope :: Var -> TCvSubst -> Bool
  294 isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
  295 
  296 elemTCvSubst :: Var -> TCvSubst -> Bool
  297 elemTCvSubst v (TCvSubst _ tenv cenv)
  298   | isTyVar v
  299   = v `elemVarEnv` tenv
  300   | otherwise
  301   = v `elemVarEnv` cenv
  302 
  303 notElemTCvSubst :: Var -> TCvSubst -> Bool
  304 notElemTCvSubst v = not . elemTCvSubst v
  305 
  306 setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
  307 setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
  308 
  309 setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
  310 setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv
  311 
  312 zapTCvSubst :: TCvSubst -> TCvSubst
  313 zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv
  314 
  315 extendTCvInScope :: TCvSubst -> Var -> TCvSubst
  316 extendTCvInScope (TCvSubst in_scope tenv cenv) var
  317   = TCvSubst (extendInScopeSet in_scope var) tenv cenv
  318 
  319 extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
  320 extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars
  321   = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv
  322 
  323 extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
  324 extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
  325   = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
  326 
  327 extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
  328 extendTCvSubst subst v ty
  329   | isTyVar v
  330   = extendTvSubst subst v ty
  331   | CoercionTy co <- ty
  332   = extendCvSubst subst v co
  333   | otherwise
  334   = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
  335 
  336 extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
  337 extendTCvSubstWithClone subst tcv
  338   | isTyVar tcv = extendTvSubstWithClone subst tcv
  339   | otherwise   = extendCvSubstWithClone subst tcv
  340 
  341 extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
  342 extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
  343   = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
  344 
  345 extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
  346 extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty
  347   = assert (isTyVar v )
  348     extendTvSubstAndInScope subst v ty
  349 extendTvSubstBinderAndInScope subst (Anon {}) _
  350   = subst
  351 
  352 extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
  353 -- Adds a new tv -> tv mapping, /and/ extends the in-scope set
  354 extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
  355   = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
  356              (extendVarEnv tenv tv (mkTyVarTy tv'))
  357              cenv
  358   where
  359     new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv'
  360 
  361 extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
  362 extendCvSubst (TCvSubst in_scope tenv cenv) v co
  363   = TCvSubst in_scope tenv (extendVarEnv cenv v co)
  364 
  365 extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
  366 extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
  367   = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
  368              tenv
  369              (extendVarEnv cenv cv (mkCoVarCo cv'))
  370   where
  371     new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv'
  372 
  373 extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
  374 -- Also extends the in-scope set
  375 extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
  376   = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
  377              (extendVarEnv tenv tv ty)
  378              cenv
  379 
  380 extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
  381 extendTvSubstList subst tvs tys
  382   = foldl2 extendTvSubst subst tvs tys
  383 
  384 extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
  385 extendTCvSubstList subst tvs tys
  386   = foldl2 extendTCvSubst subst tvs tys
  387 
  388 unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
  389 -- Works when the ranges are disjoint
  390 unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
  391   = assert (tenv1 `disjointVarEnv` tenv2
  392          && cenv1 `disjointVarEnv` cenv2 )
  393     TCvSubst (in_scope1 `unionInScope` in_scope2)
  394              (tenv1     `plusVarEnv`   tenv2)
  395              (cenv1     `plusVarEnv`   cenv2)
  396 
  397 -- mkTvSubstPrs and zipTvSubst generate the in-scope set from
  398 -- the types given; but it's just a thunk so with a bit of luck
  399 -- it'll never be evaluated
  400 
  401 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
  402 -- environment. No CoVars, please!
  403 zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
  404 zipTvSubst []  [] = emptyTCvSubst
  405 zipTvSubst tvs tys
  406   = mkTvSubst (mkInScopeSet (shallowTyCoVarsOfTypes tys)) tenv
  407   where                   
  408     tenv = zipTyEnv tvs tys
  409 
  410 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
  411 -- environment.  No TyVars, please!
  412 zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
  413 zipCvSubst []  [] = emptyTCvSubst                    
  414 zipCvSubst cvs cos
  415   = TCvSubst (mkInScopeSet (shallowTyCoVarsOfCos cos)) emptyTvSubstEnv cenv
  416   where
  417     cenv = zipCoEnv cvs cos
  418 
  419 zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
  420 zipTCvSubst []   [] = emptyTCvSubst
  421 zipTCvSubst tcvs tys
  422   = zip_tcvsubst tcvs tys $
  423     mkEmptyTCvSubst $ mkInScopeSet $ shallowTyCoVarsOfTypes tys
  424   where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
  425         zip_tcvsubst (tv:tvs) (ty:tys) subst
  426           = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty)    
  427         zip_tcvsubst [] [] subst = subst -- empty case
  428         zip_tcvsubst _  _  _     = pprPanic "zipTCvSubst: length mismatch"
  429                                             (ppr tcvs <+> ppr tys)
  430 
  431 -- | Generates the in-scope set for the 'TCvSubst' from the types in the
  432 -- incoming environment. No CoVars, please!
  433 mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst                    
  434 mkTvSubstPrs []  = emptyTCvSubst
  435 mkTvSubstPrs prs =
  436     assertPpr onlyTyVarsAndNoCoercionTy (text "prs" <+> ppr prs) $
  437     mkTvSubst in_scope tenv
  438   where tenv = mkVarEnv prs
  439         in_scope = mkInScopeSet $ shallowTyCoVarsOfTypes $ map snd prs
  440         onlyTyVarsAndNoCoercionTy =
  441           and [ isTyVar tv && not (isCoercionTy ty)
  442               | (tv, ty) <- prs ]
  443 
  444 zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
  445 zipTyEnv tyvars tys                           
  446   | debugIsOn
  447   , not (all isTyVar tyvars && (tyvars `equalLength` tys))
  448   = pprPanic "zipTyEnv" (ppr tyvars $$ ppr tys)
  449   | otherwise
  450   = assert (all (not . isCoercionTy) tys )
  451     zipToUFM tyvars tys
  452         -- There used to be a special case for when
  453         --      ty == TyVarTy tv
  454         -- (a not-uncommon case) in which case the substitution was dropped.
  455         -- But the type-tidier changes the print-name of a type variable without
  456         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
  457         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
  458         -- And it happened that t was the type variable of the class.  Post-tiding,
  459         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
  460         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
  461         -- and so generated a rep type mentioning t not t2.
  462         --
  463         -- Simplest fix is to nuke the "optimisation"
  464 
  465 zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
  466 zipCoEnv cvs cos                            
  467   | debugIsOn
  468   , not (all isCoVar cvs)       
  469   = pprPanic "zipCoEnv" (ppr cvs <+> ppr cos)
  470   | otherwise
  471   = mkVarEnv (zipEqual "zipCoEnv" cvs cos)
  472 
  473 instance Outputable TCvSubst where
  474   ppr (TCvSubst ins tenv cenv)
  475     = brackets $ sep[ text "TCvSubst",                     
  476                       nest 2 (text "In scope:" <+> ppr ins),
  477                       nest 2 (text "Type env:" <+> ppr tenv),
  478                       nest 2 (text "Co env:" <+> ppr cenv) ]
  479 
  480 {-
  481 %************************************************************************
  482 %*                                                                      *
  483                 Performing type or kind substitutions
  484 %*                                                                      *
  485 %************************************************************************
  486 
  487 Note [Sym and ForAllCo]
  488 ~~~~~~~~~~~~~~~~~~~~~~~
  489 In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
  490 how do we push sym into a ForAllCo? It's a little ugly.
  491 
  492 Here is the typing rule:
  493 
  494 h : k1 ~# k2
  495 (tv : k1) |- g : ty1 ~# ty2
  496 ----------------------------
  497 ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~#
  498                   (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h]))
  499 
  500 Here is what we want:
  501 
  502 ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~#
  503                     (ForAllTy (tv : k1) ty1)
  504 
  505 
  506 Because the kinds of the type variables to the right of the colon are the kinds
  507 coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h).
  508 
  509 Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want
  510 
  511 ForAllCo tv h' g' :
  512   (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~#
  513   (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h']))
  514 
  515 We thus see that we want
  516 
  517 g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h']
  518 
  519 and thus g' = sym (g[tv |-> tv |> h']).
  520 
  521 Putting it all together, we get this:
  522 
  523 sym (ForAllCo tv h g)
  524 ==>
  525 ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
  526 
  527 Note [Substituting in a coercion hole]
  528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  529 It seems highly suspicious to be substituting in a coercion that still
  530 has coercion holes. Yet, this can happen in a situation like this:
  531 
  532   f :: forall k. k :~: Type -> ()
  533   f Refl = let x :: forall (a :: k). [a] -> ...
  534                x = ...
  535 
  536 When we check x's type signature, we require that k ~ Type. We indeed
  537 know this due to the Refl pattern match, but the eager unifier can't
  538 make use of givens. So, when we're done looking at x's type, a coercion
  539 hole will remain. Then, when we're checking x's definition, we skolemise
  540 x's type (in order to, e.g., bring the scoped type variable `a` into scope).
  541 This requires performing a substitution for the fresh skolem variables.
  542 
  543 This substitution needs to affect the kind of the coercion hole, too --
  544 otherwise, the kind will have an out-of-scope variable in it. More problematically
  545 in practice (we won't actually notice the out-of-scope variable ever), skolems
  546 in the kind might have too high a level, triggering a failure to uphold the
  547 invariant that no free variables in a type have a higher level than the
  548 ambient level in the type checker. In the event of having free variables in the
  549 hole's kind, I'm pretty sure we'll always have an erroneous program, so we
  550 don't need to worry what will happen when the hole gets filled in. After all,
  551 a hole relating a locally-bound type variable will be unable to be solved. This
  552 is why it's OK not to look through the IORef of a coercion hole during
  553 substitution.
  554 
  555 -}
  556 
  557 -- | Type substitution, see 'zipTvSubst'
  558 substTyWith :: HasDebugCallStack => [TyVar] -> [Type] -> Type -> Type
  559 -- Works only if the domain of the substitution is a
  560 -- superset of the type being substituted into   
  561 substTyWith tvs tys = {-#SCC "substTyWith" #-}
  562                       assert (tvs `equalLength` tys )
  563                       substTy (zipTvSubst tvs tys)
  564 
  565 -- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
  566 -- The problems that the sanity checks in substTy catch are described in
  567 -- Note [The substitution invariant].
  568 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
  569 -- substTy and remove this function. Please don't use in new code.
  570 substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
  571 substTyWithUnchecked tvs tys
  572   = assert (tvs `equalLength` tys )
  573     substTyUnchecked (zipTvSubst tvs tys)
  574 
  575 -- | Substitute tyvars within a type using a known 'InScopeSet'.
  576 -- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
  577 -- invariant]; specifically it should include the free vars of 'tys',
  578 -- and of 'ty' minus the domain of the subst.
  579 substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
  580 substTyWithInScope in_scope tvs tys ty =
  581   assert (tvs `equalLength` tys )
  582   substTy (mkTvSubst in_scope tenv) ty
  583   where tenv = zipTyEnv tvs tys
  584 
  585 -- | Coercion substitution, see 'zipTvSubst'     
  586 substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
  587 substCoWith tvs tys = assert (tvs `equalLength` tys )
  588                       substCo (zipTvSubst tvs tys)
  589 
  590 -- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
  591 -- The problems that the sanity checks in substCo catch are described in
  592 -- Note [The substitution invariant].
  593 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
  594 -- substCo and remove this function. Please don't use in new code.
  595 substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
  596 substCoWithUnchecked tvs tys
  597   = assert (tvs `equalLength` tys )
  598     substCoUnchecked (zipTvSubst tvs tys)
  599 
  600 
  601                                                       
  602 -- | Substitute covars within a type
  603 substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
  604 substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
  605 
  606 -- | Type substitution, see 'zipTvSubst'           
  607 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
  608 substTysWith tvs tys = assert (tvs `equalLength` tys )
  609                        substTys (zipTvSubst tvs tys)
  610 
  611 -- | Type substitution, see 'zipTvSubst'                 
  612 substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
  613 substTysWithCoVars cvs cos = assert (cvs `equalLength` cos )
  614                              substTys (zipCvSubst cvs cos)
  615 
  616 -- | Substitute within a 'Type' after adding the free variables of the type
  617 -- to the in-scope set. This is useful for the case when the free variables
  618 -- aren't already in the in-scope set or easily available.
  619 -- See also Note [The substitution invariant].         
  620 substTyAddInScope :: TCvSubst -> Type -> Type
  621 substTyAddInScope subst ty =
  622   substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
  623 
  624 -- | When calling `substTy` it should be the case that the in-scope set in
  625 -- the substitution is a superset of the free vars of the range of the
  626 -- substitution.
  627 -- See also Note [The substitution invariant].
  628 isValidTCvSubst :: TCvSubst -> Bool
  629 isValidTCvSubst (TCvSubst in_scope tenv cenv) =
  630   (tenvFVs `varSetInScope` in_scope) &&
  631   (cenvFVs `varSetInScope` in_scope)     
  632   where
  633   tenvFVs = shallowTyCoVarsOfTyVarEnv tenv
  634   cenvFVs = shallowTyCoVarsOfCoVarEnv cenv
  635 
  636 -- | This checks if the substitution satisfies the invariant from
  637 -- Note [The substitution invariant].
  638 checkValidSubst :: HasDebugCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
  639 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
  640   = assertPpr (isValidTCvSubst subst)
  641               (text "in_scope" <+> ppr in_scope $$
  642                text "tenv" <+> ppr tenv $$
  643                text "tenvFVs" <+> ppr (shallowTyCoVarsOfTyVarEnv tenv) $$
  644                text "cenv" <+> ppr cenv $$
  645                text "cenvFVs" <+> ppr (shallowTyCoVarsOfCoVarEnv cenv) $$
  646                text "tys" <+> ppr tys $$
  647                text "cos" <+> ppr cos) $
  648     assertPpr tysCosFVsInScope
  649               (text "in_scope" <+> ppr in_scope $$
  650                text "tenv" <+> ppr tenv $$
  651                text "cenv" <+> ppr cenv $$          
  652                text "tys" <+> ppr tys $$
  653                text "cos" <+> ppr cos $$
  654                text "needInScope" <+> ppr needInScope) 
  655     a
  656   where
  657   substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
  658     -- It's OK to use nonDetKeysUFM here, because we only use this list to
  659     -- remove some elements from a set                  
  660   needInScope = (shallowTyCoVarsOfTypes tys `unionVarSet`
  661                  shallowTyCoVarsOfCos cos)
  662                 `delListFromUniqSet_Directly` substDomain
  663   tysCosFVsInScope = needInScope `varSetInScope` in_scope
  664 
  665 
  666 -- | Substitute within a 'Type'
  667 -- The substitution has to satisfy the invariants described in
  668 -- Note [The substitution invariant].
  669 substTy :: HasDebugCallStack => TCvSubst -> Type  -> Type
  670 substTy subst ty                            
  671   | isEmptyTCvSubst subst = ty
  672   | otherwise             = checkValidSubst subst [ty] [] $
  673                             subst_ty subst ty
  674 
  675 -- | Substitute within a 'Type' disabling the sanity checks.
  676 -- The problems that the sanity checks in substTy catch are described in
  677 -- Note [The substitution invariant].
  678 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
  679 -- substTy and remove this function. Please don't use in new code.
  680 substTyUnchecked :: TCvSubst -> Type -> Type               
  681 substTyUnchecked subst ty
  682                  | isEmptyTCvSubst subst = ty
  683                  | otherwise             = subst_ty subst ty          
  684 
  685 substScaledTy :: HasDebugCallStack => TCvSubst -> Scaled Type -> Scaled Type
  686 substScaledTy subst scaled_ty = mapScaledType (substTy subst) scaled_ty                 
  687 
  688 substScaledTyUnchecked :: HasDebugCallStack => TCvSubst -> Scaled Type -> Scaled Type
  689 substScaledTyUnchecked subst scaled_ty = mapScaledType (substTyUnchecked subst) scaled_ty
  690 
  691 -- | Substitute within several 'Type's
  692 -- The substitution has to satisfy the invariants described in
  693 -- Note [The substitution invariant].
  694 substTys :: HasDebugCallStack => TCvSubst -> [Type] -> [Type]         
  695 substTys subst tys
  696   | isEmptyTCvSubst subst = tys
  697   | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
  698 
  699 substScaledTys :: HasDebugCallStack => TCvSubst -> [Scaled Type] -> [Scaled Type]             
  700 substScaledTys subst scaled_tys                               
  701   | isEmptyTCvSubst subst = scaled_tys
  702   | otherwise = checkValidSubst subst (map scaledMult scaled_tys ++ map scaledThing scaled_tys) [] $
  703                 map (mapScaledType (subst_ty subst)) scaled_tys
  704 
  705 -- | Substitute within several 'Type's disabling the sanity checks.
  706 -- The problems that the sanity checks in substTys catch are described in
  707 -- Note [The substitution invariant].
  708 -- The goal of #11371 is to migrate all the calls of substTysUnchecked to
  709 -- substTys and remove this function. Please don't use in new code.
  710 substTysUnchecked :: TCvSubst -> [Type] -> [Type]                 
  711 substTysUnchecked subst tys
  712                  | isEmptyTCvSubst subst = tys
  713                  | otherwise             = map (subst_ty subst) tys
  714 
  715 substScaledTysUnchecked :: TCvSubst -> [Scaled Type] -> [Scaled Type]             
  716 substScaledTysUnchecked subst tys
  717                  | isEmptyTCvSubst subst = tys
  718                  | otherwise             = map (mapScaledType (subst_ty subst)) tys
  719 
  720 -- | Substitute within a 'ThetaType'
  721 -- The substitution has to satisfy the invariants described in
  722 -- Note [The substitution invariant].
  723 substTheta :: HasDebugCallStack => TCvSubst -> ThetaType -> ThetaType
  724 substTheta = substTys
  725 
  726 -- | Substitute within a 'ThetaType' disabling the sanity checks.
  727 -- The problems that the sanity checks in substTys catch are described in
  728 -- Note [The substitution invariant].
  729 -- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
  730 -- substTheta and remove this function. Please don't use in new code.
  731 substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
  732 substThetaUnchecked = substTysUnchecked
  733 
  734 
  735 subst_ty :: TCvSubst -> Type -> Type
  736 -- subst_ty is the main workhorse for type substitution
  737 --
  738 -- Note that the in_scope set is poked only if we hit a forall
  739 -- so it may often never be fully computed
  740 subst_ty subst ty
  741    = go ty
  742   where
  743     go (TyVarTy tv)      = substTyVar subst tv
  744     go (AppTy fun arg)   = (mkAppTy $! (go fun)) $! (go arg)
  745                 -- The mkAppTy smart constructor is important
  746                 -- we might be replacing (a Int), represented with App
  747                 -- by [Int], represented with TyConApp
  748     go ty@(TyConApp tc []) = tc `seq` ty  -- avoid allocation in this common case
  749     go (TyConApp tc tys) = (mkTyConApp $! tc) $! strictMap go tys
  750                                -- NB: mkTyConApp, not TyConApp.
  751                                -- mkTyConApp has optimizations.
  752                                -- See Note [Prefer Type over TYPE 'LiftedRep]
  753                                -- in GHC.Core.TyCo.Rep
  754     go ty@(FunTy { ft_mult = mult, ft_arg = arg, ft_res = res })
  755       = let !mult' = go mult
  756             !arg' = go arg
  757             !res' = go res
  758         in ty { ft_mult = mult', ft_arg = arg', ft_res = res' }
  759     go (ForAllTy (Bndr tv vis) ty)
  760                          = case substVarBndrUnchecked subst tv of
  761                              (subst', tv') ->
  762                                (ForAllTy $! ((Bndr $! tv') vis)) $!
  763                                             (subst_ty subst' ty)
  764     go (LitTy n)         = LitTy $! n
  765     go (CastTy ty co)    = (mkCastTy $! (go ty)) $! (subst_co subst co)
  766     go (CoercionTy co)   = CoercionTy $! (subst_co subst co)
  767 
  768 substTyVar :: TCvSubst -> TyVar -> Type
  769 substTyVar (TCvSubst _ tenv _) tv
  770   = assert (isTyVar tv) $ 
  771     case lookupVarEnv tenv tv of
  772       Just ty -> ty
  773       Nothing -> TyVarTy tv              
  774 
  775 substTyVars :: TCvSubst -> [TyVar] -> [Type]
  776 substTyVars subst = map $ substTyVar subst   
  777 
  778 substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
  779 substTyCoVars subst = map $ substTyCoVar subst
  780 
  781 substTyCoVar :: TCvSubst -> TyCoVar -> Type    
  782 substTyCoVar subst tv
  783   | isTyVar tv = substTyVar subst tv
  784   | otherwise = CoercionTy $ substCoVar subst tv
  785 
  786 lookupTyVar :: TCvSubst -> TyVar  -> Maybe Type
  787         -- See Note [Extending the TCvSubst]
  788 lookupTyVar (TCvSubst _ tenv _) tv
  789   = assert (isTyVar tv )
  790     lookupVarEnv tenv tv
  791 
  792 -- | Substitute within a 'Coercion'
  793 -- The substitution has to satisfy the invariants described in
  794 -- Note [The substitution invariant].
  795 substCo :: HasDebugCallStack => TCvSubst -> Coercion -> Coercion
  796 substCo subst co
  797   | isEmptyTCvSubst subst = co
  798   | otherwise = checkValidSubst subst [] [co] $ subst_co subst co
  799 
  800 -- | Substitute within a 'Coercion' disabling sanity checks.
  801 -- The problems that the sanity checks in substCo catch are described in
  802 -- Note [The substitution invariant].
  803 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
  804 -- substCo and remove this function. Please don't use in new code.
  805 substCoUnchecked :: TCvSubst -> Coercion -> Coercion
  806 substCoUnchecked subst co
  807   | isEmptyTCvSubst subst = co
  808   | otherwise = subst_co subst co
  809 
  810 -- | Substitute within several 'Coercion's
  811 -- The substitution has to satisfy the invariants described in
  812 -- Note [The substitution invariant].
  813 substCos :: HasDebugCallStack => TCvSubst -> [Coercion] -> [Coercion] 
  814 substCos subst cos
  815   | isEmptyTCvSubst subst = cos
  816   | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
  817 
  818 subst_co :: TCvSubst -> Coercion -> Coercion
  819 subst_co subst co
  820   = go co
  821   where
  822     go_ty :: Type -> Type
  823     go_ty = subst_ty subst
  824 
  825     go_mco :: MCoercion -> MCoercion
  826     go_mco MRefl    = MRefl
  827     go_mco (MCo co) = MCo (go co)
  828 
  829     go :: Coercion -> Coercion
  830     go (Refl ty)             = mkNomReflCo $! (go_ty ty)
  831     go (GRefl r ty mco)      = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
  832     go (TyConAppCo r tc args)= let args' = map go args
  833                                in  args' `seqList` mkTyConAppCo r tc args'
  834     go (AppCo co arg)        = (mkAppCo $! go co) $! go arg
  835     go (ForAllCo tv kind_co co)
  836       = case substForAllCoBndrUnchecked subst tv kind_co of
  837          (subst', tv', kind_co') ->
  838           ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co
  839     go (FunCo r w co1 co2)   = ((mkFunCo r $! go w) $! go co1) $! go co2
  840     go (CoVarCo cv)          = substCoVar subst cv
  841     go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
  842     go (UnivCo p r t1 t2)    = (((mkUnivCo $! go_prov p) $! r) $!
  843                                 (go_ty t1)) $! (go_ty t2)
  844     go (SymCo co)            = mkSymCo $! (go co) 
  845     go (TransCo co1 co2)     = (mkTransCo $! (go co1)) $! (go co2)
  846     go (NthCo r d co)        = mkNthCo r d $! (go co)
  847     go (LRCo lr co)          = mkLRCo lr $! (go co)
  848     go (InstCo co arg)       = (mkInstCo $! (go co)) $! go arg
  849     go (KindCo co)           = mkKindCo $! (go co)               
  850     go (SubCo co)            = mkSubCo $! (go co)
  851     go (AxiomRuleCo c cs)    = let cs1 = map go cs
  852                                 in cs1 `seqList` AxiomRuleCo c cs1
  853     go (HoleCo h)            = HoleCo $! go_hole h       
  854 
  855     go_prov (PhantomProv kco)    = PhantomProv (go kco)
  856     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
  857     go_prov p@(PluginProv _)     = p
  858     go_prov p@(CorePrepProv _)   = p
  859                                                
  860     -- See Note [Substituting in a coercion hole]
  861     go_hole h@(CoercionHole { ch_co_var = cv })
  862       = h { ch_co_var = updateVarType go_ty cv }
  863 
  864 substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
  865                   -> (TCvSubst, TyCoVar, Coercion)
  866 substForAllCoBndr subst
  867   = substForAllCoBndrUsing False (substCo subst) subst
  868 
  869 -- | Like 'substForAllCoBndr', but disables sanity checks.
  870 -- The problems that the sanity checks in substCo catch are described in
  871 -- Note [The substitution invariant].
  872 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
  873 -- substCo and remove this function. Please don't use in new code.
  874 substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion
  875                            -> (TCvSubst, TyCoVar, Coercion)
  876 substForAllCoBndrUnchecked subst
  877   = substForAllCoBndrUsing False (substCoUnchecked subst) subst
  878 
  879 -- See Note [Sym and ForAllCo]
  880 substForAllCoBndrUsing :: Bool  -- apply sym to binder?
  881                        -> (Coercion -> Coercion)  -- transformation to kind co
  882                        -> TCvSubst -> TyCoVar -> KindCoercion
  883                        -> (TCvSubst, TyCoVar, KindCoercion)   
  884 substForAllCoBndrUsing sym sco subst old_var
  885   | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var
  886   | otherwise       = substForAllCoCoVarBndrUsing sym sco subst old_var
  887 
  888 substForAllCoTyVarBndrUsing :: Bool  -- apply sym to binder?
  889                             -> (Coercion -> Coercion)  -- transformation to kind co
  890                             -> TCvSubst -> TyVar -> KindCoercion
  891                             -> (TCvSubst, TyVar, KindCoercion)
  892 substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co
  893   = assert (isTyVar old_var )
  894     ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv
  895     , new_var, new_kind_co )
  896   where
  897     new_env | no_change && not sym = delVarEnv tenv old_var
  898             | sym       = extendVarEnv tenv old_var $
  899                           TyVarTy new_var `CastTy` new_kind_co
  900             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
  901 
  902     no_kind_change = noFreeVarsOfCo old_kind_co
  903     no_change = no_kind_change && (new_var == old_var)
  904 
  905     new_kind_co | no_kind_change = old_kind_co
  906                 | otherwise      = sco old_kind_co
  907 
  908     new_ki1 = coercionLKind new_kind_co
  909     -- We could do substitution to (tyVarKind old_var). We don't do so because
  910     -- we already substituted new_kind_co, which contains the kind information
  911     -- we want. We don't want to do substitution once more. Also, in most cases,
  912     -- new_kind_co is a Refl, in which case coercionKind is really fast.
  913 
  914     new_var  = uniqAway in_scope (setTyVarKind old_var new_ki1)
  915 
  916 substForAllCoCoVarBndrUsing :: Bool  -- apply sym to binder?
  917                             -> (Coercion -> Coercion)  -- transformation to kind co
  918                             -> TCvSubst -> CoVar -> KindCoercion
  919                             -> (TCvSubst, CoVar, KindCoercion)
  920 substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
  921                             old_var old_kind_co
  922   = assert (isCoVar old_var )
  923     ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv
  924     , new_var, new_kind_co )
  925   where
  926     new_cenv | no_change && not sym = delVarEnv cenv old_var
  927              | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
  928 
  929     no_kind_change = noFreeVarsOfCo old_kind_co
  930     no_change = no_kind_change && (new_var == old_var)
  931 
  932     new_kind_co | no_kind_change = old_kind_co
  933                 | otherwise      = sco old_kind_co
  934 
  935     Pair h1 h2 = coercionKind new_kind_co
  936                                  
  937     new_var       = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type
  938     new_var_type  | sym       = h2
  939                   | otherwise = h1
  940 
  941 substCoVar :: TCvSubst -> CoVar -> Coercion
  942 substCoVar (TCvSubst _ _ cenv) cv
  943   = case lookupVarEnv cenv cv of
  944       Just co -> co
  945       Nothing -> CoVarCo cv                  
  946 
  947 substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
  948 substCoVars subst cvs = map (substCoVar subst) cvs    
  949 
  950 lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
  951 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
  952 
  953 substTyVarBndr :: HasDebugCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
  954 substTyVarBndr = substTyVarBndrUsing substTy
  955 
  956 substTyVarBndrs :: HasDebugCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
  957 substTyVarBndrs = mapAccumL substTyVarBndr
  958 
  959 substVarBndr :: HasDebugCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
  960 substVarBndr = substVarBndrUsing substTy
  961 
  962 substVarBndrs :: HasDebugCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
  963 substVarBndrs = mapAccumL substVarBndr     
  964 
  965 substCoVarBndr :: HasDebugCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
  966 substCoVarBndr = substCoVarBndrUsing substTy
  967 
  968 -- | Like 'substVarBndr', but disables sanity checks.
  969 -- The problems that the sanity checks in substTy catch are described in
  970 -- Note [The substitution invariant].
  971 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
  972 -- substTy and remove this function. Please don't use in new code.
  973 substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
  974 substVarBndrUnchecked = substVarBndrUsing substTyUnchecked
  975 
  976 substVarBndrUsing :: (TCvSubst -> Type -> Type)
  977                   -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
  978 substVarBndrUsing subst_fn subst v
  979   | isTyVar v = substTyVarBndrUsing subst_fn subst v
  980   | otherwise = substCoVarBndrUsing subst_fn subst v
  981 
  982 -- | Substitute a tyvar in a binding position, returning an
  983 -- extended subst and a new tyvar.
  984 -- Use the supplied function to substitute in the kind
  985 substTyVarBndrUsing
  986   :: (TCvSubst -> Type -> Type)  -- ^ Use this to substitute in the kind    
  987   -> TCvSubst -> TyVar -> (TCvSubst, TyVar)
  988 substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
  989   = assertPpr _no_capture (pprTyVar old_var $$ pprTyVar new_var $$ ppr subst) $
  990     assert (isTyVar old_var )
  991     (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var)
  992   where
  993     new_env | no_change = delVarEnv tenv old_var                          
  994             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
  995 
  996     _no_capture = not (new_var `elemVarSet` shallowTyCoVarsOfTyVarEnv tenv)
  997     -- Assertion check that we are not capturing something in the substitution
  998 
  999     old_ki = tyVarKind old_var
 1000     no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
 1001     no_change = no_kind_change && (new_var == old_var)
 1002         -- no_change means that the new_var is identical in
 1003         -- all respects to the old_var (same unique, same kind)
 1004         -- See Note [Extending the TCvSubst]
 1005         --
 1006         -- In that case we don't need to extend the substitution
 1007         -- to map old to new.  But instead we must zap any
 1008         -- current substitution for the variable. For example:
 1009         --      (\x.e) with id_subst = [x |-> e']
 1010         -- Here we must simply zap the substitution for x
 1011                                                                      
 1012     new_var | no_kind_change = uniqAway in_scope old_var
 1013             | otherwise = uniqAway in_scope $
 1014                           setTyVarKind old_var (subst_fn subst old_ki)
 1015         -- The uniqAway part makes sure the new variable is not already in scope
 1016 
 1017 -- | Substitute a covar in a binding position, returning an
 1018 -- extended subst and a new covar.
 1019 -- Use the supplied function to substitute in the kind
 1020 substCoVarBndrUsing
 1021   :: (TCvSubst -> Type -> Type)
 1022   -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
 1023 substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
 1024   = assert (isCoVar old_var)
 1025     (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
 1026   where
 1027     new_co         = mkCoVarCo new_var
 1028     no_kind_change = noFreeVarsOfTypes [t1, t2]
 1029     no_change      = new_var == old_var && no_kind_change
 1030 
 1031     new_cenv | no_change = delVarEnv cenv old_var
 1032              | otherwise = extendVarEnv cenv old_var new_co
 1033 
 1034     new_var = uniqAway in_scope subst_old_var
 1035     subst_old_var = mkCoVar (varName old_var) new_var_type
 1036 
 1037     (_, _, t1, t2, role) = coVarKindsTypesRole old_var
 1038     t1' = subst_fn subst t1
 1039     t2' = subst_fn subst t2
 1040     new_var_type = mkCoercionType role t1' t2'
 1041                   -- It's important to do the substitution for coercions,
 1042                   -- because they can have free type variables
 1043 
 1044 cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
 1045 cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
 1046   = assertPpr (isTyVar tv) (ppr tv)   -- I think it's only called on TyVars
 1047     (TCvSubst (extendInScopeSet in_scope tv')
 1048               (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
 1049   where
 1050     old_ki = tyVarKind tv
 1051     no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
 1052 
 1053     tv1 | no_kind_change = tv 
 1054         | otherwise      = setTyVarKind tv (substTy subst old_ki)
 1055 
 1056     tv' = setVarUnique tv1 uniq
 1057 
 1058 cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
 1059 cloneTyVarBndrs subst []     _usupply = (subst, [])
 1060 cloneTyVarBndrs subst (t:ts)  usupply = (subst'', tv:tvs)
 1061   where                                                 
 1062     (uniq, usupply') = takeUniqFromSupply usupply
 1063     (subst' , tv )   = cloneTyVarBndr subst t uniq
 1064     (subst'', tvs)   = cloneTyVarBndrs subst' ts usupply'
 1065 
 1066 substTyCoBndr :: TCvSubst -> TyCoBinder -> (TCvSubst, TyCoBinder)
 1067 substTyCoBndr subst (Anon af ty)          = (subst, Anon af (substScaledTy subst ty))
 1068 substTyCoBndr subst (Named (Bndr tv vis)) = (subst', Named (Bndr tv' vis))
 1069                                           where
 1070                                             (subst', tv') = substVarBndr subst tv
 1071