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