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