X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FKind.lhs;h=668ddda92a44cbd7839b2d10c24878bce821d616;hp=79999c27bfb5a99621141aeebb8dcb870af0841b;hb=c0687066474aa4ce4912f31a5c09c1bcd673fb06;hpb=ee2dd59cf1c96437696b9ec39b35dd1beea259a1 diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 79999c2..668ddda 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -1,196 +1,222 @@ % -% (c) The GRASP/AQUA Project, Glasgow University, 1998 +% (c) The University of Glasgow 2006 % \begin{code} module Kind ( - Kind(..), SimpleKind, - openTypeKind, liftedTypeKind, unliftedTypeKind, unboxedTypeKind, - argTypeKind, ubxTupleKind, + -- * Main data type + Kind, typeKind, - isLiftedTypeKind, isUnliftedTypeKind, isUnliftedBoxedTypeKind, - isArgTypeKind, isOpenTypeKind, - mkArrowKind, mkArrowKinds, + -- Kinds + liftedTypeKind, unliftedTypeKind, openTypeKind, + argTypeKind, ubxTupleKind, + mkArrowKind, mkArrowKinds, - isSubKind, defaultKind, - kindFunResult, splitKindFunTys, + -- Kind constructors... + liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon, + argTypeKindTyCon, ubxTupleKindTyCon, - KindVar, mkKindVar, kindVarRef, kindVarUniq, - kindVarOcc, setKindVarOcc, + -- Super Kinds + tySuperKind, tySuperKindTyCon, + + pprKind, pprParendKind, - pprKind, pprParendKind - ) where + -- ** Deconstructing Kinds + kindFunResult, kindAppResult, synTyConResKind, + splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe, + + -- ** Predicates on Kinds + isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, + isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, + isSuperKind, isCoercionKind, + isLiftedTypeKindCon, + + isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, + isSubKindCon, + + ) where #include "HsVersions.h" -import Unique ( Unique ) -import OccName ( OccName, mkOccName, tvName ) +import TypeRep +import TysPrim +import TyCon +import Var +import PrelNames import Outputable -import DATA_IOREF \end{code} -Kinds -~~~~~ -There's a little subtyping at the kind level: +%************************************************************************ +%* * + Predicates over Kinds +%* * +%************************************************************************ - ? - / \ - / \ - ?? (#) - / | \ - * ! # +\begin{code} +isTySuperKind :: SuperKind -> Bool +isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey +isTySuperKind _ = False -where * [LiftedTypeKind] means boxed type - # [UnboxedTypeKind] means unboxed type - (#) [UbxTupleKind] means unboxed tuple - ?? [ArgTypeKind] is the lub of *,# - ? [OpenTypeKind] means any type at all +------------------- +-- Lastly we need a few functions on Kinds -In particular: +isLiftedTypeKindCon :: TyCon -> Bool +isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey +\end{code} - error :: forall a:?. String -> a - (->) :: ?? -> ? -> * - (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple) +%************************************************************************ +%* * + The kind of a type +%* * +%************************************************************************ \begin{code} -data Kind - = LiftedTypeKind -- * - | OpenTypeKind -- ? - | UnboxedTypeKind -- # - | UnliftedTypeKind -- ! - | UbxTupleKind -- (##) - | ArgTypeKind -- ?? - | FunKind Kind Kind -- k1 -> k2 - | KindVar KindVar - deriving( Eq ) +typeKind :: Type -> Kind +typeKind _ty@(TyConApp tc tys) + = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty ) + -- Assertion checks for unsaturated application of (~) + -- See Note [The (~) TyCon] in TysPrim + kindAppResult (tyConKind tc) tys + +typeKind (PredTy pred) = predKind pred +typeKind (AppTy fun _) = kindFunResult (typeKind fun) +typeKind (ForAllTy _ ty) = typeKind ty +typeKind (TyVarTy tyvar) = tyVarKind tyvar +typeKind (FunTy _arg res) + -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*), + -- not unliftedTypKind (#) + -- The only things that can be after a function arrow are + -- (a) types (of kind openTypeKind or its sub-kinds) + -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *)) + | isTySuperKind k = k + | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind + where + k = typeKind res + +------------------ +predKind :: PredType -> Kind +predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted +predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are +predKind (IParam {}) = liftedTypeKind -- always represented by lifted types +\end{code} -data KindVar = KVar Unique OccName (IORef (Maybe SimpleKind)) - -- INVARIANT: a KindVar can only be instantiated by a SimpleKind +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ -type SimpleKind = Kind - -- A SimpleKind has no ? or # kinds in it: - -- sk ::= * | sk1 -> sk2 | kvar +\begin{code} +-- | Essentially 'funResultTy' on kinds +kindFunResult :: Kind -> Kind +kindFunResult (FunTy _ res) = res +kindFunResult k = pprPanic "kindFunResult" (ppr k) -instance Eq KindVar where - (KVar u1 _ _) == (KVar u2 _ _) = u1 == u2 +kindAppResult :: Kind -> [arg] -> Kind +kindAppResult k [] = k +kindAppResult k (_:as) = kindAppResult (kindFunResult k) as -mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar -mkKindVar u r = KVar u kind_var_occ r +-- | Essentially 'splitFunTys' on kinds +splitKindFunTys :: Kind -> ([Kind],Kind) +splitKindFunTys (FunTy a r) = case splitKindFunTys r of + (as, k) -> (a:as, k) +splitKindFunTys k = ([], k) -kindVarRef :: KindVar -> IORef (Maybe Kind) -kindVarRef (KVar _ _ ref) = ref +splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind) +splitKindFunTy_maybe (FunTy a r) = Just (a,r) +splitKindFunTy_maybe _ = Nothing -kindVarUniq :: KindVar -> Unique -kindVarUniq (KVar uniq _ _) = uniq +-- | Essentially 'splitFunTysN' on kinds +splitKindFunTysN :: Int -> Kind -> ([Kind],Kind) +splitKindFunTysN 0 k = ([], k) +splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of + (as, k) -> (a:as, k) +splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k) -kindVarOcc :: KindVar -> OccName -kindVarOcc (KVar _ occ _) = occ +-- | Find the result 'Kind' of a type synonym, +-- after applying it to its 'arity' number of type variables +-- Actually this function works fine on data types too, +-- but they'd always return '*', so we never need to ask +synTyConResKind :: TyCon -> Kind +synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon) -setKindVarOcc :: KindVar -> OccName -> KindVar -setKindVarOcc (KVar u _ r) occ = KVar u occ r +-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's +isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool +isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon, + isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool -kind_var_occ :: OccName -- Just one for all KindVars - -- They may be jiggled by tidying -kind_var_occ = mkOccName tvName "k" -\end{code} +isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey -Kind inference -~~~~~~~~~~~~~~ -During kind inference, a kind variable unifies only with -a "simple kind", sk - sk ::= * | sk1 -> sk2 -For example - data T a = MkT a (T Int#) -fails. We give T the kind (k -> *), and the kind variable k won't unify -with # (the kind of Int#). +isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc +isOpenTypeKind _ = False -Type inference -~~~~~~~~~~~~~~ -When creating a fresh internal type variable, we give it a kind to express -constraints on it. E.g. in (\x->e) we make up a fresh type variable for x, -with kind ??. +isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey -During unification we only bind an internal type variable to a type -whose kind is lower in the sub-kind hierarchy than the kind of the tyvar. +isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc +isUbxTupleKind _ = False -When unifying two internal type variables, we collect their kind constraints by -finding the GLB of the two. Since the partial order is a tree, they only -have a glb if one is a sub-kind of the other. In that case, we bind the -less-informative one to the more informative one. Neat, eh? +isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey +isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc +isArgTypeKind _ = False -\begin{code} -liftedTypeKind = LiftedTypeKind -unboxedTypeKind = UnboxedTypeKind -unliftedTypeKind = UnliftedTypeKind -openTypeKind = OpenTypeKind -argTypeKind = ArgTypeKind -ubxTupleKind = UbxTupleKind - -mkArrowKind :: Kind -> Kind -> Kind -mkArrowKind k1 k2 = k1 `FunKind` k2 - -mkArrowKinds :: [Kind] -> Kind -> Kind -mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds -\end{code} +isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey -%************************************************************************ -%* * - Functions over Kinds -%* * -%************************************************************************ +isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc +isUnliftedTypeKind _ = False -\begin{code} -kindFunResult :: Kind -> Kind -kindFunResult (FunKind _ k) = k -kindFunResult k = pprPanic "kindFunResult" (ppr k) +isSubOpenTypeKind :: Kind -> Bool +-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow) +isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) + ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) + False +isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True +isSubOpenTypeKind other = ASSERT( isKind other ) False + -- This is a conservative answer + -- It matters in the call to isSubKind in + -- checkExpectedKind. -splitKindFunTys :: Kind -> ([Kind],Kind) -splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of - (as, r) -> (k1:as, r) -splitKindFunTys k = ([], k) +isSubArgTypeKindCon kc + | isUnliftedTypeKindCon kc = True + | isLiftedTypeKindCon kc = True + | isArgTypeKindCon kc = True + | otherwise = False -isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool -isLiftedTypeKind LiftedTypeKind = True -isLiftedTypeKind other = False - -isUnliftedBoxedTypeKind UnliftedTypeKind = True -isUnliftedBoxedTypeKind other = False - -isUnliftedTypeKind UnliftedTypeKind = True -isUnliftedTypeKind UnboxedTypeKind = True -isUnliftedTypeKind other = False - -isArgTypeKind :: Kind -> Bool --- True of any sub-kind of ArgTypeKind -isArgTypeKind LiftedTypeKind = True -isArgTypeKind UnliftedTypeKind = True -isArgTypeKind UnboxedTypeKind = True -isArgTypeKind ArgTypeKind = True -isArgTypeKind other = False - -isOpenTypeKind :: Kind -> Bool --- True of any sub-kind of OpenTypeKind (i.e. anything except arrow) -isOpenTypeKind (FunKind _ _) = False -isOpenTypeKind (KindVar _) = False -- This is a conservative answer - -- It matters in the call to isSubKind in - -- checkExpectedKind. -isOpenTypeKind other = True +isSubArgTypeKind :: Kind -> Bool +-- ^ True of any sub-kind of ArgTypeKind +isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc +isSubArgTypeKind _ = False + +-- | Is this a super-kind (i.e. a type-of-kinds)? +isSuperKind :: Type -> Bool +isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc +isSuperKind _ = False + +-- | Is this a kind (i.e. a type-of-types)? +isKind :: Kind -> Bool +isKind k = isSuperKind (typeKind k) isSubKind :: Kind -> Kind -> Bool --- (k1 `isSubKind` k2) checks that k1 <: k2 -isSubKind LiftedTypeKind LiftedTypeKind = True -isSubKind UnliftedTypeKind UnliftedTypeKind = True -isSubKind UnboxedTypeKind UnboxedTypeKind = True -isSubKind UbxTupleKind UbxTupleKind = True -isSubKind k1 OpenTypeKind = isOpenTypeKind k1 -isSubKind k1 ArgTypeKind = isArgTypeKind k1 -isSubKind (FunKind a1 r1) (FunKind a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2) -isSubKind k1 k2 = False +-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ +isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2 +isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2) +isSubKind _ _ = False + +isSubKindCon :: TyCon -> TyCon -> Bool +-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ +isSubKindCon kc1 kc2 + | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True + | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True + | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True + | isOpenTypeKindCon kc2 = True + -- we already know kc1 is not a fun, its a TyCon + | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True + | otherwise = False defaultKind :: Kind -> Kind --- Used when generalising: default kind '?' and '??' to '*' --- +-- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more +-- information on what that means + -- When we generalise, we make generic type variables whose kind is -- simple (* or *->* etc). So generic type variables (other than -- built-in constants like 'error') always have simple kinds. This is important; @@ -202,36 +228,9 @@ defaultKind :: Kind -> Kind -- f :: forall (a::??). a -> Bool -- because that would allow a call like (f 3#) as well as (f True), --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr. -defaultKind OpenTypeKind = LiftedTypeKind -defaultKind ArgTypeKind = LiftedTypeKind -defaultKind kind = kind -\end{code} - - -%************************************************************************ -%* * - Pretty printing -%* * -%************************************************************************ +defaultKind k + | isSubOpenTypeKind k = liftedTypeKind + | isSubArgTypeKind k = liftedTypeKind + | otherwise = k -\begin{code} -instance Outputable KindVar where - ppr (KVar uniq occ _) = ppr occ <> ifPprDebug (ppr uniq) - -instance Outputable Kind where - ppr k = pprKind k - -pprParendKind :: Kind -> SDoc -pprParendKind k@(FunKind _ _) = parens (pprKind k) -pprParendKind k = pprKind k - -pprKind (KindVar v) = ppr v -pprKind LiftedTypeKind = ptext SLIT("*") -pprKind UnliftedTypeKind = ptext SLIT("!") -pprKind UnboxedTypeKind = ptext SLIT("#") -pprKind OpenTypeKind = ptext SLIT("?") -pprKind ArgTypeKind = ptext SLIT("??") -pprKind UbxTupleKind = ptext SLIT("(#)") -pprKind (FunKind k1 k2) = sep [ pprParendKind k1, arrow <+> pprKind k2] - -\end{code} +\end{code} \ No newline at end of file