X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypes%2FKind.lhs;h=336e9b6c7c01d2994f9c219f7e4bf2906ae93865;hb=845db8182942e006a9164e41e9839adb39f24268;hp=6d6e8a39d76db2100a1807934fc4656d51f27702;hpb=dac953bc82de9816f29d1992c1c48d3b19c3fd8b;p=ghc-hetmet.git diff --git a/ghc/compiler/types/Kind.lhs b/ghc/compiler/types/Kind.lhs index 6d6e8a3..336e9b6 100644 --- a/ghc/compiler/types/Kind.lhs +++ b/ghc/compiler/types/Kind.lhs @@ -1,102 +1,208 @@ % -% (c) The AQUA Project, Glasgow University, 1996 +% (c) The GRASP/AQUA Project, Glasgow University, 1998 % -\section[Kind]{The @Kind@ datatype} \begin{code} -#include "HsVersions.h" - module Kind ( - Kind(..), -- Only visible to friends: TcKind + Kind(..), KindVar(..), SimpleKind, + openTypeKind, liftedTypeKind, unliftedTypeKind, + argTypeKind, ubxTupleKind, - mkArrowKind, - mkTypeKind, - mkUnboxedTypeKind, - mkBoxedTypeKind, + isLiftedTypeKind, isUnliftedTypeKind, + isArgTypeKind, isOpenTypeKind, + mkArrowKind, mkArrowKinds, - hasMoreBoxityInfo, - resultKind, argKind, + isSubKind, defaultKind, + kindFunResult, splitKindFunTys, mkKindVar, - pprKind, pprParendKind, + pprKind, pprParendKind + ) where - isUnboxedTypeKind, isTypeKind, isBoxedTypeKind, - notArrowKind - ) where +#include "HsVersions.h" -IMP_Ubiq(){-uitous-} +import Unique ( Unique ) +import Outputable +import DATA_IOREF +\end{code} -import Util ( panic, assertPanic ) +Kinds +~~~~~ +There's a little subtyping at the kind level: -import Outputable ( Outputable(..), pprQuote ) -import Pretty -\end{code} + ? + / \ + / \ + ?? (#) + / \ + * # -\begin{code} -data Kind - = TypeKind -- Any type (incl unboxed types) - | BoxedTypeKind -- Any boxed type - | UnboxedTypeKind -- Any unboxed type - | ArrowKind Kind Kind - deriving Eq +where * [LiftedTypeKind] means boxed type + # [UnliftedTypeKind] means unboxed type + (#) [UbxTupleKind] means unboxed tuple + ?? [ArgTypeKind] is the lub of *,# + ? [OpenTypeKind] means any type at all -mkArrowKind = ArrowKind -mkTypeKind = TypeKind -mkUnboxedTypeKind = UnboxedTypeKind -mkBoxedTypeKind = BoxedTypeKind +In particular: -isTypeKind :: Kind -> Bool -isTypeKind TypeKind = True -isTypeKind other = False + error :: forall a:. String -> a + (->) :: ?? -> ? -> * + (\(x::t) -> ...) Here t:: (i.e. not unboxed tuple) -isBoxedTypeKind :: Kind -> Bool -isBoxedTypeKind BoxedTypeKind = True -isBoxedTypeKind other = False +\begin{code} +data Kind + = LiftedTypeKind -- * + | OpenTypeKind -- ? + | UnliftedTypeKind -- # + | UbxTupleKind -- (##) + | ArgTypeKind -- ?? + | FunKind Kind Kind -- k1 -> k2 + | KindVar KindVar + deriving( Eq ) + +data KindVar = KVar Unique (IORef (Maybe SimpleKind)) + -- INVARIANT: a KindVar can only be instantaited by a SimpleKind + +type SimpleKind = Kind + -- A SimpleKind has no ? or # kinds in it: + -- sk ::= * | sk1 -> sk2 | kvar + +instance Eq KindVar where + (KVar u1 _) == (KVar u2 _) = u1 == u2 + +mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar +mkKindVar = KVar +\end{code} -isUnboxedTypeKind :: Kind -> Bool -isUnboxedTypeKind UnboxedTypeKind = True -isUnboxedTypeKind other = False +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#). -hasMoreBoxityInfo :: Kind -> Kind -> Bool +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 ??. -BoxedTypeKind `hasMoreBoxityInfo` TypeKind = True -BoxedTypeKind `hasMoreBoxityInfo` BoxedTypeKind = True +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. -UnboxedTypeKind `hasMoreBoxityInfo` TypeKind = True -UnboxedTypeKind `hasMoreBoxityInfo` UnboxedTypeKind = True +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? -TypeKind `hasMoreBoxityInfo` TypeKind = True -kind1@(ArrowKind _ _) `hasMoreBoxityInfo` kind2@(ArrowKind _ _) = ASSERT( kind1 == kind2 ) - True - -- The two kinds can be arrow kinds; for example when unifying - -- (m1 Int) and (m2 Int) we end up unifying m1 and m2, which should - -- have the same kind. +\begin{code} +liftedTypeKind = LiftedTypeKind +unliftedTypeKind = UnliftedTypeKind +openTypeKind = OpenTypeKind +argTypeKind = ArgTypeKind +ubxTupleKind = UbxTupleKind -kind1 `hasMoreBoxityInfo` kind2 = False +mkArrowKind :: Kind -> Kind -> Kind +mkArrowKind k1 k2 = k1 `FunKind` k2 -notArrowKind (ArrowKind _ _) = False -notArrowKind other_kind = True +mkArrowKinds :: [Kind] -> Kind -> Kind +mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds +\end{code} -resultKind :: Kind -> Kind -- Get result from arrow kind -resultKind (ArrowKind _ res_kind) = res_kind -resultKind other_kind = panic "resultKind" +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ -argKind :: Kind -> Kind -- Get argument from arrow kind -argKind (ArrowKind arg_kind _) = arg_kind -argKind other_kind = panic "argKind" +\begin{code} +kindFunResult :: Kind -> Kind +kindFunResult (FunKind _ k) = k +kindFunResult k = pprPanic "kindFunResult" (ppr k) + +splitKindFunTys :: Kind -> ([Kind],Kind) +splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of + (as, r) -> (k1:as, r) +splitKindFunTys k = ([], k) + +isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool +isLiftedTypeKind LiftedTypeKind = True +isLiftedTypeKind other = False + +isUnliftedTypeKind UnliftedTypeKind = True +isUnliftedTypeKind other = False + +isArgTypeKind :: Kind -> Bool +-- True of any sub-kind of ArgTypeKind +isArgTypeKind LiftedTypeKind = True +isArgTypeKind UnliftedTypeKind = 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 other = True + +isSubKind :: Kind -> Kind -> Bool +-- (k1 `isSubKind` k2) checks that k1 <: k2 +isSubKind LiftedTypeKind LiftedTypeKind = True +isSubKind UnliftedTypeKind UnliftedTypeKind = 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 + +defaultKind :: Kind -> Kind +-- Used when generalising: default kind '?' and '??' to '*' +-- +-- 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; +-- consider +-- f x = True +-- We want f to get type +-- f :: forall (a::*). a -> Bool +-- Not +-- 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} -Printing -~~~~~~~~ + +%************************************************************************ +%* * + Pretty printing +%* * +%************************************************************************ + \begin{code} +instance Outputable KindVar where + ppr (KVar uniq _) = text "k_" <> ppr uniq + instance Outputable Kind where - ppr sty kind = pprQuote sty $ \ _ -> pprKind kind + 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 OpenTypeKind = ptext SLIT("?") +pprKind ArgTypeKind = ptext SLIT("??") +pprKind UbxTupleKind = ptext SLIT("(#)") +pprKind (FunKind k1 k2) = sep [ pprParendKind k1, arrow <+> pprKind k2] +\end{code} + -pprKind TypeKind = text "**" -- Can be boxed or unboxed -pprKind BoxedTypeKind = char '*' -pprKind UnboxedTypeKind = text "*#" -- Unboxed -pprKind (ArrowKind k1 k2) = sep [pprParendKind k1, text "->", pprKind k2] -pprParendKind k@(ArrowKind _ _) = parens (pprKind k) -pprParendKind k = pprKind k -\end{code}