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