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