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.
10 -- Coercions are represented as types, and their kinds tell what types the
11 -- coercion works on. The coercion kind constructor is a special TyCon that
12 -- must always be saturated, like so:
14 -- > typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]
20 -- ** Deconstructing Kinds
21 kindFunResult, splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
23 -- ** Predicates on Kinds
24 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
25 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
26 isCoSuperKind, isSuperKind, isCoercionKind,
27 mkArrowKind, mkArrowKinds,
29 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
32 mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
33 coercionKind, coercionKinds, isIdentityCoercion,
35 -- ** Equality predicates
36 isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
38 -- ** Coercion transformations
40 mkSymCoercion, mkTransCoercion,
41 mkLeftCoercion, mkRightCoercion,
42 mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
43 mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
44 mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
45 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
48 unsafeCoercionTyCon, symCoercionTyCon,
49 transCoercionTyCon, leftCoercionTyCon,
50 rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
51 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
54 decompLR_maybe, decompCsel_maybe, decompInst_maybe,
56 splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
59 coreEqCoercion, coreEqCoercion2,
65 mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
68 mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
72 #include "HsVersions.h"
88 %************************************************************************
92 %************************************************************************
95 -- | Essentially 'funResultTy' on kinds
96 kindFunResult :: Kind -> Kind
97 kindFunResult k = funResultTy k
99 -- | Essentially 'splitFunTys' on kinds
100 splitKindFunTys :: Kind -> ([Kind],Kind)
101 splitKindFunTys k = splitFunTys k
103 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
104 splitKindFunTy_maybe = splitFunTy_maybe
106 -- | Essentially 'splitFunTysN' on kinds
107 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
108 splitKindFunTysN k = splitFunTysN k
110 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
111 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
112 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
113 isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
115 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
117 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
118 isOpenTypeKind _ = False
120 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
122 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
123 isUbxTupleKind _ = False
125 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
127 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
128 isArgTypeKind _ = False
130 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
132 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
133 isUnliftedTypeKind _ = False
135 isSubOpenTypeKind :: Kind -> Bool
136 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
137 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
138 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
140 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
141 isSubOpenTypeKind other = ASSERT( isKind other ) False
142 -- This is a conservative answer
143 -- It matters in the call to isSubKind in
144 -- checkExpectedKind.
146 isSubArgTypeKindCon kc
147 | isUnliftedTypeKindCon kc = True
148 | isLiftedTypeKindCon kc = True
149 | isArgTypeKindCon kc = True
152 isSubArgTypeKind :: Kind -> Bool
153 -- ^ True of any sub-kind of ArgTypeKind
154 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
155 isSubArgTypeKind _ = False
157 -- | Is this a super-kind (i.e. a type-of-kinds)?
158 isSuperKind :: Type -> Bool
159 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
160 isSuperKind _ = False
162 -- | Is this a kind (i.e. a type-of-types)?
163 isKind :: Kind -> Bool
164 isKind k = isSuperKind (typeKind k)
166 isSubKind :: Kind -> Kind -> Bool
167 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
168 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
169 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
170 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
171 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
172 isSubKind _ _ = False
174 eqKind :: Kind -> Kind -> Bool
177 isSubKindCon :: TyCon -> TyCon -> Bool
178 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
180 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
181 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
182 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
183 | isOpenTypeKindCon kc2 = True
184 -- we already know kc1 is not a fun, its a TyCon
185 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
188 defaultKind :: Kind -> Kind
189 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
190 -- information on what that means
192 -- When we generalise, we make generic type variables whose kind is
193 -- simple (* or *->* etc). So generic type variables (other than
194 -- built-in constants like 'error') always have simple kinds. This is important;
197 -- We want f to get type
198 -- f :: forall (a::*). a -> Bool
200 -- f :: forall (a::??). a -> Bool
201 -- because that would allow a call like (f 3#) as well as (f True),
202 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
204 | isSubOpenTypeKind k = liftedTypeKind
205 | isSubArgTypeKind k = liftedTypeKind
209 %************************************************************************
213 %************************************************************************
217 -- | A 'Coercion' represents a 'Type' something should be coerced to.
220 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
221 -- types that a 'Coercion' will work on.
222 type CoercionKind = Kind
224 ------------------------------
226 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
227 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
229 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
230 decomposeCo :: Arity -> Coercion -> [Coercion]
235 go n co cos = go (n-1) (mkLeftCoercion co)
236 (mkRightCoercion co : cos)
238 ------------------------------
240 -------------------------------------------------------
241 -- and some coercion kind stuff
243 coVarKind :: CoVar -> (Type,Type)
245 coVarKind cv = case coVarKind_maybe cv of
247 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
249 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
250 coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
252 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
253 -- Panics if the argument is not a valid 'CoercionKind'
254 splitCoKind_maybe :: Kind -> Maybe (Type, Type)
255 splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
256 splitCoKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
257 splitCoKind_maybe _ = Nothing
259 -- | Makes a 'CoercionKind' from two types: the types whose equality
260 -- is proven by the relevant 'Coercion'
261 mkCoKind :: Type -> Type -> CoercionKind
262 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
264 -- | (mkCoPredTy s t r) produces the type: (s~t) => r
265 mkCoPredTy :: Type -> Type -> Type -> Type
266 mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
268 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
269 splitCoPredTy_maybe ty
270 | Just (cv,r) <- splitForAllTy_maybe ty
272 , Just (s,t) <- coVarKind_maybe cv
277 -- | Tests whether a type is just a type equality predicate
278 isEqPredTy :: Type -> Bool
279 isEqPredTy (PredTy pred) = isEqPred pred
282 -- | Creates a type equality predicate
283 mkEqPred :: (Type, Type) -> PredType
284 mkEqPred (ty1, ty2) = EqPred ty1 ty2
286 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
288 getEqPredTys :: PredType -> (Type,Type)
289 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
290 getEqPredTys other = pprPanic "getEqPredTys" (ppr other)
292 isIdentityCoercion :: Coercion -> Bool
293 isIdentityCoercion co
294 = case coercionKind co of
295 (t1,t2) -> t1 `coreEqType` t2
298 %************************************************************************
302 %************************************************************************
304 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
307 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
308 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
310 mkCoercion :: TyCon -> [Type] -> Coercion
311 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
314 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
315 -- 'Coercion' constructor of some kind
316 mkAppCoercion :: Coercion -> Coercion -> Coercion
317 mkAppCoercion co1 co2 = mkAppTy co1 co2
319 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
320 -- See also 'mkAppCoercion'
321 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
322 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
324 -- | Apply a type constructor to a list of coercions.
325 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
326 mkTyConCoercion con cos = mkTyConApp con cos
328 -- | Make a function 'Coercion' between two other 'Coercion's
329 mkFunCoercion :: Coercion -> Coercion -> Coercion
330 mkFunCoercion co1 co2 = mkFunTy co1 co2
332 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
333 mkForAllCoercion :: Var -> Coercion -> Coercion
334 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
335 mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co
338 -------------------------------
340 mkSymCoercion :: Coercion -> Coercion
341 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
342 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
343 -- becomes the kind @t2 ~ t1@.
344 mkSymCoercion g = mkCoercion symCoercionTyCon [g]
346 mkTransCoercion :: Coercion -> Coercion -> Coercion
347 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
348 mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
350 mkLeftCoercion :: Coercion -> Coercion
351 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
352 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
354 -- > mkLeftCoercion c :: f ~ g
355 mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
357 mkRightCoercion :: Coercion -> Coercion
358 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
359 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
361 -- > mkLeftCoercion c :: x ~ y
362 mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
364 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
365 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
366 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
367 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
369 -------------------------------
370 mkInstCoercion :: Coercion -> Type -> Coercion
371 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
372 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
373 mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty]
375 mkInstsCoercion :: Coercion -> [Type] -> Coercion
376 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
377 mkInstsCoercion co tys = foldl mkInstCoercion co tys
379 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
380 -- but it is used when we know we are dealing with bottom, which is one case in which
381 -- it is safe. This is also used implement the @unsafeCoerce#@ primitive.
382 mkUnsafeCoercion :: Type -> Type -> Coercion
383 mkUnsafeCoercion ty1 ty2 = mkCoercion unsafeCoercionTyCon [ty1, ty2]
386 -- See note [Newtype coercions] in TyCon
388 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
389 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
390 -- type the appropriate right hand side of the @newtype@, with the free variables
391 -- a subset of those 'TyVar's.
392 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
393 mkNewTypeCoercion name tycon tvs rhs_ty
394 = mkCoercionTyCon name arity desc
397 desc = CoAxiom { co_ax_tvs = tvs
398 , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
399 , co_ax_rhs = rhs_ty }
401 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
402 -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
403 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
404 -- representation tycon.
405 mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
406 -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
407 -> TyCon -- ^ Family tycon (@F@)
408 -> [Type] -- ^ Type instance (@ts@)
409 -> TyCon -- ^ Representation tycon (@R@)
410 -> TyCon -- ^ Coercion tycon (@Co@)
411 mkFamInstCoercion name tvs family inst_tys rep_tycon
412 = mkCoercionTyCon name arity desc
415 desc = CoAxiom { co_ax_tvs = tvs
416 , co_ax_lhs = mkTyConApp family inst_tys
417 , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
421 %************************************************************************
423 Coercion Type Constructors
425 %************************************************************************
427 Example. The coercion ((sym c) (sym d) (sym e))
428 will be represented by (TyConApp sym [c, sym d, sym e])
432 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
435 -- | Coercion type constructors: avoid using these directly and instead use
436 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
438 -- Each coercion TyCon is built with the special CoercionTyCon record and
439 -- carries its own kinding rule. Such CoercionTyCons must be fully applied
440 -- by any TyConApp in which they are applied, however they may also be over
441 -- applied (see example above) and the kinding function must deal with this.
442 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
443 rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
444 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
446 symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym
447 transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans
448 leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft
449 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight
450 instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst
451 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
452 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
453 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
454 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
456 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
457 rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
458 csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
460 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
461 symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
462 leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
463 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
464 instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
465 csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
466 csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
467 cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
468 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
470 mkCoConName :: FastString -> Unique -> TyCon -> Name
471 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
472 key (ATyCon coCon) BuiltInSyntax
477 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
478 -- Helper for left and right. Finds coercion kind of its input and
479 -- returns the left and right projections of the coercion...
481 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
482 decompLR_maybe (ty1,ty2)
483 | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
484 , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
485 = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
486 decompLR_maybe _ = Nothing
489 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
490 decompInst_maybe (ty1, ty2)
491 | Just (tv1,r1) <- splitForAllTy_maybe ty1
492 , Just (tv2,r2) <- splitForAllTy_maybe ty2
493 = Just ((tv1,tv2), (r1,r2))
494 decompInst_maybe _ = Nothing
497 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
498 -- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
499 -- Then csel1 co :: s1 ~ s2
500 -- csel2 co :: t1 ~ t2
501 -- cselR co :: r1 ~ r2
502 decompCsel_maybe (ty1, ty2)
503 | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
504 , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
505 = Just ((s1,s2), (t1,t2), (r1,r2))
506 decompCsel_maybe _ = Nothing
510 %************************************************************************
514 %************************************************************************
517 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
518 -- ^ If @co :: T ts ~ rep_ty@ then:
520 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
521 instNewTyCon_maybe tc tys
522 | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
523 = ASSERT( tys `lengthIs` tyConArity tc )
524 Just (substTyWith tvs tys ty,
527 Just co_tc -> ACo (mkTyConApp co_tc tys))
531 -- this is here to avoid module loops
532 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
533 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
534 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
535 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
536 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
538 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
540 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
541 splitNewTypeRepCo_maybe ty
542 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
543 splitNewTypeRepCo_maybe (TyConApp tc tys)
544 | Just (ty', coi) <- instNewTyCon_maybe tc tys
546 ACo co -> Just (ty', co)
547 IdCo -> panic "splitNewTypeRepCo_maybe"
548 -- This case handled by coreView
549 splitNewTypeRepCo_maybe _
552 -- | Determines syntactic equality of coercions
553 coreEqCoercion :: Coercion -> Coercion -> Bool
554 coreEqCoercion = coreEqType
556 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
557 coreEqCoercion2 = coreEqType2
561 %************************************************************************
563 CoercionI and its constructors
565 %************************************************************************
567 --------------------------------------
568 -- CoercionI smart constructors
569 -- lifted smart constructors of ordinary coercions
572 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
573 -- can represent either one of:
575 -- 1. A proper 'Coercion'
577 -- 2. The identity coercion
578 data CoercionI = IdCo | ACo Coercion
580 instance Outputable CoercionI where
581 ppr IdCo = ptext (sLit "IdCo")
582 ppr (ACo co) = ppr co
584 isIdentityCoI :: CoercionI -> Bool
585 isIdentityCoI IdCo = True
586 isIdentityCoI _ = False
588 -- | Tests whether all the given 'CoercionI's represent the identity coercion
589 allIdCoIs :: [CoercionI] -> Bool
590 allIdCoIs = all isIdentityCoI
592 -- | For each 'CoercionI' in the input list, return either the 'Coercion' it
593 -- contains or the corresponding 'Type' from the other list
594 zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
595 zipCoArgs cois tys = zipWith fromCoI cois tys
597 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
598 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
599 fromCoI :: CoercionI -> Type -> Type
600 fromCoI IdCo ty = ty -- Identity coercion represented
601 fromCoI (ACo co) _ = co -- by the type itself
603 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
604 mkSymCoI :: CoercionI -> CoercionI
606 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
607 -- the smart constructor
608 -- is too smart with tyvars
610 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
611 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
612 mkTransCoI IdCo aco = aco
613 mkTransCoI aco IdCo = aco
614 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
616 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
617 mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
618 mkTyConAppCoI tyCon tys cois
619 | allIdCoIs cois = IdCo
620 | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys))
622 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
623 mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
624 mkAppTyCoI _ IdCo _ IdCo = IdCo
625 mkAppTyCoI ty1 coi1 ty2 coi2 =
626 ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
629 mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
630 mkFunTyCoI _ IdCo _ IdCo = IdCo
631 mkFunTyCoI ty1 coi1 ty2 coi2 =
632 ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
634 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
635 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
636 mkForAllTyCoI _ IdCo = IdCo
637 mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
639 -- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
641 fromACo :: CoercionI -> Coercion
642 fromACo (ACo co) = co
643 fromACo (IdCo {}) = panic "fromACo"
645 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
647 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
648 mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
649 mkClassPPredCoI cls tys cois
650 | allIdCoIs cois = IdCo
651 | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
653 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
654 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
655 mkIParamPredCoI _ IdCo = IdCo
656 mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
658 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
659 mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
660 mkEqPredCoI _ IdCo _ IdCo = IdCo
661 mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
662 mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
665 %************************************************************************
667 The kind of a type, and of a coercion
669 %************************************************************************
672 typeKind :: Type -> Kind
673 typeKind ty@(TyConApp tc tys)
674 | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
675 | otherwise = foldr (\_ k -> kindFunResult k) (tyConKind tc) tys
676 -- During coercion optimisation we *do* match a type
677 -- against a coercion (see OptCoercion.matchesAxiomLhs)
678 -- So the use of typeKind in Unify.match_kind must work on coercions too
679 -- Hence the isCoercionTyCon case above
681 typeKind (PredTy pred) = predKind pred
682 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
683 typeKind (ForAllTy _ ty) = typeKind ty
684 typeKind (TyVarTy tyvar) = tyVarKind tyvar
685 typeKind (FunTy _arg res)
686 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
687 -- not unliftedTypKind (#)
688 -- The only things that can be after a function arrow are
689 -- (a) types (of kind openTypeKind or its sub-kinds)
690 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
691 | isTySuperKind k = k
692 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
697 predKind :: PredType -> Kind
698 predKind (EqPred {}) = coSuperKind -- A coercion kind!
699 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
700 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
703 -- | If it is the case that
707 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
708 coercionKind :: Coercion -> (Type, Type)
709 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
710 | otherwise = (ty, ty)
711 coercionKind (AppTy ty1 ty2)
712 = let (s1, t1) = coercionKind ty1
713 (s2, t2) = coercionKind ty2 in
714 (mkAppTy s1 s2, mkAppTy t1 t2)
715 coercionKind co@(TyConApp tc args)
716 | Just (ar, desc) <- isCoercionTyCon_maybe tc
717 -- CoercionTyCons carry their kinding rule, so we use it here
718 = WARN( not (length args >= ar), ppr co ) -- Always saturated
719 (let (ty1, ty2) = coTyConAppKind desc (take ar args)
720 (tys1, tys2) = coercionKinds (drop ar args)
721 in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
724 = let (lArgs, rArgs) = coercionKinds args in
725 (TyConApp tc lArgs, TyConApp tc rArgs)
727 coercionKind (FunTy ty1 ty2)
728 = let (t1, t2) = coercionKind ty1
729 (s1, s2) = coercionKind ty2 in
730 (mkFunTy t1 s1, mkFunTy t2 s2)
732 coercionKind (ForAllTy tv ty)
734 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
735 -- ----------------------------------------------
736 -- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
739 = let (c1,c2) = coVarKind tv
740 (s1,s2) = coercionKind c1
741 (t1,t2) = coercionKind c2
742 (r1,r2) = coercionKind ty
744 (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
747 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
748 -- ----------------------------------------------
749 -- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
750 = let (ty1, ty2) = coercionKind ty in
751 (ForAllTy tv ty1, ForAllTy tv ty2)
753 coercionKind (PredTy (ClassP cl args))
754 = let (lArgs, rArgs) = coercionKinds args in
755 (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
756 coercionKind (PredTy (IParam name ty))
757 = let (ty1, ty2) = coercionKind ty in
758 (PredTy (IParam name ty1), PredTy (IParam name ty2))
759 coercionKind (PredTy (EqPred c1 c2))
760 = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
761 -- These should not show up in coercions at all
762 -- becuase they are in the form of for-alls
763 let k1 = coercionKindPredTy c1
764 k2 = coercionKindPredTy c2 in
767 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
770 -- | Apply 'coercionKind' to multiple 'Coercion's
771 coercionKinds :: [Coercion] -> ([Type], [Type])
772 coercionKinds tys = unzip $ map coercionKind tys
775 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
776 -- and constructs the types that the resulting coercion relates.
777 -- Fails (in the monad) if ill-kinded.
778 -- Typically the monad is
779 -- either the Lint monad (with the consistency-check flag = True),
780 -- or the ID monad with a panic on failure (and the consistency-check flag = False)
783 -> [Type] -- Exactly right number of args
784 -> (Type, Type) -- Kind of this application
785 coTyConAppKind CoUnsafe (ty1:ty2:_)
787 coTyConAppKind CoSym (co:_)
788 | (ty1,ty2) <- coercionKind co = (ty2,ty1)
789 coTyConAppKind CoTrans (co1:co2:_)
790 = (fst (coercionKind co1), snd (coercionKind co2))
791 coTyConAppKind CoLeft (co:_)
792 | Just (res,_) <- decompLR_maybe (coercionKind co) = res
793 coTyConAppKind CoRight (co:_)
794 | Just (_,res) <- decompLR_maybe (coercionKind co) = res
795 coTyConAppKind CoCsel1 (co:_)
796 | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
797 coTyConAppKind CoCsel2 (co:_)
798 | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
799 coTyConAppKind CoCselR (co:_)
800 | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
801 coTyConAppKind CoInst (co:ty:_)
802 | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
803 = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
804 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
805 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
806 = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
808 (tys1, tys2) = coercionKinds cos
809 coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)