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, kindAppResult, synTyConResKind,
22 splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
24 -- ** Predicates on Kinds
25 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
26 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
27 isCoSuperKind, isSuperKind, isCoercionKind,
28 mkArrowKind, mkArrowKinds,
30 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
33 mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
34 coercionKind, coercionKinds, isIdentityCoercion,
36 -- ** Equality predicates
37 isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
39 -- ** Coercion transformations
41 mkSymCoercion, mkTransCoercion,
42 mkLeftCoercion, mkRightCoercion,
43 mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
44 mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
45 mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
46 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
48 mkClassPPredCo, mkIParamPredCo, mkEqPredCo,
49 mkCoVarCoercion, mkCoPredCo,
52 unsafeCoercionTyCon, symCoercionTyCon,
53 transCoercionTyCon, leftCoercionTyCon,
54 rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
55 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
58 decompLR_maybe, decompCsel_maybe, decompInst_maybe,
60 splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
63 coreEqCoercion, coreEqCoercion2,
69 mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
72 mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI
76 #include "HsVersions.h"
93 %************************************************************************
97 %************************************************************************
100 -- | Essentially 'funResultTy' on kinds
101 kindFunResult :: Kind -> Kind
102 kindFunResult k = funResultTy k
104 kindAppResult :: Kind -> [arg] -> Kind
105 kindAppResult k [] = k
106 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
108 -- | Essentially 'splitFunTys' on kinds
109 splitKindFunTys :: Kind -> ([Kind],Kind)
110 splitKindFunTys k = splitFunTys k
112 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
113 splitKindFunTy_maybe = splitFunTy_maybe
115 -- | Essentially 'splitFunTysN' on kinds
116 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
117 splitKindFunTysN k = splitFunTysN k
119 -- | Find the result 'Kind' of a type synonym,
120 -- after applying it to its 'arity' number of type variables
121 -- Actually this function works fine on data types too,
122 -- but they'd always return '*', so we never need to ask
123 synTyConResKind :: TyCon -> Kind
124 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
126 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
127 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
128 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
129 isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
131 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
133 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
134 isOpenTypeKind _ = False
136 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
138 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
139 isUbxTupleKind _ = False
141 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
143 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
144 isArgTypeKind _ = False
146 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
148 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
149 isUnliftedTypeKind _ = False
151 isSubOpenTypeKind :: Kind -> Bool
152 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
153 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
154 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
156 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
157 isSubOpenTypeKind other = ASSERT( isKind other ) False
158 -- This is a conservative answer
159 -- It matters in the call to isSubKind in
160 -- checkExpectedKind.
162 isSubArgTypeKindCon kc
163 | isUnliftedTypeKindCon kc = True
164 | isLiftedTypeKindCon kc = True
165 | isArgTypeKindCon kc = True
168 isSubArgTypeKind :: Kind -> Bool
169 -- ^ True of any sub-kind of ArgTypeKind
170 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
171 isSubArgTypeKind _ = False
173 -- | Is this a super-kind (i.e. a type-of-kinds)?
174 isSuperKind :: Type -> Bool
175 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
176 isSuperKind _ = False
178 -- | Is this a kind (i.e. a type-of-types)?
179 isKind :: Kind -> Bool
180 isKind k = isSuperKind (typeKind k)
182 isSubKind :: Kind -> Kind -> Bool
183 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
184 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
185 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
186 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
187 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
188 isSubKind _ _ = False
190 eqKind :: Kind -> Kind -> Bool
193 isSubKindCon :: TyCon -> TyCon -> Bool
194 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
196 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
197 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
198 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
199 | isOpenTypeKindCon kc2 = True
200 -- we already know kc1 is not a fun, its a TyCon
201 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
204 defaultKind :: Kind -> Kind
205 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
206 -- information on what that means
208 -- When we generalise, we make generic type variables whose kind is
209 -- simple (* or *->* etc). So generic type variables (other than
210 -- built-in constants like 'error') always have simple kinds. This is important;
213 -- We want f to get type
214 -- f :: forall (a::*). a -> Bool
216 -- f :: forall (a::??). a -> Bool
217 -- because that would allow a call like (f 3#) as well as (f True),
218 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
220 | isSubOpenTypeKind k = liftedTypeKind
221 | isSubArgTypeKind k = liftedTypeKind
225 %************************************************************************
229 %************************************************************************
233 -- | A 'Coercion' represents a 'Type' something should be coerced to.
236 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
237 -- types that a 'Coercion' will work on.
238 type CoercionKind = Kind
240 ------------------------------
242 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
243 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
245 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
246 decomposeCo :: Arity -> Coercion -> [Coercion]
251 go n co cos = go (n-1) (mkLeftCoercion co)
252 (mkRightCoercion co : cos)
255 -------------------------------------------------------
256 -- and some coercion kind stuff
258 coVarKind :: CoVar -> (Type,Type)
260 coVarKind cv = case coVarKind_maybe cv of
262 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
264 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
265 coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
267 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
268 -- Panics if the argument is not a valid 'CoercionKind'
269 splitCoKind_maybe :: Kind -> Maybe (Type, Type)
270 splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
271 splitCoKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
272 splitCoKind_maybe _ = Nothing
274 -- | Makes a 'CoercionKind' from two types: the types whose equality
275 -- is proven by the relevant 'Coercion'
276 mkCoKind :: Type -> Type -> CoercionKind
277 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
279 -- | (mkCoPredTy s t r) produces the type: (s~t) => r
280 mkCoPredTy :: Type -> Type -> Type -> Type
281 mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
284 co_var = mkWildCoVar (mkCoKind s t)
286 mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion
287 -- Creates a coercion between (s1~t1) => r1 and (s2~t2) => r2
288 mkCoPredCo = mkCoPredTy
291 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
292 splitCoPredTy_maybe ty
293 | Just (cv,r) <- splitForAllTy_maybe ty
295 , Just (s,t) <- coVarKind_maybe cv
300 -- | Tests whether a type is just a type equality predicate
301 isEqPredTy :: Type -> Bool
302 isEqPredTy (PredTy pred) = isEqPred pred
305 -- | Creates a type equality predicate
306 mkEqPred :: (Type, Type) -> PredType
307 mkEqPred (ty1, ty2) = EqPred ty1 ty2
309 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
311 getEqPredTys :: PredType -> (Type,Type)
312 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
313 getEqPredTys other = pprPanic "getEqPredTys" (ppr other)
315 isIdentityCoercion :: Coercion -> Bool
316 isIdentityCoercion co
317 = case coercionKind co of
318 (t1,t2) -> t1 `coreEqType` t2
321 %************************************************************************
325 %************************************************************************
327 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
330 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
331 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
333 mkCoercion :: TyCon -> [Type] -> Coercion
334 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
337 mkCoVarCoercion :: CoVar -> Coercion
338 mkCoVarCoercion cv = mkTyVarTy cv
340 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
341 -- 'Coercion' constructor of some kind
342 mkAppCoercion :: Coercion -> Coercion -> Coercion
343 mkAppCoercion co1 co2 = mkAppTy co1 co2
345 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
346 -- See also 'mkAppCoercion'
347 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
348 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
350 -- | Apply a type constructor to a list of coercions.
351 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
352 mkTyConCoercion con cos = mkTyConApp con cos
354 -- | Make a function 'Coercion' between two other 'Coercion's
355 mkFunCoercion :: Coercion -> Coercion -> Coercion
356 mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds!
358 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
359 mkForAllCoercion :: Var -> Coercion -> Coercion
360 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
361 mkForAllCoercion tv co = ASSERT ( isTyCoVar tv ) mkForAllTy tv co
364 -------------------------------
366 mkSymCoercion :: Coercion -> Coercion
367 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
368 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
369 -- becomes the kind @t2 ~ t1@.
370 mkSymCoercion g = mkCoercion symCoercionTyCon [g]
372 mkTransCoercion :: Coercion -> Coercion -> Coercion
373 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
374 mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
376 mkLeftCoercion :: Coercion -> Coercion
377 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
378 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
380 -- > mkLeftCoercion c :: f ~ g
381 mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
383 mkRightCoercion :: Coercion -> Coercion
384 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
385 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
387 -- > mkLeftCoercion c :: x ~ y
388 mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
390 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
391 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
392 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
393 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
395 -------------------------------
396 mkInstCoercion :: Coercion -> Type -> Coercion
397 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
398 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
399 mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty]
401 mkInstsCoercion :: Coercion -> [Type] -> Coercion
402 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
403 mkInstsCoercion co tys = foldl mkInstCoercion co tys
405 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
406 -- but it is used when we know we are dealing with bottom, which is one case in which
407 -- it is safe. This is also used implement the @unsafeCoerce#@ primitive.
408 -- Optimise by pushing down through type constructors
409 mkUnsafeCoercion :: Type -> Type -> Coercion
410 mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
412 = TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
414 mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
415 = FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)
417 mkUnsafeCoercion ty1 ty2
418 | ty1 `coreEqType` ty2 = ty1
419 | otherwise = mkCoercion unsafeCoercionTyCon [ty1, ty2]
421 -- See note [Newtype coercions] in TyCon
423 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
424 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
425 -- type the appropriate right hand side of the @newtype@, with the free variables
426 -- a subset of those 'TyVar's.
427 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
428 mkNewTypeCoercion name tycon tvs rhs_ty
429 = mkCoercionTyCon name arity desc
432 desc = CoAxiom { co_ax_tvs = tvs
433 , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
434 , co_ax_rhs = rhs_ty }
436 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
437 -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
438 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
439 -- representation tycon.
440 mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
441 -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
442 -> TyCon -- ^ Family tycon (@F@)
443 -> [Type] -- ^ Type instance (@ts@)
444 -> TyCon -- ^ Representation tycon (@R@)
445 -> TyCon -- ^ Coercion tycon (@Co@)
446 mkFamInstCoercion name tvs family inst_tys rep_tycon
447 = mkCoercionTyCon name arity desc
450 desc = CoAxiom { co_ax_tvs = tvs
451 , co_ax_lhs = mkTyConApp family inst_tys
452 , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
455 mkClassPPredCo :: Class -> [Coercion] -> Coercion
456 mkClassPPredCo cls = (PredTy . ClassP cls)
458 mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
459 mkIParamPredCo ipn = (PredTy . IParam ipn)
461 mkEqPredCo :: Coercion -> Coercion -> Coercion
462 mkEqPredCo co1 co2 = PredTy (EqPred co1 co2)
468 %************************************************************************
470 Coercion Type Constructors
472 %************************************************************************
474 Example. The coercion ((sym c) (sym d) (sym e))
475 will be represented by (TyConApp sym [c, sym d, sym e])
479 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
482 -- | Coercion type constructors: avoid using these directly and instead use
483 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
485 -- Each coercion TyCon is built with the special CoercionTyCon record and
486 -- carries its own kinding rule. Such CoercionTyCons must be fully applied
487 -- by any TyConApp in which they are applied, however they may also be over
488 -- applied (see example above) and the kinding function must deal with this.
489 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
490 rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
491 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
493 symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym
494 transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans
495 leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft
496 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight
497 instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst
498 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
499 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
500 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
501 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
503 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
504 rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
505 csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
507 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
508 symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
509 leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
510 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
511 instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
512 csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
513 csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
514 cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
515 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
517 mkCoConName :: FastString -> Unique -> TyCon -> Name
518 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
519 key (ATyCon coCon) BuiltInSyntax
524 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
525 -- Helper for left and right. Finds coercion kind of its input and
526 -- returns the left and right projections of the coercion...
528 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
529 decompLR_maybe (ty1,ty2)
530 | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
531 , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
532 = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
533 decompLR_maybe _ = Nothing
536 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
537 decompInst_maybe (ty1, ty2)
538 | Just (tv1,r1) <- splitForAllTy_maybe ty1
539 , Just (tv2,r2) <- splitForAllTy_maybe ty2
540 = Just ((tv1,tv2), (r1,r2))
541 decompInst_maybe _ = Nothing
544 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
545 -- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
546 -- Then csel1 co :: s1 ~ s2
547 -- csel2 co :: t1 ~ t2
548 -- cselR co :: r1 ~ r2
549 decompCsel_maybe (ty1, ty2)
550 | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
551 , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
552 = Just ((s1,s2), (t1,t2), (r1,r2))
553 decompCsel_maybe _ = Nothing
557 %************************************************************************
561 %************************************************************************
564 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
565 -- ^ If @co :: T ts ~ rep_ty@ then:
567 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
568 instNewTyCon_maybe tc tys
569 | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
570 = ASSERT( tys `lengthIs` tyConArity tc )
571 Just (substTyWith tvs tys ty,
573 Nothing -> IdCo (mkTyConApp tc tys)
574 Just co_tc -> ACo (mkTyConApp co_tc tys))
578 -- this is here to avoid module loops
579 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
580 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
581 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
582 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
583 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
585 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
587 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
588 splitNewTypeRepCo_maybe ty
589 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
590 splitNewTypeRepCo_maybe (TyConApp tc tys)
591 | Just (ty', coi) <- instNewTyCon_maybe tc tys
593 ACo co -> Just (ty', co)
594 IdCo _ -> panic "splitNewTypeRepCo_maybe"
595 -- This case handled by coreView
596 splitNewTypeRepCo_maybe _
599 -- | Determines syntactic equality of coercions
600 coreEqCoercion :: Coercion -> Coercion -> Bool
601 coreEqCoercion = coreEqType
603 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
604 coreEqCoercion2 = coreEqType2
608 %************************************************************************
610 CoercionI and its constructors
612 %************************************************************************
614 --------------------------------------
615 -- CoercionI smart constructors
616 -- lifted smart constructors of ordinary coercions
619 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
620 -- can represent either one of:
622 -- 1. A proper 'Coercion'
624 -- 2. The identity coercion
625 data CoercionI = IdCo Type | ACo Coercion
627 liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
628 liftCoI f (IdCo ty) = IdCo (f ty)
629 liftCoI f (ACo ty) = ACo (f ty)
631 liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
632 liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
633 liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2))
635 liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
636 liftCoIs f cois = go_id [] cois
638 go_id rev_tys [] = IdCo (f (reverse rev_tys))
639 go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois
640 go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
642 go_aco rev_tys [] = ACo (f (reverse rev_tys))
643 go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
644 go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
646 instance Outputable CoercionI where
647 ppr (IdCo _) = ptext (sLit "IdCo")
648 ppr (ACo co) = ppr co
650 isIdentityCoI :: CoercionI -> Bool
651 isIdentityCoI (IdCo _) = True
652 isIdentityCoI (ACo _) = False
654 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
655 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
656 fromCoI :: CoercionI -> Type
657 fromCoI (IdCo ty) = ty -- Identity coercion represented
658 fromCoI (ACo co) = co -- by the type itself
660 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
661 mkSymCoI :: CoercionI -> CoercionI
662 mkSymCoI (IdCo ty) = IdCo ty
663 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
664 -- the smart constructor
665 -- is too smart with tyvars
667 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
668 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
669 mkTransCoI (IdCo _) aco = aco
670 mkTransCoI aco (IdCo _) = aco
671 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
673 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
674 mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
675 mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
677 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
678 mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
679 mkAppTyCoI = liftCoI2 mkAppTy
681 mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
682 mkFunTyCoI = liftCoI2 mkFunTy
684 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
685 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
686 mkForAllTyCoI tv = liftCoI (ForAllTy tv)
688 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
690 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
691 mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
692 mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
694 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
695 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
696 mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
698 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
699 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
700 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
702 mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
703 mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
708 %************************************************************************
710 The kind of a type, and of a coercion
712 %************************************************************************
715 typeKind :: Type -> Kind
716 typeKind ty@(TyConApp tc tys)
717 | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
718 | otherwise = kindAppResult (tyConKind tc) tys
719 -- During coercion optimisation we *do* match a type
720 -- against a coercion (see OptCoercion.matchesAxiomLhs)
721 -- So the use of typeKind in Unify.match_kind must work on coercions too
722 -- Hence the isCoercionTyCon case above
724 typeKind (PredTy pred) = predKind pred
725 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
726 typeKind (ForAllTy _ ty) = typeKind ty
727 typeKind (TyVarTy tyvar) = tyVarKind tyvar
728 typeKind (FunTy _arg res)
729 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
730 -- not unliftedTypKind (#)
731 -- The only things that can be after a function arrow are
732 -- (a) types (of kind openTypeKind or its sub-kinds)
733 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
734 | isTySuperKind k = k
735 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
740 predKind :: PredType -> Kind
741 predKind (EqPred {}) = coSuperKind -- A coercion kind!
742 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
743 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
746 -- | If it is the case that
750 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@,
751 -- then @coercionKind c = (t1, t2)@.
752 coercionKind :: Coercion -> (Type, Type)
753 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
754 | otherwise = (ty, ty)
755 coercionKind (AppTy ty1 ty2)
756 = let (s1, t1) = coercionKind ty1
757 (s2, t2) = coercionKind ty2 in
758 (mkAppTy s1 s2, mkAppTy t1 t2)
759 coercionKind co@(TyConApp tc args)
760 | Just (ar, desc) <- isCoercionTyCon_maybe tc
761 -- CoercionTyCons carry their kinding rule, so we use it here
762 = WARN( not (length args >= ar), ppr co ) -- Always saturated
763 (let (ty1, ty2) = coTyConAppKind desc (take ar args)
764 (tys1, tys2) = coercionKinds (drop ar args)
765 in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
768 = let (lArgs, rArgs) = coercionKinds args in
769 (TyConApp tc lArgs, TyConApp tc rArgs)
771 coercionKind (FunTy ty1 ty2)
772 = let (t1, t2) = coercionKind ty1
773 (s1, s2) = coercionKind ty2 in
774 (mkFunTy t1 s1, mkFunTy t2 s2)
776 coercionKind (ForAllTy tv ty)
778 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
779 -- ----------------------------------------------
780 -- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
783 = let (c1,c2) = coVarKind tv
784 (s1,s2) = coercionKind c1
785 (t1,t2) = coercionKind c2
786 (r1,r2) = coercionKind ty
788 (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
791 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
792 -- ----------------------------------------------
793 -- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
794 = let (ty1, ty2) = coercionKind ty in
795 (ForAllTy tv ty1, ForAllTy tv ty2)
797 coercionKind (PredTy (ClassP cl args))
798 = let (lArgs, rArgs) = coercionKinds args in
799 (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
800 coercionKind (PredTy (IParam name ty))
801 = let (ty1, ty2) = coercionKind ty in
802 (PredTy (IParam name ty1), PredTy (IParam name ty2))
803 coercionKind (PredTy (EqPred c1 c2))
804 = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
805 -- These should not show up in coercions at all
806 -- becuase they are in the form of for-alls
807 let k1 = coercionKindPredTy c1
808 k2 = coercionKindPredTy c2 in
811 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
814 -- | Apply 'coercionKind' to multiple 'Coercion's
815 coercionKinds :: [Coercion] -> ([Type], [Type])
816 coercionKinds tys = unzip $ map coercionKind tys
819 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
820 -- and constructs the types that the resulting coercion relates.
821 -- Fails (in the monad) if ill-kinded.
822 -- Typically the monad is
823 -- either the Lint monad (with the consistency-check flag = True),
824 -- or the ID monad with a panic on failure (and the consistency-check flag = False)
827 -> [Type] -- Exactly right number of args
828 -> (Type, Type) -- Kind of this application
829 coTyConAppKind CoUnsafe (ty1:ty2:_)
831 coTyConAppKind CoSym (co:_)
832 | (ty1,ty2) <- coercionKind co = (ty2,ty1)
833 coTyConAppKind CoTrans (co1:co2:_)
834 = (fst (coercionKind co1), snd (coercionKind co2))
835 coTyConAppKind CoLeft (co:_)
836 | Just (res,_) <- decompLR_maybe (coercionKind co) = res
837 coTyConAppKind CoRight (co:_)
838 | Just (_,res) <- decompLR_maybe (coercionKind co) = res
839 coTyConAppKind CoCsel1 (co:_)
840 | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
841 coTyConAppKind CoCsel2 (co:_)
842 | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
843 coTyConAppKind CoCselR (co:_)
844 | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
845 coTyConAppKind CoInst (co:ty:_)
846 | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
847 = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
848 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
849 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
850 = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
852 (tys1, tys2) = coercionKinds cos
853 coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
854 [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
856 coercionKind (head cos)