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