Mainly, rename LiteralTy to LitTy
[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,
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   | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey
322   | otherwise                         = False
323 \end{code}
324
325
326 \begin{code}
327 tyCoVarsOfCo :: Coercion -> VarSet
328 -- Extracts type and coercion variables from a coercion
329 tyCoVarsOfCo (Refl ty)           = tyVarsOfType ty
330 tyCoVarsOfCo (TyConAppCo _ cos)  = tyCoVarsOfCos cos
331 tyCoVarsOfCo (AppCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
332 tyCoVarsOfCo (ForAllCo tv co)    = tyCoVarsOfCo co `delVarSet` tv
333 tyCoVarsOfCo (CoVarCo v)         = unitVarSet v
334 tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
335 tyCoVarsOfCo (UnsafeCo ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
336 tyCoVarsOfCo (SymCo co)          = tyCoVarsOfCo co
337 tyCoVarsOfCo (TransCo co1 co2)   = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
338 tyCoVarsOfCo (NthCo _ co)        = tyCoVarsOfCo co
339 tyCoVarsOfCo (InstCo co ty)      = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
340
341 tyCoVarsOfCos :: [Coercion] -> VarSet
342 tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
343
344 coVarsOfCo :: Coercion -> VarSet
345 -- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
346 coVarsOfCo (Refl _)            = emptyVarSet
347 coVarsOfCo (TyConAppCo _ cos)  = coVarsOfCos cos
348 coVarsOfCo (AppCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
349 coVarsOfCo (ForAllCo _ co)     = coVarsOfCo co
350 coVarsOfCo (CoVarCo v)         = unitVarSet v
351 coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
352 coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
353 coVarsOfCo (SymCo co)          = coVarsOfCo co
354 coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
355 coVarsOfCo (NthCo _ co)        = coVarsOfCo co
356 coVarsOfCo (InstCo co _)       = coVarsOfCo co
357
358 coVarsOfCos :: [Coercion] -> VarSet
359 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
360
361 coercionSize :: Coercion -> Int
362 coercionSize (Refl ty)           = typeSize ty
363 coercionSize (TyConAppCo _ cos)  = 1 + sum (map coercionSize cos)
364 coercionSize (AppCo co1 co2)     = coercionSize co1 + coercionSize co2
365 coercionSize (ForAllCo _ co)     = 1 + coercionSize co
366 coercionSize (CoVarCo _)         = 1
367 coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
368 coercionSize (UnsafeCo ty1 ty2)  = typeSize ty1 + typeSize ty2
369 coercionSize (SymCo co)          = 1 + coercionSize co
370 coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
371 coercionSize (NthCo _ co)        = 1 + coercionSize co
372 coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
373 \end{code}
374
375 %************************************************************************
376 %*                                                                      *
377                    Pretty-printing coercions
378 %*                                                                      *
379 %************************************************************************
380
381 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
382 function is defined to use this.  @pprParendCo@ is the same, except it
383 puts parens around the type, except for the atomic cases.
384 @pprParendCo@ works just by setting the initial context precedence
385 very high.
386
387 \begin{code}
388 instance Outputable Coercion where
389   ppr = pprCo
390
391 pprCo, pprParendCo :: Coercion -> SDoc
392 pprCo       co = ppr_co TopPrec   co
393 pprParendCo co = ppr_co TyConPrec co
394
395 ppr_co :: Prec -> Coercion -> SDoc
396 ppr_co _ (Refl ty) = angleBrackets (ppr ty)
397
398 ppr_co p co@(TyConAppCo tc [_,_])
399   | tc `hasKey` funTyConKey = ppr_fun_co p co
400
401 ppr_co p (TyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
402 ppr_co p (AppCo co1 co2)       = maybeParen p TyConPrec $
403                                  pprCo co1 <+> ppr_co TyConPrec co2
404 ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
405 ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
406 ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
407
408 ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
409                              ppr_co FunPrec co1
410                              <+> ptext (sLit ";")
411                              <+> ppr_co FunPrec co2
412 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
413                           pprParendCo co <> ptext (sLit "@") <> pprType ty
414
415 ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) 
416                                            [pprParendType ty1, pprParendType ty2]
417 ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
418 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
419
420
421 ppr_fun_co :: Prec -> Coercion -> SDoc
422 ppr_fun_co p co = pprArrowChain p (split co)
423   where
424     split :: Coercion -> [SDoc]
425     split (TyConAppCo f [arg,res])
426       | f `hasKey` funTyConKey
427       = ppr_co FunPrec arg : split res
428     split co = [ppr_co TopPrec co]
429
430 ppr_forall_co :: Prec -> Coercion -> SDoc
431 ppr_forall_co p ty
432   = maybeParen p FunPrec $
433     sep [pprForAll tvs, ppr_co TopPrec rho]
434   where
435     (tvs,  rho) = split1 [] ty
436     split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
437     split1 tvs ty               = (reverse tvs, ty)
438 \end{code}
439
440 \begin{code}
441 pprCoAxiom :: CoAxiom -> SDoc
442 pprCoAxiom ax
443   = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax)
444         , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
445 \end{code}
446
447 %************************************************************************
448 %*                                                                      *
449         Functions over Kinds            
450 %*                                                                      *
451 %************************************************************************
452
453 \begin{code}
454 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
455 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
456 --
457 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
458 decomposeCo :: Arity -> Coercion -> [Coercion]
459 decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]
460                        -- Remember, Nth is zero-indexed
461
462 -- | Attempts to obtain the type variable underlying a 'Coercion'
463 getCoVar_maybe :: Coercion -> Maybe CoVar
464 getCoVar_maybe (CoVarCo cv) = Just cv  
465 getCoVar_maybe _            = Nothing
466
467 -- | Attempts to tease a coercion apart into a type constructor and the application
468 -- of a number of coercion arguments to that constructor
469 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
470 splitTyConAppCo_maybe (Refl ty)           = (fmap . second . map) Refl (splitTyConApp_maybe ty)
471 splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
472 splitTyConAppCo_maybe _                   = Nothing
473
474 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
475 -- ^ Attempt to take a coercion application apart.
476 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
477 splitAppCo_maybe (TyConAppCo tc cos)
478   | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc 
479   , Just (cos', co') <- snocView cos
480   = Just (mkTyConAppCo tc cos', co')    -- Never create unsaturated type family apps!
481        -- Use mkTyConAppCo to preserve the invariant
482        --  that identity coercions are always represented by Refl
483 splitAppCo_maybe (Refl ty) 
484   | Just (ty1, ty2) <- splitAppTy_maybe ty 
485   = Just (Refl ty1, Refl ty2)
486 splitAppCo_maybe _ = Nothing
487
488 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
489 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
490 splitForAllCo_maybe _                = Nothing
491
492 -------------------------------------------------------
493 -- and some coercion kind stuff
494
495 coVarKind :: CoVar -> (Type,Type) 
496 coVarKind cv
497  | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
498  = ASSERT (tc `hasKey` eqPrimTyConKey)
499    (ty1,ty2)
500  | otherwise = panic "coVarKind, non coercion variable"
501
502 -- | Makes a coercion type from two types: the types whose equality 
503 -- is proven by the relevant 'Coercion'
504 mkCoercionType :: Type -> Type -> Type
505 mkCoercionType = curry mkPrimEqType
506
507 isReflCo :: Coercion -> Bool
508 isReflCo (Refl {}) = True
509 isReflCo _         = False
510
511 isReflCo_maybe :: Coercion -> Maybe Type
512 isReflCo_maybe (Refl ty) = Just ty
513 isReflCo_maybe _         = Nothing
514 \end{code}
515
516 %************************************************************************
517 %*                                                                      *
518             Building coercions
519 %*                                                                      *
520 %************************************************************************
521
522 \begin{code}
523 mkCoVarCo :: CoVar -> Coercion
524 -- cv :: s ~# t
525 mkCoVarCo cv
526   | ty1 `eqType` ty2 = Refl ty1
527   | otherwise        = CoVarCo cv
528   where
529     (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
530
531 mkReflCo :: Type -> Coercion
532 mkReflCo = Refl
533
534 mkAxInstCo :: CoAxiom -> [Type] -> Coercion
535 -- mkAxInstCo can legitimately be called over-staturated; 
536 -- i.e. with more type arguments than the coercion requires
537 mkAxInstCo ax tys
538   | arity == n_tys = AxiomInstCo ax rtys
539   | otherwise      = ASSERT( arity < n_tys )
540                      foldl AppCo (AxiomInstCo ax (take arity rtys))
541                                  (drop arity rtys)
542   where
543     n_tys = length tys
544     arity = coAxiomArity ax
545     rtys  = map Refl tys
546
547 mkAxInstRHS :: CoAxiom -> [Type] -> Type
548 -- Instantiate the axiom with specified types,
549 -- returning the instantiated RHS
550 -- A companion to mkAxInstCo: 
551 --    mkAxInstRhs ax tys = snd (coercionKind (mkAxInstCo ax tys))
552 mkAxInstRHS ax tys
553   = ASSERT( tvs `equalLength` tys1 ) 
554     mkAppTys rhs' tys2
555   where
556     tvs          = coAxiomTyVars ax
557     (tys1, tys2) = splitAtList tvs tys
558     rhs'         = substTyWith tvs tys1 (coAxiomRHS ax)
559
560 -- | Apply a 'Coercion' to another 'Coercion'.
561 mkAppCo :: Coercion -> Coercion -> Coercion
562 mkAppCo (Refl ty1) (Refl ty2)       = Refl (mkAppTy ty1 ty2)
563 mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
564 mkAppCo (TyConAppCo tc cos) co      = TyConAppCo tc (cos ++ [co])
565 mkAppCo co1 co2                     = AppCo co1 co2
566 -- Note, mkAppCo is careful to maintain invariants regarding
567 -- where Refl constructors appear; see the comments in the definition
568 -- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
569
570 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
571 -- See also 'mkAppCo'
572 mkAppCos :: Coercion -> [Coercion] -> Coercion
573 mkAppCos co1 tys = foldl mkAppCo co1 tys
574
575 -- | Apply a type constructor to a list of coercions.
576 mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
577 mkTyConAppCo tc cos
578                -- Expand type synonyms
579   | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
580   = mkAppCos (liftCoSubst tv_co_prs rhs_ty) leftover_cos
581
582   | Just tys <- traverse isReflCo_maybe cos 
583   = Refl (mkTyConApp tc tys)    -- See Note [Refl invariant]
584
585   | otherwise = TyConAppCo tc cos
586
587 -- | Make a function 'Coercion' between two other 'Coercion's
588 mkFunCo :: Coercion -> Coercion -> Coercion
589 mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
590
591 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
592 mkForAllCo :: Var -> Coercion -> Coercion
593 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
594 mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
595 mkForAllCo tv  co       = ASSERT ( isTyVar tv ) ForAllCo tv co
596
597 -------------------------------
598
599 -- | Create a symmetric version of the given 'Coercion' that asserts
600 --   equality between the same types but in the other "direction", so
601 --   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
602 mkSymCo :: Coercion -> Coercion
603
604 -- Do a few simple optimizations, but don't bother pushing occurrences
605 -- of symmetry to the leaves; the optimizer will take care of that.
606 mkSymCo co@(Refl {})              = co
607 mkSymCo    (UnsafeCo ty1 ty2)    = UnsafeCo ty2 ty1
608 mkSymCo    (SymCo co)            = co
609 mkSymCo co                       = SymCo co
610
611 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
612 mkTransCo :: Coercion -> Coercion -> Coercion
613 mkTransCo (Refl _) co = co
614 mkTransCo co (Refl _) = co
615 mkTransCo co1 co2     = TransCo co1 co2
616
617 mkNthCo :: Int -> Coercion -> Coercion
618 mkNthCo n (Refl ty) = Refl (tyConAppArgN n ty)
619 mkNthCo n co        = NthCo n co
620
621 -- | Instantiates a 'Coercion' with a 'Type' argument. 
622 mkInstCo :: Coercion -> Type -> Coercion
623 mkInstCo co ty = InstCo co ty
624
625 -- | Manufacture a coercion from thin air. Needless to say, this is
626 --   not usually safe, but it is used when we know we are dealing with
627 --   bottom, which is one case in which it is safe.  This is also used
628 --   to implement the @unsafeCoerce#@ primitive.  Optimise by pushing
629 --   down through type constructors.
630 mkUnsafeCo :: Type -> Type -> Coercion
631 mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
632 mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
633   | tc1 == tc2
634   = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
635
636 mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
637   = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
638
639 mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
640
641 -- See note [Newtype coercions] in TyCon
642
643 -- | Create a coercion constructor (axiom) suitable for the given
644 --   newtype 'TyCon'. The 'Name' should be that of a new coercion
645 --   'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
646 --   the type the appropriate right hand side of the @newtype@, with
647 --   the free variables a subset of those 'TyVar's.
648 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
649 mkNewTypeCo name tycon tvs rhs_ty
650   = CoAxiom { co_ax_unique   = nameUnique name
651             , co_ax_name     = name
652             , co_ax_implicit = True  -- See Note [Implicit axioms] in TyCon
653             , co_ax_tvs      = tvs
654             , co_ax_lhs      = mkTyConApp tycon (mkTyVarTys tvs)
655             , co_ax_rhs      = rhs_ty }
656
657 mkPiCos :: [Var] -> Coercion -> Coercion
658 mkPiCos vs co = foldr mkPiCo co vs
659
660 mkPiCo  :: Var -> Coercion -> Coercion
661 mkPiCo v co | isTyVar v = mkForAllCo v co
662             | otherwise = mkFunCo (mkReflCo (varType v)) co
663 \end{code}
664
665 %************************************************************************
666 %*                                                                      *
667             Newtypes
668 %*                                                                      *
669 %************************************************************************
670
671 \begin{code}
672 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
673 -- ^ If @co :: T ts ~ rep_ty@ then:
674 --
675 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
676 instNewTyCon_maybe tc tys
677   | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
678   = ASSERT( tys `lengthIs` tyConArity tc )
679     Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
680   | otherwise
681   = Nothing
682
683 -- this is here to avoid module loops
684 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
685 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
686 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
687 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
688 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
689 --
690 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
691 --
692 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
693 splitNewTypeRepCo_maybe ty 
694   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
695 splitNewTypeRepCo_maybe (TyConApp tc tys)
696   | Just (ty', co) <- instNewTyCon_maybe tc tys
697   = case co of
698         Refl _ -> panic "splitNewTypeRepCo_maybe"
699                         -- This case handled by coreView
700         _      -> Just (ty', co)
701 splitNewTypeRepCo_maybe _
702   = Nothing
703
704 -- | Determines syntactic equality of coercions
705 coreEqCoercion :: Coercion -> Coercion -> Bool
706 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
707   where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
708
709 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
710 coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
711 coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
712   = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
713
714 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
715   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
716
717 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
718   = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
719
720 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
721   = rnOccL env cv1 == rnOccR env cv2
722
723 coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
724   = con1 == con2
725     && all2 (coreEqCoercion2 env) cos1 cos2
726
727 coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
728   = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
729
730 coreEqCoercion2 env (SymCo co1) (SymCo co2)
731   = coreEqCoercion2 env co1 co2
732
733 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
734   = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
735
736 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
737   = d1 == d2 && coreEqCoercion2 env co1 co2
738
739 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
740   = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
741
742 coreEqCoercion2 _ _ _ = False
743 \end{code}
744
745 %************************************************************************
746 %*                                                                      *
747                    Substitution of coercions
748 %*                                                                      *
749 %************************************************************************
750
751 \begin{code}
752 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
753 --   doing a \"lifting\" substitution)
754 type CvSubstEnv = VarEnv Coercion
755
756 emptyCvSubstEnv :: CvSubstEnv
757 emptyCvSubstEnv = emptyVarEnv
758
759 data CvSubst            
760   = CvSubst InScopeSet  -- The in-scope type variables
761             TvSubstEnv  -- Substitution of types
762             CvSubstEnv  -- Substitution of coercions
763
764 instance Outputable CvSubst where
765   ppr (CvSubst ins tenv cenv)
766     = brackets $ sep[ ptext (sLit "CvSubst"),
767                       nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
768                       nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
769                       nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
770
771 emptyCvSubst :: CvSubst
772 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
773
774 isEmptyCvSubst :: CvSubst -> Bool
775 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
776
777 getCvInScope :: CvSubst -> InScopeSet
778 getCvInScope (CvSubst in_scope _ _) = in_scope
779
780 zapCvSubstEnv :: CvSubst -> CvSubst
781 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
782
783 cvTvSubst :: CvSubst -> TvSubst
784 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
785
786 tvCvSubst :: TvSubst -> CvSubst
787 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
788
789 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
790 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
791   = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
792
793 extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
794 -- Also extends the in-scope set
795 extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
796   = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
797             tenv
798             (extendVarEnv cenv cv co)
799
800 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
801 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
802   = ASSERT( isCoVar old_var )
803     (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
804   where
805     -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
806     -- In that case, mkCoVarCo will return a ReflCoercion, and
807     -- we want to substitute that (not new_var) for old_var
808     new_co    = mkCoVarCo new_var
809     no_change = new_var == old_var && not (isReflCo new_co)
810
811     new_cenv | no_change = delVarEnv cenv old_var
812              | otherwise = extendVarEnv cenv old_var new_co
813
814     new_var = uniqAway in_scope subst_old_var
815     subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
816                   -- It's important to do the substitution for coercions,
817                   -- because they can have free type variables
818
819 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
820 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
821   = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
822       (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
823
824 mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
825 mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)
826
827 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
828 zipOpenCvSubst vs cos
829   | debugIsOn && (length vs /= length cos)
830   = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
831   | otherwise 
832   = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
833
834 substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
835 substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
836
837 substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
838 substCoWithTys in_scope tvs tys co
839   | debugIsOn && (length tvs /= length tys)
840   = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
841   | otherwise 
842   = ASSERT( length tvs == length tys )
843     substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
844
845 -- | Substitute within a 'Coercion'
846 substCo :: CvSubst -> Coercion -> Coercion
847 substCo subst co | isEmptyCvSubst subst = co
848                  | otherwise            = subst_co subst co
849
850 -- | Substitute within several 'Coercion's
851 substCos :: CvSubst -> [Coercion] -> [Coercion]
852 substCos subst cos | isEmptyCvSubst subst = cos
853                    | otherwise            = map (substCo subst) cos
854
855 substTy :: CvSubst -> Type -> Type
856 substTy subst = Type.substTy (cvTvSubst subst)
857
858 subst_co :: CvSubst -> Coercion -> Coercion
859 subst_co subst co
860   = go co
861   where
862     go_ty :: Type -> Type
863     go_ty = Coercion.substTy subst
864
865     go :: Coercion -> Coercion
866     go (Refl ty)             = Refl $! go_ty ty
867     go (TyConAppCo tc cos)   = let args = map go cos
868                                in  args `seqList` TyConAppCo tc args
869     go (AppCo co1 co2)       = mkAppCo (go co1) $! go co2
870     go (ForAllCo tv co)      = case substTyVarBndr subst tv of
871                                  (subst', tv') ->
872                                    ForAllCo tv' $! subst_co subst' co
873     go (CoVarCo cv)          = substCoVar subst cv
874     go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
875     go (UnsafeCo ty1 ty2)    = (UnsafeCo $! go_ty ty1) $! go_ty ty2
876     go (SymCo co)            = mkSymCo (go co)
877     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
878     go (NthCo d co)          = mkNthCo d (go co)
879     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
880
881 substCoVar :: CvSubst -> CoVar -> Coercion
882 substCoVar (CvSubst in_scope _ cenv) cv
883   | Just co  <- lookupVarEnv cenv cv      = co
884   | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
885   | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
886                 ASSERT( isCoVar cv ) CoVarCo cv
887
888 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
889 substCoVars subst cvs = map (substCoVar subst) cvs
890
891 lookupTyVar :: CvSubst -> TyVar  -> Maybe Type
892 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
893
894 lookupCoVar :: CvSubst -> Var  -> Maybe Coercion
895 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
896 \end{code}
897
898 %************************************************************************
899 %*                                                                      *
900                    "Lifting" substitution
901            [(TyVar,Coercion)] -> Type -> Coercion
902 %*                                                                      *
903 %************************************************************************
904
905 \begin{code}
906 data LiftCoSubst = LCS InScopeSet LiftCoEnv
907
908 type LiftCoEnv = VarEnv Coercion
909      -- Maps *type variables* to *coercions*
910      -- That's the whole point of this function!
911
912 liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
913 liftCoSubstWith tvs cos ty
914   = liftCoSubst (zipEqual "liftCoSubstWith" tvs cos) ty
915
916 liftCoSubst :: [(TyVar,Coercion)] -> Type -> Coercion
917 liftCoSubst prs ty
918  | null prs  = Refl ty
919  | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
920                                 (mkVarEnv prs)) ty
921
922 -- | The \"lifting\" operation which substitutes coercions for type
923 --   variables in a type to produce a coercion.
924 --
925 --   For the inverse operation, see 'liftCoMatch' 
926 ty_co_subst :: LiftCoSubst -> Type -> Coercion
927 ty_co_subst subst ty
928   = go ty
929   where
930     go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
931                              -- A type variable from a non-cloned forall
932                              -- won't be in the substitution
933     go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
934     go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
935                            -- IA0_NOTE: Do we need to do anything
936                            -- about kind instantiations? I don't think
937                            -- so.  see Note [Kind coercions]
938     go (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
939     go (ForAllTy v ty)   = mkForAllCo v' $! (ty_co_subst subst' ty)
940                          where
941                            (subst', v') = liftCoSubstTyVarBndr subst v
942     go ty@(LitTy {})     = mkReflCo ty
943
944 liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
945 liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv 
946
947 liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
948 liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
949   = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)               
950   where
951     new_cenv | no_change = delVarEnv cenv old_var
952              | otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
953
954     no_change = new_var == old_var
955     new_var = uniqAway in_scope old_var
956 \end{code}
957
958 \begin{code}
959 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
960 --   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
961 --   That is, it matches a type against a coercion of the same
962 --   "shape", and returns a lifting substitution which could have been
963 --   used to produce the given coercion from the given type.
964 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
965 liftCoMatch tmpls ty co 
966   = case ty_co_match menv emptyVarEnv ty co of
967       Just cenv -> Just (LCS in_scope cenv)
968       Nothing   -> Nothing
969   where
970     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
971     in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
972     -- Like tcMatchTy, assume all the interesting variables 
973     -- in ty are in tmpls
974
975 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
976 ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
977 ty_co_match menv subst ty co 
978   | Just ty' <- coreView ty = ty_co_match menv subst ty' co
979
980   -- Match a type variable against a non-refl coercion
981 ty_co_match menv cenv (TyVarTy tv1) co
982   | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
983   = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
984     then Just cenv
985     else Nothing       -- no match since tv1 matches two different coercions
986
987   | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
988   = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
989     then Nothing      -- occurs check failed
990     else return (extendVarEnv cenv tv1' co)
991         -- BAY: I don't think we need to do any kind matching here yet
992         -- (compare 'match'), but we probably will when moving to SHE.
993
994   | otherwise    -- tv1 is not a template ty var, so the only thing it
995                  -- can match is a reflexivity coercion for itself.
996                  -- But that case is dealt with already
997   = Nothing
998
999   where
1000     rn_env = me_env menv
1001     tv1' = rnOccL rn_env tv1
1002
1003 ty_co_match menv subst (AppTy ty1 ty2) co
1004   | Just (co1, co2) <- splitAppCo_maybe co      -- c.f. Unify.match on AppTy
1005   = do { subst' <- ty_co_match menv subst ty1 co1 
1006        ; ty_co_match menv subst' ty2 co2 }
1007
1008 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
1009   | tc1 == tc2 = ty_co_matches menv subst tys cos
1010
1011 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
1012   | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1013
1014 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co) 
1015   = ty_co_match menv' subst ty co
1016   where
1017     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1018
1019 ty_co_match menv subst ty co
1020   | Just co' <- pushRefl co = ty_co_match menv subst ty co'
1021   | otherwise               = Nothing
1022
1023 ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1024 ty_co_matches menv = matchList (ty_co_match menv)
1025
1026 pushRefl :: Coercion -> Maybe Coercion
1027 pushRefl (Refl (AppTy ty1 ty2))   = Just (AppCo (Refl ty1) (Refl ty2))
1028 pushRefl (Refl (FunTy ty1 ty2))   = Just (TyConAppCo funTyCon [Refl ty1, Refl ty2])
1029 pushRefl (Refl (TyConApp tc tys)) = Just (TyConAppCo tc (map Refl tys))
1030 pushRefl (Refl (ForAllTy tv ty))  = Just (ForAllCo tv (Refl ty))
1031 pushRefl _                        = Nothing
1032 \end{code}
1033
1034 %************************************************************************
1035 %*                                                                      *
1036             Sequencing on coercions
1037 %*                                                                      *
1038 %************************************************************************
1039
1040 \begin{code}
1041 seqCo :: Coercion -> ()
1042 seqCo (Refl ty)             = seqType ty
1043 seqCo (TyConAppCo tc cos)   = tc `seq` seqCos cos
1044 seqCo (AppCo co1 co2)       = seqCo co1 `seq` seqCo co2
1045 seqCo (ForAllCo tv co)      = tv `seq` seqCo co
1046 seqCo (CoVarCo cv)          = cv `seq` ()
1047 seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
1048 seqCo (UnsafeCo ty1 ty2)    = seqType ty1 `seq` seqType ty2
1049 seqCo (SymCo co)            = seqCo co
1050 seqCo (TransCo co1 co2)     = seqCo co1 `seq` seqCo co2
1051 seqCo (NthCo _ co)          = seqCo co
1052 seqCo (InstCo co ty)        = seqCo co `seq` seqType ty
1053
1054 seqCos :: [Coercion] -> ()
1055 seqCos []       = ()
1056 seqCos (co:cos) = seqCo co `seq` seqCos cos
1057 \end{code}
1058
1059
1060 %************************************************************************
1061 %*                                                                      *
1062              The kind of a type, and of a coercion
1063 %*                                                                      *
1064 %************************************************************************
1065
1066 \begin{code}
1067 coercionType :: Coercion -> Type
1068 coercionType co = case coercionKind co of
1069                     Pair ty1 ty2 -> mkCoercionType ty1 ty2
1070
1071 ------------------
1072 -- | If it is the case that
1073 --
1074 -- > c :: (t1 ~ t2)
1075 --
1076 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1077
1078 coercionKind :: Coercion -> Pair Type 
1079 coercionKind co = go co
1080   where 
1081     go (Refl ty)            = Pair ty ty
1082     go (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
1083     go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
1084     go (ForAllCo tv co)     = mkForAllTy tv <$> go co
1085     go (CoVarCo cv)         = toPair $ coVarKind cv
1086     go (AxiomInstCo ax cos) = let Pair tys1 tys2 = sequenceA $ map go cos 
1087                               in  Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) 
1088                                        (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
1089     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
1090     go (SymCo co)           = swap $ go co
1091     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
1092     go (NthCo d co)         = tyConAppArgN d <$> go co
1093     go (InstCo aco ty)      = go_app aco [ty]
1094
1095     go_app :: Coercion -> [Type] -> Pair Type
1096     -- Collect up all the arguments and apply all at once
1097     -- See Note [Nested InstCos]
1098     go_app (InstCo co ty) tys = go_app co (ty:tys)
1099     go_app co             tys = (`applyTys` tys) <$> go co
1100
1101 -- | Apply 'coercionKind' to multiple 'Coercion's
1102 coercionKinds :: [Coercion] -> Pair [Type]
1103 coercionKinds tys = sequenceA $ map coercionKind tys
1104 \end{code}
1105
1106 Note [Nested InstCos]
1107 ~~~~~~~~~~~~~~~~~~~~~
1108 In Trac #5631 we found that 70% of the entire compilation time was
1109 being spent in coercionKind!  The reason was that we had
1110    (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
1111 where 
1112    g :: forall a1 a2 .. a100. phi
1113 If we deal with the InstCos one at a time, we'll do this:
1114    1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
1115    2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
1116 But this is a *quadratic* algorithm, and the blew up Trac #5631.
1117 So it's very important to do the substitution simultaneously.
1118
1119 cf Type.applyTys (which in fact we call here)
1120
1121
1122 \begin{code}
1123 applyCo :: Type -> Coercion -> Type
1124 -- Gives the type of (e co) where e :: (a~b) => ty
1125 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
1126 applyCo (FunTy _ ty) _ = ty
1127 applyCo _            _ = panic "applyCo"
1128 \end{code}
1129
1130 Note [Kind coercions]
1131 ~~~~~~~~~~~~~~~~~~~~~
1132 Kind coercions are only of the form: Refl kind. They are only used to
1133 instantiate kind polymorphic type constructors in TyConAppCo. Remember
1134 that kind instantiation only happens with TyConApp, not AppTy.