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,
51 unsafeCoercionTyCon, symCoercionTyCon,
52 transCoercionTyCon, leftCoercionTyCon,
53 rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
54 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
57 decompLR_maybe, decompCsel_maybe, decompInst_maybe,
59 splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
62 coreEqCoercion, coreEqCoercion2,
68 mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
71 mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
75 #include "HsVersions.h"
91 %************************************************************************
95 %************************************************************************
98 -- | Essentially 'funResultTy' on kinds
99 kindFunResult :: Kind -> Kind
100 kindFunResult k = funResultTy k
102 kindAppResult :: Kind -> [arg] -> Kind
103 kindAppResult k [] = k
104 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
106 -- | Essentially 'splitFunTys' on kinds
107 splitKindFunTys :: Kind -> ([Kind],Kind)
108 splitKindFunTys k = splitFunTys k
110 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
111 splitKindFunTy_maybe = splitFunTy_maybe
113 -- | Essentially 'splitFunTysN' on kinds
114 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
115 splitKindFunTysN k = splitFunTysN k
117 -- | Find the result 'Kind' of a type synonym,
118 -- after applying it to its 'arity' number of type variables
119 -- Actually this function works fine on data types too,
120 -- but they'd always return '*', so we never need to ask
121 synTyConResKind :: TyCon -> Kind
122 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
124 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
125 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
126 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
127 isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
129 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
131 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
132 isOpenTypeKind _ = False
134 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
136 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
137 isUbxTupleKind _ = False
139 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
141 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
142 isArgTypeKind _ = False
144 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
146 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
147 isUnliftedTypeKind _ = False
149 isSubOpenTypeKind :: Kind -> Bool
150 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
151 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
152 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
154 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
155 isSubOpenTypeKind other = ASSERT( isKind other ) False
156 -- This is a conservative answer
157 -- It matters in the call to isSubKind in
158 -- checkExpectedKind.
160 isSubArgTypeKindCon kc
161 | isUnliftedTypeKindCon kc = True
162 | isLiftedTypeKindCon kc = True
163 | isArgTypeKindCon kc = True
166 isSubArgTypeKind :: Kind -> Bool
167 -- ^ True of any sub-kind of ArgTypeKind
168 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
169 isSubArgTypeKind _ = False
171 -- | Is this a super-kind (i.e. a type-of-kinds)?
172 isSuperKind :: Type -> Bool
173 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
174 isSuperKind _ = False
176 -- | Is this a kind (i.e. a type-of-types)?
177 isKind :: Kind -> Bool
178 isKind k = isSuperKind (typeKind k)
180 isSubKind :: Kind -> Kind -> Bool
181 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
182 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
183 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
184 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
185 = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
186 isSubKind _ _ = False
188 eqKind :: Kind -> Kind -> Bool
191 isSubKindCon :: TyCon -> TyCon -> Bool
192 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
194 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
195 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
196 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
197 | isOpenTypeKindCon kc2 = True
198 -- we already know kc1 is not a fun, its a TyCon
199 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
202 defaultKind :: Kind -> Kind
203 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
204 -- information on what that means
206 -- When we generalise, we make generic type variables whose kind is
207 -- simple (* or *->* etc). So generic type variables (other than
208 -- built-in constants like 'error') always have simple kinds. This is important;
211 -- We want f to get type
212 -- f :: forall (a::*). a -> Bool
214 -- f :: forall (a::??). a -> Bool
215 -- because that would allow a call like (f 3#) as well as (f True),
216 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
218 | isSubOpenTypeKind k = liftedTypeKind
219 | isSubArgTypeKind k = liftedTypeKind
223 %************************************************************************
227 %************************************************************************
231 -- | A 'Coercion' represents a 'Type' something should be coerced to.
234 -- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
235 -- types that a 'Coercion' will work on.
236 type CoercionKind = Kind
238 ------------------------------
240 -- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
241 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
243 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
244 decomposeCo :: Arity -> Coercion -> [Coercion]
249 go n co cos = go (n-1) (mkLeftCoercion co)
250 (mkRightCoercion co : cos)
253 -------------------------------------------------------
254 -- and some coercion kind stuff
256 coVarKind :: CoVar -> (Type,Type)
258 coVarKind cv = case coVarKind_maybe cv of
260 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
262 coVarKind_maybe :: CoVar -> Maybe (Type,Type)
263 coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
265 -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
266 -- Panics if the argument is not a valid 'CoercionKind'
267 splitCoKind_maybe :: Kind -> Maybe (Type, Type)
268 splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
269 splitCoKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
270 splitCoKind_maybe _ = Nothing
272 -- | Makes a 'CoercionKind' from two types: the types whose equality
273 -- is proven by the relevant 'Coercion'
274 mkCoKind :: Type -> Type -> CoercionKind
275 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
277 -- | (mkCoPredTy s t r) produces the type: (s~t) => r
278 mkCoPredTy :: Type -> Type -> Type -> Type
279 mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
281 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
282 splitCoPredTy_maybe ty
283 | Just (cv,r) <- splitForAllTy_maybe ty
285 , Just (s,t) <- coVarKind_maybe cv
290 -- | Tests whether a type is just a type equality predicate
291 isEqPredTy :: Type -> Bool
292 isEqPredTy (PredTy pred) = isEqPred pred
295 -- | Creates a type equality predicate
296 mkEqPred :: (Type, Type) -> PredType
297 mkEqPred (ty1, ty2) = EqPred ty1 ty2
299 -- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
301 getEqPredTys :: PredType -> (Type,Type)
302 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
303 getEqPredTys other = pprPanic "getEqPredTys" (ppr other)
305 isIdentityCoercion :: Coercion -> Bool
306 isIdentityCoercion co
307 = case coercionKind co of
308 (t1,t2) -> t1 `coreEqType` t2
311 %************************************************************************
315 %************************************************************************
317 Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
320 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
321 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
323 mkCoercion :: TyCon -> [Type] -> Coercion
324 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
327 mkCoVarCoercion :: CoVar -> Coercion
328 mkCoVarCoercion cv = mkTyVarTy cv
330 -- | Apply a 'Coercion' to another 'Coercion', which is presumably a
331 -- 'Coercion' constructor of some kind
332 mkAppCoercion :: Coercion -> Coercion -> Coercion
333 mkAppCoercion co1 co2 = mkAppTy co1 co2
335 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
336 -- See also 'mkAppCoercion'
337 mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
338 mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
340 -- | Apply a type constructor to a list of coercions.
341 mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
342 mkTyConCoercion con cos = mkTyConApp con cos
344 -- | Make a function 'Coercion' between two other 'Coercion's
345 mkFunCoercion :: Coercion -> Coercion -> Coercion
346 mkFunCoercion co1 co2 = mkFunTy co1 co2
348 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
349 mkForAllCoercion :: Var -> Coercion -> Coercion
350 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
351 mkForAllCoercion tv co = ASSERT ( isTyCoVar tv ) mkForAllTy tv co
354 -------------------------------
356 mkSymCoercion :: Coercion -> Coercion
357 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality
358 -- between the same types but in the other "direction", so a kind of @t1 ~ t2@
359 -- becomes the kind @t2 ~ t1@.
360 mkSymCoercion g = mkCoercion symCoercionTyCon [g]
362 mkTransCoercion :: Coercion -> Coercion -> Coercion
363 -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
364 mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
366 mkLeftCoercion :: Coercion -> Coercion
367 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
368 -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
370 -- > mkLeftCoercion c :: f ~ g
371 mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
373 mkRightCoercion :: Coercion -> Coercion
374 -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of
375 -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
377 -- > mkLeftCoercion c :: x ~ y
378 mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
380 mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
381 mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
382 mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
383 mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
385 -------------------------------
386 mkInstCoercion :: Coercion -> Type -> Coercion
387 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
388 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
389 mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty]
391 mkInstsCoercion :: Coercion -> [Type] -> Coercion
392 -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
393 mkInstsCoercion co tys = foldl mkInstCoercion co tys
395 -- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
396 -- but it is used when we know we are dealing with bottom, which is one case in which
397 -- it is safe. This is also used implement the @unsafeCoerce#@ primitive.
398 -- Optimise by pushing down through type constructors
399 mkUnsafeCoercion :: Type -> Type -> Coercion
400 mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
402 = TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
404 mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
405 = FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)
407 mkUnsafeCoercion ty1 ty2
408 | ty1 `coreEqType` ty2 = ty1
409 | otherwise = mkCoercion unsafeCoercionTyCon [ty1, ty2]
411 -- See note [Newtype coercions] in TyCon
413 -- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
414 -- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
415 -- type the appropriate right hand side of the @newtype@, with the free variables
416 -- a subset of those 'TyVar's.
417 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
418 mkNewTypeCoercion name tycon tvs rhs_ty
419 = mkCoercionTyCon name arity desc
422 desc = CoAxiom { co_ax_tvs = tvs
423 , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
424 , co_ax_rhs = rhs_ty }
426 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
427 -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is
428 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
429 -- representation tycon.
430 mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
431 -> [TyVar] -- ^ Type parameters of the coercion (@tvs@)
432 -> TyCon -- ^ Family tycon (@F@)
433 -> [Type] -- ^ Type instance (@ts@)
434 -> TyCon -- ^ Representation tycon (@R@)
435 -> TyCon -- ^ Coercion tycon (@Co@)
436 mkFamInstCoercion name tvs family inst_tys rep_tycon
437 = mkCoercionTyCon name arity desc
440 desc = CoAxiom { co_ax_tvs = tvs
441 , co_ax_lhs = mkTyConApp family inst_tys
442 , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
446 %************************************************************************
448 Coercion Type Constructors
450 %************************************************************************
452 Example. The coercion ((sym c) (sym d) (sym e))
453 will be represented by (TyConApp sym [c, sym d, sym e])
457 then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
460 -- | Coercion type constructors: avoid using these directly and instead use
461 -- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
463 -- Each coercion TyCon is built with the special CoercionTyCon record and
464 -- carries its own kinding rule. Such CoercionTyCons must be fully applied
465 -- by any TyConApp in which they are applied, however they may also be over
466 -- applied (see example above) and the kinding function must deal with this.
467 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
468 rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
469 csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
471 symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym
472 transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans
473 leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft
474 rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight
475 instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst
476 csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
477 csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
478 cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
479 unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
481 transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
482 rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
483 csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
485 transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
486 symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
487 leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
488 rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
489 instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
490 csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
491 csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
492 cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
493 unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
495 mkCoConName :: FastString -> Unique -> TyCon -> Name
496 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
497 key (ATyCon coCon) BuiltInSyntax
502 decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
503 -- Helper for left and right. Finds coercion kind of its input and
504 -- returns the left and right projections of the coercion...
506 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
507 decompLR_maybe (ty1,ty2)
508 | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
509 , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
510 = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
511 decompLR_maybe _ = Nothing
514 decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
515 decompInst_maybe (ty1, ty2)
516 | Just (tv1,r1) <- splitForAllTy_maybe ty1
517 , Just (tv2,r2) <- splitForAllTy_maybe ty2
518 = Just ((tv1,tv2), (r1,r2))
519 decompInst_maybe _ = Nothing
522 decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
523 -- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
524 -- Then csel1 co :: s1 ~ s2
525 -- csel2 co :: t1 ~ t2
526 -- cselR co :: r1 ~ r2
527 decompCsel_maybe (ty1, ty2)
528 | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
529 , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
530 = Just ((s1,s2), (t1,t2), (r1,r2))
531 decompCsel_maybe _ = Nothing
535 %************************************************************************
539 %************************************************************************
542 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
543 -- ^ If @co :: T ts ~ rep_ty@ then:
545 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
546 instNewTyCon_maybe tc tys
547 | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
548 = ASSERT( tys `lengthIs` tyConArity tc )
549 Just (substTyWith tvs tys ty,
551 Nothing -> IdCo (mkTyConApp tc tys)
552 Just co_tc -> ACo (mkTyConApp co_tc tys))
556 -- this is here to avoid module loops
557 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
558 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
559 -- This function only strips *one layer* of @newtype@ off, so the caller will usually call
560 -- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
561 -- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
563 -- > splitNewTypeRepCo_maybe ty = Just (ty', co)
565 -- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
566 splitNewTypeRepCo_maybe ty
567 | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
568 splitNewTypeRepCo_maybe (TyConApp tc tys)
569 | Just (ty', coi) <- instNewTyCon_maybe tc tys
571 ACo co -> Just (ty', co)
572 IdCo _ -> panic "splitNewTypeRepCo_maybe"
573 -- This case handled by coreView
574 splitNewTypeRepCo_maybe _
577 -- | Determines syntactic equality of coercions
578 coreEqCoercion :: Coercion -> Coercion -> Bool
579 coreEqCoercion = coreEqType
581 coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
582 coreEqCoercion2 = coreEqType2
586 %************************************************************************
588 CoercionI and its constructors
590 %************************************************************************
592 --------------------------------------
593 -- CoercionI smart constructors
594 -- lifted smart constructors of ordinary coercions
597 -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
598 -- can represent either one of:
600 -- 1. A proper 'Coercion'
602 -- 2. The identity coercion
603 data CoercionI = IdCo Type | ACo Coercion
605 liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
606 liftCoI f (IdCo ty) = IdCo (f ty)
607 liftCoI f (ACo ty) = ACo (f ty)
609 liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
610 liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
611 liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2))
613 liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
614 liftCoIs f cois = go_id [] cois
616 go_id rev_tys [] = IdCo (f (reverse rev_tys))
617 go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois
618 go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
620 go_aco rev_tys [] = ACo (f (reverse rev_tys))
621 go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
622 go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois
624 instance Outputable CoercionI where
625 ppr (IdCo _) = ptext (sLit "IdCo")
626 ppr (ACo co) = ppr co
628 isIdentityCoI :: CoercionI -> Bool
629 isIdentityCoI (IdCo _) = True
630 isIdentityCoI (ACo _) = False
632 -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
633 -- 'Type' if the 'CoercionI' is the identity 'Coercion'
634 fromCoI :: CoercionI -> Type
635 fromCoI (IdCo ty) = ty -- Identity coercion represented
636 fromCoI (ACo co) = co -- by the type itself
638 -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
639 mkSymCoI :: CoercionI -> CoercionI
640 mkSymCoI (IdCo ty) = IdCo ty
641 mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
642 -- the smart constructor
643 -- is too smart with tyvars
645 -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
646 mkTransCoI :: CoercionI -> CoercionI -> CoercionI
647 mkTransCoI (IdCo _) aco = aco
648 mkTransCoI aco (IdCo _) = aco
649 mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
651 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
652 mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
653 mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
655 -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
656 mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
657 mkAppTyCoI = liftCoI2 mkAppTy
659 mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
660 mkFunTyCoI = liftCoI2 mkFunTy
662 -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
663 mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
664 mkForAllTyCoI tv = liftCoI (ForAllTy tv)
666 -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
668 -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
669 mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
670 mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
672 -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
673 mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
674 mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
676 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
677 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
678 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
681 %************************************************************************
683 The kind of a type, and of a coercion
685 %************************************************************************
688 typeKind :: Type -> Kind
689 typeKind ty@(TyConApp tc tys)
690 | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
691 | otherwise = kindAppResult (tyConKind tc) tys
692 -- During coercion optimisation we *do* match a type
693 -- against a coercion (see OptCoercion.matchesAxiomLhs)
694 -- So the use of typeKind in Unify.match_kind must work on coercions too
695 -- Hence the isCoercionTyCon case above
697 typeKind (PredTy pred) = predKind pred
698 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
699 typeKind (ForAllTy _ ty) = typeKind ty
700 typeKind (TyVarTy tyvar) = tyVarKind tyvar
701 typeKind (FunTy _arg res)
702 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
703 -- not unliftedTypKind (#)
704 -- The only things that can be after a function arrow are
705 -- (a) types (of kind openTypeKind or its sub-kinds)
706 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
707 | isTySuperKind k = k
708 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
713 predKind :: PredType -> Kind
714 predKind (EqPred {}) = coSuperKind -- A coercion kind!
715 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
716 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
719 -- | If it is the case that
723 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
724 coercionKind :: Coercion -> (Type, Type)
725 coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
726 | otherwise = (ty, ty)
727 coercionKind (AppTy ty1 ty2)
728 = let (s1, t1) = coercionKind ty1
729 (s2, t2) = coercionKind ty2 in
730 (mkAppTy s1 s2, mkAppTy t1 t2)
731 coercionKind co@(TyConApp tc args)
732 | Just (ar, desc) <- isCoercionTyCon_maybe tc
733 -- CoercionTyCons carry their kinding rule, so we use it here
734 = WARN( not (length args >= ar), ppr co ) -- Always saturated
735 (let (ty1, ty2) = coTyConAppKind desc (take ar args)
736 (tys1, tys2) = coercionKinds (drop ar args)
737 in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
740 = let (lArgs, rArgs) = coercionKinds args in
741 (TyConApp tc lArgs, TyConApp tc rArgs)
743 coercionKind (FunTy ty1 ty2)
744 = let (t1, t2) = coercionKind ty1
745 (s1, s2) = coercionKind ty2 in
746 (mkFunTy t1 s1, mkFunTy t2 s2)
748 coercionKind (ForAllTy tv ty)
750 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
751 -- ----------------------------------------------
752 -- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
755 = let (c1,c2) = coVarKind tv
756 (s1,s2) = coercionKind c1
757 (t1,t2) = coercionKind c2
758 (r1,r2) = coercionKind ty
760 (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
763 -- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
764 -- ----------------------------------------------
765 -- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
766 = let (ty1, ty2) = coercionKind ty in
767 (ForAllTy tv ty1, ForAllTy tv ty2)
769 coercionKind (PredTy (ClassP cl args))
770 = let (lArgs, rArgs) = coercionKinds args in
771 (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
772 coercionKind (PredTy (IParam name ty))
773 = let (ty1, ty2) = coercionKind ty in
774 (PredTy (IParam name ty1), PredTy (IParam name ty2))
775 coercionKind (PredTy (EqPred c1 c2))
776 = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
777 -- These should not show up in coercions at all
778 -- becuase they are in the form of for-alls
779 let k1 = coercionKindPredTy c1
780 k2 = coercionKindPredTy c2 in
783 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
786 -- | Apply 'coercionKind' to multiple 'Coercion's
787 coercionKinds :: [Coercion] -> ([Type], [Type])
788 coercionKinds tys = unzip $ map coercionKind tys
791 -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
792 -- and constructs the types that the resulting coercion relates.
793 -- Fails (in the monad) if ill-kinded.
794 -- Typically the monad is
795 -- either the Lint monad (with the consistency-check flag = True),
796 -- or the ID monad with a panic on failure (and the consistency-check flag = False)
799 -> [Type] -- Exactly right number of args
800 -> (Type, Type) -- Kind of this application
801 coTyConAppKind CoUnsafe (ty1:ty2:_)
803 coTyConAppKind CoSym (co:_)
804 | (ty1,ty2) <- coercionKind co = (ty2,ty1)
805 coTyConAppKind CoTrans (co1:co2:_)
806 = (fst (coercionKind co1), snd (coercionKind co2))
807 coTyConAppKind CoLeft (co:_)
808 | Just (res,_) <- decompLR_maybe (coercionKind co) = res
809 coTyConAppKind CoRight (co:_)
810 | Just (_,res) <- decompLR_maybe (coercionKind co) = res
811 coTyConAppKind CoCsel1 (co:_)
812 | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
813 coTyConAppKind CoCsel2 (co:_)
814 | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
815 coTyConAppKind CoCselR (co:_)
816 | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
817 coTyConAppKind CoInst (co:ty:_)
818 | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
819 = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2)
820 coTyConAppKind (CoAxiom { co_ax_tvs = tvs
821 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
822 = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
824 (tys1, tys2) = coercionKinds cos
825 coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)