Create a deterministic version of tyVarsOfType
[ghc.git] / compiler / types / Coercion.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP, DeriveDataTypeable #-}
4
5 -- | Module for (a) type kinds and (b) type coercions,
6 -- as used in System FC. See 'CoreSyn.Expr' for
7 -- more on System FC and how coercions fit into it.
8 --
9 module Coercion (
10 -- * Main data type
11 Coercion(..), Var, CoVar,
12 LeftOrRight(..), pickLR,
13 Role(..), ltRole,
14
15 -- ** Functions over coercions
16 coVarKind, coVarRole,
17 coercionType, coercionKind, coercionKinds, isReflCo,
18 isReflCo_maybe, coercionRole, coercionKindRole,
19 mkCoercionType,
20
21 -- ** Constructing coercions
22 mkReflCo, mkCoVarCo,
23 mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
24 mkUnbranchedAxInstRHS,
25 mkPiCo, mkPiCos, mkCoCast,
26 mkSymCo, mkTransCo, mkNthCo, mkNthCoRole, mkLRCo,
27 mkInstCo, mkAppCo, mkAppCoFlexible, mkTyConAppCo, mkFunCo,
28 mkForAllCo, mkUnsafeCo, mkUnivCo, mkSubCo, mkPhantomCo,
29 mkNewTypeCo, downgradeRole,
30 mkAxiomRuleCo,
31
32 -- ** Decomposition
33 instNewTyCon_maybe,
34
35 NormaliseStepper, NormaliseStepResult(..), composeSteppers,
36 modifyStepResultCo, unwrapNewTypeStepper,
37 topNormaliseNewType_maybe, topNormaliseTypeX_maybe,
38
39 decomposeCo, getCoVar_maybe,
40 splitAppCo_maybe,
41 splitForAllCo_maybe,
42 nthRole, tyConRolesX,
43 setNominalRole_maybe,
44
45 -- ** Coercion variables
46 mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
47
48 -- ** Free variables
49 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
50 tyCoVarsOfCoAcc, tyCoVarsOfCosAcc,
51
52 -- ** Substitution
53 CvSubstEnv, emptyCvSubstEnv,
54 CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
55 isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
56 substCo, substCos, substCoVar, substCoVars,
57 substCoWithTy, substCoWithTys,
58 cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
59 substTy, extendTvSubst,
60 extendCvSubstAndInScope, extendTvSubstAndInScope,
61 substTyVarBndr, substCoVarBndr,
62
63 -- ** Lifting
64 liftCoMatch, liftCoSubstTyVar, liftCoSubstWith,
65
66 -- ** Comparison
67 coreEqCoercion, coreEqCoercion2,
68
69 -- ** Forcing evaluation of coercions
70 seqCo,
71
72 -- * Pretty-printing
73 pprCo, pprParendCo,
74 pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
75
76 -- * Tidying
77 tidyCo, tidyCos,
78
79 -- * Other
80 applyCo,
81 ) where
82
83 #include "HsVersions.h"
84
85 import Unify ( MatchEnv(..), matchList )
86 import TypeRep
87 import qualified Type
88 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
89 import TyCon
90 import CoAxiom
91 import Var
92 import VarEnv
93 import VarSet
94 import Binary
95 import Maybes ( orElse )
96 import Name ( Name, NamedThing(..), nameUnique, nameModule, getSrcSpan )
97 import OccName ( parenSymOcc )
98 import Util
99 import BasicTypes
100 import Outputable
101 import Unique
102 import Pair
103 import SrcLoc
104 import PrelNames ( funTyConKey, eqPrimTyConKey, eqReprPrimTyConKey )
105 #if __GLASGOW_HASKELL__ < 709
106 import Control.Applicative hiding ( empty )
107 import Data.Traversable (traverse, sequenceA)
108 #endif
109 import FastString
110 import ListSetOps
111 import FV
112
113 import qualified Data.Data as Data hiding ( TyCon )
114 import Control.Arrow ( first )
115
116 {-
117 ************************************************************************
118 * *
119 Coercions
120 * *
121 ************************************************************************
122 -}
123
124 -- | A 'Coercion' is concrete evidence of the equality/convertibility
125 -- of two types.
126
127 -- If you edit this type, you may need to update the GHC formalism
128 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
129 data Coercion
130 -- Each constructor has a "role signature", indicating the way roles are
131 -- propagated through coercions. P, N, and R stand for coercions of the
132 -- given role. e stands for a coercion of a specific unknown role (think
133 -- "role polymorphism"). "e" stands for an explicit role parameter
134 -- indicating role e. _ stands for a parameter that is not a Role or
135 -- Coercion.
136
137 -- These ones mirror the shape of types
138 = -- Refl :: "e" -> _ -> e
139 Refl Role Type -- See Note [Refl invariant]
140 -- Invariant: applications of (Refl T) to a bunch of identity coercions
141 -- always show up as Refl.
142 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
143
144 -- Applications of (Refl T) to some coercions, at least one of
145 -- which is NOT the identity, show up as TyConAppCo.
146 -- (They may not be fully saturated however.)
147 -- ConAppCo coercions (like all coercions other than Refl)
148 -- are NEVER the identity.
149
150 -- Use (Refl Representational _), not (SubCo (Refl Nominal _))
151
152 -- These ones simply lift the correspondingly-named
153 -- Type constructors into Coercions
154
155 -- TyConAppCo :: "e" -> _ -> ?? -> e
156 -- See Note [TyConAppCo roles]
157 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp
158 -- The TyCon is never a synonym;
159 -- we expand synonyms eagerly
160 -- But it can be a type function
161
162 | AppCo Coercion Coercion -- lift AppTy
163 -- AppCo :: e -> N -> e
164
165 -- See Note [Forall coercions]
166 | ForAllCo TyVar Coercion -- forall a. g
167 -- :: _ -> e -> e
168
169 -- These are special
170 | CoVarCo CoVar -- :: _ -> (N or R)
171 -- result role depends on the tycon of the variable's type
172
173 -- AxiomInstCo :: e -> _ -> [N] -> e
174 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
175 -- See also [CoAxiom index]
176 -- The coercion arguments always *precisely* saturate
177 -- arity of (that branch of) the CoAxiom. If there are
178 -- any left over, we use AppCo. See
179 -- See [Coercion axioms applied to coercions]
180
181 -- see Note [UnivCo]
182 | UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e
183 -- the FastString is just a note for provenance
184 | SymCo Coercion -- :: e -> e
185 | TransCo Coercion Coercion -- :: e -> e -> e
186
187 -- The number of types and coercions should match exactly the expectations
188 -- of the CoAxiomRule (i.e., the rule is fully saturated).
189 | AxiomRuleCo CoAxiomRule [Type] [Coercion]
190
191 -- These are destructors
192
193 | NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
194 -- and (F t0 ... tn), assuming F is injective.
195 -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
196 -- See Note [NthCo and newtypes]
197
198 | LRCo LeftOrRight Coercion -- Decomposes (t_left t_right)
199 -- :: _ -> N -> N
200 | InstCo Coercion Type
201 -- :: e -> _ -> e
202
203 | SubCo Coercion -- Turns a ~N into a ~R
204 -- :: N -> R
205 deriving (Data.Data, Data.Typeable)
206
207 -- If you edit this type, you may need to update the GHC formalism
208 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
209 data LeftOrRight = CLeft | CRight
210 deriving( Eq, Data.Data, Data.Typeable )
211
212 instance Binary LeftOrRight where
213 put_ bh CLeft = putByte bh 0
214 put_ bh CRight = putByte bh 1
215
216 get bh = do { h <- getByte bh
217 ; case h of
218 0 -> return CLeft
219 _ -> return CRight }
220
221 pickLR :: LeftOrRight -> (a,a) -> a
222 pickLR CLeft (l,_) = l
223 pickLR CRight (_,r) = r
224
225 {-
226 Note [Refl invariant]
227 ~~~~~~~~~~~~~~~~~~~~~
228 Coercions have the following invariant
229 Refl is always lifted as far as possible.
230
231 You might think that a consequencs is:
232 Every identity coercions has Refl at the root
233
234 But that's not quite true because of coercion variables. Consider
235 g where g :: Int~Int
236 Left h where h :: Maybe Int ~ Maybe Int
237 etc. So the consequence is only true of coercions that
238 have no coercion variables.
239
240 Note [Coercion axioms applied to coercions]
241 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
242 The reason coercion axioms can be applied to coercions and not just
243 types is to allow for better optimization. There are some cases where
244 we need to be able to "push transitivity inside" an axiom in order to
245 expose further opportunities for optimization.
246
247 For example, suppose we have
248
249 C a : t[a] ~ F a
250 g : b ~ c
251
252 and we want to optimize
253
254 sym (C b) ; t[g] ; C c
255
256 which has the kind
257
258 F b ~ F c
259
260 (stopping through t[b] and t[c] along the way).
261
262 We'd like to optimize this to just F g -- but how? The key is
263 that we need to allow axioms to be instantiated by *coercions*,
264 not just by types. Then we can (in certain cases) push
265 transitivity inside the axiom instantiations, and then react
266 opposite-polarity instantiations of the same axiom. In this
267 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
268 obtain the substitution a |-> g (note this operation is sort
269 of the dual of lifting!) and hence end up with
270
271 C g : t[b] ~ F c
272
273 which indeed has the same kind as t[g] ; C c.
274
275 Now we have
276
277 sym (C b) ; C g
278
279 which can be optimized to F g.
280
281 Note [CoAxiom index]
282 ~~~~~~~~~~~~~~~~~~~~
283 A CoAxiom has 1 or more branches. Each branch has contains a list
284 of the free type variables in that branch, the LHS type patterns,
285 and the RHS type for that branch. When we apply an axiom to a list
286 of coercions, we must choose which branch of the axiom we wish to
287 use, as the different branches may have different numbers of free
288 type variables. (The number of type patterns is always the same
289 among branches, but that doesn't quite concern us here.)
290
291 The Int in the AxiomInstCo constructor is the 0-indexed number
292 of the chosen branch.
293
294 Note [Forall coercions]
295 ~~~~~~~~~~~~~~~~~~~~~~~
296 Constructing coercions between forall-types can be a bit tricky.
297 Currently, the situation is as follows:
298
299 ForAllCo TyVar Coercion
300
301 represents a coercion between polymorphic types, with the rule
302
303 v : k g : t1 ~ t2
304 ----------------------------------------------
305 ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
306
307 Note that it's only necessary to coerce between polymorphic types
308 where the type variables have identical kinds, because equality on
309 kinds is trivial.
310
311 Note [Predicate coercions]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~
313 Suppose we have
314 g :: a~b
315 How can we coerce between types
316 ([c]~a) => [a] -> c
317 and
318 ([c]~b) => [b] -> c
319 where the equality predicate *itself* differs?
320
321 Answer: we simply treat (~) as an ordinary type constructor, so these
322 types really look like
323
324 ((~) [c] a) -> [a] -> c
325 ((~) [c] b) -> [b] -> c
326
327 So the coercion between the two is obviously
328
329 ((~) [c] g) -> [g] -> c
330
331 Another way to see this to say that we simply collapse predicates to
332 their representation type (see Type.coreView and Type.predTypeRep).
333
334 This collapse is done by mkPredCo; there is no PredCo constructor
335 in Coercion. This is important because we need Nth to work on
336 predicates too:
337 Nth 1 ((~) [c] g) = g
338 See Simplify.simplCoercionF, which generates such selections.
339
340 Note [Kind coercions]
341 ~~~~~~~~~~~~~~~~~~~~~
342 Suppose T :: * -> *, and g :: A ~ B
343 Then the coercion
344 TyConAppCo T [g] T g : T A ~ T B
345
346 Now suppose S :: forall k. k -> *, and g :: A ~ B
347 Then the coercion
348 TyConAppCo S [Refl *, g] T <*> g : T * A ~ T * B
349
350 Notice that the arguments to TyConAppCo are coercions, but the first
351 represents a *kind* coercion. Now, we don't allow any non-trivial kind
352 coercions, so it's an invariant that any such kind coercions are Refl.
353 Lint checks this.
354
355 However it's inconvenient to insist that these kind coercions are always
356 *structurally* (Refl k), because the key function exprIsConApp_maybe
357 pushes coercions into constructor arguments, so
358 C k ty e |> g
359 may turn into
360 C (Nth 0 g) ....
361 Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.
362
363 Note [Roles]
364 ~~~~~~~~~~~~
365 Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
366 in Trac #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
367 http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
368
369 Here is one way to phrase the problem:
370
371 Given:
372 newtype Age = MkAge Int
373 type family F x
374 type instance F Age = Bool
375 type instance F Int = Char
376
377 This compiles down to:
378 axAge :: Age ~ Int
379 axF1 :: F Age ~ Bool
380 axF2 :: F Int ~ Char
381
382 Then, we can make:
383 (sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
384
385 Yikes!
386
387 The solution is _roles_, as articulated in "Generative Type Abstraction and
388 Type-level Computation" (POPL 2010), available at
389 http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
390
391 The specification for roles has evolved somewhat since that paper. For the
392 current full details, see the documentation in docs/core-spec. Here are some
393 highlights.
394
395 We label every equality with a notion of type equivalence, of which there are
396 three options: Nominal, Representational, and Phantom. A ground type is
397 nominally equivalent only with itself. A newtype (which is considered a ground
398 type in Haskell) is representationally equivalent to its representation.
399 Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
400 to denote the equivalences.
401
402 The axioms above would be:
403 axAge :: Age ~R Int
404 axF1 :: F Age ~N Bool
405 axF2 :: F Age ~N Char
406
407 Then, because transitivity applies only to coercions proving the same notion
408 of equivalence, the above construction is impossible.
409
410 However, there is still an escape hatch: we know that any two types that are
411 nominally equivalent are representationally equivalent as well. This is what
412 the form SubCo proves -- it "demotes" a nominal equivalence into a
413 representational equivalence. So, it would seem the following is possible:
414
415 sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
416
417 What saves us here is that the arguments to a type function F, lifted into a
418 coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
419 we are safe.
420
421 Roles are attached to parameters to TyCons. When lifting a TyCon into a
422 coercion (through TyConAppCo), we need to ensure that the arguments to the
423 TyCon respect their roles. For example:
424
425 data T a b = MkT a (F b)
426
427 If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
428 that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
429 the type function F branches on b's *name*, not representation. So, we say
430 that 'a' has role Representational and 'b' has role Nominal. The third role,
431 Phantom, is for parameters not used in the type's definition. Given the
432 following definition
433
434 data Q a = MkQ Int
435
436 the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
437 can construct the coercion Bool ~P Char (using UnivCo).
438
439 See the paper cited above for more examples and information.
440
441 Note [UnivCo]
442 ~~~~~~~~~~~~~
443 The UnivCo ("universal coercion") serves two rather separate functions:
444 - the implementation for unsafeCoerce#
445 - placeholder for phantom parameters in a TyConAppCo
446
447 At Representational, it asserts that two (possibly unrelated)
448 types have the same representation and can be casted to one another.
449 This form is necessary for unsafeCoerce#.
450
451 For optimisation purposes, it is convenient to allow UnivCo to appear
452 at Nominal role. If we have
453
454 data Foo a = MkFoo (F a) -- F is a type family
455
456 and we want an unsafe coercion from Foo Int to Foo Bool, then it would
457 be nice to have (TyConAppCo Foo (UnivCo Nominal Int Bool)). So, we allow
458 Nominal UnivCo's.
459
460 At Phantom role, it is used as an argument to TyConAppCo in the place
461 of a phantom parameter (a type parameter unused in the type definition).
462
463 For example:
464
465 data Q a = MkQ Int
466
467 We want a coercion for (Q Bool) ~R (Q Char).
468
469 (TyConAppCo Representational Q [UnivCo Phantom Bool Char]) does the trick.
470
471 Note [TyConAppCo roles]
472 ~~~~~~~~~~~~~~~~~~~~~~~
473 The TyConAppCo constructor has a role parameter, indicating the role at
474 which the coercion proves equality. The choice of this parameter affects
475 the required roles of the arguments of the TyConAppCo. To help explain
476 it, assume the following definition:
477
478 type instance F Int = Bool -- Axiom axF : F Int ~N Bool
479 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
480 data Foo a = MkFoo a -- Role on Foo's parameter is Representational
481
482 TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
483 For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
484 So that Foo Age ~N Foo Int does *not* hold.
485
486 TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
487 TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
488 For (TyConAppCo Representational), all arguments must have the roles
489 corresponding to the result of tyConRoles on the TyCon. This is the
490 whole point of having roles on the TyCon to begin with. So, we can
491 have Foo Age ~R Foo Int, if Foo's parameter has role R.
492
493 If a Representational TyConAppCo is over-saturated (which is otherwise fine),
494 the spill-over arguments must all be at Nominal. This corresponds to the
495 behavior for AppCo.
496
497 TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
498 All arguments must have role Phantom. This one isn't strictly
499 necessary for soundness, but this choice removes ambiguity.
500
501 The rules here dictate the roles of the parameters to mkTyConAppCo
502 (should be checked by Lint).
503
504 Note [NthCo and newtypes]
505 ~~~~~~~~~~~~~~~~~~~~~~~~~
506 Suppose we have
507
508 newtype N a = MkN Int
509 type role N representational
510
511 This yields axiom
512
513 NTCo:N :: forall a. N a ~R Int
514
515 We can then build
516
517 co :: forall a b. N a ~R N b
518 co = NTCo:N a ; sym (NTCo:N b)
519
520 for any `a` and `b`. Because of the role annotation on N, if we use
521 NthCo, we'll get out a representational coercion. That is:
522
523 NthCo 0 co :: forall a b. a ~R b
524
525 Yikes! Clearly, this is terrible. The solution is simple: forbid
526 NthCo to be used on newtypes if the internal coercion is representational.
527
528 This is not just some corner case discovered by a segfault somewhere;
529 it was discovered in the proof of soundness of roles and described
530 in the "Safe Coercions" paper (ICFP '14).
531
532 ************************************************************************
533 * *
534 \subsection{Coercion variables}
535 * *
536 ************************************************************************
537 -}
538
539 coVarName :: CoVar -> Name
540 coVarName = varName
541
542 setCoVarUnique :: CoVar -> Unique -> CoVar
543 setCoVarUnique = setVarUnique
544
545 setCoVarName :: CoVar -> Name -> CoVar
546 setCoVarName = setVarName
547
548 isCoVar :: Var -> Bool
549 isCoVar v = isCoVarType (varType v)
550
551 isCoVarType :: Type -> Bool
552 isCoVarType ty -- Tests for t1 ~# t2, the unboxed equality
553 = case splitTyConApp_maybe ty of
554 Just (tc,tys) -> (tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
555 && tys `lengthAtLeast` 2
556 Nothing -> False
557
558 tyCoVarsOfCo :: Coercion -> VarSet
559 tyCoVarsOfCo co = runFVSet $ tyCoVarsOfCoAcc co
560 -- Extracts type and coercion variables from a coercion
561
562 tyCoVarsOfCos :: [Coercion] -> VarSet
563 tyCoVarsOfCos cos = runFVSet $ tyCoVarsOfCosAcc cos
564
565 tyCoVarsOfCoAcc :: Coercion -> FV
566 tyCoVarsOfCoAcc (Refl _ ty) fv_cand in_scope acc =
567 tyVarsOfTypeAcc ty fv_cand in_scope acc
568 tyCoVarsOfCoAcc (TyConAppCo _ _ cos) fv_cand in_scope acc =
569 tyCoVarsOfCosAcc cos fv_cand in_scope acc
570 tyCoVarsOfCoAcc (AppCo co1 co2) fv_cand in_scope acc =
571 (tyCoVarsOfCoAcc co1 `unionFV` tyCoVarsOfCoAcc co2) fv_cand in_scope acc
572 tyCoVarsOfCoAcc (ForAllCo tv co) fv_cand in_scope acc =
573 delFV tv (tyCoVarsOfCoAcc co) fv_cand in_scope acc
574 tyCoVarsOfCoAcc (CoVarCo v) fv_cand in_scope acc = oneVar v fv_cand in_scope acc
575 tyCoVarsOfCoAcc (AxiomInstCo _ _ cos) fv_cand in_scope acc =
576 tyCoVarsOfCosAcc cos fv_cand in_scope acc
577 tyCoVarsOfCoAcc (UnivCo _ _ ty1 ty2) fv_cand in_scope acc =
578 (tyVarsOfTypeAcc ty1 `unionFV` tyVarsOfTypeAcc ty2) fv_cand in_scope acc
579 tyCoVarsOfCoAcc (SymCo co) fv_cand in_scope acc =
580 tyCoVarsOfCoAcc co fv_cand in_scope acc
581 tyCoVarsOfCoAcc (TransCo co1 co2) fv_cand in_scope acc =
582 (tyCoVarsOfCoAcc co1 `unionFV` tyCoVarsOfCoAcc co2) fv_cand in_scope acc
583 tyCoVarsOfCoAcc (NthCo _ co) fv_cand in_scope acc =
584 tyCoVarsOfCoAcc co fv_cand in_scope acc
585 tyCoVarsOfCoAcc (LRCo _ co) fv_cand in_scope acc =
586 tyCoVarsOfCoAcc co fv_cand in_scope acc
587 tyCoVarsOfCoAcc (InstCo co ty) fv_cand in_scope acc =
588 (tyCoVarsOfCoAcc co `unionFV` tyVarsOfTypeAcc ty) fv_cand in_scope acc
589 tyCoVarsOfCoAcc (SubCo co) fv_cand in_scope acc =
590 tyCoVarsOfCoAcc co fv_cand in_scope acc
591 tyCoVarsOfCoAcc (AxiomRuleCo _ ts cs) fv_cand in_scope acc =
592 (tyVarsOfTypesAcc ts `unionFV` tyCoVarsOfCosAcc cs) fv_cand in_scope acc
593
594 tyCoVarsOfCosAcc :: [Coercion] -> FV
595 tyCoVarsOfCosAcc (co:cos) fv_cand in_scope acc =
596 (tyCoVarsOfCoAcc co `unionFV` tyCoVarsOfCosAcc cos) fv_cand in_scope acc
597 tyCoVarsOfCosAcc [] fv_cand in_scope acc = noVars fv_cand in_scope acc
598
599 coVarsOfCo :: Coercion -> VarSet
600 -- Extract *coerction* variables only. Tiresome to repeat the code, but easy.
601 coVarsOfCo (Refl _ _) = emptyVarSet
602 coVarsOfCo (TyConAppCo _ _ cos) = coVarsOfCos cos
603 coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
604 coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
605 coVarsOfCo (CoVarCo v) = unitVarSet v
606 coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
607 coVarsOfCo (UnivCo _ _ _ _) = emptyVarSet
608 coVarsOfCo (SymCo co) = coVarsOfCo co
609 coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
610 coVarsOfCo (NthCo _ co) = coVarsOfCo co
611 coVarsOfCo (LRCo _ co) = coVarsOfCo co
612 coVarsOfCo (InstCo co _) = coVarsOfCo co
613 coVarsOfCo (SubCo co) = coVarsOfCo co
614 coVarsOfCo (AxiomRuleCo _ _ cos) = coVarsOfCos cos
615
616 coVarsOfCos :: [Coercion] -> VarSet
617 coVarsOfCos = mapUnionVarSet coVarsOfCo
618
619 coercionSize :: Coercion -> Int
620 coercionSize (Refl _ ty) = typeSize ty
621 coercionSize (TyConAppCo _ _ cos) = 1 + sum (map coercionSize cos)
622 coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
623 coercionSize (ForAllCo _ co) = 1 + coercionSize co
624 coercionSize (CoVarCo _) = 1
625 coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
626 coercionSize (UnivCo _ _ ty1 ty2) = typeSize ty1 + typeSize ty2
627 coercionSize (SymCo co) = 1 + coercionSize co
628 coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
629 coercionSize (NthCo _ co) = 1 + coercionSize co
630 coercionSize (LRCo _ co) = 1 + coercionSize co
631 coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
632 coercionSize (SubCo co) = 1 + coercionSize co
633 coercionSize (AxiomRuleCo _ tys cos) = 1 + sum (map typeSize tys)
634 + sum (map coercionSize cos)
635
636 {-
637 ************************************************************************
638 * *
639 Tidying coercions
640 * *
641 ************************************************************************
642 -}
643
644 tidyCo :: TidyEnv -> Coercion -> Coercion
645 tidyCo env@(_, subst) co
646 = go co
647 where
648 go (Refl r ty) = Refl r (tidyType env ty)
649 go (TyConAppCo r tc cos) = let args = map go cos
650 in args `seqList` TyConAppCo r tc args
651 go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
652 go (ForAllCo tv co) = ForAllCo tvp $! (tidyCo envp co)
653 where
654 (envp, tvp) = tidyTyVarBndr env tv
655 go (CoVarCo cv) = case lookupVarEnv subst cv of
656 Nothing -> CoVarCo cv
657 Just cv' -> CoVarCo cv'
658 go (AxiomInstCo con ind cos) = let args = tidyCos env cos
659 in args `seqList` AxiomInstCo con ind args
660 go (UnivCo s r ty1 ty2) = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
661 go (SymCo co) = SymCo $! go co
662 go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
663 go (NthCo d co) = NthCo d $! go co
664 go (LRCo lr co) = LRCo lr $! go co
665 go (InstCo co ty) = (InstCo $! go co) $! tidyType env ty
666 go (SubCo co) = SubCo $! go co
667
668 go (AxiomRuleCo ax tys cos) = let tys1 = map (tidyType env) tys
669 cos1 = tidyCos env cos
670 in tys1 `seqList` cos1 `seqList`
671 AxiomRuleCo ax tys1 cos1
672
673
674 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
675 tidyCos env = map (tidyCo env)
676
677 {-
678 ************************************************************************
679 * *
680 Pretty-printing coercions
681 * *
682 ************************************************************************
683
684 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
685 function is defined to use this. @pprParendCo@ is the same, except it
686 puts parens around the type, except for the atomic cases.
687 @pprParendCo@ works just by setting the initial context precedence
688 very high.
689 -}
690
691 instance Outputable Coercion where
692 ppr = pprCo
693
694 pprCo, pprParendCo :: Coercion -> SDoc
695 pprCo co = ppr_co TopPrec co
696 pprParendCo co = ppr_co TyConPrec co
697
698 ppr_co :: TyPrec -> Coercion -> SDoc
699 ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
700
701 ppr_co p co@(TyConAppCo _ tc [_,_])
702 | tc `hasKey` funTyConKey = ppr_fun_co p co
703
704 ppr_co _ (TyConAppCo r tc cos) = pprTcApp TyConPrec ppr_co tc cos <> ppr_role r
705 ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
706 pprCo co1 <+> ppr_co TyConPrec co2
707 ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
708 ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
709 ppr_co p (AxiomInstCo con index cos)
710 = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
711 (map (ppr_co TyConPrec) cos)
712
713 ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
714 case trans_co_list co [] of
715 [] -> panic "ppr_co"
716 (co:cos) -> sep ( ppr_co FunPrec co
717 : [ char ';' <+> ppr_co FunPrec co | co <- cos])
718 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
719 pprParendCo co <> ptext (sLit "@") <> pprType ty
720
721 ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
722 [pprParendType ty1, pprParendType ty2]
723 ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
724 ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
725 ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
726 ppr_co p (SubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendCo co]
727 ppr_co p (AxiomRuleCo co ts cs) = maybeParen p TopPrec $
728 ppr_axiom_rule_co co ts cs
729
730 ppr_axiom_rule_co :: CoAxiomRule -> [Type] -> [Coercion] -> SDoc
731 ppr_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
732 where
733 ppTs [] = Outputable.empty
734 ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
735 ppTs ts = ptext (sLit "@") <>
736 parens (hsep $ punctuate comma $ map pprType ts)
737
738 ppPs [] = Outputable.empty
739 ppPs [p] = pprParendCo p
740 ppPs (p : ps) = ptext (sLit "(") <+> pprCo p $$
741 vcat [ ptext (sLit ",") <+> pprCo q | q <- ps ] $$
742 ptext (sLit ")")
743
744
745
746 ppr_role :: Role -> SDoc
747 ppr_role r = underscore <> pp_role
748 where pp_role = case r of
749 Nominal -> char 'N'
750 Representational -> char 'R'
751 Phantom -> char 'P'
752
753 trans_co_list :: Coercion -> [Coercion] -> [Coercion]
754 trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
755 trans_co_list co cos = co : cos
756
757 instance Outputable LeftOrRight where
758 ppr CLeft = ptext (sLit "Left")
759 ppr CRight = ptext (sLit "Right")
760
761 ppr_fun_co :: TyPrec -> Coercion -> SDoc
762 ppr_fun_co p co = pprArrowChain p (split co)
763 where
764 split :: Coercion -> [SDoc]
765 split (TyConAppCo _ f [arg,res])
766 | f `hasKey` funTyConKey
767 = ppr_co FunPrec arg : split res
768 split co = [ppr_co TopPrec co]
769
770 ppr_forall_co :: TyPrec -> Coercion -> SDoc
771 ppr_forall_co p ty
772 = maybeParen p FunPrec $
773 sep [pprForAll tvs, ppr_co TopPrec rho]
774 where
775 (tvs, rho) = split1 [] ty
776 split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
777 split1 tvs ty = (reverse tvs, ty)
778
779 pprCoAxiom :: CoAxiom br -> SDoc
780 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
781 = hang (text "axiom" <+> ppr ax <+> dcolon)
782 2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
783
784 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
785 pprCoAxBranch = ppr_co_ax_branch pprRhs
786 where
787 pprRhs fam_tc (TyConApp tycon _)
788 | isDataFamilyTyCon fam_tc
789 = pprDataCons tycon
790 pprRhs _ rhs = ppr rhs
791
792 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
793 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
794
795 ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
796 ppr_co_ax_branch ppr_rhs
797 (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
798 (CoAxBranch { cab_tvs = tvs
799 , cab_lhs = lhs
800 , cab_rhs = rhs
801 , cab_loc = loc })
802 = foldr1 (flip hangNotEmpty 2)
803 [ pprUserForAll tvs
804 , pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
805 , text "-- Defined" <+> pprLoc loc ]
806 where
807 pprLoc loc
808 | isGoodSrcSpan loc
809 = text "at" <+> ppr (srcSpanStart loc)
810
811 | otherwise
812 = text "in" <+>
813 quotes (ppr (nameModule name))
814
815 {-
816 ************************************************************************
817 * *
818 Functions over Kinds
819 * *
820 ************************************************************************
821 -}
822
823 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
824 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
825 --
826 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
827 decomposeCo :: Arity -> Coercion -> [Coercion]
828 decomposeCo arity co
829 = [mkNthCo n co | n <- [0..(arity-1)] ]
830 -- Remember, Nth is zero-indexed
831
832 -- | Attempts to obtain the type variable underlying a 'Coercion'
833 getCoVar_maybe :: Coercion -> Maybe CoVar
834 getCoVar_maybe (CoVarCo cv) = Just cv
835 getCoVar_maybe _ = Nothing
836
837 -- first result has role equal to input; second result is Nominal
838 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
839 -- ^ Attempt to take a coercion application apart.
840 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
841 splitAppCo_maybe (TyConAppCo r tc cos)
842 | mightBeUnsaturatedTyCon tc || cos `lengthExceeds` tyConArity tc
843 , Just (cos', co') <- snocView cos
844 , Just co'' <- setNominalRole_maybe co'
845 = Just (mkTyConAppCo r tc cos', co'') -- Never create unsaturated type family apps!
846 -- Use mkTyConAppCo to preserve the invariant
847 -- that identity coercions are always represented by Refl
848 splitAppCo_maybe (Refl r ty)
849 | Just (ty1, ty2) <- splitAppTy_maybe ty
850 = Just (Refl r ty1, Refl Nominal ty2)
851 splitAppCo_maybe _ = Nothing
852
853 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
854 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
855 splitForAllCo_maybe _ = Nothing
856
857 -------------------------------------------------------
858 -- and some coercion kind stuff
859
860 coVarKind :: CoVar -> (Type,Type)
861 coVarKind cv
862 | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
863 = ASSERT(tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey)
864 (ty1,ty2)
865 | otherwise = panic "coVarKind, non coercion variable"
866
867 coVarRole :: CoVar -> Role
868 coVarRole cv
869 | tc `hasKey` eqPrimTyConKey
870 = Nominal
871 | tc `hasKey` eqReprPrimTyConKey
872 = Representational
873 | otherwise
874 = pprPanic "coVarRole: unknown tycon" (ppr cv)
875
876 where
877 tc = case tyConAppTyCon_maybe (varType cv) of
878 Just tc0 -> tc0
879 Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
880
881 -- | Makes a coercion type from two types: the types whose equality
882 -- is proven by the relevant 'Coercion'
883 mkCoercionType :: Role -> Type -> Type -> Type
884 mkCoercionType Nominal = mkPrimEqPred
885 mkCoercionType Representational = mkReprPrimEqPred
886 mkCoercionType Phantom = panic "mkCoercionType"
887
888 isReflCo :: Coercion -> Bool
889 isReflCo (Refl {}) = True
890 isReflCo _ = False
891
892 isReflCo_maybe :: Coercion -> Maybe Type
893 isReflCo_maybe (Refl _ ty) = Just ty
894 isReflCo_maybe _ = Nothing
895
896 {-
897 ************************************************************************
898 * *
899 Building coercions
900 * *
901 ************************************************************************
902
903 Note [Role twiddling functions]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905
906 There are a plethora of functions for twiddling roles:
907
908 mkSubCo: Requires a nominal input coercion and always produces a
909 representational output. This is used when you (the programmer) are sure you
910 know exactly that role you have and what you want.
911
912 downgradeRole_maybe: This function takes both the input role and the output role
913 as parameters. (The *output* role comes first!) It can only *downgrade* a
914 role -- that is, change it from N to R or P, or from R to P. This one-way
915 behavior is why there is the "_maybe". If an upgrade is requested, this
916 function produces Nothing. This is used when you need to change the role of a
917 coercion, but you're not sure (as you're writing the code) of which roles are
918 involved.
919
920 This function could have been written using coercionRole to ascertain the role
921 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
922 often knows the input role. So, this is more efficient.
923
924 downgradeRole: This is just like downgradeRole_maybe, but it panics if the conversion
925 isn't a downgrade.
926
927 setNominalRole_maybe: This is the only function that can *upgrade* a coercion. The result
928 (if it exists) is always Nominal. The input can be at any role. It works on a
929 "best effort" basis, as it should never be strictly necessary to upgrade a coercion
930 during compilation. It is currently only used within GHC in splitAppCo_maybe. In order
931 to be a proper inverse of mkAppCo, the second coercion that splitAppCo_maybe returns
932 must be nominal. But, it's conceivable that splitAppCo_maybe is operating over a
933 TyConAppCo that uses a representational coercion. Hence the need for setNominalRole_maybe.
934 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus, it is
935 not absolutely critical that setNominalRole_maybe be complete.
936
937 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
938 UnivCos are perfectly type-safe, whereas representational and nominal ones are
939 not. Indeed, `unsafeCoerce` is implemented via a representational UnivCo.
940 (Nominal ones are no worse than representational ones, so this function *will*
941 change a UnivCo Representational to a UnivCo Nominal.)
942
943 Conal Elliott also came across a need for this function while working with the GHC
944 API, as he was decomposing Core casts. The Core casts use representational coercions,
945 as they must, but his use case required nominal coercions (he was building a GADT).
946 So, that's why this function is exported from this module.
947
948 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as appropriate?
949 I (Richard E.) have decided not to do this, because upgrading a role is bizarre and
950 a caller should have to ask for this behavior explicitly.
951 -}
952
953 mkCoVarCo :: CoVar -> Coercion
954 -- cv :: s ~# t
955 mkCoVarCo cv
956 | ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
957 | otherwise = CoVarCo cv
958 where
959 (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
960
961 mkReflCo :: Role -> Type -> Coercion
962 mkReflCo = Refl
963
964 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
965 -- mkAxInstCo can legitimately be called over-staturated;
966 -- i.e. with more type arguments than the coercion requires
967 mkAxInstCo role ax index tys
968 | arity == n_tys = downgradeRole role ax_role $ AxiomInstCo ax_br index rtys
969 | otherwise = ASSERT( arity < n_tys )
970 downgradeRole role ax_role $
971 foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
972 (drop arity rtys)
973 where
974 n_tys = length tys
975 ax_br = toBranchedAxiom ax
976 branch = coAxiomNthBranch ax_br index
977 arity = length $ coAxBranchTyVars branch
978 arg_roles = coAxBranchRoles branch
979 rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
980 ax_role = coAxiomRole ax
981
982 -- to be used only with unbranched axioms
983 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> Coercion
984 mkUnbranchedAxInstCo role ax tys
985 = mkAxInstCo role ax 0 tys
986
987 mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
988 -- Instantiate the axiom with specified types,
989 -- returning the instantiated RHS
990 -- A companion to mkAxInstCo:
991 -- mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
992 mkAxInstLHS ax index tys
993 | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
994 , (tys1, tys2) <- splitAtList tvs tys
995 = ASSERT( tvs `equalLength` tys1 )
996 mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
997
998 mkAxInstRHS ax index tys
999 | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
1000 , (tys1, tys2) <- splitAtList tvs tys
1001 = ASSERT( tvs `equalLength` tys1 )
1002 mkAppTys (substTyWith tvs tys1 rhs) tys2
1003
1004 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
1005 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
1006
1007 -- | Apply a 'Coercion' to another 'Coercion'.
1008 -- The second coercion must be Nominal, unless the first is Phantom.
1009 -- If the first is Phantom, then the second can be either Phantom or Nominal.
1010 mkAppCo :: Coercion -> Coercion -> Coercion
1011 mkAppCo co1 co2 = mkAppCoFlexible co1 Nominal co2
1012 -- Note, mkAppCo is careful to maintain invariants regarding
1013 -- where Refl constructors appear; see the comments in the definition
1014 -- of Coercion and the Note [Refl invariant] in types/TypeRep.hs.
1015
1016 -- | Apply a 'Coercion' to another 'Coercion'.
1017 -- The second 'Coercion's role is given, making this more flexible than
1018 -- 'mkAppCo'.
1019 mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
1020 mkAppCoFlexible (Refl r ty1) _ (Refl _ ty2)
1021 = Refl r (mkAppTy ty1 ty2)
1022 mkAppCoFlexible (Refl r ty1) r2 co2
1023 | Just (tc, tys) <- splitTyConApp_maybe ty1
1024 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
1025 = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
1026 where
1027 zip_roles (r1:_) [] = [downgradeRole r1 r2 co2]
1028 zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
1029 zip_roles _ _ = panic "zip_roles" -- but the roles are infinite...
1030 mkAppCoFlexible (TyConAppCo r tc cos) r2 co
1031 = case r of
1032 Nominal -> ASSERT( r2 == Nominal )
1033 TyConAppCo Nominal tc (cos ++ [co])
1034 Representational -> TyConAppCo Representational tc (cos ++ [co'])
1035 where new_role = (tyConRolesX Representational tc) !! (length cos)
1036 co' = downgradeRole new_role r2 co
1037 Phantom -> TyConAppCo Phantom tc (cos ++ [mkPhantomCo co])
1038
1039 mkAppCoFlexible co1 _r2 co2 = ASSERT( _r2 == Nominal )
1040 AppCo co1 co2
1041
1042
1043 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
1044 -- See also 'mkAppCo'.
1045 mkAppCos :: Coercion -> [Coercion] -> Coercion
1046 mkAppCos co1 cos = foldl mkAppCo co1 cos
1047
1048 -- | Apply a type constructor to a list of coercions. It is the
1049 -- caller's responsibility to get the roles correct on argument coercions.
1050 mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
1051 mkTyConAppCo r tc cos
1052 -- Expand type synonyms
1053 | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
1054 = mkAppCos (liftCoSubst r tv_co_prs rhs_ty) leftover_cos
1055
1056 | Just tys <- traverse isReflCo_maybe cos
1057 = Refl r (mkTyConApp tc tys) -- See Note [Refl invariant]
1058
1059 | otherwise = TyConAppCo r tc cos
1060
1061 -- | Make a function 'Coercion' between two other 'Coercion's
1062 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
1063 mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
1064
1065 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
1066 mkForAllCo :: Var -> Coercion -> Coercion
1067 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
1068 mkForAllCo tv (Refl r ty) = ASSERT( isTyVar tv ) Refl r (mkForAllTy tv ty)
1069 mkForAllCo tv co = ASSERT( isTyVar tv ) ForAllCo tv co
1070
1071 -------------------------------
1072
1073 -- | Create a symmetric version of the given 'Coercion' that asserts
1074 -- equality between the same types but in the other "direction", so
1075 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
1076 mkSymCo :: Coercion -> Coercion
1077
1078 -- Do a few simple optimizations, but don't bother pushing occurrences
1079 -- of symmetry to the leaves; the optimizer will take care of that.
1080 mkSymCo co@(Refl {}) = co
1081 mkSymCo (UnivCo s r ty1 ty2) = UnivCo s r ty2 ty1
1082 mkSymCo (SymCo co) = co
1083 mkSymCo co = SymCo co
1084
1085 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
1086 mkTransCo :: Coercion -> Coercion -> Coercion
1087 mkTransCo (Refl {}) co = co
1088 mkTransCo co (Refl {}) = co
1089 mkTransCo co1 co2 = TransCo co1 co2
1090
1091 -- the Role is the desired one. It is the caller's responsibility to make
1092 -- sure this request is reasonable
1093 mkNthCoRole :: Role -> Int -> Coercion -> Coercion
1094 mkNthCoRole role n co
1095 = downgradeRole role nth_role $ nth_co
1096 where
1097 nth_co = mkNthCo n co
1098 nth_role = coercionRole nth_co
1099
1100 mkNthCo :: Int -> Coercion -> Coercion
1101 mkNthCo n (Refl r ty) = ASSERT( ok_tc_app ty n )
1102 Refl r' (tyConAppArgN n ty)
1103 where tc = tyConAppTyCon ty
1104 r' = nthRole r tc n
1105 mkNthCo n co = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
1106 NthCo n co
1107 where
1108 Pair _ty1 _ty2 = coercionKind co
1109
1110
1111 mkLRCo :: LeftOrRight -> Coercion -> Coercion
1112 mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
1113 mkLRCo lr co = LRCo lr co
1114
1115 ok_tc_app :: Type -> Int -> Bool
1116 ok_tc_app ty n = case splitTyConApp_maybe ty of
1117 Just (_, tys) -> tys `lengthExceeds` n
1118 Nothing -> False
1119
1120 -- | Instantiates a 'Coercion' with a 'Type' argument.
1121 mkInstCo :: Coercion -> Type -> Coercion
1122 mkInstCo co ty = InstCo co ty
1123
1124 -- | Manufacture an unsafe coercion from thin air.
1125 -- Currently (May 14) this is used only to implement the
1126 -- @unsafeCoerce#@ primitive. Optimise by pushing
1127 -- down through type constructors.
1128 mkUnsafeCo :: Type -> Type -> Coercion
1129 mkUnsafeCo = mkUnivCo (fsLit "mkUnsafeCo") Representational
1130
1131 mkUnivCo :: FastString -> Role -> Type -> Type -> Coercion
1132 mkUnivCo prov role ty1 ty2
1133 | ty1 `eqType` ty2 = Refl role ty1
1134 | otherwise = UnivCo prov role ty1 ty2
1135
1136 mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
1137 mkAxiomRuleCo = AxiomRuleCo
1138
1139 -- input coercion is Nominal; see also Note [Role twiddling functions]
1140 mkSubCo :: Coercion -> Coercion
1141 mkSubCo (Refl Nominal ty) = Refl Representational ty
1142 mkSubCo (TyConAppCo Nominal tc cos)
1143 = TyConAppCo Representational tc (applyRoles tc cos)
1144 mkSubCo (UnivCo s Nominal ty1 ty2) = UnivCo s Representational ty1 ty2
1145 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
1146 SubCo co
1147
1148 -- only *downgrades* a role. See Note [Role twiddling functions]
1149 downgradeRole_maybe :: Role -- desired role
1150 -> Role -- current role
1151 -> Coercion
1152 -> Maybe Coercion
1153 -- In (downgradeRole_maybe dr cr co) it's a precondition that
1154 -- cr = coercionRole co
1155 downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
1156 downgradeRole_maybe Nominal Representational _ = Nothing
1157 downgradeRole_maybe Phantom Phantom co = Just co
1158 downgradeRole_maybe Phantom _ co = Just (mkPhantomCo co)
1159 downgradeRole_maybe _ Phantom _ = Nothing
1160 downgradeRole_maybe _ _ co = Just co
1161
1162 -- panics if the requested conversion is not a downgrade.
1163 -- See also Note [Role twiddling functions]
1164 downgradeRole :: Role -- desired role
1165 -> Role -- current role
1166 -> Coercion -> Coercion
1167 downgradeRole r1 r2 co
1168 = case downgradeRole_maybe r1 r2 co of
1169 Just co' -> co'
1170 Nothing -> pprPanic "downgradeRole" (ppr co)
1171
1172 -- Converts a coercion to be nominal, if possible.
1173 -- See also Note [Role twiddling functions]
1174 setNominalRole_maybe :: Coercion -> Maybe Coercion
1175 setNominalRole_maybe co
1176 | Nominal <- coercionRole co = Just co
1177 setNominalRole_maybe (SubCo co) = Just co
1178 setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
1179 setNominalRole_maybe (TyConAppCo Representational tc coes)
1180 = do { cos' <- mapM setNominalRole_maybe coes
1181 ; return $ TyConAppCo Nominal tc cos' }
1182 setNominalRole_maybe (UnivCo s Representational ty1 ty2) = Just $ UnivCo s Nominal ty1 ty2
1183 -- We do *not* promote UnivCo Phantom, as that's unsafe.
1184 -- UnivCo Nominal is no more unsafe than UnivCo Representational
1185 setNominalRole_maybe (TransCo co1 co2)
1186 = TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
1187 setNominalRole_maybe (AppCo co1 co2)
1188 = AppCo <$> setNominalRole_maybe co1 <*> pure co2
1189 setNominalRole_maybe (ForAllCo tv co)
1190 = ForAllCo tv <$> setNominalRole_maybe co
1191 setNominalRole_maybe (NthCo n co)
1192 = NthCo n <$> setNominalRole_maybe co
1193 setNominalRole_maybe (InstCo co ty)
1194 = InstCo <$> setNominalRole_maybe co <*> pure ty
1195 setNominalRole_maybe _ = Nothing
1196
1197 -- takes any coercion and turns it into a Phantom coercion
1198 mkPhantomCo :: Coercion -> Coercion
1199 mkPhantomCo co
1200 | Just ty <- isReflCo_maybe co = Refl Phantom ty
1201 | Pair ty1 ty2 <- coercionKind co = UnivCo (fsLit "mkPhantomCo") Phantom ty1 ty2
1202 -- don't optimise here... wait for OptCoercion
1203
1204 -- All input coercions are assumed to be Nominal,
1205 -- or, if Role is Phantom, the Coercion can be Phantom, too.
1206 applyRole :: Role -> Coercion -> Coercion
1207 applyRole Nominal = id
1208 applyRole Representational = mkSubCo
1209 applyRole Phantom = mkPhantomCo
1210
1211 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
1212 applyRoles :: TyCon -> [Coercion] -> [Coercion]
1213 applyRoles tc cos
1214 = zipWith applyRole (tyConRolesX Representational tc) cos
1215
1216 -- the Role parameter is the Role of the TyConAppCo
1217 -- defined here because this is intimiately concerned with the implementation
1218 -- of TyConAppCo
1219 tyConRolesX :: Role -> TyCon -> [Role]
1220 tyConRolesX Representational tc = tyConRoles tc ++ repeat Nominal
1221 tyConRolesX role _ = repeat role
1222
1223 nthRole :: Role -> TyCon -> Int -> Role
1224 nthRole Nominal _ _ = Nominal
1225 nthRole Phantom _ _ = Phantom
1226 nthRole Representational tc n
1227 = (tyConRolesX Representational tc) !! n
1228
1229 ltRole :: Role -> Role -> Bool
1230 -- Is one role "less" than another?
1231 -- Nominal < Representational < Phantom
1232 ltRole Phantom _ = False
1233 ltRole Representational Phantom = True
1234 ltRole Representational _ = False
1235 ltRole Nominal Nominal = False
1236 ltRole Nominal _ = True
1237
1238 -- See note [Newtype coercions] in TyCon
1239 -- | Create a coercion constructor (axiom) suitable for the given
1240 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
1241 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
1242 -- the type the appropriate right hand side of the @newtype@, with
1243 -- the free variables a subset of those 'TyVar's.
1244 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
1245 mkNewTypeCo name tycon tvs roles rhs_ty
1246 = CoAxiom { co_ax_unique = nameUnique name
1247 , co_ax_name = name
1248 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
1249 , co_ax_role = Representational
1250 , co_ax_tc = tycon
1251 , co_ax_branches = unbranched branch }
1252 where branch = CoAxBranch { cab_loc = getSrcSpan name
1253 , cab_tvs = tvs
1254 , cab_lhs = mkTyVarTys tvs
1255 , cab_roles = roles
1256 , cab_rhs = rhs_ty
1257 , cab_incomps = [] }
1258
1259 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
1260 mkPiCos r vs co = foldr (mkPiCo r) co vs
1261
1262 mkPiCo :: Role -> Var -> Coercion -> Coercion
1263 mkPiCo r v co | isTyVar v = mkForAllCo v co
1264 | otherwise = mkFunCo r (mkReflCo r (varType v)) co
1265
1266 -- The first coercion *must* be Nominal.
1267 mkCoCast :: Coercion -> Coercion -> Coercion
1268 -- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
1269 mkCoCast c g
1270 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
1271 where
1272 -- g :: (s1 ~# s2) ~# (t1 ~# t2)
1273 -- g1 :: s1 ~# t1
1274 -- g2 :: s2 ~# t2
1275 [_reflk, g1, g2] = decomposeCo 3 g
1276 -- Remember, (~#) :: forall k. k -> k -> *
1277 -- so it takes *three* arguments, not two
1278
1279 {-
1280 ************************************************************************
1281 * *
1282 Newtypes
1283 * *
1284 ************************************************************************
1285 -}
1286
1287 -- | If @co :: T ts ~ rep_ty@ then:
1288 --
1289 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
1290 --
1291 -- Checks for a newtype, and for being saturated
1292 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
1293 instNewTyCon_maybe tc tys
1294 | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype
1295 , tvs `leLength` tys -- Check saturated enough
1296 = Just ( applyTysX tvs ty tys
1297 , mkUnbranchedAxInstCo Representational co_tc tys)
1298 | otherwise
1299 = Nothing
1300
1301 {-
1302 ************************************************************************
1303 * *
1304 Type normalisation
1305 * *
1306 ************************************************************************
1307 -}
1308
1309 -- | A function to check if we can reduce a type by one step. Used
1310 -- with 'topNormaliseTypeX_maybe'.
1311 type NormaliseStepper = RecTcChecker
1312 -> TyCon -- tc
1313 -> [Type] -- tys
1314 -> NormaliseStepResult
1315
1316 -- | The result of stepping in a normalisation function.
1317 -- See 'topNormaliseTypeX_maybe'.
1318 data NormaliseStepResult
1319 = NS_Done -- ^ Nothing more to do
1320 | NS_Abort -- ^ Utter failure. The outer function should fail too.
1321 | NS_Step RecTcChecker Type Coercion -- ^ We stepped, yielding new bits;
1322 -- ^ co :: old type ~ new type
1323
1324 modifyStepResultCo :: (Coercion -> Coercion)
1325 -> NormaliseStepResult -> NormaliseStepResult
1326 modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
1327 modifyStepResultCo _ result = result
1328
1329 -- | Try one stepper and then try the next,
1330 -- if the first doesn't make progress.
1331 -- So if it returns NS_Done, it means that both steppers are satisfied
1332 composeSteppers :: NormaliseStepper -> NormaliseStepper
1333 -> NormaliseStepper
1334 composeSteppers step1 step2 rec_nts tc tys
1335 = case step1 rec_nts tc tys of
1336 success@(NS_Step {}) -> success
1337 NS_Done -> step2 rec_nts tc tys
1338 NS_Abort -> NS_Abort
1339
1340 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
1341 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
1342 unwrapNewTypeStepper :: NormaliseStepper
1343 unwrapNewTypeStepper rec_nts tc tys
1344 | Just (ty', co) <- instNewTyCon_maybe tc tys
1345 = case checkRecTc rec_nts tc of
1346 Just rec_nts' -> NS_Step rec_nts' ty' co
1347 Nothing -> NS_Abort
1348
1349 | otherwise
1350 = NS_Done
1351
1352 -- | A general function for normalising the top-level of a type. It continues
1353 -- to use the provided 'NormaliseStepper' until that function fails, and then
1354 -- this function returns. The roles of the coercions produced by the
1355 -- 'NormaliseStepper' must all be the same, which is the role returned from
1356 -- the call to 'topNormaliseTypeX_maybe'.
1357 topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
1358 topNormaliseTypeX_maybe stepper
1359 = go initRecTc Nothing
1360 where
1361 go rec_nts mb_co1 ty
1362 | Just (tc, tys) <- splitTyConApp_maybe ty
1363 = case stepper rec_nts tc tys of
1364 NS_Step rec_nts' ty' co2
1365 -> go rec_nts' (mb_co1 `trans` co2) ty'
1366
1367 NS_Done -> all_done
1368 NS_Abort -> Nothing
1369
1370 | otherwise
1371 = all_done
1372 where
1373 all_done | Just co <- mb_co1 = Just (co, ty)
1374 | otherwise = Nothing
1375
1376 Nothing `trans` co2 = Just co2
1377 (Just co1) `trans` co2 = Just (co1 `mkTransCo` co2)
1378
1379 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
1380 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
1381 -- This function strips off @newtype@ layers enough to reveal something that isn't
1382 -- a @newtype@, or responds False to ok_tc. Specifically, here's the invariant:
1383 --
1384 -- > topNormaliseNewType_maybe ty = Just (co, ty')
1385 --
1386 -- then (a) @co : ty0 ~ ty'@.
1387 -- (b) ty' is not a newtype.
1388 --
1389 -- The function returns @Nothing@ for non-@newtypes@,
1390 -- or unsaturated applications
1391 --
1392 -- This function does *not* look through type families, because it has no access to
1393 -- the type family environment. If you do have that at hand, consider to use
1394 -- topNormaliseType_maybe, which should be a drop-in replacement for
1395 -- topNormaliseNewType_maybe
1396 --
1397 topNormaliseNewType_maybe ty
1398 = topNormaliseTypeX_maybe unwrapNewTypeStepper ty
1399
1400 {-
1401 ************************************************************************
1402 * *
1403 Equality of coercions
1404 * *
1405 ************************************************************************
1406 -}
1407
1408 -- | Determines syntactic equality of coercions
1409 coreEqCoercion :: Coercion -> Coercion -> Bool
1410 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
1411 where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
1412
1413 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
1414 coreEqCoercion2 env (Refl eq1 ty1) (Refl eq2 ty2) = eq1 == eq2 && eqTypeX env ty1 ty2
1415 coreEqCoercion2 env (TyConAppCo eq1 tc1 cos1) (TyConAppCo eq2 tc2 cos2)
1416 = eq1 == eq2 && tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
1417
1418 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
1419 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
1420
1421 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
1422 = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
1423
1424 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
1425 = rnOccL env cv1 == rnOccR env cv2
1426
1427 coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
1428 = con1 == con2
1429 && ind1 == ind2
1430 && all2 (coreEqCoercion2 env) cos1 cos2
1431
1432 -- the provenance string is just a note, so don't use in comparisons
1433 coreEqCoercion2 env (UnivCo _ r1 ty11 ty12) (UnivCo _ r2 ty21 ty22)
1434 = r1 == r2 && eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
1435
1436 coreEqCoercion2 env (SymCo co1) (SymCo co2)
1437 = coreEqCoercion2 env co1 co2
1438
1439 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
1440 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
1441
1442 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
1443 = d1 == d2 && coreEqCoercion2 env co1 co2
1444 coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
1445 = d1 == d2 && coreEqCoercion2 env co1 co2
1446
1447 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
1448 = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
1449
1450 coreEqCoercion2 env (SubCo co1) (SubCo co2)
1451 = coreEqCoercion2 env co1 co2
1452
1453 coreEqCoercion2 env (AxiomRuleCo a1 ts1 cs1) (AxiomRuleCo a2 ts2 cs2)
1454 = a1 == a2 && all2 (eqTypeX env) ts1 ts2 && all2 (coreEqCoercion2 env) cs1 cs2
1455
1456 coreEqCoercion2 _ _ _ = False
1457
1458 {-
1459 ************************************************************************
1460 * *
1461 Substitution of coercions
1462 * *
1463 ************************************************************************
1464 -}
1465
1466 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
1467 -- doing a \"lifting\" substitution)
1468 type CvSubstEnv = VarEnv Coercion
1469
1470 emptyCvSubstEnv :: CvSubstEnv
1471 emptyCvSubstEnv = emptyVarEnv
1472
1473 data CvSubst
1474 = CvSubst InScopeSet -- The in-scope type variables
1475 TvSubstEnv -- Substitution of types
1476 CvSubstEnv -- Substitution of coercions
1477
1478 instance Outputable CvSubst where
1479 ppr (CvSubst ins tenv cenv)
1480 = brackets $ sep[ ptext (sLit "CvSubst"),
1481 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
1482 nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
1483 nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
1484
1485 emptyCvSubst :: CvSubst
1486 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
1487
1488 isEmptyCvSubst :: CvSubst -> Bool
1489 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
1490
1491 getCvInScope :: CvSubst -> InScopeSet
1492 getCvInScope (CvSubst in_scope _ _) = in_scope
1493
1494 zapCvSubstEnv :: CvSubst -> CvSubst
1495 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
1496
1497 cvTvSubst :: CvSubst -> TvSubst
1498 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
1499
1500 tvCvSubst :: TvSubst -> CvSubst
1501 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
1502
1503 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
1504 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
1505 = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
1506
1507 extendTvSubstAndInScope :: CvSubst -> TyVar -> Type -> CvSubst
1508 extendTvSubstAndInScope (CvSubst in_scope tenv cenv) tv ty
1509 = CvSubst (in_scope `extendInScopeSetSet` tyVarsOfType ty)
1510 (extendVarEnv tenv tv ty)
1511 cenv
1512
1513 extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
1514 -- Also extends the in-scope set
1515 extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
1516 = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
1517 tenv
1518 (extendVarEnv cenv cv co)
1519
1520 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
1521 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
1522 = ASSERT( isCoVar old_var )
1523 (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
1524 where
1525 -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
1526 -- In that case, mkCoVarCo will return a ReflCoercion, and
1527 -- we want to substitute that (not new_var) for old_var
1528 new_co = mkCoVarCo new_var
1529 no_change = new_var == old_var && not (isReflCo new_co)
1530
1531 new_cenv | no_change = delVarEnv cenv old_var
1532 | otherwise = extendVarEnv cenv old_var new_co
1533
1534 new_var = uniqAway in_scope subst_old_var
1535 subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
1536 -- It's important to do the substitution for coercions,
1537 -- because they can have free type variables
1538
1539 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
1540 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
1541 = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
1542 (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
1543
1544 mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
1545 mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
1546
1547 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
1548 zipOpenCvSubst vs cos
1549 | debugIsOn && (length vs /= length cos)
1550 = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
1551 | otherwise
1552 = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
1553
1554 substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
1555 substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
1556
1557 substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
1558 substCoWithTys in_scope tvs tys co
1559 | debugIsOn && (length tvs /= length tys)
1560 = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
1561 | otherwise
1562 = ASSERT( length tvs == length tys )
1563 substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
1564
1565 -- | Substitute within a 'Coercion'
1566 substCo :: CvSubst -> Coercion -> Coercion
1567 substCo subst co | isEmptyCvSubst subst = co
1568 | otherwise = subst_co subst co
1569
1570 -- | Substitute within several 'Coercion's
1571 substCos :: CvSubst -> [Coercion] -> [Coercion]
1572 substCos subst cos | isEmptyCvSubst subst = cos
1573 | otherwise = map (substCo subst) cos
1574
1575 substTy :: CvSubst -> Type -> Type
1576 substTy subst = Type.substTy (cvTvSubst subst)
1577
1578 subst_co :: CvSubst -> Coercion -> Coercion
1579 subst_co subst co
1580 = go co
1581 where
1582 go_ty :: Type -> Type
1583 go_ty = Coercion.substTy subst
1584
1585 go :: Coercion -> Coercion
1586 go (Refl eq ty) = Refl eq $! go_ty ty
1587 go (TyConAppCo eq tc cos) = let args = map go cos
1588 in args `seqList` TyConAppCo eq tc args
1589 go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
1590 go (ForAllCo tv co) = case substTyVarBndr subst tv of
1591 (subst', tv') ->
1592 ForAllCo tv' $! subst_co subst' co
1593 go (CoVarCo cv) = substCoVar subst cv
1594 go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
1595 go (UnivCo s r ty1 ty2) = (UnivCo s r $! go_ty ty1) $! go_ty ty2
1596 go (SymCo co) = mkSymCo (go co)
1597 go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
1598 go (NthCo d co) = mkNthCo d (go co)
1599 go (LRCo lr co) = mkLRCo lr (go co)
1600 go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
1601 go (SubCo co) = mkSubCo (go co)
1602 go (AxiomRuleCo co ts cs) = let ts1 = map go_ty ts
1603 cs1 = map go cs
1604 in ts1 `seqList` cs1 `seqList`
1605 AxiomRuleCo co ts1 cs1
1606
1607
1608
1609 substCoVar :: CvSubst -> CoVar -> Coercion
1610 substCoVar (CvSubst in_scope _ cenv) cv
1611 | Just co <- lookupVarEnv cenv cv = co
1612 | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
1613 | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
1614 ASSERT( isCoVar cv ) CoVarCo cv
1615
1616 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
1617 substCoVars subst cvs = map (substCoVar subst) cvs
1618
1619 lookupTyVar :: CvSubst -> TyVar -> Maybe Type
1620 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
1621
1622 lookupCoVar :: CvSubst -> Var -> Maybe Coercion
1623 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
1624
1625 {-
1626 ************************************************************************
1627 * *
1628 "Lifting" substitution
1629 [(TyVar,Coercion)] -> Type -> Coercion
1630 * *
1631 ************************************************************************
1632
1633 Note [Lifting coercions over types: liftCoSubst]
1634 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1635 The KPUSH rule deals with this situation
1636 data T a = MkK (a -> Maybe a)
1637 g :: T t1 ~ K t2
1638 x :: t1 -> Maybe t1
1639
1640 case (K @t1 x) |> g of
1641 K (y:t2 -> Maybe t2) -> rhs
1642
1643 We want to push the coercion inside the constructor application.
1644 So we do this
1645
1646 g' :: t1~t2 = Nth 0 g
1647
1648 case K @t2 (x |> g' -> Maybe g') of
1649 K (y:t2 -> Maybe t2) -> rhs
1650
1651 The crucial operation is that we
1652 * take the type of K's argument: a -> Maybe a
1653 * and substitute g' for a
1654 thus giving *coercion*. This is what liftCoSubst does.
1655
1656 Note [Substituting kinds in liftCoSubst]
1657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1658 We need to take care with kind polymorphism. Suppose
1659 K :: forall k (a:k). (forall b:k. a -> b) -> T k a
1660
1661 Now given (K @kk1 @ty1 v) |> g) where
1662 g :: T kk1 ty1 ~ T kk2 ty2
1663 we want to compute
1664 (forall b:k a->b) [ Nth 0 g/k, Nth 1 g/a ]
1665 Notice that we MUST substitute for 'k'; this happens in
1666 liftCoSubstTyVarBndr. But what should we substitute?
1667 We need to take b's kind 'k' and return a Kind, not a Coercion!
1668
1669 Happily we can do this because we know that all kind coercions
1670 ((Nth 0 g) in this case) are Refl. So we need a special purpose
1671 subst_kind: LiftCoSubst -> Kind -> Kind
1672 that expects a Refl coercion (or something equivalent to Refl)
1673 when it looks up a kind variable.
1674 -}
1675
1676 -- ----------------------------------------------------
1677 -- See Note [Lifting coercions over types: liftCoSubst]
1678 -- ----------------------------------------------------
1679
1680 data LiftCoSubst = LCS InScopeSet LiftCoEnv
1681
1682 type LiftCoEnv = VarEnv Coercion
1683 -- Maps *type variables* to *coercions*
1684 -- That's the whole point of this function!
1685
1686 liftCoSubstWith :: Role -> [TyVar] -> [Coercion] -> Type -> Coercion
1687 liftCoSubstWith r tvs cos ty
1688 = liftCoSubst r (zipEqual "liftCoSubstWith" tvs cos) ty
1689
1690 liftCoSubst :: Role -> [(TyVar,Coercion)] -> Type -> Coercion
1691 liftCoSubst r prs ty
1692 | null prs = Refl r ty
1693 | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
1694 (mkVarEnv prs)) r ty
1695
1696 -- | The \"lifting\" operation which substitutes coercions for type
1697 -- variables in a type to produce a coercion.
1698 --
1699 -- For the inverse operation, see 'liftCoMatch'
1700
1701 -- The Role parameter is the _desired_ role
1702 ty_co_subst :: LiftCoSubst -> Role -> Type -> Coercion
1703 ty_co_subst subst role ty
1704 = go role ty
1705 where
1706 go Phantom ty = lift_phantom ty
1707 go role (TyVarTy tv) = liftCoSubstTyVar subst role tv
1708 `orElse` Refl role (TyVarTy tv)
1709 -- A type variable from a non-cloned forall
1710 -- won't be in the substitution
1711 go role (AppTy ty1 ty2) = mkAppCo (go role ty1) (go Nominal ty2)
1712 go role (TyConApp tc tys) = mkTyConAppCo role tc
1713 (zipWith go (tyConRolesX role tc) tys)
1714 -- IA0_NOTE: Do we need to do anything
1715 -- about kind instantiations? I don't think
1716 -- so. see Note [Kind coercions]
1717 go role (FunTy ty1 ty2) = mkFunCo role (go role ty1) (go role ty2)
1718 go role (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' role ty)
1719 where
1720 (subst', v') = liftCoSubstTyVarBndr subst v
1721 go role ty@(LitTy {}) = ASSERT( role == Nominal )
1722 mkReflCo role ty
1723
1724 lift_phantom ty = mkUnivCo (fsLit "lift_phantom")
1725 Phantom (liftCoSubstLeft subst ty)
1726 (liftCoSubstRight subst ty)
1727
1728 {-
1729 Note [liftCoSubstTyVar]
1730 ~~~~~~~~~~~~~~~~~~~~~~~
1731 This function can fail (i.e., return Nothing) for two separate reasons:
1732 1) The variable is not in the substutition
1733 2) The coercion found is of too low a role
1734
1735 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
1736 also in matchAxiom in OptCoercion. From liftCoSubst, the so-called lifting
1737 lemma guarantees that the roles work out. If we fail for reason 2) in this
1738 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
1739 failing for reason 2) is fine. matchAxiom is trying to find a set of coercions
1740 that match, but it may fail, and this is healthy behavior. Bottom line: if
1741 you find that liftCoSubst is doing weird things (like leaving out-of-scope
1742 variables lying around), disable coercion optimization (bypassing matchAxiom)
1743 and use downgradeRole instead of downgradeRole_maybe. The panic will then happen,
1744 and you may learn something useful.
1745 -}
1746
1747 liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
1748 liftCoSubstTyVar (LCS _ cenv) r tv
1749 = do { co <- lookupVarEnv cenv tv
1750 ; let co_role = coercionRole co -- could theoretically take this as
1751 -- a parameter, but painful
1752 ; downgradeRole_maybe r co_role co } -- see Note [liftCoSubstTyVar]
1753
1754 liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
1755 liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
1756 = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
1757 where
1758 new_cenv | no_change = delVarEnv cenv old_var
1759 | otherwise = extendVarEnv cenv old_var (Refl Nominal (TyVarTy new_var))
1760
1761 no_change = no_kind_change && (new_var == old_var)
1762
1763 new_var1 = uniqAway in_scope old_var
1764
1765 old_ki = tyVarKind old_var
1766 no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
1767 new_var | no_kind_change = new_var1
1768 | otherwise = setTyVarKind new_var1 (subst_kind subst old_ki)
1769
1770 -- map every variable to the type on the *left* of its mapped coercion
1771 liftCoSubstLeft :: LiftCoSubst -> Type -> Type
1772 liftCoSubstLeft (LCS in_scope cenv) ty
1773 = Type.substTy (mkTvSubst in_scope (mapVarEnv (pFst . coercionKind) cenv)) ty
1774
1775 -- same, but to the type on the right
1776 liftCoSubstRight :: LiftCoSubst -> Type -> Type
1777 liftCoSubstRight (LCS in_scope cenv) ty
1778 = Type.substTy (mkTvSubst in_scope (mapVarEnv (pSnd . coercionKind) cenv)) ty
1779
1780 subst_kind :: LiftCoSubst -> Kind -> Kind
1781 -- See Note [Substituting kinds in liftCoSubst]
1782 subst_kind subst@(LCS _ cenv) kind
1783 = go kind
1784 where
1785 go (LitTy n) = n `seq` LitTy n
1786 go (TyVarTy kv) = subst_kv kv
1787 go (TyConApp tc tys) = let args = map go tys
1788 in args `seqList` TyConApp tc args
1789
1790 go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
1791 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
1792 go (ForAllTy tv ty) = case liftCoSubstTyVarBndr subst tv of
1793 (subst', tv') ->
1794 ForAllTy tv' $! (subst_kind subst' ty)
1795
1796 subst_kv kv
1797 | Just co <- lookupVarEnv cenv kv
1798 , let co_kind = coercionKind co
1799 = ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
1800 pFst co_kind
1801 | otherwise
1802 = TyVarTy kv
1803
1804 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1805 -- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
1806 -- That is, it matches a type against a coercion of the same
1807 -- "shape", and returns a lifting substitution which could have been
1808 -- used to produce the given coercion from the given type.
1809 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
1810 liftCoMatch tmpls ty co
1811 = case ty_co_match menv emptyVarEnv ty co of
1812 Just cenv -> Just (LCS in_scope cenv)
1813 Nothing -> Nothing
1814 where
1815 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1816 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1817 -- Like tcMatchTy, assume all the interesting variables
1818 -- in ty are in tmpls
1819
1820 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1821 ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
1822 ty_co_match menv subst ty co
1823 | Just ty' <- coreView ty = ty_co_match menv subst ty' co
1824
1825 -- Match a type variable against a non-refl coercion
1826 ty_co_match menv cenv (TyVarTy tv1) co
1827 | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
1828 = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
1829 then Just cenv
1830 else Nothing -- no match since tv1 matches two different coercions
1831
1832 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1833 = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
1834 then Nothing -- occurs check failed
1835 else return (extendVarEnv cenv tv1' co)
1836 -- BAY: I don't think we need to do any kind matching here yet
1837 -- (compare 'match'), but we probably will when moving to SHE.
1838
1839 | otherwise -- tv1 is not a template ty var, so the only thing it
1840 -- can match is a reflexivity coercion for itself.
1841 -- But that case is dealt with already
1842 = Nothing
1843
1844 where
1845 rn_env = me_env menv
1846 tv1' = rnOccL rn_env tv1
1847
1848 ty_co_match menv subst (AppTy ty1 ty2) co
1849 | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1850 = do { subst' <- ty_co_match menv subst ty1 co1
1851 ; ty_co_match menv subst' ty2 co2 }
1852
1853 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos)
1854 | tc1 == tc2 = ty_co_matches menv subst tys cos
1855
1856 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo _ tc cos)
1857 | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1858
1859 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
1860 = ty_co_match menv' subst ty co
1861 where
1862 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1863
1864 ty_co_match menv subst ty co
1865 | Just co' <- pushRefl co = ty_co_match menv subst ty co'
1866 | otherwise = Nothing
1867
1868 ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1869 ty_co_matches menv = matchList (ty_co_match menv)
1870
1871 pushRefl :: Coercion -> Maybe Coercion
1872 pushRefl (Refl Nominal (AppTy ty1 ty2))
1873 = Just (AppCo (Refl Nominal ty1) (Refl Nominal ty2))
1874 pushRefl (Refl r (FunTy ty1 ty2))
1875 = Just (TyConAppCo r funTyCon [Refl r ty1, Refl r ty2])
1876 pushRefl (Refl r (TyConApp tc tys))
1877 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1878 pushRefl (Refl r (ForAllTy tv ty)) = Just (ForAllCo tv (Refl r ty))
1879 pushRefl _ = Nothing
1880
1881 {-
1882 ************************************************************************
1883 * *
1884 Sequencing on coercions
1885 * *
1886 ************************************************************************
1887 -}
1888
1889 seqCo :: Coercion -> ()
1890 seqCo (Refl eq ty) = eq `seq` seqType ty
1891 seqCo (TyConAppCo eq tc cos) = eq `seq` tc `seq` seqCos cos
1892 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
1893 seqCo (ForAllCo tv co) = seqType (tyVarKind tv) `seq` seqCo co
1894 seqCo (CoVarCo cv) = cv `seq` ()
1895 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
1896 seqCo (UnivCo s r ty1 ty2) = s `seq` r `seq` seqType ty1 `seq` seqType ty2
1897 seqCo (SymCo co) = seqCo co
1898 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
1899 seqCo (NthCo n co) = n `seq` seqCo co
1900 seqCo (LRCo lr co) = lr `seq` seqCo co
1901 seqCo (InstCo co ty) = seqCo co `seq` seqType ty
1902 seqCo (SubCo co) = seqCo co
1903 seqCo (AxiomRuleCo _ ts cs) = seqTypes ts `seq` seqCos cs
1904
1905 seqCos :: [Coercion] -> ()
1906 seqCos [] = ()
1907 seqCos (co:cos) = seqCo co `seq` seqCos cos
1908
1909 {-
1910 ************************************************************************
1911 * *
1912 The kind of a type, and of a coercion
1913 * *
1914 ************************************************************************
1915
1916 Note [Computing a coercion kind and role]
1917 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1918 To compute a coercion's kind is straightforward: see coercionKind.
1919 But to compute a coercion's role, in the case for NthCo we need
1920 its kind as well. So if we have two separate functions (one for kinds
1921 and one for roles) we can get exponentially bad behaviour, since each
1922 NthCo node makes a separate call to coercionKind, which traverses the
1923 sub-tree again. This was part of the problem in Trac #9233.
1924
1925 Solution: compute both together; hence coercionKindRole. We keep a
1926 separate coercionKind function because it's a bit more efficient if
1927 the kind is all you want.
1928 -}
1929
1930 coercionType :: Coercion -> Type
1931 coercionType co = case coercionKindRole co of
1932 (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
1933
1934 ------------------
1935 -- | If it is the case that
1936 --
1937 -- > c :: (t1 ~ t2)
1938 --
1939 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1940
1941 coercionKind :: Coercion -> Pair Type
1942 coercionKind co = go co
1943 where
1944 go (Refl _ ty) = Pair ty ty
1945 go (TyConAppCo _ tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
1946 go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
1947 go (ForAllCo tv co) = mkForAllTy tv <$> go co
1948 go (CoVarCo cv) = toPair $ coVarKind cv
1949 go (AxiomInstCo ax ind cos)
1950 | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
1951 , Pair tys1 tys2 <- sequenceA (map go cos)
1952 = ASSERT( cos `equalLength` tvs ) -- Invariant of AxiomInstCo: cos should
1953 -- exactly saturate the axiom branch
1954 Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
1955 (substTyWith tvs tys2 rhs)
1956 go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
1957 go (SymCo co) = swap $ go co
1958 go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
1959 go (NthCo d co) = tyConAppArgN d <$> go co
1960 go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
1961 go (InstCo aco ty) = go_app aco [ty]
1962 go (SubCo co) = go co
1963 go (AxiomRuleCo ax tys cos) =
1964 case coaxrProves ax tys (map go cos) of
1965 Just res -> res
1966 Nothing -> panic "coercionKind: Malformed coercion"
1967
1968 go_app :: Coercion -> [Type] -> Pair Type
1969 -- Collect up all the arguments and apply all at once
1970 -- See Note [Nested InstCos]
1971 go_app (InstCo co ty) tys = go_app co (ty:tys)
1972 go_app co tys = (`applyTys` tys) <$> go co
1973
1974 -- | Apply 'coercionKind' to multiple 'Coercion's
1975 coercionKinds :: [Coercion] -> Pair [Type]
1976 coercionKinds tys = sequenceA $ map coercionKind tys
1977
1978 -- | Get a coercion's kind and role.
1979 -- Why both at once? See Note [Computing a coercion kind and role]
1980 coercionKindRole :: Coercion -> (Pair Type, Role)
1981 coercionKindRole = go
1982 where
1983 go (Refl r ty) = (Pair ty ty, r)
1984 go (TyConAppCo r tc cos)
1985 = (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r)
1986 go (AppCo co1 co2)
1987 = let (tys1, r1) = go co1 in
1988 (mkAppTy <$> tys1 <*> coercionKind co2, r1)
1989 go (ForAllCo tv co)
1990 = let (tys, r) = go co in
1991 (mkForAllTy tv <$> tys, r)
1992 go (CoVarCo cv) = (toPair $ coVarKind cv, coVarRole cv)
1993 go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
1994 go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
1995 go (SymCo co) = first swap $ go co
1996 go (TransCo co1 co2)
1997 = let (tys1, r) = go co1 in
1998 (Pair (pFst tys1) (pSnd $ coercionKind co2), r)
1999 go (NthCo d co)
2000 = let (Pair t1 t2, r) = go co
2001 (tc1, args1) = splitTyConApp t1
2002 (_tc2, args2) = splitTyConApp t2
2003 in
2004 ASSERT( tc1 == _tc2 )
2005 ((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
2006 go co@(LRCo {}) = (coercionKind co, Nominal)
2007 go (InstCo co ty) = go_app co [ty]
2008 go (SubCo co) = (coercionKind co, Representational)
2009 go co@(AxiomRuleCo ax _ _) = (coercionKind co, coaxrRole ax)
2010
2011 go_app :: Coercion -> [Type] -> (Pair Type, Role)
2012 -- Collect up all the arguments and apply all at once
2013 -- See Note [Nested InstCos]
2014 go_app (InstCo co ty) tys = go_app co (ty:tys)
2015 go_app co tys
2016 = let (pair, r) = go co in
2017 ((`applyTys` tys) <$> pair, r)
2018
2019 -- | Retrieve the role from a coercion.
2020 coercionRole :: Coercion -> Role
2021 coercionRole = snd . coercionKindRole
2022 -- There's not a better way to do this, because NthCo needs the *kind*
2023 -- and role of its argument. Luckily, laziness should generally avoid
2024 -- the need for computing kinds in other cases.
2025
2026 {-
2027 Note [Nested InstCos]
2028 ~~~~~~~~~~~~~~~~~~~~~
2029 In Trac #5631 we found that 70% of the entire compilation time was
2030 being spent in coercionKind! The reason was that we had
2031 (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos
2032 where
2033 g :: forall a1 a2 .. a100. phi
2034 If we deal with the InstCos one at a time, we'll do this:
2035 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
2036 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst
2037 But this is a *quadratic* algorithm, and the blew up Trac #5631.
2038 So it's very important to do the substitution simultaneously.
2039
2040 cf Type.applyTys (which in fact we call here)
2041 -}
2042
2043 applyCo :: Type -> Coercion -> Type
2044 -- Gives the type of (e co) where e :: (a~b) => ty
2045 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
2046 applyCo (FunTy _ ty) _ = ty
2047 applyCo _ _ = panic "applyCo"
2048
2049 {-
2050 Note [Kind coercions]
2051 ~~~~~~~~~~~~~~~~~~~~~
2052 Kind coercions are only of the form: Refl kind. They are only used to
2053 instantiate kind polymorphic type constructors in TyConAppCo. Remember
2054 that kind instantiation only happens with TyConApp, not AppTy.
2055 -}