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,
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)
466 %************************************************************************
468 Coercion Type Constructors
470 %************************************************************************
472 Example. The coercion ((sym c) (sym d) (sym e))
473 will be represented by (TyConApp sym [c, sym d, sym e])
477 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
480 -- | Coercion type constructors: avoid using these directly and instead use
481 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
483 -- Each coercion TyCon is built with the special CoercionTyCon record and
484 -- carries its own kinding rule. Such CoercionTyCons must be fully applied
485 -- by any TyConApp in which they are applied, however they may also be over
486 -- applied (see example above) and the kinding function must deal with this.
487 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
488 rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
489 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
491 symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym
492 transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans
493 leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft
494 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight
495 instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst
496 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
497 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
498 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
499 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
501 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
502 rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
503 csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
505 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
506 symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
507 leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
508 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
509 instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
510 csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
511 csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
512 cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
513 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
515 mkCoConName :: FastString -> Unique -> TyCon -> Name
516 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
517 key (ATyCon coCon) BuiltInSyntax
522 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
523 -- Helper for left and right. Finds coercion kind of its input and
524 -- returns the left and right projections of the coercion...
526 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
527 decompLR_maybe (ty1,ty2)
528 | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
529 , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
530 = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
531 decompLR_maybe _ = Nothing
534 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
535 decompInst_maybe (ty1, ty2)
536 | Just (tv1,r1) <- splitForAllTy_maybe ty1
537 , Just (tv2,r2) <- splitForAllTy_maybe ty2
538 = Just ((tv1,tv2), (r1,r2))
539 decompInst_maybe _ = Nothing
542 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
543 -- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
544 -- Then csel1 co :: s1 ~ s2
545 -- csel2 co :: t1 ~ t2
546 -- cselR co :: r1 ~ r2
547 decompCsel_maybe (ty1, ty2)
548 | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
549 , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
550 = Just ((s1,s2), (t1,t2), (r1,r2))
551 decompCsel_maybe _ = Nothing
555 %************************************************************************
559 %************************************************************************
562 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
563 -- ^ If @co :: T ts ~ rep_ty@ then:
565 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
566 instNewTyCon_maybe tc tys
567 | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
568 = ASSERT( tys `lengthIs` tyConArity tc )
569 Just (substTyWith tvs tys ty,
571 Nothing -> IdCo (mkTyConApp tc tys)
572 Just co_tc -> ACo (mkTyConApp co_tc tys))
576 -- this is here to avoid module loops
577 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
578 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
579 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
580 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
581 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
583 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
585 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
586 splitNewTypeRepCo_maybe ty
587 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
588 splitNewTypeRepCo_maybe (TyConApp tc tys)
589 | Just (ty', coi) <- instNewTyCon_maybe tc tys
591 ACo co -> Just (ty', co)
592 IdCo _ -> panic "splitNewTypeRepCo_maybe"
593 -- This case handled by coreView
594 splitNewTypeRepCo_maybe _
597 -- | Determines syntactic equality of coercions
598 coreEqCoercion :: Coercion -> Coercion -> Bool
599 coreEqCoercion = coreEqType
601 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
602 coreEqCoercion2 = coreEqType2
606 %************************************************************************
608 CoercionI and its constructors
610 %************************************************************************
612 --------------------------------------
613 -- CoercionI smart constructors
614 -- lifted smart constructors of ordinary coercions
617 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
618 -- can represent either one of:
620 -- 1. A proper 'Coercion'
622 -- 2. The identity coercion
623 data CoercionI = IdCo Type | ACo Coercion
625 liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
626 liftCoI f (IdCo ty) = IdCo (f ty)
627 liftCoI f (ACo ty) = ACo (f ty)
629 liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
630 liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
631 liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2))
633 liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
634 liftCoIs f cois = go_id [] cois
636 go_id rev_tys [] = IdCo (f (reverse rev_tys))
637 go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois
638 go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
640 go_aco rev_tys [] = ACo (f (reverse rev_tys))
641 go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
642 go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
644 instance Outputable CoercionI where
645 ppr (IdCo _) = ptext (sLit "IdCo")
646 ppr (ACo co) = ppr co
648 isIdentityCoI :: CoercionI -> Bool
649 isIdentityCoI (IdCo _) = True
650 isIdentityCoI (ACo _) = False
652 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
653 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
654 fromCoI :: CoercionI -> Type
655 fromCoI (IdCo ty) = ty -- Identity coercion represented
656 fromCoI (ACo co) = co -- by the type itself
658 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
659 mkSymCoI :: CoercionI -> CoercionI
660 mkSymCoI (IdCo ty) = IdCo ty
661 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
662 -- the smart constructor
663 -- is too smart with tyvars
665 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
666 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
667 mkTransCoI (IdCo _) aco = aco
668 mkTransCoI aco (IdCo _) = aco
669 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
671 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
672 mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
673 mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
675 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
676 mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
677 mkAppTyCoI = liftCoI2 mkAppTy
679 mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
680 mkFunTyCoI = liftCoI2 mkFunTy
682 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
683 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
684 mkForAllTyCoI tv = liftCoI (ForAllTy tv)
686 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
688 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
689 mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
690 mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
692 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
693 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
694 mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
696 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
697 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
698 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
700 mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
701 mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
706 %************************************************************************
708 The kind of a type, and of a coercion
710 %************************************************************************
713 typeKind :: Type -> Kind
714 typeKind ty@(TyConApp tc tys)
715 | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
716 | otherwise = kindAppResult (tyConKind tc) tys
717 -- During coercion optimisation we *do* match a type
718 -- against a coercion (see OptCoercion.matchesAxiomLhs)
719 -- So the use of typeKind in Unify.match_kind must work on coercions too
720 -- Hence the isCoercionTyCon case above
722 typeKind (PredTy pred) = predKind pred
723 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
724 typeKind (ForAllTy _ ty) = typeKind ty
725 typeKind (TyVarTy tyvar) = tyVarKind tyvar
726 typeKind (FunTy _arg res)
727 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
728 -- not unliftedTypKind (#)
729 -- The only things that can be after a function arrow are
730 -- (a) types (of kind openTypeKind or its sub-kinds)
731 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
732 | isTySuperKind k = k
733 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
738 predKind :: PredType -> Kind
739 predKind (EqPred {}) = coSuperKind -- A coercion kind!
740 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
741 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
744 -- | If it is the case that
748 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@,
749 -- then @coercionKind c = (t1, t2)@.
750 coercionKind :: Coercion -> (Type, Type)
751 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
752 | otherwise = (ty, ty)
753 coercionKind (AppTy ty1 ty2)
754 = let (s1, t1) = coercionKind ty1
755 (s2, t2) = coercionKind ty2 in
756 (mkAppTy s1 s2, mkAppTy t1 t2)
757 coercionKind co@(TyConApp tc args)
758 | Just (ar, desc) <- isCoercionTyCon_maybe tc
759 -- CoercionTyCons carry their kinding rule, so we use it here
760 = WARN( not (length args >= ar), ppr co ) -- Always saturated
761 (let (ty1, ty2) = coTyConAppKind desc (take ar args)
762 (tys1, tys2) = coercionKinds (drop ar args)
763 in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
766 = let (lArgs, rArgs) = coercionKinds args in
767 (TyConApp tc lArgs, TyConApp tc rArgs)
769 coercionKind (FunTy ty1 ty2)
770 = let (t1, t2) = coercionKind ty1
771 (s1, s2) = coercionKind ty2 in
772 (mkFunTy t1 s1, mkFunTy t2 s2)
774 coercionKind (ForAllTy tv ty)
776 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
777 -- ----------------------------------------------
778 -- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
781 = let (c1,c2) = coVarKind tv
782 (s1,s2) = coercionKind c1
783 (t1,t2) = coercionKind c2
784 (r1,r2) = coercionKind ty
786 (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
789 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
790 -- ----------------------------------------------
791 -- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
792 = let (ty1, ty2) = coercionKind ty in
793 (ForAllTy tv ty1, ForAllTy tv ty2)
795 coercionKind (PredTy (ClassP cl args))
796 = let (lArgs, rArgs) = coercionKinds args in
797 (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
798 coercionKind (PredTy (IParam name ty))
799 = let (ty1, ty2) = coercionKind ty in
800 (PredTy (IParam name ty1), PredTy (IParam name ty2))
801 coercionKind (PredTy (EqPred c1 c2))
802 = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
803 -- These should not show up in coercions at all
804 -- becuase they are in the form of for-alls
805 let k1 = coercionKindPredTy c1
806 k2 = coercionKindPredTy c2 in
809 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
812 -- | Apply 'coercionKind' to multiple 'Coercion's
813 coercionKinds :: [Coercion] -> ([Type], [Type])
814 coercionKinds tys = unzip $ map coercionKind tys
817 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
818 -- and constructs the types that the resulting coercion relates.
819 -- Fails (in the monad) if ill-kinded.
820 -- Typically the monad is
821 -- either the Lint monad (with the consistency-check flag = True),
822 -- or the ID monad with a panic on failure (and the consistency-check flag = False)
825 -> [Type] -- Exactly right number of args
826 -> (Type, Type) -- Kind of this application
827 coTyConAppKind CoUnsafe (ty1:ty2:_)
829 coTyConAppKind CoSym (co:_)
830 | (ty1,ty2) <- coercionKind co = (ty2,ty1)
831 coTyConAppKind CoTrans (co1:co2:_)
832 = (fst (coercionKind co1), snd (coercionKind co2))
833 coTyConAppKind CoLeft (co:_)
834 | Just (res,_) <- decompLR_maybe (coercionKind co) = res
835 coTyConAppKind CoRight (co:_)
836 | Just (_,res) <- decompLR_maybe (coercionKind co) = res
837 coTyConAppKind CoCsel1 (co:_)
838 | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
839 coTyConAppKind CoCsel2 (co:_)
840 | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
841 coTyConAppKind CoCselR (co:_)
842 | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
843 coTyConAppKind CoInst (co:ty:_)
844 | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
845 = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
846 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
847 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
848 = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
850 (tys1, tys2) = coercionKinds cos
851 coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
852 [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
854 coercionKind (head cos)