2 % (c) The University of Glasgow 2006
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.
12 Coercion(..), Var, CoVar,
14 -- ** Deconstructing Kinds
15 kindFunResult, kindAppResult, synTyConResKind,
16 splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
18 -- ** Predicates on Kinds
19 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
20 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
21 isSuperKind, isCoercionKind,
22 mkArrowKind, mkArrowKinds,
24 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
27 mkCoType, coVarKind, coVarKind_maybe,
28 coercionType, coercionKind, coercionKinds, isReflCo,
30 -- ** Constructing coercions
32 mkAxInstCo, mkPiCo, mkPiCos,
33 mkSymCo, mkTransCo, mkNthCo,
34 mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
35 mkForAllCo, mkUnsafeCo,
36 mkNewTypeCo, mkFamInstCo,
41 splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
44 splitTyConAppCo_maybe,
48 -- ** Coercion variables
49 mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
52 tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
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,
65 liftCoMatch, liftCoSubst, liftCoSubstTyVar, liftCoSubstWith,
68 coreEqCoercion, coreEqCoercion2,
70 -- ** Forcing evaluation of coercions
81 #include "HsVersions.h"
83 import Unify ( MatchEnv(..), ruleMatchTyX, matchList )
86 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
92 import UniqFM ( minusUFM )
93 import Maybes ( orElse )
94 import Name ( Name, NamedThing(..), nameUnique )
95 import OccName ( isSymOcc )
101 import PrelNames( funTyConKey )
102 import Control.Applicative
103 import Data.Traversable (traverse, sequenceA)
104 import Control.Arrow (second)
107 import qualified Data.Data as Data hiding ( TyCon )
110 %************************************************************************
114 %************************************************************************
117 -- | A 'Coercion' is concrete evidence of the equality/convertibility
120 -- These ones mirror the shape of types
121 = Refl Type -- See Note [Refl invariant]
122 -- Invariant: applications of (Refl T) to a bunch of identity coercions
123 -- always show up as Refl.
124 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
126 -- Applications of (Refl T) to some coercions, at least one of
127 -- which is NOT the identity, show up as TyConAppCo.
128 -- (They may not be fully saturated however.)
129 -- ConAppCo coercions (like all coercions other than Refl)
130 -- are NEVER the identity.
132 -- These ones simply lift the correspondingly-named
133 -- Type constructors into Coercions
134 | TyConAppCo TyCon [Coercion] -- lift TyConApp
135 -- The TyCon is never a synonym;
136 -- we expand synonyms eagerly
138 | AppCo Coercion Coercion -- lift AppTy
140 -- See Note [Forall coercions]
141 | ForAllCo TyVar Coercion -- forall a. g
142 | PredCo (Pred Coercion) -- (g1~g2) etc
146 | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely*
147 -- saturate arity of CoAxiom.
148 -- See [Coercion axioms applied to coercions]
151 | TransCo Coercion Coercion
153 -- These are destructors
154 | NthCo Int Coercion -- Zero-indexed
155 | InstCo Coercion Type
156 deriving (Data.Data, Data.Typeable)
159 Note [Refl invariant]
160 ~~~~~~~~~~~~~~~~~~~~~
161 Coercions have the following invariant
162 Refl is always lifted as far as possible.
164 You might think that a consequencs is:
165 Every identity coercions has Refl at the root
167 But that's not quite true because of coercion variables. Consider
169 Left h where h :: Maybe Int ~ Maybe Int
170 etc. So the consequence is only true of coercions that
171 have no coercion variables.
173 Note [Coercion axioms applied to coercions]
174 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
175 The reason coercion axioms can be applied to coercions and not just
176 types is to allow for better optimization. There are some cases where
177 we need to be able to "push transitivity inside" an axiom in order to
178 expose further opportunities for optimization.
180 For example, suppose we have
185 and we want to optimize
187 sym (C b) ; t[g] ; C c
193 (stopping through t[b] and t[c] along the way).
195 We'd like to optimize this to just F g -- but how? The key is
196 that we need to allow axioms to be instantiated by *coercions*,
197 not just by types. Then we can (in certain cases) push
198 transitivity inside the axiom instantiations, and then react
199 opposite-polarity instantiations of the same axiom. In this
200 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
201 obtain the substitution a |-> g (note this operation is sort
202 of the dual of lifting!) and hence end up with
206 which indeed has the same kind as t[g] ; C c.
212 which can be optimized to F g.
215 Note [Forall coercions]
216 ~~~~~~~~~~~~~~~~~~~~~~~
217 Constructing coercions between forall-types can be a bit tricky.
218 Currently, the situation is as follows:
220 ForAllCo TyVar Coercion
222 represents a coercion between polymorphic types, with the rule
225 ----------------------------------------------
226 ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
228 Note that it's only necessary to coerce between polymorphic types
229 where the type variables have identical kinds, because equality on
232 ForAllCoCo Coercion Coercion Coercion
234 represents a coercion between types abstracted over equality proofs,
235 which we might more suggestively write as
237 ForAllCoCo (_:Coercion~Coercion) Coercion
241 g1 : t1 ~ t1' g2 : t2 ~ t2' g3 : t3 ~ t3'
242 ------------------------------------------------------------------
243 ForAllCoCo g1 g2 g3 : ( (t1 ~ t2) => t3 ) ~ ( (t1' ~ t2') => t3' )
245 There are several things to note. First, we don't need to bind a
246 variable, since coercion variables do not appear in types. Second,
247 note that here we DO need to convert between "kinds" (the types of the
250 In the future, if we collapse the type and kind levels and add a bit
251 more dependency, we will need something like
253 | ForAllCo TyVar Coercion Coercion
254 | ForAllCoCo CoVar Coercion Coercion Coercion
256 The addition of the extra coercion in the first case handles
257 converting between possibly different kinds; the addition of a CoVar
258 in the second case is needed since now types may mention coercion
259 variables (in casts).
262 %************************************************************************
264 \subsection{Coercion variables}
266 %************************************************************************
269 coVarName :: CoVar -> Name
272 setCoVarUnique :: CoVar -> Unique -> CoVar
273 setCoVarUnique = setVarUnique
275 setCoVarName :: CoVar -> Name -> CoVar
276 setCoVarName = setVarName
278 isCoVar :: Var -> Bool
279 isCoVar v = isCoVarType (varType v)
281 isCoVarType :: Type -> Bool
282 isCoVarType = isEqPredTy
287 tyCoVarsOfCo :: Coercion -> VarSet
288 -- Extracts type and coercion variables from a coercion
289 tyCoVarsOfCo (Refl ty) = tyVarsOfType ty
290 tyCoVarsOfCo (TyConAppCo _ cos) = tyCoVarsOfCos cos
291 tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
292 tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
293 tyCoVarsOfCo (PredCo pred) = varsOfPred tyCoVarsOfCo pred
294 tyCoVarsOfCo (CoVarCo v) = unitVarSet v
295 tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
296 tyCoVarsOfCo (UnsafeCo ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
297 tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
298 tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
299 tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
300 tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
302 tyCoVarsOfCos :: [Coercion] -> VarSet
303 tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
305 coVarsOfCo :: Coercion -> VarSet
306 -- Extract *coerction* variables only. Tiresome to repeat the code, but easy.
307 coVarsOfCo (Refl _) = emptyVarSet
308 coVarsOfCo (TyConAppCo _ cos) = coVarsOfCos cos
309 coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
310 coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
311 coVarsOfCo (PredCo pred) = varsOfPred coVarsOfCo pred
312 coVarsOfCo (CoVarCo v) = unitVarSet v
313 coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
314 coVarsOfCo (UnsafeCo _ _) = emptyVarSet
315 coVarsOfCo (SymCo co) = coVarsOfCo co
316 coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
317 coVarsOfCo (NthCo _ co) = coVarsOfCo co
318 coVarsOfCo (InstCo co _) = coVarsOfCo co
320 coVarsOfCos :: [Coercion] -> VarSet
321 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
323 coercionSize :: Coercion -> Int
324 coercionSize (Refl ty) = typeSize ty
325 coercionSize (TyConAppCo _ cos) = 1 + sum (map coercionSize cos)
326 coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
327 coercionSize (ForAllCo _ co) = 1 + coercionSize co
328 coercionSize (PredCo pred) = predSize coercionSize pred
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
338 %************************************************************************
340 Pretty-printing coercions
342 %************************************************************************
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
351 instance Outputable Coercion where
354 pprCo, pprParendCo :: Coercion -> SDoc
355 pprCo co = ppr_co TopPrec co
356 pprParendCo co = ppr_co TyConPrec co
358 ppr_co :: Prec -> Coercion -> SDoc
359 ppr_co _ (Refl ty) = angles (ppr ty)
361 ppr_co p co@(TyConAppCo tc cos)
362 | tc `hasKey` funTyConKey = ppr_fun_co p co
363 | otherwise = maybeParen p TyConPrec $
364 pprTcApp p ppr_co tc cos
366 ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
367 pprCo co1 <+> ppr_co TyConPrec co2
369 ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
370 ppr_co _ (PredCo pred) = pprPred ppr_co pred
372 ppr_co _ (CoVarCo cv)
373 | isSymOcc (getOccName cv) = parens (ppr cv)
376 ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
379 ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
382 <+> ppr_co FunPrec co2
383 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
384 pprParendCo co <> ptext (sLit "@") <> pprType ty
386 ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) [pprParendType ty1, pprParendType ty2]
387 ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
388 ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
391 angles :: SDoc -> SDoc
392 angles p = char '<' <> p <> char '>'
394 ppr_fun_co :: Prec -> Coercion -> SDoc
395 ppr_fun_co p co = pprArrowChain p (split co)
397 split (TyConAppCo f [arg,res])
398 | f `hasKey` funTyConKey
399 = ppr_co FunPrec arg : split res
400 split co = [ppr_co TopPrec co]
402 ppr_forall_co :: Prec -> Coercion -> SDoc
404 = maybeParen p FunPrec $
405 sep [pprForAll tvs, pprThetaArrow ppr_co ctxt, ppr_co TopPrec tau]
407 (tvs, rho) = split1 [] ty
408 (ctxt, tau) = split2 [] rho
410 -- We need to be extra careful here as equality constraints will occur as
411 -- type variables with an equality kind. So, while collecting quantified
412 -- variables, we separate the coercion variables out and turn them into
413 -- equality predicates.
414 split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
415 split1 tvs ty = (reverse tvs, ty)
417 split2 ps (TyConAppCo tc [PredCo p, co])
418 | tc `hasKey` funTyConKey = split2 (p:ps) co
419 split2 ps co = (reverse ps, co)
423 %************************************************************************
427 %************************************************************************
430 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
431 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
433 -- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
434 decomposeCo :: Arity -> Coercion -> [Coercion]
435 decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]
437 -- | Attempts to obtain the type variable underlying a 'Coercion'
438 getCoVar_maybe :: Coercion -> Maybe CoVar
439 getCoVar_maybe (CoVarCo cv) = Just cv
440 getCoVar_maybe _ = Nothing
442 -- | Attempts to tease a coercion apart into a type constructor and the application
443 -- of a number of coercion arguments to that constructor
444 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
445 splitTyConAppCo_maybe (Refl ty) = (fmap . second . map) Refl (splitTyConApp_maybe ty)
446 splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
447 splitTyConAppCo_maybe _ = Nothing
449 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
450 -- ^ Attempt to take a coercion application apart.
451 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
452 splitAppCo_maybe (TyConAppCo tc cos)
453 | not (null cos) = Just (mkTyConAppCo tc (init cos), last cos)
454 -- Use mkTyConAppCo to preserve the invariant
455 -- that identity coercions are always represented by Refl
456 splitAppCo_maybe (Refl ty)
457 | Just (ty1, ty2) <- splitAppTy_maybe ty = Just (Refl ty1, Refl ty2)
458 | otherwise = Nothing
459 splitAppCo_maybe _ = Nothing
461 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
462 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
463 splitForAllCo_maybe _ = Nothing
465 -------------------------------------------------------
466 -- and some coercion kind stuff
468 coVarPred :: CoVar -> PredType
470 = ASSERT( isCoVar cv )
471 case splitPredTy_maybe (varType cv) of
473 other -> pprPanic "coVarPred" (ppr cv $$ ppr other)
475 coVarKind :: CoVar -> (Type,Type)
477 coVarKind cv = case coVarKind_maybe cv of
479 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
481 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
482 coVarKind_maybe cv = splitEqPredTy_maybe (varType cv)
484 -- | Makes a coercion type from two types: the types whose equality
485 -- is proven by the relevant 'Coercion'
486 mkCoType :: Type -> Type -> Type
487 mkCoType ty1 ty2 = PredTy (EqPred ty1 ty2)
489 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
490 splitCoPredTy_maybe ty
491 | Just (cv,r) <- splitForAllTy_maybe ty
493 , Just (s,t) <- coVarKind_maybe cv
498 isReflCo :: Coercion -> Bool
499 isReflCo (Refl {}) = True
502 isReflCo_maybe :: Coercion -> Maybe Type
503 isReflCo_maybe (Refl ty) = Just ty
504 isReflCo_maybe _ = Nothing
507 %************************************************************************
511 %************************************************************************
514 mkCoVarCo :: CoVar -> Coercion
516 | ty1 `eqType` ty2 = Refl ty1
517 | otherwise = CoVarCo cv
519 (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
521 mkReflCo :: Type -> Coercion
524 mkAxInstCo :: CoAxiom -> [Type] -> Coercion
526 | arity == n_tys = AxiomInstCo ax rtys
527 | otherwise = ASSERT( arity < n_tys )
528 foldl AppCo (AxiomInstCo ax (take arity rtys))
532 arity = coAxiomArity ax
535 -- | Apply a 'Coercion' to another 'Coercion'.
536 mkAppCo :: Coercion -> Coercion -> Coercion
537 mkAppCo (Refl ty1) (Refl ty2) = Refl (mkAppTy ty1 ty2)
538 mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
539 mkAppCo (TyConAppCo tc cos) co = TyConAppCo tc (cos ++ [co])
540 mkAppCo co1 co2 = AppCo co1 co2
541 -- Note, mkAppCo is careful to maintain invariants regarding
542 -- where Refl constructors appear; see the comments in the definition
543 -- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
545 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
546 -- See also 'mkAppCo'
547 mkAppCos :: Coercion -> [Coercion] -> Coercion
548 mkAppCos co1 tys = foldl mkAppCo co1 tys
550 -- | Apply a type constructor to a list of coercions.
551 mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
553 -- Expand type synonyms
554 | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
555 = mkAppCos (liftCoSubst (mkTopCvSubst tv_co_prs) rhs_ty) leftover_cos
557 | Just tys <- traverse isReflCo_maybe cos
558 = Refl (mkTyConApp tc tys) -- See Note [Refl invariant]
560 | otherwise = TyConAppCo tc cos
562 -- | Make a function 'Coercion' between two other 'Coercion's
563 mkFunCo :: Coercion -> Coercion -> Coercion
564 mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
566 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
567 mkForAllCo :: Var -> Coercion -> Coercion
568 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
569 mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
570 mkForAllCo tv co = ASSERT ( isTyVar tv ) ForAllCo tv co
572 mkPredCo :: Pred Coercion -> Coercion
574 = case traverse isReflCo_maybe pred_co of
575 Just pred_ty -> Refl (PredTy pred_ty)
576 Nothing -> PredCo pred_co
578 -------------------------------
580 -- | Create a symmetric version of the given 'Coercion' that asserts
581 -- equality between the same types but in the other "direction", so
582 -- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
583 mkSymCo :: Coercion -> Coercion
585 -- Do a few simple optimizations, but don't bother pushing occurrences
586 -- of symmetry to the leaves; the optimizer will take care of that.
587 mkSymCo co@(Refl {}) = co
588 mkSymCo (UnsafeCo ty1 ty2) = UnsafeCo ty2 ty1
589 mkSymCo (SymCo co) = co
590 mkSymCo co = SymCo co
592 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
593 mkTransCo :: Coercion -> Coercion -> Coercion
594 mkTransCo (Refl _) co = co
595 mkTransCo co (Refl _) = co
596 mkTransCo co1 co2 = TransCo co1 co2
598 mkNthCo :: Int -> Coercion -> Coercion
599 mkNthCo n (Refl ty) = Refl (getNth n ty)
600 mkNthCo n co = NthCo n co
602 -- | Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
603 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
604 mkInstCo :: Coercion -> Type -> Coercion
605 mkInstCo (ForAllCo tv co) ty = substCoWithTy tv ty co
606 mkInstCo co ty = InstCo co ty
608 -- | Manufacture a coercion from thin air. Needless to say, this is
609 -- not usually safe, but it is used when we know we are dealing with
610 -- bottom, which is one case in which it is safe. This is also used
611 -- to implement the @unsafeCoerce#@ primitive. Optimise by pushing
612 -- down through type constructors.
613 mkUnsafeCo :: Type -> Type -> Coercion
614 mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
615 mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
617 = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
619 mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
620 = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
622 mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
624 -- See note [Newtype coercions] in TyCon
626 -- | Create a coercion constructor (axiom) suitable for the given
627 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
628 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
629 -- the type the appropriate right hand side of the @newtype@, with
630 -- the free variables a subset of those 'TyVar's.
631 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
632 mkNewTypeCo name tycon tvs rhs_ty
633 = CoAxiom { co_ax_unique = nameUnique name
636 , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
637 , co_ax_rhs = rhs_ty }
639 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
640 -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
641 -- the coercion constructor built here, @F@ the family tycon and @R@ the (derived)
642 -- representation tycon.
643 mkFamInstCo :: Name -- ^ Unique name for the coercion tycon
644 -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
645 -> TyCon -- ^ Family tycon (@F@)
646 -> [Type] -- ^ Type instance (@ts@)
647 -> TyCon -- ^ Representation tycon (@R@)
648 -> CoAxiom -- ^ Coercion constructor (@Co@)
649 mkFamInstCo name tvs family inst_tys rep_tycon
650 = CoAxiom { co_ax_unique = nameUnique name
653 , co_ax_lhs = mkTyConApp family inst_tys
654 , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
656 mkPiCos :: [Var] -> Coercion -> Coercion
657 mkPiCos vs co = foldr mkPiCo co vs
659 mkPiCo :: Var -> Coercion -> Coercion
660 mkPiCo v co | isTyVar v = mkForAllCo v co
661 | otherwise = mkFunCo (mkReflCo (varType v)) co
664 %************************************************************************
668 %************************************************************************
671 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
672 -- ^ If @co :: T ts ~ rep_ty@ then:
674 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
675 instNewTyCon_maybe tc tys
676 | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
677 = ASSERT( tys `lengthIs` tyConArity tc )
678 Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
682 -- this is here to avoid module loops
683 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
684 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
685 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
686 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
687 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
689 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
691 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
692 splitNewTypeRepCo_maybe ty
693 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
694 splitNewTypeRepCo_maybe (TyConApp tc tys)
695 | Just (ty', co) <- instNewTyCon_maybe tc tys
697 Refl _ -> panic "splitNewTypeRepCo_maybe"
698 -- This case handled by coreView
700 splitNewTypeRepCo_maybe _
703 -- | Determines syntactic equality of coercions
704 coreEqCoercion :: Coercion -> Coercion -> Bool
705 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
706 where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
708 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
709 coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
710 coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
711 = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
713 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
714 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
716 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
717 = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
719 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
720 = rnOccL env cv1 == rnOccR env cv2
722 coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
724 && all2 (coreEqCoercion2 env) cos1 cos2
726 coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
727 = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
729 coreEqCoercion2 env (SymCo co1) (SymCo co2)
730 = coreEqCoercion2 env co1 co2
732 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
733 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
735 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
736 = d1 == d2 && coreEqCoercion2 env co1 co2
738 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
739 = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
741 coreEqCoercion2 _ _ _ = False
744 %************************************************************************
746 Substitution of coercions
748 %************************************************************************
751 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
752 -- doing a \"lifting\" substitution)
753 type CvSubstEnv = VarEnv Coercion
755 emptyCvSubstEnv :: CvSubstEnv
756 emptyCvSubstEnv = emptyVarEnv
759 = CvSubst InScopeSet -- The in-scope type variables
760 TvSubstEnv -- Substitution of types
761 CvSubstEnv -- Substitution of coercions
763 instance Outputable CvSubst where
764 ppr (CvSubst ins tenv cenv)
765 = brackets $ sep[ ptext (sLit "CvSubst"),
766 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
767 nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
768 nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
770 emptyCvSubst :: CvSubst
771 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
773 isEmptyCvSubst :: CvSubst -> Bool
774 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
776 getCvInScope :: CvSubst -> InScopeSet
777 getCvInScope (CvSubst in_scope _ _) = in_scope
779 zapCvSubstEnv :: CvSubst -> CvSubst
780 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
782 cvTvSubst :: CvSubst -> TvSubst
783 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
785 tvCvSubst :: TvSubst -> CvSubst
786 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
788 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
789 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
790 = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
792 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
793 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
794 = ASSERT( isCoVar old_var )
795 (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
797 -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
798 -- In that case, mkCoVarCo will return a ReflCoercion, and
799 -- we want to substitute that (not new_var) for old_var
800 new_co = mkCoVarCo new_var
801 no_change = new_var == old_var && not (isReflCo new_co)
803 new_cenv | no_change = delVarEnv cenv old_var
804 | otherwise = extendVarEnv cenv old_var new_co
806 new_var = uniqAway in_scope subst_old_var
807 subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
808 -- It's important to do the substitution for coercions,
809 -- because only they can have free type variables
811 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
812 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
813 = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
814 (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
816 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
817 zipOpenCvSubst vs cos
818 | debugIsOn && (length vs /= length cos)
819 = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
821 = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
823 mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
824 mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
826 substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
827 substCoWithTy tv ty = substCoWithTys [tv] [ty]
829 substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
830 substCoWithTys tvs tys co
831 | debugIsOn && (length tvs /= length tys)
832 = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
834 = ASSERT( length tvs == length tys )
835 substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
837 in_scope = mkInScopeSet (tyVarsOfTypes tys)
839 -- | Substitute within a 'Coercion'
840 substCo :: CvSubst -> Coercion -> Coercion
841 substCo subst co | isEmptyCvSubst subst = co
842 | otherwise = subst_co subst co
844 -- | Substitute within several 'Coercion's
845 substCos :: CvSubst -> [Coercion] -> [Coercion]
846 substCos subst cos | isEmptyCvSubst subst = cos
847 | otherwise = map (substCo subst) cos
849 substTy :: CvSubst -> Type -> Type
850 substTy subst = Type.substTy (cvTvSubst subst)
852 subst_co :: CvSubst -> Coercion -> Coercion
856 go_ty :: Type -> Type
857 go_ty = Coercion.substTy subst
859 go :: Coercion -> Coercion
860 go (Refl ty) = Refl $! go_ty ty
861 go (TyConAppCo tc cos) = let args = map go cos
862 in args `seqList` TyConAppCo tc args
864 go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
865 go (ForAllCo tv co) = case substTyVarBndr subst tv of
867 ForAllCo tv' $! subst_co subst' co
869 go (PredCo p) = mkPredCo (go <$> p)
870 go (CoVarCo cv) = substCoVar subst cv
871 go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
872 go (UnsafeCo ty1 ty2) = (UnsafeCo $! go_ty ty1) $! go_ty ty2
873 go (SymCo co) = mkSymCo (go co)
874 go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
875 go (NthCo d co) = mkNthCo d (go co)
876 go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
878 substCoVar :: CvSubst -> CoVar -> Coercion
879 substCoVar (CvSubst in_scope _ cenv) cv
880 | Just co <- lookupVarEnv cenv cv = co
881 | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
882 | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
883 ASSERT( isCoVar cv ) CoVarCo cv
885 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
886 substCoVars subst cvs = map (substCoVar subst) cvs
888 lookupTyVar :: CvSubst -> TyVar -> Maybe Type
889 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
891 lookupCoVar :: CvSubst -> Var -> Maybe Coercion
892 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
895 %************************************************************************
897 "Lifting" substitution
898 [(TyVar,Coercion)] -> Type -> Coercion
900 %************************************************************************
903 liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
904 liftCoSubstWith tvs cos = liftCoSubst (zipOpenCvSubst tvs cos)
906 -- | The \"lifting\" operation which substitutes coercions for type
907 -- variables in a type to produce a coercion.
909 -- For the inverse operation, see 'liftCoMatch'
910 liftCoSubst :: CvSubst -> Type -> Coercion
911 -- The CvSubst maps TyVar -> Type (mainly for cloning foralls)
912 -- TyVar -> Coercion (this is the payload)
913 -- The unusual thing is that the *coercion* substitution maps
914 -- some *type* variables. That's the whole point of this function!
915 liftCoSubst subst ty | isEmptyCvSubst subst = Refl ty
916 | otherwise = ty_co_subst subst ty
918 ty_co_subst :: CvSubst -> Type -> Coercion
922 go (TyVarTy tv) = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
923 go (AppTy ty1 ty2) = mkAppCo (go ty1) (go ty2)
924 go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
925 go (FunTy ty1 ty2) = mkFunCo (go ty1) (go ty2)
926 go (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' ty)
928 (subst', v') = liftCoSubstTyVarBndr subst v
929 go (PredTy p) = mkPredCo (go <$> p)
931 liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
932 liftCoSubstTyVar subst@(CvSubst _ tenv cenv) tv
933 = case (lookupVarEnv tenv tv, lookupVarEnv cenv tv) of
934 (Nothing, Nothing) -> Nothing
935 (Just ty, Nothing) -> Just (Refl ty)
936 (Nothing, Just co) -> Just co
937 (Just {}, Just {}) -> pprPanic "ty_co_subst" (ppr tv $$ ppr subst)
939 liftCoSubstTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
940 liftCoSubstTyVarBndr (CvSubst in_scope tenv cenv) old_var
941 = (CvSubst (in_scope `extendInScopeSet` new_var)
943 (delVarEnv cenv old_var) -- See Note [Lifting substitutions]
946 new_tenv | no_change = delVarEnv tenv old_var
947 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
949 no_change = new_var == old_var
950 new_var = uniqAway in_scope old_var
953 Note [Lifting substitutions]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 Consider liftCoSubstWith [a] [co] (a, forall a. a)
956 Then we want to substitute for the free 'a', but obviously not for
957 the bound 'a'. hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr.
959 This also why we need a full CvSubst when doing lifting substitutions.
962 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
963 -- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
964 -- That is, it matches a type against a coercion of the same
965 -- "shape", and returns a lifting substitution which could have been
966 -- used to produce the given coercion from the given type.
967 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
968 liftCoMatch tmpls ty co
969 = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of
970 Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env)
973 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
974 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
975 -- Like tcMatchTy, assume all the interesting variables
976 -- in ty are in tmpls
978 type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv)
979 -- Used locally inside ty_co_match only
981 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
982 ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv
983 ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co
985 -- Deal with the Refl case by delegating to type matching
986 ty_co_match menv (tenv, cenv) ty co
987 | Just ty' <- isReflCo_maybe co
988 = case ruleMatchTyX ty_menv tenv ty ty' of
989 Just tenv' -> Just (tenv', cenv)
992 ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv }
993 -- Remove from the template set any variables already bound to non-refl coercions
995 -- Match a type variable against a non-refl coercion
996 ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co
997 | Just {} <- lookupVarEnv tenv tv1' -- tv1' is already bound to (Refl ty)
998 = Nothing -- The coercion 'co' is not Refl
1000 | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
1001 = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
1003 else Nothing -- no match since tv1 matches two different coercions
1005 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1006 = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
1007 then Nothing -- occurs check failed
1008 else return (tenv, extendVarEnv cenv tv1' co)
1009 -- BAY: I don't think we need to do any kind matching here yet
1010 -- (compare 'match'), but we probably will when moving to SHE.
1012 | otherwise -- tv1 is not a template ty var, so the only thing it
1013 -- can match is a reflexivity coercion for itself.
1014 -- But that case is dealt with already
1018 rn_env = me_env menv
1019 tv1' = rnOccL rn_env tv1
1021 ty_co_match menv subst (AppTy ty1 ty2) (AppCo co1 co2) -- BAY: do we need to work harder to decompose the AppCo?
1022 = do { subst' <- ty_co_match menv subst ty1 co1
1023 ; ty_co_match menv subst' ty2 co2 }
1025 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
1026 | tc1 == tc2 = ty_co_matches menv subst tys cos
1028 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
1029 | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1031 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
1032 = ty_co_match menv' subst ty co
1034 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1036 ty_co_match _ _ _ _ = Nothing
1038 ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv
1039 ty_co_matches menv = matchList (ty_co_match menv)
1042 %************************************************************************
1044 Sequencing on coercions
1046 %************************************************************************
1049 seqCo :: Coercion -> ()
1050 seqCo (Refl ty) = seqType ty
1051 seqCo (TyConAppCo tc cos) = tc `seq` seqCos cos
1052 seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
1053 seqCo (ForAllCo tv co) = tv `seq` seqCo co
1054 seqCo (PredCo p) = seqPred seqCo p
1055 seqCo (CoVarCo cv) = cv `seq` ()
1056 seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
1057 seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2
1058 seqCo (SymCo co) = seqCo co
1059 seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
1060 seqCo (NthCo _ co) = seqCo co
1061 seqCo (InstCo co ty) = seqCo co `seq` seqType ty
1063 seqCos :: [Coercion] -> ()
1065 seqCos (co:cos) = seqCo co `seq` seqCos cos
1069 %************************************************************************
1071 The kind of a type, and of a coercion
1073 %************************************************************************
1076 coercionType :: Coercion -> Type
1077 coercionType co = case coercionKind co of
1078 Pair ty1 ty2 -> mkCoType ty1 ty2
1081 -- | If it is the case that
1085 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1086 coercionKind :: Coercion -> Pair Type
1087 coercionKind (Refl ty) = Pair ty ty
1088 coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
1089 coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
1090 coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
1091 -- BAY*: is the above still correct for equality
1092 -- abstractions? the System FC paper seems to imply we can
1093 -- only ever construct coercions between foralls whose
1094 -- variables have *equal* kinds. But there was this comment
1095 -- below suggesting otherwise:
1097 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
1098 -- ----------------------------------------------
1099 -- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
1102 coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv
1103 coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
1104 in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
1105 (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
1106 coercionKind (UnsafeCo ty1 ty2) = Pair ty1 ty2
1107 coercionKind (SymCo co) = swap $ coercionKind co
1108 coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
1109 coercionKind (NthCo d co) = getNth d <$> coercionKind co
1110 coercionKind (InstCo co ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind co
1111 = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
1112 -- fall-through error case.
1113 coercionKind co = pprPanic "coercionKind" (ppr co)
1115 -- | Apply 'coercionKind' to multiple 'Coercion's
1116 coercionKinds :: [Coercion] -> Pair [Type]
1117 coercionKinds tys = sequenceA $ map coercionKind tys
1119 getNth :: Int -> Type -> Type
1120 getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty
1121 = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
1122 getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
1126 applyCo :: Type -> Coercion -> Type
1127 -- Gives the type of (e co) where e :: (a~b) => ty
1128 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
1129 applyCo (FunTy _ ty) _ = ty
1130 applyCo _ _ = panic "applyCo"