diff options
Diffstat (limited to 'compiler/types/Kind.lhs')
| -rw-r--r-- | compiler/types/Kind.lhs | 218 |
1 files changed, 94 insertions, 124 deletions
diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 3fda25c592..b3684151b1 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -36,18 +36,18 @@ module Kind ( -- ** Predicates on Kinds isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isUbxTupleKind, isArgTypeKind, isConstraintKind, - isConstraintOrLiftedKind, isKind, - isSuperKind, isSuperKindTyCon, noHashInKind, + isConstraintOrLiftedKind, isKind, isKindVar, + isSuperKind, isSuperKindTyCon, isLiftedTypeKindCon, isConstraintKindCon, isAnyKind, isAnyKindCon, + okArrowArgKind, okArrowResultKind, - isSubArgTypeKind, tcIsSubArgTypeKind, - isSubOpenTypeKind, tcIsSubOpenTypeKind, - isSubKind, tcIsSubKind, defaultKind, - isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon, + isSubArgTypeKind, isSubOpenTypeKind, + isSubKind, isSubKindCon, + tcIsSubKind, tcIsSubKindCon, + defaultKind, -- ** Functions on variables - isKiVar, splitKiTyVars, partitionKiTyVars, kiVarsOfKind, kiVarsOfKinds ) where @@ -59,38 +59,9 @@ import {-# SOURCE #-} Type ( typeKind, substKiWith, eqKind ) import TypeRep import TysPrim import TyCon -import Var import VarSet import PrelNames import Outputable - -import Data.List ( partition ) -\end{code} - -%************************************************************************ -%* * - Predicates over Kinds -%* * -%************************************************************************ - -\begin{code} -------------------- --- Lastly we need a few functions on Kinds - -isLiftedTypeKindCon :: TyCon -> Bool -isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey - --- This checks that its argument does not contain # or (#). --- It is used in tcTyVarBndrs. -noHashInKind :: Kind -> Bool -noHashInKind (TyVarTy {}) = True -noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2 -noHashInKind (ForAllTy _ ki) = noHashInKind ki -noHashInKind (TyConApp kc kis) - = not (kc `hasKey` unliftedTypeKindTyConKey) - && not (kc `hasKey` ubxTupleKindTyConKey) - && all noHashInKind kis -noHashInKind _ = panic "noHashInKind" \end{code} %************************************************************************ @@ -139,37 +110,34 @@ isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind, isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon, - isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon, - isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon, - isAnyKindCon :: TyCon -> Bool + isUnliftedTypeKindCon, isSubArgTypeKindCon, + isSubOpenTypeKindCon, isConstraintKindCon, + isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool -isAnyKindCon tc = tyConUnique tc == anyKindTyConKey + +isLiftedTypeKindCon tc = tyConUnique tc == liftedTypeKindTyConKey +isAnyKindCon tc = tyConUnique tc == anyKindTyConKey +isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey +isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey +isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey +isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey +isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey isAnyKind (TyConApp tc _) = isAnyKindCon tc isAnyKind _ = False -isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey - isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc isOpenTypeKind _ = False -isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey - isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc isUbxTupleKind _ = False -isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey - isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc isArgTypeKind _ = False -isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey - isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc isUnliftedTypeKind _ = False -isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey - isConstraintKind (TyConApp tc _) = isConstraintKindCon tc isConstraintKind _ = False @@ -177,106 +145,120 @@ isConstraintOrLiftedKind (TyConApp tc _) = isConstraintKindCon tc || isLiftedTypeKindCon tc isConstraintOrLiftedKind _ = False --- Subkinding +-------------------------------------------- +-- Kinding for arrow (->) +-- Says when a kind is acceptable on lhs or rhs of an arrow +-- arg -> res + +okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool +okArrowArgKindCon kc + | isLiftedTypeKindCon kc = True + | isUnliftedTypeKindCon kc = True + | isConstraintKindCon kc = True + | otherwise = False + +okArrowResultKindCon kc + | okArrowArgKindCon kc = True + | isUbxTupleKindCon kc = True + | otherwise = False + +okArrowArgKind, okArrowResultKind :: Kind -> Bool +okArrowArgKind (TyConApp kc []) = okArrowArgKindCon kc +okArrowArgKind _ = False + +okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc +okArrowResultKind _ = False + +----------------------------------------- +-- Subkinding -- 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 argTypeKind -isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool +isSubOpenTypeKind :: Kind -> Bool -- ^ True of any sub-kind of OpenTypeKind isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc isSubOpenTypeKind _ = False --- ^ True of any sub-kind of OpenTypeKind -tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc -tcIsSubOpenTypeKind _ = False - isSubOpenTypeKindCon kc - | isSubArgTypeKindCon kc = True - | isUbxTupleKindCon kc = True - | isOpenTypeKindCon kc = True - | otherwise = False - -tcIsSubOpenTypeKindCon kc - | tcIsSubArgTypeKindCon kc = True - | isUbxTupleKindCon kc = True - | isOpenTypeKindCon kc = True - | otherwise = False + = isSubArgTypeKindCon kc + || isUbxTupleKindCon kc + || isOpenTypeKindCon kc + || isConstraintKindCon kc -- Needed for error (Num a) "blah" + -- and so that (Ord a -> Eq a) is well-kinded isSubArgTypeKindCon kc - | isUnliftedTypeKindCon kc = True - | isLiftedTypeKindCon kc = True - | isArgTypeKindCon kc = True - | isConstraintKindCon kc = True - | otherwise = False + = isUnliftedTypeKindCon kc + || isLiftedTypeKindCon kc + || isArgTypeKindCon kc -tcIsSubArgTypeKindCon kc - | isConstraintKindCon kc = False - | otherwise = isSubArgTypeKindCon kc - -isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool +isSubArgTypeKind :: Kind -> Bool -- ^ True of any sub-kind of ArgTypeKind isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc isSubArgTypeKind _ = False -tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc -tcIsSubArgTypeKind _ = False - --- | Is this a super-kind (i.e. a type-of-kinds)? -isSuperKind :: Type -> Bool -isSuperKind (TyConApp skc []) = isSuperKindTyCon skc -isSuperKind _ = False - -isSuperKindTyCon :: TyCon -> Bool -isSuperKindTyCon tc = tc `hasKey` superKindTyConKey - -- | Is this a kind (i.e. a type-of-types)? isKind :: Kind -> Bool isKind k = isSuperKind (typeKind k) -isSubKind, tcIsSubKind :: Kind -> Kind -> Bool -isSubKind = isSubKind' False -tcIsSubKind = isSubKind' True - --- The first argument denotes whether we are in the type-checking phase or not -isSubKind' :: Bool -> Kind -> Kind -> Bool +isSubKind :: Kind -> Kind -> Bool -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ -isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2) - = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2) +isSuperKindTyCon :: TyCon -> Bool +isSuperKindTyCon tc = tc `hasKey` superKindTyConKey + +isSubKind (FunTy a1 r1) (FunTy a2 r2) + = (isSubKind a2 a1) && (isSubKind r1 r2) -isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) +isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2 -- handles promoted kinds (List *, Nat, etc.) - = eqKind k1 k2 + = eqKind k1 k2 | isSuperKindTyCon kc1 || isSuperKindTyCon kc2 -- handles BOX - = WARN( not (isSuperKindTyCon kc2 && isSuperKindTyCon kc2 - && null k1s && null k2s), + = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 + && null k1s && null k2s, ppr kc1 <+> ppr kc2 ) - kc1 == 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 ) - if duringTc then kc1 `tcIsSubKindCon` kc2 - else kc1 `isSubKindCon` kc2 + kc1 `isSubKindCon` kc2 -isSubKind' _duringTc k1 k2 = eqKind k1 k2 +isSubKind k1 k2 = eqKind k1 k2 isSubKindCon :: TyCon -> TyCon -> Bool -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ isSubKindCon kc1 kc2 - | kc1 == kc2 = True - | isSubArgTypeKindCon kc1 && isArgTypeKindCon kc2 = True - | isSubOpenTypeKindCon kc1 && isOpenTypeKindCon kc2 = True - | otherwise = False + | kc1 == kc2 = True + | isArgTypeKindCon kc2 = isSubArgTypeKindCon kc1 + | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 + | otherwise = False + +------------------------- +-- Hack alert: we need a tiny variant for the typechecker +-- Reason: f :: Int -> (a~b) +-- g :: forall (c::Constraint). Int -> c +-- We want to reject these, even though Constraint is +-- a sub-kind of OpenTypeKind. It must be a sub-kind of OpenTypeKind +-- *after* the typechecker +-- a) So that (Ord a -> Eq a) is a legal type +-- b) So that the simplifer can generate (error (Eq a) "urk") +-- +-- Easiest way to reject is simply to make Constraint not +-- below OpenTypeKind when type checking + +tcIsSubKind :: Kind -> Kind -> Bool +tcIsSubKind k1 k2 + | isConstraintKind k1 = isConstraintKind k2 + | otherwise = isSubKind k1 k2 tcIsSubKindCon :: TyCon -> TyCon -> Bool tcIsSubKindCon kc1 kc2 - | kc1 == kc2 = True - | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False - | otherwise = isSubKindCon kc1 kc2 + | isConstraintKindCon kc1 = isConstraintKindCon kc2 + | otherwise = isSubKindCon kc1 kc2 +------------------------- defaultKind :: Kind -> Kind -- ^ Used when generalising: default OpenKind and ArgKind to *. -- See "Type#kind_subtyping" for more information on what that means @@ -294,20 +276,8 @@ defaultKind :: Kind -> Kind -- and the calling conventions differ. -- This defaulting is done in TcMType.zonkTcTyVarBndr. defaultKind k - | tcIsSubOpenTypeKind k = liftedTypeKind - | otherwise = k - -splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) --- Precondition: kind variables should precede type variables --- Postcondition: appending the two result lists gives the input! -splitKiTyVars = span (isSuperKind . tyVarKind) - -partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) -partitionKiTyVars = partition (isSuperKind . tyVarKind) - --- Checks if this "type or kind" variable is a kind variable -isKiVar :: TyVar -> Bool -isKiVar v = isSuperKind (varType v) + | isSubOpenTypeKind k = liftedTypeKind + | otherwise = k -- Returns the free kind variables in a kind kiVarsOfKind :: Kind -> VarSet |