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