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