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
74 pprCo, pprParendCo, pprCoAxiom,
81 #include "HsVersions.h"
83 import Unify ( MatchEnv(..), ruleMatchTyX, matchList )
86 import Type hiding( substTy, substTyVarBndr, extendTvSubst )
88 import Class ( classTyCon )
93 import UniqFM ( minusUFM )
94 import Maybes ( orElse )
95 import Name ( Name, NamedThing(..), nameUnique )
96 import OccName ( isSymOcc )
102 import TysPrim ( eqPredPrimTyCon )
103 import PrelNames ( funTyConKey )
104 import Control.Applicative
105 import Data.Traversable (traverse, sequenceA)
106 import Control.Arrow (second)
109 import qualified Data.Data as Data hiding ( TyCon )
112 %************************************************************************
116 %************************************************************************
119 -- | A 'Coercion' is concrete evidence of the equality/convertibility
123 -- These ones mirror the shape of types
124 = Refl Type -- See Note [Refl invariant]
125 -- Invariant: applications of (Refl T) to a bunch of identity coercions
126 -- always show up as Refl.
127 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
129 -- Applications of (Refl T) to some coercions, at least one of
130 -- which is NOT the identity, show up as TyConAppCo.
131 -- (They may not be fully saturated however.)
132 -- ConAppCo coercions (like all coercions other than Refl)
133 -- are NEVER the identity.
135 -- These ones simply lift the correspondingly-named
136 -- Type constructors into Coercions
137 | TyConAppCo TyCon [Coercion] -- lift TyConApp
138 -- The TyCon is never a synonym;
139 -- we expand synonyms eagerly
141 | AppCo Coercion Coercion -- lift AppTy
143 -- See Note [Forall coercions]
144 | ForAllCo TyVar Coercion -- forall a. g
148 | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely*
149 -- saturate arity of CoAxiom.
150 -- See [Coercion axioms applied to coercions]
153 | TransCo Coercion Coercion
155 -- These are destructors
156 | NthCo Int Coercion -- Zero-indexed
157 | InstCo Coercion Type
158 deriving (Data.Data, Data.Typeable)
161 Note [Refl invariant]
162 ~~~~~~~~~~~~~~~~~~~~~
163 Coercions have the following invariant
164 Refl is always lifted as far as possible.
166 You might think that a consequencs is:
167 Every identity coercions has Refl at the root
169 But that's not quite true because of coercion variables. Consider
171 Left h where h :: Maybe Int ~ Maybe Int
172 etc. So the consequence is only true of coercions that
173 have no coercion variables.
175 Note [Coercion axioms applied to coercions]
176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
177 The reason coercion axioms can be applied to coercions and not just
178 types is to allow for better optimization. There are some cases where
179 we need to be able to "push transitivity inside" an axiom in order to
180 expose further opportunities for optimization.
182 For example, suppose we have
187 and we want to optimize
189 sym (C b) ; t[g] ; C c
195 (stopping through t[b] and t[c] along the way).
197 We'd like to optimize this to just F g -- but how? The key is
198 that we need to allow axioms to be instantiated by *coercions*,
199 not just by types. Then we can (in certain cases) push
200 transitivity inside the axiom instantiations, and then react
201 opposite-polarity instantiations of the same axiom. In this
202 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
203 obtain the substitution a |-> g (note this operation is sort
204 of the dual of lifting!) and hence end up with
208 which indeed has the same kind as t[g] ; C c.
214 which can be optimized to F g.
217 Note [Forall coercions]
218 ~~~~~~~~~~~~~~~~~~~~~~~
219 Constructing coercions between forall-types can be a bit tricky.
220 Currently, the situation is as follows:
222 ForAllCo TyVar Coercion
224 represents a coercion between polymorphic types, with the rule
227 ----------------------------------------------
228 ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
230 Note that it's only necessary to coerce between polymorphic types
231 where the type variables have identical kinds, because equality on
234 Note [Predicate coercions]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~
238 How can we coerce between types
242 where the equality predicate *itself* differs?
244 Answer: we simply treat (~) as an ordinary type constructor, so these
245 types really look like
247 ((~) [c] a) -> [a] -> c
248 ((~) [c] b) -> [b] -> c
250 So the coercion between the two is obviously
252 ((~) [c] g) -> [g] -> c
254 Another way to see this to say that we simply collapse predicates to
255 their representation type (see Type.coreView and Type.predTypeRep).
257 This collapse is done by mkPredCo; there is no PredCo constructor
258 in Coercion. This is important because we need Nth to work on
260 Nth 1 ((~) [c] g) = g
261 See Simplify.simplCoercionF, which generates such selections.
263 %************************************************************************
265 \subsection{Coercion variables}
267 %************************************************************************
270 coVarName :: CoVar -> Name
273 setCoVarUnique :: CoVar -> Unique -> CoVar
274 setCoVarUnique = setVarUnique
276 setCoVarName :: CoVar -> Name -> CoVar
277 setCoVarName = setVarName
279 isCoVar :: Var -> Bool
280 isCoVar v = isCoVarType (varType v)
282 isCoVarType :: Type -> Bool
283 isCoVarType = isEqPredTy
288 tyCoVarsOfCo :: Coercion -> VarSet
289 -- Extracts type and coercion variables from a coercion
290 tyCoVarsOfCo (Refl ty) = tyVarsOfType ty
291 tyCoVarsOfCo (TyConAppCo _ cos) = tyCoVarsOfCos cos
292 tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
293 tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
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 (CoVarCo v) = unitVarSet v
312 coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
313 coVarsOfCo (UnsafeCo _ _) = emptyVarSet
314 coVarsOfCo (SymCo co) = coVarsOfCo co
315 coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
316 coVarsOfCo (NthCo _ co) = coVarsOfCo co
317 coVarsOfCo (InstCo co _) = coVarsOfCo co
319 coVarsOfCos :: [Coercion] -> VarSet
320 coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
322 coercionSize :: Coercion -> Int
323 coercionSize (Refl ty) = typeSize ty
324 coercionSize (TyConAppCo _ cos) = 1 + sum (map coercionSize cos)
325 coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
326 coercionSize (ForAllCo _ co) = 1 + coercionSize co
327 coercionSize (CoVarCo _) = 1
328 coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
329 coercionSize (UnsafeCo ty1 ty2) = typeSize ty1 + typeSize ty2
330 coercionSize (SymCo co) = 1 + coercionSize co
331 coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
332 coercionSize (NthCo _ co) = 1 + coercionSize co
333 coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
336 %************************************************************************
338 Pretty-printing coercions
340 %************************************************************************
342 @pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
343 function is defined to use this. @pprParendCo@ is the same, except it
344 puts parens around the type, except for the atomic cases.
345 @pprParendCo@ works just by setting the initial context precedence
349 instance Outputable Coercion where
352 pprCo, pprParendCo :: Coercion -> SDoc
353 pprCo co = ppr_co TopPrec co
354 pprParendCo co = ppr_co TyConPrec co
356 ppr_co :: Prec -> Coercion -> SDoc
357 ppr_co _ (Refl ty) = angles (ppr ty)
359 ppr_co p co@(TyConAppCo tc cos)
360 | tc `hasKey` funTyConKey = ppr_fun_co p co
361 | otherwise = pprTcApp p ppr_co tc cos
363 ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
364 pprCo co1 <+> ppr_co TyConPrec co2
366 ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
368 ppr_co _ (CoVarCo cv)
369 | isSymOcc (getOccName cv) = parens (ppr cv)
372 ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
375 ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
378 <+> ppr_co FunPrec co2
379 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
380 pprParendCo co <> ptext (sLit "@") <> pprType ty
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]
387 angles :: SDoc -> SDoc
388 angles p = char '<' <> p <> char '>'
390 ppr_fun_co :: Prec -> Coercion -> SDoc
391 ppr_fun_co p co = pprArrowChain p (split co)
393 split (TyConAppCo f [arg,res])
394 | f `hasKey` funTyConKey
395 = ppr_co FunPrec arg : split res
396 split co = [ppr_co TopPrec co]
398 ppr_forall_co :: Prec -> Coercion -> SDoc
400 = maybeParen p FunPrec $
401 sep [pprForAll tvs, ppr_co TopPrec rho]
403 (tvs, rho) = split1 [] ty
404 split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
405 split1 tvs ty = (reverse tvs, ty)
409 pprCoAxiom :: CoAxiom -> SDoc
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))) ]
415 %************************************************************************
419 %************************************************************************
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:
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)] ]
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
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
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
455 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
456 splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
457 splitForAllCo_maybe _ = Nothing
459 -------------------------------------------------------
460 -- and some coercion kind stuff
462 coVarPred :: CoVar -> PredType
464 = ASSERT( isCoVar cv )
465 case splitPredTy_maybe (varType cv) of
467 other -> pprPanic "coVarPred" (ppr cv $$ ppr other)
469 coVarKind :: CoVar -> (Type,Type)
471 coVarKind cv = case coVarKind_maybe cv of
473 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
475 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
476 coVarKind_maybe cv = splitEqPredTy_maybe (varType cv)
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)
483 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
484 splitCoPredTy_maybe ty
485 | Just (cv,r) <- splitForAllTy_maybe ty
487 , Just (s,t) <- coVarKind_maybe cv
492 isReflCo :: Coercion -> Bool
493 isReflCo (Refl {}) = True
496 isReflCo_maybe :: Coercion -> Maybe Type
497 isReflCo_maybe (Refl ty) = Just ty
498 isReflCo_maybe _ = Nothing
501 %************************************************************************
505 %************************************************************************
508 mkCoVarCo :: CoVar -> Coercion
510 | ty1 `eqType` ty2 = Refl ty1
511 | otherwise = CoVarCo cv
513 (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
515 mkReflCo :: Type -> Coercion
518 mkAxInstCo :: CoAxiom -> [Type] -> Coercion
520 | arity == n_tys = AxiomInstCo ax rtys
521 | otherwise = ASSERT( arity < n_tys )
522 foldl AppCo (AxiomInstCo ax (take arity rtys))
526 arity = coAxiomArity ax
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.
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
544 -- | Apply a type constructor to a list of coercions.
545 mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
547 -- Expand type synonyms
548 | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
549 = mkAppCos (liftCoSubst (mkTopCvSubst tv_co_prs) rhs_ty) leftover_cos
551 | Just tys <- traverse isReflCo_maybe cos
552 = Refl (mkTyConApp tc tys) -- See Note [Refl invariant]
554 | otherwise = TyConAppCo tc cos
556 -- | Make a function 'Coercion' between two other 'Coercion's
557 mkFunCo :: Coercion -> Coercion -> Coercion
558 mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
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
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
572 -------------------------------
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
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
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
592 mkNthCo :: Int -> Coercion -> Coercion
593 mkNthCo n (Refl ty) = Refl (getNth n ty)
594 mkNthCo n co = NthCo n co
596 -- | Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
597 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
598 mkInstCo :: Coercion -> Type -> Coercion
599 mkInstCo (ForAllCo tv co) ty = substCoWithTy tv ty co
600 mkInstCo co ty = InstCo co ty
602 -- | Manufacture a coercion from thin air. Needless to say, this is
603 -- not usually safe, but it is used when we know we are dealing with
604 -- bottom, which is one case in which it is safe. This is also used
605 -- to implement the @unsafeCoerce#@ primitive. Optimise by pushing
606 -- down through type constructors.
607 mkUnsafeCo :: Type -> Type -> Coercion
608 mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
609 mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
611 = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
613 mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
614 = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
616 mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
618 -- See note [Newtype coercions] in TyCon
620 -- | Create a coercion constructor (axiom) suitable for the given
621 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
622 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
623 -- the type the appropriate right hand side of the @newtype@, with
624 -- the free variables a subset of those 'TyVar's.
625 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
626 mkNewTypeCo name tycon tvs rhs_ty
627 = CoAxiom { co_ax_unique = nameUnique name
630 , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
631 , co_ax_rhs = rhs_ty }
633 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
634 -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
635 -- the coercion constructor built here, @F@ the family tycon and @R@ the (derived)
636 -- representation tycon.
637 mkFamInstCo :: Name -- ^ Unique name for the coercion tycon
638 -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
639 -> TyCon -- ^ Family tycon (@F@)
640 -> [Type] -- ^ Type instance (@ts@)
641 -> TyCon -- ^ Representation tycon (@R@)
642 -> CoAxiom -- ^ Coercion constructor (@Co@)
643 mkFamInstCo name tvs family inst_tys rep_tycon
644 = CoAxiom { co_ax_unique = nameUnique name
647 , co_ax_lhs = mkTyConApp family inst_tys
648 , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
650 mkPiCos :: [Var] -> Coercion -> Coercion
651 mkPiCos vs co = foldr mkPiCo co vs
653 mkPiCo :: Var -> Coercion -> Coercion
654 mkPiCo v co | isTyVar v = mkForAllCo v co
655 | otherwise = mkFunCo (mkReflCo (varType v)) co
658 %************************************************************************
662 %************************************************************************
665 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
666 -- ^ If @co :: T ts ~ rep_ty@ then:
668 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
669 instNewTyCon_maybe tc tys
670 | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
671 = ASSERT( tys `lengthIs` tyConArity tc )
672 Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
676 -- this is here to avoid module loops
677 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
678 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
679 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
680 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
681 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
683 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
685 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
686 splitNewTypeRepCo_maybe ty
687 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
688 splitNewTypeRepCo_maybe (TyConApp tc tys)
689 | Just (ty', co) <- instNewTyCon_maybe tc tys
691 Refl _ -> panic "splitNewTypeRepCo_maybe"
692 -- This case handled by coreView
694 splitNewTypeRepCo_maybe _
697 -- | Determines syntactic equality of coercions
698 coreEqCoercion :: Coercion -> Coercion -> Bool
699 coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
700 where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
702 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
703 coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
704 coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
705 = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2
707 coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
708 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
710 coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
711 = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2
713 coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
714 = rnOccL env cv1 == rnOccR env cv2
716 coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
718 && all2 (coreEqCoercion2 env) cos1 cos2
720 coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
721 = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
723 coreEqCoercion2 env (SymCo co1) (SymCo co2)
724 = coreEqCoercion2 env co1 co2
726 coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
727 = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22
729 coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
730 = d1 == d2 && coreEqCoercion2 env co1 co2
732 coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
733 = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2
735 coreEqCoercion2 _ _ _ = False
738 %************************************************************************
740 Substitution of coercions
742 %************************************************************************
745 -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
746 -- doing a \"lifting\" substitution)
747 type CvSubstEnv = VarEnv Coercion
749 emptyCvSubstEnv :: CvSubstEnv
750 emptyCvSubstEnv = emptyVarEnv
753 = CvSubst InScopeSet -- The in-scope type variables
754 TvSubstEnv -- Substitution of types
755 CvSubstEnv -- Substitution of coercions
757 instance Outputable CvSubst where
758 ppr (CvSubst ins tenv cenv)
759 = brackets $ sep[ ptext (sLit "CvSubst"),
760 nest 2 (ptext (sLit "In scope:") <+> ppr ins),
761 nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
762 nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
764 emptyCvSubst :: CvSubst
765 emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
767 isEmptyCvSubst :: CvSubst -> Bool
768 isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
770 getCvInScope :: CvSubst -> InScopeSet
771 getCvInScope (CvSubst in_scope _ _) = in_scope
773 zapCvSubstEnv :: CvSubst -> CvSubst
774 zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
776 cvTvSubst :: CvSubst -> TvSubst
777 cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
779 tvCvSubst :: TvSubst -> CvSubst
780 tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
782 extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
783 extendTvSubst (CvSubst in_scope tenv cenv) tv ty
784 = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
786 substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
787 substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
788 = ASSERT( isCoVar old_var )
789 (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
791 -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
792 -- In that case, mkCoVarCo will return a ReflCoercion, and
793 -- we want to substitute that (not new_var) for old_var
794 new_co = mkCoVarCo new_var
795 no_change = new_var == old_var && not (isReflCo new_co)
797 new_cenv | no_change = delVarEnv cenv old_var
798 | otherwise = extendVarEnv cenv old_var new_co
800 new_var = uniqAway in_scope subst_old_var
801 subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
802 -- It's important to do the substitution for coercions,
803 -- because only they can have free type variables
805 substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
806 substTyVarBndr (CvSubst in_scope tenv cenv) old_var
807 = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
808 (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
810 zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
811 zipOpenCvSubst vs cos
812 | debugIsOn && (length vs /= length cos)
813 = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
815 = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
817 mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
818 mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
820 substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
821 substCoWithTy tv ty = substCoWithTys [tv] [ty]
823 substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
824 substCoWithTys tvs tys co
825 | debugIsOn && (length tvs /= length tys)
826 = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
828 = ASSERT( length tvs == length tys )
829 substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
831 in_scope = mkInScopeSet (tyVarsOfTypes tys)
833 -- | Substitute within a 'Coercion'
834 substCo :: CvSubst -> Coercion -> Coercion
835 substCo subst co | isEmptyCvSubst subst = co
836 | otherwise = subst_co subst co
838 -- | Substitute within several 'Coercion's
839 substCos :: CvSubst -> [Coercion] -> [Coercion]
840 substCos subst cos | isEmptyCvSubst subst = cos
841 | otherwise = map (substCo subst) cos
843 substTy :: CvSubst -> Type -> Type
844 substTy subst = Type.substTy (cvTvSubst subst)
846 subst_co :: CvSubst -> Coercion -> Coercion
850 go_ty :: Type -> Type
851 go_ty = Coercion.substTy subst
853 go :: Coercion -> Coercion
854 go (Refl ty) = Refl $! go_ty ty
855 go (TyConAppCo tc cos) = let args = map go cos
856 in args `seqList` TyConAppCo tc args
857 go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
858 go (ForAllCo tv co) = case substTyVarBndr subst tv of
860 ForAllCo tv' $! subst_co subst' co
861 go (CoVarCo cv) = substCoVar subst cv
862 go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
863 go (UnsafeCo ty1 ty2) = (UnsafeCo $! go_ty ty1) $! go_ty ty2
864 go (SymCo co) = mkSymCo (go co)
865 go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
866 go (NthCo d co) = mkNthCo d (go co)
867 go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
869 substCoVar :: CvSubst -> CoVar -> Coercion
870 substCoVar (CvSubst in_scope _ cenv) cv
871 | Just co <- lookupVarEnv cenv cv = co
872 | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
873 | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
874 ASSERT( isCoVar cv ) CoVarCo cv
876 substCoVars :: CvSubst -> [CoVar] -> [Coercion]
877 substCoVars subst cvs = map (substCoVar subst) cvs
879 lookupTyVar :: CvSubst -> TyVar -> Maybe Type
880 lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
882 lookupCoVar :: CvSubst -> Var -> Maybe Coercion
883 lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
886 %************************************************************************
888 "Lifting" substitution
889 [(TyVar,Coercion)] -> Type -> Coercion
891 %************************************************************************
894 liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
895 liftCoSubstWith tvs cos = liftCoSubst (zipOpenCvSubst tvs cos)
897 -- | The \"lifting\" operation which substitutes coercions for type
898 -- variables in a type to produce a coercion.
900 -- For the inverse operation, see 'liftCoMatch'
901 liftCoSubst :: CvSubst -> Type -> Coercion
902 -- The CvSubst maps TyVar -> Type (mainly for cloning foralls)
903 -- TyVar -> Coercion (this is the payload)
904 -- The unusual thing is that the *coercion* substitution maps
905 -- some *type* variables. That's the whole point of this function!
906 liftCoSubst subst ty | isEmptyCvSubst subst = Refl ty
907 | otherwise = ty_co_subst subst ty
909 ty_co_subst :: CvSubst -> Type -> Coercion
913 go (TyVarTy tv) = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
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)
919 (subst', v') = liftCoSubstTyVarBndr subst v
920 go (PredTy p) = mkPredCo (go <$> p)
922 liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
923 liftCoSubstTyVar subst@(CvSubst _ tenv cenv) tv
924 = case (lookupVarEnv tenv tv, lookupVarEnv cenv tv) of
925 (Nothing, Nothing) -> Nothing
926 (Just ty, Nothing) -> Just (Refl ty)
927 (Nothing, Just co) -> Just co
928 (Just {}, Just {}) -> pprPanic "ty_co_subst" (ppr tv $$ ppr subst)
930 liftCoSubstTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
931 liftCoSubstTyVarBndr (CvSubst in_scope tenv cenv) old_var
932 = (CvSubst (in_scope `extendInScopeSet` new_var)
934 (delVarEnv cenv old_var) -- See Note [Lifting substitutions]
937 new_tenv | no_change = delVarEnv tenv old_var
938 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
940 no_change = new_var == old_var
941 new_var = uniqAway in_scope old_var
944 Note [Lifting substitutions]
945 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
946 Consider liftCoSubstWith [a] [co] (a, forall a. a)
947 Then we want to substitute for the free 'a', but obviously not for
948 the bound 'a'. hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr.
950 This also why we need a full CvSubst when doing lifting substitutions.
953 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
954 -- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
955 -- That is, it matches a type against a coercion of the same
956 -- "shape", and returns a lifting substitution which could have been
957 -- used to produce the given coercion from the given type.
958 liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
959 liftCoMatch tmpls ty co
960 = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of
961 Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env)
964 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
965 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
966 -- Like tcMatchTy, assume all the interesting variables
967 -- in ty are in tmpls
969 type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv)
970 -- Used locally inside ty_co_match only
972 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
973 ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv
974 ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co
976 -- Deal with the Refl case by delegating to type matching
977 ty_co_match menv (tenv, cenv) ty co
978 | Just ty' <- isReflCo_maybe co
979 = case ruleMatchTyX ty_menv tenv ty ty' of
980 Just tenv' -> Just (tenv', cenv)
983 ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv }
984 -- Remove from the template set any variables already bound to non-refl coercions
986 -- Match a type variable against a non-refl coercion
987 ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co
988 | Just {} <- lookupVarEnv tenv tv1' -- tv1' is already bound to (Refl ty)
989 = Nothing -- The coercion 'co' is not Refl
991 | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
992 = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
994 else Nothing -- no match since tv1 matches two different coercions
996 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
997 = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
998 then Nothing -- occurs check failed
999 else return (tenv, extendVarEnv cenv tv1' co)
1000 -- BAY: I don't think we need to do any kind matching here yet
1001 -- (compare 'match'), but we probably will when moving to SHE.
1003 | otherwise -- tv1 is not a template ty var, so the only thing it
1004 -- can match is a reflexivity coercion for itself.
1005 -- But that case is dealt with already
1009 rn_env = me_env menv
1010 tv1' = rnOccL rn_env tv1
1012 ty_co_match menv subst (AppTy ty1 ty2) co
1013 | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1014 = do { subst' <- ty_co_match menv subst ty1 co1
1015 ; ty_co_match menv subst' ty2 co2 }
1017 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
1018 | tc1 == tc2 = ty_co_matches menv subst tys cos
1020 ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
1021 | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1023 ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
1024 = ty_co_match menv' subst ty co
1026 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
1028 ty_co_match _ _ _ _ = Nothing
1030 ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv
1031 ty_co_matches menv = matchList (ty_co_match menv)
1034 %************************************************************************
1036 Sequencing on coercions
1038 %************************************************************************
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
1054 seqCos :: [Coercion] -> ()
1056 seqCos (co:cos) = seqCo co `seq` seqCos cos
1060 %************************************************************************
1062 The kind of a type, and of a coercion
1064 %************************************************************************
1067 coercionType :: Coercion -> Type
1068 coercionType co = case coercionKind co of
1069 Pair ty1 ty2 -> mkCoType ty1 ty2
1072 -- | If it is the case that
1076 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1077 coercionKind :: Coercion -> Pair Type
1078 coercionKind (Refl ty) = Pair ty ty
1079 coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
1080 coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
1081 coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
1082 coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv
1083 coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
1084 in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
1085 (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
1086 coercionKind (UnsafeCo ty1 ty2) = Pair ty1 ty2
1087 coercionKind (SymCo co) = swap $ coercionKind co
1088 coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
1089 coercionKind (NthCo d co) = getNth d <$> coercionKind co
1090 coercionKind co@(InstCo aco ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco
1091 = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
1092 | otherwise = pprPanic "coercionKind" (ppr co)
1094 -- | Apply 'coercionKind' to multiple 'Coercion's
1095 coercionKinds :: [Coercion] -> Pair [Type]
1096 coercionKinds tys = sequenceA $ map coercionKind tys
1098 getNth :: Int -> Type -> Type
1099 getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty
1100 = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
1101 getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
1105 applyCo :: Type -> Coercion -> Type
1106 -- Gives the type of (e co) where e :: (a~b) => ty
1107 applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
1108 applyCo (FunTy _ ty) _ = ty
1109 applyCo _ _ = panic "applyCo"