Merge branch 'master' of darcs.haskell.org:/home/darcs/ghc
[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
22         -- ** Functions over coercions
23         coVarKind,
24         coercionType, coercionKind, coercionKinds, isReflCo,
25         isReflCo_maybe,
26         mkCoercionType,
27
28         -- ** Constructing coercions
29         mkReflCo, mkCoVarCo, 
30         mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
31         mkUnbranchedAxInstRHS,
32         mkPiCo, mkPiCos, mkCoCast,
33         mkSymCo, mkTransCo, mkNthCo, mkLRCo,
34         mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
35         mkForAllCo, mkUnsafeCo,
36         mkNewTypeCo, 
37
38         -- ** Decomposition
39         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
40         getCoVar_maybe,
41
42         splitTyConAppCo_maybe,
43         splitAppCo_maybe,
44         splitForAllCo_maybe,
45
46         -- ** Coercion variables
47         mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
48
49         -- ** Free variables
50         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
51         
52         -- ** Substitution
53         CvSubstEnv, emptyCvSubstEnv, 
54         CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
55         isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
56         substCo, substCos, substCoVar, substCoVars,
57         substCoWithTy, substCoWithTys, 
58         cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst,
59         substTy, extendTvSubst, extendCvSubstAndInScope,
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, pprCoAxiom, 
73
74         -- * Other
75         applyCo
76        ) where 
77
78 #include "HsVersions.h"
79
80 import Unify    ( MatchEnv(..), matchList )
81 import TypeRep
82 import qualified Type
83 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
84 import TyCon
85 import CoAxiom
86 import Var
87 import VarEnv
88 import VarSet
89 import Maybes   ( orElse )
90 import Name     ( Name, NamedThing(..), nameUnique, getSrcSpan )
91 import OccName  ( parenSymOcc )
92 import Util
93 import BasicTypes
94 import Outputable
95 import Unique
96 import Pair
97 import PrelNames        ( funTyConKey, eqPrimTyConKey )
98 import Control.Applicative
99 import Data.Traversable (traverse, sequenceA)
100 import Control.Arrow (second)
101 import FastString
102
103 import qualified Data.Data as Data hiding ( TyCon )
104 \end{code}
105
106 %************************************************************************
107 %*                                                                      *
108             Coercions
109 %*                                                                      *
110 %************************************************************************
111
112 \begin{code}
113 -- | A 'Coercion' is concrete evidence of the equality/convertibility
114 -- of two types.
115
116 -- If you edit this type, you may need to update the GHC formalism
117 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
118 data Coercion 
119   -- These ones mirror the shape of types
120   = Refl Type  -- See Note [Refl invariant]
121           -- Invariant: applications of (Refl T) to a bunch of identity coercions
122           --            always show up as Refl.
123           -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
124
125           -- Applications of (Refl T) to some coercions, at least one of
126           -- which is NOT the identity, show up as TyConAppCo.
127           -- (They may not be fully saturated however.)
128           -- ConAppCo coercions (like all coercions other than Refl)
129           -- are NEVER the identity.
130
131   -- These ones simply lift the correspondingly-named 
132   -- Type constructors into Coercions
133   | TyConAppCo TyCon [Coercion]    -- lift TyConApp 
134                -- The TyCon is never a synonym; 
135                -- we expand synonyms eagerly
136                -- But it can be a type function
137
138   | AppCo Coercion Coercion        -- lift AppTy
139
140   -- See Note [Forall coercions]
141   | ForAllCo TyVar Coercion       -- forall a. g
142
143   -- These are special
144   | CoVarCo CoVar
145   | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
146      -- See also [CoAxiom index]
147      -- The coercion arguments always *precisely* saturate 
148      -- arity of (that branch of) the CoAxiom.  If there are
149      -- any left over, we use AppCo.  See 
150      -- See [Coercion axioms applied to coercions]
151
152   | UnsafeCo Type Type
153   | SymCo Coercion
154   | TransCo Coercion Coercion
155
156   -- These are destructors
157   | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
158   | LRCo   LeftOrRight Coercion     -- Decomposes (t_left t_right)
159   | InstCo Coercion Type
160   deriving (Data.Data, Data.Typeable)
161
162 -- If you edit this type, you may need to update the GHC formalism
163 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
164 data LeftOrRight = CLeft | CRight 
165                  deriving( Eq, Data.Data, Data.Typeable )
166
167 pickLR :: LeftOrRight -> (a,a) -> a
168 pickLR CLeft  (l,_) = l
169 pickLR CRight (_,r) = r
170 \end{code}
171
172
173 Note [Refl invariant]
174 ~~~~~~~~~~~~~~~~~~~~~
175 Coercions have the following invariant 
176      Refl is always lifted as far as possible.  
177
178 You might think that a consequencs is:
179      Every identity coercions has Refl at the root
180
181 But that's not quite true because of coercion variables.  Consider
182      g         where g :: Int~Int
183      Left h    where h :: Maybe Int ~ Maybe Int
184 etc.  So the consequence is only true of coercions that
185 have no coercion variables.
186
187 Note [Coercion axioms applied to coercions]
188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
189 The reason coercion axioms can be applied to coercions and not just
190 types is to allow for better optimization.  There are some cases where
191 we need to be able to "push transitivity inside" an axiom in order to
192 expose further opportunities for optimization.  
193
194 For example, suppose we have
195
196   C a : t[a] ~ F a
197   g   : b ~ c
198
199 and we want to optimize
200
201   sym (C b) ; t[g] ; C c
202
203 which has the kind
204
205   F b ~ F c
206
207 (stopping through t[b] and t[c] along the way).
208
209 We'd like to optimize this to just F g -- but how?  The key is
210 that we need to allow axioms to be instantiated by *coercions*,
211 not just by types.  Then we can (in certain cases) push
212 transitivity inside the axiom instantiations, and then react
213 opposite-polarity instantiations of the same axiom.  In this
214 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
215 obtain the substitution  a |-> g  (note this operation is sort
216 of the dual of lifting!) and hence end up with
217
218   C g : t[b] ~ F c
219
220 which indeed has the same kind as  t[g] ; C c.
221
222 Now we have
223
224   sym (C b) ; C g
225
226 which can be optimized to F g.
227
228 Note [CoAxiom index]
229 ~~~~~~~~~~~~~~~~~~~~
230 A CoAxiom has 1 or more branches. Each branch has contains a list
231 of the free type variables in that branch, the LHS type patterns,
232 and the RHS type for that branch. When we apply an axiom to a list
233 of coercions, we must choose which branch of the axiom we wish to
234 use, as the different branches may have different numbers of free
235 type variables. (The number of type patterns is always the same
236 among branches, but that doesn't quite concern us here.)
237
238 The Int in the AxiomInstCo constructor is the 0-indexed number
239 of the chosen branch.
240
241 Note [Forall coercions]
242 ~~~~~~~~~~~~~~~~~~~~~~~
243 Constructing coercions between forall-types can be a bit tricky.
244 Currently, the situation is as follows:
245
246   ForAllCo TyVar Coercion
247
248 represents a coercion between polymorphic types, with the rule
249
250            v : k       g : t1 ~ t2
251   ----------------------------------------------
252   ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
253
254 Note that it's only necessary to coerce between polymorphic types
255 where the type variables have identical kinds, because equality on
256 kinds is trivial.
257
258 Note [Predicate coercions]
259 ~~~~~~~~~~~~~~~~~~~~~~~~~~
260 Suppose we have
261    g :: a~b
262 How can we coerce between types
263    ([c]~a) => [a] -> c
264 and
265    ([c]~b) => [b] -> c
266 where the equality predicate *itself* differs?
267
268 Answer: we simply treat (~) as an ordinary type constructor, so these
269 types really look like
270
271    ((~) [c] a) -> [a] -> c
272    ((~) [c] b) -> [b] -> c
273
274 So the coercion between the two is obviously
275
276    ((~) [c] g) -> [g] -> c
277
278 Another way to see this to say that we simply collapse predicates to
279 their representation type (see Type.coreView and Type.predTypeRep).
280
281 This collapse is done by mkPredCo; there is no PredCo constructor
282 in Coercion.  This is important because we need Nth to work on 
283 predicates too:
284     Nth 1 ((~) [c] g) = g
285 See Simplify.simplCoercionF, which generates such selections.
286
287 Note [Kind coercions]
288 ~~~~~~~~~~~~~~~~~~~~~
289 Suppose T :: * -> *, and g :: A ~ B
290 Then the coercion
291    TyConAppCo T [g]      T g : T A ~ T B
292
293 Now suppose S :: forall k. k -> *, and g :: A ~ B
294 Then the coercion
295    TyConAppCo S [Refl *, g]   T <*> g : T * A ~ T * B
296
297 Notice that the arguments to TyConAppCo are coercions, but the first
298 represents a *kind* coercion. Now, we don't allow any non-trivial kind
299 coercions, so it's an invariant that any such kind coercions are Refl.
300 Lint checks this. 
301
302 However it's inconvenient to insist that these kind coercions are always
303 *structurally* (Refl k), because the key function exprIsConApp_maybe
304 pushes coercions into constructor arguments, so 
305        C k ty e |> g
306 may turn into
307        C (Nth 0 g) ....
308 Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.
309
310 %************************************************************************
311 %*                                                                      *
312 \subsection{Coercion variables}
313 %*                                                                      *
314 %************************************************************************
315
316 \begin{code}
317 coVarName :: CoVar -> Name
318 coVarName = varName
319
320 setCoVarUnique :: CoVar -> Unique -> CoVar
321 setCoVarUnique = setVarUnique
322
323 setCoVarName :: CoVar -> Name -> CoVar
324 setCoVarName   = setVarName
325
326 isCoVar :: Var -> Bool
327 isCoVar v = isCoVarType (varType v)
328
329 isCoVarType :: Type -> Bool
330 isCoVarType ty      -- Tests for t1 ~# t2, the unboxed equality
331   = case splitTyConApp_maybe ty of
332       Just (tc,tys) -> tc `hasKey` eqPrimTyConKey && tys `lengthAtLeast` 2
333       Nothing       -> False
334 \end{code}
335
336
337 \begin{code}
338 tyCoVarsOfCo :: Coercion -> VarSet
339 -- Extracts type and coercion variables from a coercion
340 tyCoVarsOfCo (Refl ty)           = tyVarsOfType ty
341 tyCoVarsOfCo (TyConAppCo _ cos)  = tyCoVarsOfCos cos
342 tyCoVarsOfCo (AppCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
343 tyCoVarsOfCo (ForAllCo tv co)    = tyCoVarsOfCo co `delVarSet` tv
344 tyCoVarsOfCo (CoVarCo v)         = unitVarSet v
345 tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
346 tyCoVarsOfCo (UnsafeCo ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
347 tyCoVarsOfCo (SymCo co)          = tyCoVarsOfCo co
348 tyCoVarsOfCo (TransCo co1 co2)   = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
349 tyCoVarsOfCo (NthCo _ co)        = tyCoVarsOfCo co
350 tyCoVarsOfCo (LRCo _ co)         = tyCoVarsOfCo co
351 tyCoVarsOfCo (InstCo co ty)      = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
352
353 tyCoVarsOfCos :: [Coercion] -> VarSet
354 tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
355
356 coVarsOfCo :: Coercion -> VarSet
357 -- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
358 coVarsOfCo (Refl _)            = emptyVarSet
359 coVarsOfCo (TyConAppCo _ cos)  = coVarsOfCos cos
360 coVarsOfCo (AppCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
361 coVarsOfCo (ForAllCo _ co)     = coVarsOfCo co
362 coVarsOfCo (CoVarCo v)         = unitVarSet v
363 coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
364 coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
365 coVarsOfCo (SymCo co)          = coVarsOfCo co
366 coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
367 coVarsOfCo (NthCo _ co)        = coVarsOfCo co
368 coVarsOfCo (LRCo _ co)         = coVarsOfCo co
369 coVarsOfCo (InstCo co _)       = coVarsOfCo co
370
371 coVarsOfCos :: [Coercion] -> VarSet
372 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
373
374 coercionSize :: Coercion -> Int
375 coercionSize (Refl ty)           = typeSize ty
376 coercionSize (TyConAppCo _ cos)  = 1 + sum (map coercionSize cos)
377 coercionSize (AppCo co1 co2)     = coercionSize co1 + coercionSize co2
378 coercionSize (ForAllCo _ co)     = 1 + coercionSize co
379 coercionSize (CoVarCo _)         = 1
380 coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
381 coercionSize (UnsafeCo ty1 ty2)  = typeSize ty1 + typeSize ty2
382 coercionSize (SymCo co)          = 1 + coercionSize co
383 coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
384 coercionSize (NthCo _ co)        = 1 + coercionSize co
385 coercionSize (LRCo  _ co)        = 1 + coercionSize co
386 coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
387 \end{code}
388
389 %************************************************************************
390 %*                                                                      *
391                    Pretty-printing coercions
392 %*                                                                      *
393 %************************************************************************
394
395 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
396 function is defined to use this.  @pprParendCo@ is the same, except it
397 puts parens around the type, except for the atomic cases.
398 @pprParendCo@ works just by setting the initial context precedence
399 very high.
400
401 \begin{code}
402 instance Outputable Coercion where
403   ppr = pprCo
404
405 pprCo, pprParendCo :: Coercion -> SDoc
406 pprCo       co = ppr_co TopPrec   co
407 pprParendCo co = ppr_co TyConPrec co
408
409 ppr_co :: Prec -> Coercion -> SDoc
410 ppr_co _ (Refl ty) = angleBrackets (ppr ty)
411
412 ppr_co p co@(TyConAppCo tc [_,_])
413   | tc `hasKey` funTyConKey = ppr_fun_co p co
414
415 ppr_co p (TyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
416 ppr_co p (AppCo co1 co2)       = maybeParen p TyConPrec $
417                                  pprCo co1 <+> ppr_co TyConPrec co2
418 ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
419 ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
420 ppr_co p (AxiomInstCo con index cos)
421   = angleBrackets (pprPrefixApp p 
422                     (ppr (getName con) <> brackets (ppr index))
423                     (map (ppr_co TyConPrec) cos))
424
425 ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
426                            case trans_co_list co [] of
427                              [] -> panic "ppr_co"
428                              (co:cos) -> sep ( ppr_co FunPrec co
429                                              : [ char ';' <+> ppr_co FunPrec co | co <- cos])
430 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
431                           pprParendCo co <> ptext (sLit "@") <> pprType ty
432
433 ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) 
434                                            [pprParendType ty1, pprParendType ty2]
435 ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
436 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
437 ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
438
439 trans_co_list :: Coercion -> [Coercion] -> [Coercion]
440 trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
441 trans_co_list co                cos = co : cos
442
443 instance Outputable LeftOrRight where
444   ppr CLeft    = ptext (sLit "Left")
445   ppr CRight   = ptext (sLit "Right")
446
447 ppr_fun_co :: Prec -> Coercion -> SDoc
448 ppr_fun_co p co = pprArrowChain p (split co)
449   where
450     split :: Coercion -> [SDoc]
451     split (TyConAppCo f [arg,res])
452       | f `hasKey` funTyConKey
453       = ppr_co FunPrec arg : split res
454     split co = [ppr_co TopPrec co]
455
456 ppr_forall_co :: Prec -> Coercion -> SDoc
457 ppr_forall_co p ty
458   = maybeParen p FunPrec $
459     sep [pprForAll tvs, ppr_co TopPrec rho]
460   where
461     (tvs,  rho) = split1 [] ty
462     split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
463     split1 tvs ty               = (reverse tvs, ty)
464 \end{code}
465
466 \begin{code}
467 pprCoAxiom :: CoAxiom br -> SDoc
468 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
469   = hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
470        2 (vcat (map (pprCoAxBranch tc) $ fromBranchList branches))
471
472 pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
473 pprCoAxBranch tc (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
474   = ptext (sLit "forall") <+> pprTvBndrs tvs <> dot <+> 
475       pprEqPred (Pair (mkTyConApp tc lhs) rhs)
476
477 \end{code}
478
479 %************************************************************************
480 %*                                                                      *
481         Functions over Kinds            
482 %*                                                                      *
483 %************************************************************************
484
485 \begin{code}
486 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
487 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
488 --
489 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
490 decomposeCo :: Arity -> Coercion -> [Coercion]
491 decomposeCo arity co 
492   = [mkNthCo n co | n <- [0..(arity-1)] ]
493            -- Remember, Nth is zero-indexed
494
495 -- | Attempts to obtain the type variable underlying a 'Coercion'
496 getCoVar_maybe :: Coercion -> Maybe CoVar
497 getCoVar_maybe (CoVarCo cv) = Just cv  
498 getCoVar_maybe _            = Nothing
499
500 -- | Attempts to tease a coercion apart into a type constructor and the application
501 -- of a number of coercion arguments to that constructor
502 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
503 splitTyConAppCo_maybe (Refl ty)           = (fmap . second . map) Refl (splitTyConApp_maybe ty)
504 splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
505 splitTyConAppCo_maybe _                   = Nothing
506
507 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
508 -- ^ Attempt to take a coercion application apart.
509 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
510 splitAppCo_maybe (TyConAppCo tc cos)
511   | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc 
512   , Just (cos', co') <- snocView cos
513   = Just (mkTyConAppCo tc cos', co')    -- Never create unsaturated type family apps!
514        -- Use mkTyConAppCo to preserve the invariant
515        --  that identity coercions are always represented by Refl
516 splitAppCo_maybe (Refl ty) 
517   | Just (ty1, ty2) <- splitAppTy_maybe ty 
518   = Just (Refl ty1, Refl ty2)
519 splitAppCo_maybe _ = Nothing
520
521 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
522 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
523 splitForAllCo_maybe _                = Nothing
524
525 -------------------------------------------------------
526 -- and some coercion kind stuff
527
528 coVarKind :: CoVar -> (Type,Type) 
529 coVarKind cv
530  | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
531  = ASSERT (tc `hasKey` eqPrimTyConKey)
532    (ty1,ty2)
533  | otherwise = panic "coVarKind, non coercion variable"
534
535 -- | Makes a coercion type from two types: the types whose equality 
536 -- is proven by the relevant 'Coercion'
537 mkCoercionType :: Type -> Type -> Type
538 mkCoercionType = mkPrimEqPred
539
540 isReflCo :: Coercion -> Bool
541 isReflCo (Refl {}) = True
542 isReflCo _         = False
543
544 isReflCo_maybe :: Coercion -> Maybe Type
545 isReflCo_maybe (Refl ty) = Just ty
546 isReflCo_maybe _         = Nothing
547 \end{code}
548
549 %************************************************************************
550 %*                                                                      *
551             Building coercions
552 %*                                                                      *
553 %************************************************************************
554
555 \begin{code}
556 mkCoVarCo :: CoVar -> Coercion
557 -- cv :: s ~# t
558 mkCoVarCo cv
559   | ty1 `eqType` ty2 = Refl ty1
560   | otherwise        = CoVarCo cv
561   where
562     (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
563
564 mkReflCo :: Type -> Coercion
565 mkReflCo = Refl
566
567 mkAxInstCo :: CoAxiom br -> Int -> [Type] -> Coercion
568 -- mkAxInstCo can legitimately be called over-staturated; 
569 -- i.e. with more type arguments than the coercion requires
570 mkAxInstCo ax index tys
571   | arity == n_tys = AxiomInstCo ax_br index rtys
572   | otherwise      = ASSERT( arity < n_tys )
573                      foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
574                                  (drop arity rtys)
575   where
576     n_tys = length tys
577     arity = coAxiomArity ax index
578     rtys  = map Refl tys
579     ax_br = toBranchedAxiom ax
580
581 -- to be used only with unbranched axioms
582 mkUnbranchedAxInstCo :: CoAxiom Unbranched -> [Type] -> Coercion
583 mkUnbranchedAxInstCo ax tys
584   = mkAxInstCo ax 0 tys
585
586 mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
587 -- Instantiate the axiom with specified types,
588 -- returning the instantiated RHS
589 -- A companion to mkAxInstCo: 
590 --    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
591 mkAxInstLHS ax index tys
592   | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
593   , (tys1, tys2) <- splitAtList tvs tys
594   = ASSERT( tvs `equalLength` tys1 ) 
595     mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
596   where
597
598 mkAxInstRHS ax index tys
599   | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
600   , (tys1, tys2) <- splitAtList tvs tys
601   = ASSERT( tvs `equalLength` tys1 ) 
602     mkAppTys (substTyWith tvs tys1 rhs) tys2
603
604 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
605 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
606
607 -- | Apply a 'Coercion' to another 'Coercion'.
608 mkAppCo :: Coercion -> Coercion -> Coercion
609 mkAppCo (Refl ty1) (Refl ty2)       = Refl (mkAppTy ty1 ty2)
610 mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
611 mkAppCo (TyConAppCo tc cos) co      = TyConAppCo tc (cos ++ [co])
612 mkAppCo co1 co2                     = AppCo co1 co2
613 -- Note, mkAppCo is careful to maintain invariants regarding
614 -- where Refl constructors appear; see the comments in the definition
615 -- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
616
617 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
618 -- See also 'mkAppCo'
619 mkAppCos :: Coercion -> [Coercion] -> Coercion
620 mkAppCos co1 tys = foldl mkAppCo co1 tys
621
622 -- | Apply a type constructor to a list of coercions.
623 mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
624 mkTyConAppCo tc cos
625                -- Expand type synonyms
626   | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
627   = mkAppCos (liftCoSubst tv_co_prs rhs_ty) leftover_cos
628
629   | Just tys <- traverse isReflCo_maybe cos 
630   = Refl (mkTyConApp tc tys)    -- See Note [Refl invariant]
631
632   | otherwise = TyConAppCo tc cos
633
634 -- | Make a function 'Coercion' between two other 'Coercion's
635 mkFunCo :: Coercion -> Coercion -> Coercion
636 mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
637
638 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
639 mkForAllCo :: Var -> Coercion -> Coercion
640 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
641 mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
642 mkForAllCo tv  co       = ASSERT ( isTyVar tv ) ForAllCo tv co
643
644 -------------------------------
645
646 -- | Create a symmetric version of the given 'Coercion' that asserts
647 --   equality between the same types but in the other "direction", so
648 --   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
649 mkSymCo :: Coercion -> Coercion
650
651 -- Do a few simple optimizations, but don't bother pushing occurrences
652 -- of symmetry to the leaves; the optimizer will take care of that.
653 mkSymCo co@(Refl {})              = co
654 mkSymCo    (UnsafeCo ty1 ty2)    = UnsafeCo ty2 ty1
655 mkSymCo    (SymCo co)            = co
656 mkSymCo co                       = SymCo co
657
658 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
659 mkTransCo :: Coercion -> Coercion -> Coercion
660 mkTransCo (Refl _) co = co
661 mkTransCo co (Refl _) = co
662 mkTransCo co1 co2     = TransCo co1 co2
663
664 mkNthCo :: Int -> Coercion -> Coercion
665 mkNthCo n (Refl ty) = ASSERT( ok_tc_app ty n ) 
666                       Refl (tyConAppArgN n ty)
667 mkNthCo n co        = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
668                       NthCo n co
669                     where
670                       Pair _ty1 _ty2 = coercionKind co
671
672 mkLRCo :: LeftOrRight -> Coercion -> Coercion
673 mkLRCo lr (Refl ty) = Refl (pickLR lr (splitAppTy ty))
674 mkLRCo lr co        = LRCo lr co
675
676 ok_tc_app :: Type -> Int -> Bool
677 ok_tc_app ty n = case splitTyConApp_maybe ty of
678                    Just (_, tys) -> tys `lengthExceeds` n
679                    Nothing       -> False
680
681 -- | Instantiates a 'Coercion' with a 'Type' argument. 
682 mkInstCo :: Coercion -> Type -> Coercion
683 mkInstCo co ty = InstCo co ty
684
685 -- | Manufacture a coercion from thin air. Needless to say, this is
686 --   not usually safe, but it is used when we know we are dealing with
687 --   bottom, which is one case in which it is safe.  This is also used
688 --   to implement the @unsafeCoerce#@ primitive.  Optimise by pushing
689 --   down through type constructors.
690 mkUnsafeCo :: Type -> Type -> Coercion
691 mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
692 mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
693   | tc1 == tc2
694   = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
695
696 mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
697   = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
698
699 mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
700
701 -- See note [Newtype coercions] in TyCon
702
703 -- | Create a coercion constructor (axiom) suitable for the given
704 --   newtype 'TyCon'. The 'Name' should be that of a new coercion
705 --   'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
706 --   the type the appropriate right hand side of the @newtype@, with
707 --   the free variables a subset of those 'TyVar's.
708 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom Unbranched
709 mkNewTypeCo name tycon tvs rhs_ty
710   = CoAxiom { co_ax_unique   = nameUnique name
711             , co_ax_name     = name
712             , co_ax_implicit = True  -- See Note [Implicit axioms] in TyCon
713             , co_ax_tc       = tycon
714             , co_ax_branches = FirstBranch branch }
715   where branch = CoAxBranch { cab_loc = getSrcSpan name
716                             , cab_tvs = tvs
717                             , cab_lhs = mkTyVarTys tvs
718                             , cab_rhs = rhs_ty }
719
720 mkPiCos :: [Var] -> Coercion -> Coercion
721 mkPiCos vs co = foldr mkPiCo co vs
722
723 mkPiCo  :: Var -> Coercion -> Coercion
724 mkPiCo v co | isTyVar v = mkForAllCo v co
725             | otherwise = mkFunCo (mkReflCo (varType v)) co
726
727 mkCoCast :: Coercion -> Coercion -> Coercion
728 -- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
729 mkCoCast c g
730   = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
731   where
732        -- g  :: (s1 ~# s2) ~# (t1 ~#  t2)
733        -- g1 :: s1 ~# t1
734        -- g2 :: s2 ~# t2
735     [_reflk, g1, g2] = decomposeCo 3 g
736             -- Remember, (~#) :: forall k. k -> k -> *
737             -- so it takes *three* arguments, not two
738 \end{code}
739
740 %************************************************************************
741 %*                                                                      *
742             Newtypes
743 %*                                                                      *
744 %************************************************************************
745
746 \begin{code}
747 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
748 -- ^ If @co :: T ts ~ rep_ty@ then:
749 --
750 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
751 instNewTyCon_maybe tc tys
752   | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
753   = ASSERT( tys `lengthIs` tyConArity tc )
754     Just (substTyWith tvs tys ty, mkUnbranchedAxInstCo co_tc tys)
755   | otherwise
756   = Nothing
757
758 -- this is here to avoid module loops
759 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
760 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
761 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
762 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
763 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
764 --
765 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
766 --
767 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
768 splitNewTypeRepCo_maybe ty 
769   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
770 splitNewTypeRepCo_maybe (TyConApp tc tys)
771   | Just (ty', co) <- instNewTyCon_maybe tc tys
772   = case co of
773         Refl _ -> panic "splitNewTypeRepCo_maybe"
774                         -- This case handled by coreView
775         _      -> Just (ty', co)
776 splitNewTypeRepCo_maybe _
777   = Nothing
778
779 -- | Determines syntactic equality of coercions
780 coreEqCoercion :: Coercion -> Coercion -> Bool
781 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
782   where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
783
784 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
785 coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
786 coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
787   = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
788
789 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
790   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
791
792 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
793   = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
794
795 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
796   = rnOccL env cv1 == rnOccR env cv2
797
798 coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
799   = con1 == con2
800     && ind1 == ind2
801     && all2 (coreEqCoercion2 env) cos1 cos2
802
803 coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
804   = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
805
806 coreEqCoercion2 env (SymCo co1) (SymCo co2)
807   = coreEqCoercion2 env co1 co2
808
809 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
810   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
811
812 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
813   = d1 == d2 && coreEqCoercion2 env co1 co2
814 coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
815   = d1 == d2 && coreEqCoercion2 env co1 co2
816
817 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
818   = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
819
820 coreEqCoercion2 _ _ _ = False
821 \end{code}
822
823 %************************************************************************
824 %*                                                                      *
825                    Substitution of coercions
826 %*                                                                      *
827 %************************************************************************
828
829 \begin{code}
830 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
831 --   doing a \"lifting\" substitution)
832 type CvSubstEnv = VarEnv Coercion
833
834 emptyCvSubstEnv :: CvSubstEnv
835 emptyCvSubstEnv = emptyVarEnv
836
837 data CvSubst            
838   = CvSubst InScopeSet  -- The in-scope type variables
839             TvSubstEnv  -- Substitution of types
840             CvSubstEnv  -- Substitution of coercions
841
842 instance Outputable CvSubst where
843   ppr (CvSubst ins tenv cenv)
844     = brackets $ sep[ ptext (sLit "CvSubst"),
845                       nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
846                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
847                       nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
848
849 emptyCvSubst :: CvSubst
850 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
851
852 isEmptyCvSubst :: CvSubst -> Bool
853 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
854
855 getCvInScope :: CvSubst -> InScopeSet
856 getCvInScope (CvSubst in_scope _ _) = in_scope
857
858 zapCvSubstEnv :: CvSubst -> CvSubst
859 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
860
861 cvTvSubst :: CvSubst -> TvSubst
862 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
863
864 tvCvSubst :: TvSubst -> CvSubst
865 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
866
867 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
868 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
869   = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
870
871 extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
872 -- Also extends the in-scope set
873 extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
874   = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
875             tenv
876             (extendVarEnv cenv cv co)
877
878 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
879 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
880   = ASSERT( isCoVar old_var )
881     (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
882   where
883     -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
884     -- In that case, mkCoVarCo will return a ReflCoercion, and
885     -- we want to substitute that (not new_var) for old_var
886     new_co    = mkCoVarCo new_var
887     no_change = new_var == old_var && not (isReflCo new_co)
888
889     new_cenv | no_change = delVarEnv cenv old_var
890              | otherwise = extendVarEnv cenv old_var new_co
891
892     new_var = uniqAway in_scope subst_old_var
893     subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
894                   -- It's important to do the substitution for coercions,
895                   -- because they can have free type variables
896
897 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
898 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
899   = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
900       (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
901
902 mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
903 mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
904
905 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
906 zipOpenCvSubst vs cos
907   | debugIsOn && (length vs /= length cos)
908   = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
909   | otherwise 
910   = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
911
912 substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
913 substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
914
915 substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
916 substCoWithTys in_scope tvs tys co
917   | debugIsOn && (length tvs /= length tys)
918   = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
919   | otherwise 
920   = ASSERT( length tvs == length tys )
921     substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
922
923 -- | Substitute within a 'Coercion'
924 substCo :: CvSubst -> Coercion -> Coercion
925 substCo subst co | isEmptyCvSubst subst = co
926                  | otherwise            = subst_co subst co
927
928 -- | Substitute within several 'Coercion's
929 substCos :: CvSubst -> [Coercion] -> [Coercion]
930 substCos subst cos | isEmptyCvSubst subst = cos
931                    | otherwise            = map (substCo subst) cos
932
933 substTy :: CvSubst -> Type -> Type
934 substTy subst = Type.substTy (cvTvSubst subst)
935
936 subst_co :: CvSubst -> Coercion -> Coercion
937 subst_co subst co
938   = go co
939   where
940     go_ty :: Type -> Type
941     go_ty = Coercion.substTy subst
942
943     go :: Coercion -> Coercion
944     go (Refl ty)             = Refl $! go_ty ty
945     go (TyConAppCo tc cos)   = let args = map go cos
946                                in  args `seqList` TyConAppCo tc args
947     go (AppCo co1 co2)       = mkAppCo (go co1) $! go co2
948     go (ForAllCo tv co)      = case substTyVarBndr subst tv of
949                                  (subst', tv') ->
950                                    ForAllCo tv' $! subst_co subst' co
951     go (CoVarCo cv)          = substCoVar subst cv
952     go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
953     go (UnsafeCo ty1 ty2)    = (UnsafeCo $! go_ty ty1) $! go_ty ty2
954     go (SymCo co)            = mkSymCo (go co)
955     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
956     go (NthCo d co)          = mkNthCo d (go co)
957     go (LRCo lr co)          = mkLRCo lr (go co)
958     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
959
960 substCoVar :: CvSubst -> CoVar -> Coercion
961 substCoVar (CvSubst in_scope _ cenv) cv
962   | Just co  <- lookupVarEnv cenv cv      = co
963   | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
964   | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
965                 ASSERT( isCoVar cv ) CoVarCo cv
966
967 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
968 substCoVars subst cvs = map (substCoVar subst) cvs
969
970 lookupTyVar :: CvSubst -> TyVar  -> Maybe Type
971 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
972
973 lookupCoVar :: CvSubst -> Var  -> Maybe Coercion
974 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
975 \end{code}
976
977 %************************************************************************
978 %*                                                                      *
979                    "Lifting" substitution
980            [(TyVar,Coercion)] -> Type -> Coercion
981 %*                                                                      *
982 %************************************************************************
983
984 \begin{code}
985 data LiftCoSubst = LCS InScopeSet LiftCoEnv
986
987 type LiftCoEnv = VarEnv Coercion
988      -- Maps *type variables* to *coercions*
989      -- That's the whole point of this function!
990
991 liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
992 liftCoSubstWith tvs cos ty
993   = liftCoSubst (zipEqual "liftCoSubstWith" tvs cos) ty
994
995 liftCoSubst :: [(TyVar,Coercion)] -> Type -> Coercion
996 liftCoSubst prs ty
997  | null prs  = Refl ty
998  | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
999                                 (mkVarEnv prs)) ty
1000
1001 -- | The \"lifting\" operation which substitutes coercions for type
1002 --   variables in a type to produce a coercion.
1003 --
1004 --   For the inverse operation, see 'liftCoMatch' 
1005 ty_co_subst :: LiftCoSubst -> Type -> Coercion
1006 ty_co_subst subst ty
1007   = go ty
1008   where
1009     go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
1010                              -- A type variable from a non-cloned forall
1011                              -- won't be in the substitution
1012     go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
1013     go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
1014                            -- IA0_NOTE: Do we need to do anything
1015                            -- about kind instantiations? I don't think
1016                            -- so.  see Note [Kind coercions]
1017     go (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
1018     go (ForAllTy v ty)   = mkForAllCo v' $! (ty_co_subst subst' ty)
1019                          where
1020                            (subst', v') = liftCoSubstTyVarBndr subst v
1021     go ty@(LitTy {})     = mkReflCo ty
1022
1023 liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
1024 liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv 
1025
1026 liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
1027 liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
1028   = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)               
1029   where
1030     new_cenv | no_change = delVarEnv cenv old_var
1031              | otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
1032
1033     no_change = new_var == old_var
1034     new_var = uniqAway in_scope old_var
1035 \end{code}
1036
1037 \begin{code}
1038 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
1039 --   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
1040 --   That is, it matches a type against a coercion of the same
1041 --   "shape", and returns a lifting substitution which could have been
1042 --   used to produce the given coercion from the given type.
1043 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
1044 liftCoMatch tmpls ty co 
1045   = case ty_co_match menv emptyVarEnv ty co of
1046       Just cenv -> Just (LCS in_scope cenv)
1047       Nothing   -> Nothing
1048   where
1049     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1050     in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1051     -- Like tcMatchTy, assume all the interesting variables 
1052     -- in ty are in tmpls
1053
1054 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1055 ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
1056 ty_co_match menv subst ty co 
1057   | Just ty' <- coreView ty = ty_co_match menv subst ty' co
1058
1059   -- Match a type variable against a non-refl coercion
1060 ty_co_match menv cenv (TyVarTy tv1) co
1061   | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
1062   = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
1063     then Just cenv
1064     else Nothing       -- no match since tv1 matches two different coercions
1065
1066   | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
1067   = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
1068     then Nothing      -- occurs check failed
1069     else return (extendVarEnv cenv tv1' co)
1070         -- BAY: I don't think we need to do any kind matching here yet
1071         -- (compare 'match'), but we probably will when moving to SHE.
1072
1073   | otherwise    -- tv1 is not a template ty var, so the only thing it
1074                  -- can match is a reflexivity coercion for itself.
1075                  -- But that case is dealt with already
1076   = Nothing
1077
1078   where
1079     rn_env = me_env menv
1080     tv1' = rnOccL rn_env tv1
1081
1082 ty_co_match menv subst (AppTy ty1 ty2) co
1083   | Just (co1, co2) <- splitAppCo_maybe co      -- c.f. Unify.match on AppTy
1084   = do { subst' <- ty_co_match menv subst ty1 co1 
1085        ; ty_co_match menv subst' ty2 co2 }
1086
1087 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
1088   | tc1 == tc2 = ty_co_matches menv subst tys cos
1089
1090 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
1091   | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1092
1093 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co) 
1094   = ty_co_match menv' subst ty co
1095   where
1096     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1097
1098 ty_co_match menv subst ty co
1099   | Just co' <- pushRefl co = ty_co_match menv subst ty co'
1100   | otherwise               = Nothing
1101
1102 ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1103 ty_co_matches menv = matchList (ty_co_match menv)
1104
1105 pushRefl :: Coercion -> Maybe Coercion
1106 pushRefl (Refl (AppTy ty1 ty2))   = Just (AppCo (Refl ty1) (Refl ty2))
1107 pushRefl (Refl (FunTy ty1 ty2))   = Just (TyConAppCo funTyCon [Refl ty1, Refl ty2])
1108 pushRefl (Refl (TyConApp tc tys)) = Just (TyConAppCo tc (map Refl tys))
1109 pushRefl (Refl (ForAllTy tv ty))  = Just (ForAllCo tv (Refl ty))
1110 pushRefl _                        = Nothing
1111 \end{code}
1112
1113 %************************************************************************
1114 %*                                                                      *
1115             Sequencing on coercions
1116 %*                                                                      *
1117 %************************************************************************
1118
1119 \begin{code}
1120 seqCo :: Coercion -> ()
1121 seqCo (Refl ty)             = seqType ty
1122 seqCo (TyConAppCo tc cos)   = tc `seq` seqCos cos
1123 seqCo (AppCo co1 co2)       = seqCo co1 `seq` seqCo co2
1124 seqCo (ForAllCo tv co)      = tv `seq` seqCo co
1125 seqCo (CoVarCo cv)          = cv `seq` ()
1126 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
1127 seqCo (UnsafeCo ty1 ty2)    = seqType ty1 `seq` seqType ty2
1128 seqCo (SymCo co)            = seqCo co
1129 seqCo (TransCo co1 co2)     = seqCo co1 `seq` seqCo co2
1130 seqCo (NthCo _ co)          = seqCo co
1131 seqCo (LRCo _ co)           = seqCo co
1132 seqCo (InstCo co ty)        = seqCo co `seq` seqType ty
1133
1134 seqCos :: [Coercion] -> ()
1135 seqCos []       = ()
1136 seqCos (co:cos) = seqCo co `seq` seqCos cos
1137 \end{code}
1138
1139
1140 %************************************************************************
1141 %*                                                                      *
1142              The kind of a type, and of a coercion
1143 %*                                                                      *
1144 %************************************************************************
1145
1146 \begin{code}
1147 coercionType :: Coercion -> Type
1148 coercionType co = case coercionKind co of
1149                     Pair ty1 ty2 -> mkCoercionType ty1 ty2
1150
1151 ------------------
1152 -- | If it is the case that
1153 --
1154 -- > c :: (t1 ~ t2)
1155 --
1156 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1157
1158 coercionKind :: Coercion -> Pair Type 
1159 coercionKind co = go co
1160   where 
1161     go (Refl ty)            = Pair ty ty
1162     go (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
1163     go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
1164     go (ForAllCo tv co)     = mkForAllTy tv <$> go co
1165     go (CoVarCo cv)         = toPair $ coVarKind cv
1166     go (AxiomInstCo ax ind cos)
1167       | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
1168       , Pair tys1 tys2 <- sequenceA (map go cos)
1169       = ASSERT( cos `equalLength` tvs )  -- Invariant of AxiomInstCo: cos should 
1170                                          -- exactly saturate the axiom branch
1171         Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
1172              (substTyWith tvs tys2 rhs)
1173     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
1174     go (SymCo co)           = swap $ go co
1175     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
1176     go (NthCo d co)         = tyConAppArgN d <$> go co
1177     go (LRCo lr co)         = (pickLR lr . splitAppTy) <$> go co
1178     go (InstCo aco ty)      = go_app aco [ty]
1179
1180     go_app :: Coercion -> [Type] -> Pair Type
1181     -- Collect up all the arguments and apply all at once
1182     -- See Note [Nested InstCos]
1183     go_app (InstCo co ty) tys = go_app co (ty:tys)
1184     go_app co             tys = (`applyTys` tys) <$> go co
1185
1186 -- | Apply 'coercionKind' to multiple 'Coercion's
1187 coercionKinds :: [Coercion] -> Pair [Type]
1188 coercionKinds tys = sequenceA $ map coercionKind tys
1189 \end{code}
1190
1191 Note [Nested InstCos]
1192 ~~~~~~~~~~~~~~~~~~~~~
1193 In Trac #5631 we found that 70% of the entire compilation time was
1194 being spent in coercionKind!  The reason was that we had
1195    (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
1196 where 
1197    g :: forall a1 a2 .. a100. phi
1198 If we deal with the InstCos one at a time, we'll do this:
1199    1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
1200    2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
1201 But this is a *quadratic* algorithm, and the blew up Trac #5631.
1202 So it's very important to do the substitution simultaneously.
1203
1204 cf Type.applyTys (which in fact we call here)
1205
1206
1207 \begin{code}
1208 applyCo :: Type -> Coercion -> Type
1209 -- Gives the type of (e co) where e :: (a~b) => ty
1210 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
1211 applyCo (FunTy _ ty) _ = ty
1212 applyCo _            _ = panic "applyCo"
1213 \end{code}
1214
1215 Note [Kind coercions]
1216 ~~~~~~~~~~~~~~~~~~~~~
1217 Kind coercions are only of the form: Refl kind. They are only used to
1218 instantiate kind polymorphic type constructors in TyConAppCo. Remember
1219 that kind instantiation only happens with TyConApp, not AppTy.