diff options
| -rw-r--r-- | compiler/iface/IfaceType.lhs | 2 | ||||
| -rw-r--r-- | compiler/types/Kind.lhs | 59 | ||||
| -rw-r--r-- | compiler/types/Type.lhs | 18 |
3 files changed, 55 insertions, 24 deletions
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs index 4a35f0049b..7b38bcb1a3 100644 --- a/compiler/iface/IfaceType.lhs +++ b/compiler/iface/IfaceType.lhs @@ -195,7 +195,7 @@ pprParendIfaceType = ppr_ty tYCON_PREC isIfacePredTy :: IfaceType -> Bool isIfacePredTy _ = False -- FIXME: fix this to print iface pred tys correctly --- isIfacePredTy ty = ifaceTypeKind ty `eqKind` constraintKind +-- isIfacePredTy ty = isConstraintKind (ifaceTypeKind ty) ppr_ty :: Int -> IfaceType -> SDoc ppr_ty _ (IfaceTyVar tyvar) = ppr tyvar diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 50d382f5fa..6ce2dd9957 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -70,6 +70,30 @@ import Util %* * %************************************************************************ +Note [Kind Constraint and kind *] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The kind Constraint is the kind of classes and other type constraints. +The special thing about types of kind Constraint is that + * They are displayed with double arrow: + f :: Ord a => a -> a + * They are implicitly instantiated at call sites; so the type inference + engine inserts an extra argument of type (Ord a) at every call site + to f. + +Howver, once type inference is over, there is *no* distinction between +Constraint and *. Indeed we can have coercions between the two. Consider + class C a where + op :: a -> a +For this single-method class we may genreate a newtype, which in turn +generates an axiom witnessing + Ord a ~ (a -> a) +so on the left we have Constraint, and on the right we have *. +See Trac #7451. + +Bottom line: although '*' and 'Constraint' are distinct TyCons, with +distinct uniques, they are treated as equal at all times except +during type inference. Hence cmpTc treats them as equal. + \begin{code} -- | Essentially 'funResultTy' on kinds handling pi-types too kindFunResult :: Kind -> KindOrType -> Kind @@ -111,7 +135,7 @@ isOpenTypeKind, isUnliftedTypeKind, isOpenTypeKindCon, isUnliftedTypeKindCon, isSubOpenTypeKindCon, isConstraintKindCon, - isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool + isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool isLiftedTypeKindCon tc = tyConUnique tc == liftedTypeKindTyConKey @@ -119,6 +143,7 @@ isAnyKindCon tc = tyConUnique tc == anyKindTyConKey isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey +isSuperKindTyCon tc = tyConUnique tc == superKindTyConKey isAnyKind (TyConApp tc _) = isAnyKindCon tc isAnyKind _ = False @@ -168,6 +193,7 @@ okArrowResultKind _ = False -- The tc variants are used during type-checking, where we don't want the -- Constraint kind to be a subkind of anything -- After type-checking (in core), Constraint is a subkind of openTypeKind + isSubOpenTypeKind :: Kind -> Bool -- ^ True of any sub-kind of OpenTypeKind isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc @@ -180,6 +206,7 @@ isSubOpenTypeKindCon kc || isConstraintKindCon kc -- Needed for error (Num a) "blah" -- and so that (Ord a -> Eq a) is well-kinded -- and so that (# Eq a, Ord b #) is well-kinded + -- See Note [Kind Constraint and kind *] -- | Is this a kind (i.e. a type-of-types)? isKind :: Kind -> Bool @@ -187,37 +214,29 @@ isKind k = isSuperKind (typeKind k) isSubKind :: Kind -> Kind -> Bool -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ - -isSuperKindTyCon :: TyCon -> Bool -isSuperKindTyCon tc = tc `hasKey` superKindTyConKey - -isSubKind (FunTy a1 r1) (FunTy a2 r2) - = (isSubKind a2 a1) && (isSubKind r1 r2) +-- Sub-kinding is extremely simple and does not look +-- under arrrows or type constructors isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) | isPromotedTyCon kc1 || isPromotedTyCon kc2 -- handles promoted kinds (List *, Nat, etc.) = eqKind k1 k2 - | isSuperKindTyCon kc1 || isSuperKindTyCon kc2 - -- handles BOX - = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 - && null k1s && null k2s, - ppr kc1 <+> ppr kc2 ) - True -- If one is BOX, the other must be too - - | otherwise = -- handles usual kinds (*, #, (#), etc.) - ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 ) - kc1 `isSubKindCon` kc2 + | otherwise -- handles usual kinds (*, #, (#), etc.) + = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 ) + kc1 `isSubKindCon` kc2 isSubKind k1 k2 = eqKind k1 k2 isSubKindCon :: TyCon -> TyCon -> Bool -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ isSubKindCon kc1 kc2 - | kc1 == kc2 = True - | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 - | otherwise = False + | kc1 == kc2 = True + | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 + | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2 + | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2 + | otherwise = False + -- See Note [Kind Constraint and kind *] ------------------------- -- Hack alert: we need a tiny variant for the typechecker diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 57706612e2..f6983074fc 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -153,7 +153,8 @@ import Class import TyCon import TysPrim import {-# SOURCE #-} TysWiredIn ( eqTyCon, mkBoxedTupleTy ) -import PrelNames ( eqTyConKey, ipClassNameKey ) +import PrelNames ( eqTyConKey, ipClassNameKey, + constraintKindTyConKey, liftedTypeKindTyConKey ) -- others import Unique ( Unique, hasKey ) @@ -844,7 +845,7 @@ noParenPred p = not (isIPPred p) && isClassPred p || isEqPred p isPredTy :: Type -> Bool isPredTy ty | isSuperKind ty = False - | otherwise = typeKind ty `eqKind` constraintKind + | otherwise = isConstraintKind (typeKind ty) isKindTy :: Type -> Bool isKindTy = isSuperKind . typeKind @@ -1232,7 +1233,7 @@ cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX env (tyVarKind t `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2 cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2 cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2 -cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2 +cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `cmpTc` tc2) `thenCmp` cmpTypesX env tys1 tys2 cmpTypeX _ (LitTy l1) (LitTy l2) = compare l1 l2 -- Deal with the rest: TyVarTy < AppTy < FunTy < LitTy < TyConApp < ForAllTy < PredTy @@ -1264,6 +1265,17 @@ cmpTypesX _ [] [] = EQ cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2 cmpTypesX _ [] _ = LT cmpTypesX _ _ [] = GT + +------------- +cmpTc :: TyCon -> TyCon -> Ordering +-- Here we treat * and Constraint as equal +-- See Note [Kind Constraint and kind *] in Kinds.lhs +cmpTc tc1 tc2 = nu1 `compare` nu2 + where + u1 = tyConUnique tc1 + nu1 = if u1==constraintKindTyConKey then liftedTypeKindTyConKey else u1 + u2 = tyConUnique tc2 + nu2 = if u2==constraintKindTyConKey then liftedTypeKindTyConKey else u2 \end{code} Note [cmpTypeX] |