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