X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypes%2FKind.lhs;h=0e88536ad6c2733c31f090685dee1a428bdc6718;hb=339d5220bcb7e8ca344ca5ec6e862d2373267be8;hp=d4fe4a3981cb27441b40aed5f0828f7f95dc7a74;hpb=9dd6e1c216993624a2cd74b62ca0f0569c02c26b;p=ghc-hetmet.git diff --git a/ghc/compiler/types/Kind.lhs b/ghc/compiler/types/Kind.lhs index d4fe4a3..0e88536 100644 --- a/ghc/compiler/types/Kind.lhs +++ b/ghc/compiler/types/Kind.lhs @@ -1,110 +1,208 @@ % -% (c) The AQUA Project, Glasgow University, 1996 +% (c) The GRASP/AQUA Project, Glasgow University, 1998 % -\section[Kind]{The @Kind@ datatype} \begin{code} module Kind ( - GenKind(..), -- Only visible to friends: TcKind - Kind, + 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, - - isUnboxedTypeKind, isTypeKind, isBoxedTypeKind - ) where + pprKind, pprParendKind + ) where #include "HsVersions.h" -import Util ( panic, assertPanic ) -import Unique ( Unique, pprUnique ) -import BasicTypes ( Unused ) +import Unique ( Unique ) import Outputable +import DATA_IOREF \end{code} +Kinds +~~~~~ +There's a little subtyping at the kind level: + + ? + / \ + / \ + ?? (#) + / \ + * # + +where * [LiftedTypeKind] means boxed type + # [UnliftedTypeKind] means unboxed type + (#) [UbxTupleKind] means unboxed tuple + ?? [ArgTypeKind] is the lub of *,# + ? [OpenTypeKind] means any type at all + +In particular: + + error :: forall a:?. String -> a + (->) :: ?? -> ? -> * + (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple) + \begin{code} -data GenKind flexi - = TypeKind -- Any type (incl unboxed types) - | BoxedTypeKind -- Any boxed type - | UnboxedTypeKind -- Any unboxed type - | ArrowKind (GenKind flexi) (GenKind flexi) - | VarKind Unique flexi - -type Kind = GenKind Unused -- No variables at all - -instance Eq (GenKind flexi) where - TypeKind == TypeKind = True - BoxedTypeKind == BoxedTypeKind = True - UnboxedTypeKind == UnboxedTypeKind = True - (ArrowKind j1 j2) == (ArrowKind k1 k2) = j1==k1 && j2==k2 - (VarKind u1 _) == (VarKind u2 _) = u1==u2 - k1 == k2 = False - -mkArrowKind = ArrowKind -mkTypeKind = TypeKind -mkUnboxedTypeKind = UnboxedTypeKind -mkBoxedTypeKind = BoxedTypeKind - -isTypeKind :: GenKind flexi -> Bool -isTypeKind TypeKind = True -isTypeKind other = False - -isBoxedTypeKind :: GenKind flexi -> Bool -isBoxedTypeKind BoxedTypeKind = True -isBoxedTypeKind other = False - -isUnboxedTypeKind :: GenKind flexi -> Bool -isUnboxedTypeKind UnboxedTypeKind = True -isUnboxedTypeKind other = False - -hasMoreBoxityInfo :: GenKind flexi -> GenKind flexi -> Bool - -BoxedTypeKind `hasMoreBoxityInfo` TypeKind = True -BoxedTypeKind `hasMoreBoxityInfo` BoxedTypeKind = True - -UnboxedTypeKind `hasMoreBoxityInfo` TypeKind = True -UnboxedTypeKind `hasMoreBoxityInfo` UnboxedTypeKind = True - -TypeKind `hasMoreBoxityInfo` TypeKind = True - -kind1@(ArrowKind _ _) `hasMoreBoxityInfo` kind2@(ArrowKind _ _) - = ASSERT( if kind1 == kind2 then True - else pprPanic "hadMoreBoxityInfo" (ppr kind1 <> comma <+> ppr 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. - -kind1 `hasMoreBoxityInfo` kind2 = False - -resultKind :: GenKind flexi -> GenKind flexi -- Get result from arrow kind -resultKind (ArrowKind _ res_kind) = res_kind -resultKind other_kind = panic "resultKind" - -argKind :: GenKind flexi -> GenKind flexi -- Get argument from arrow kind -argKind (ArrowKind arg_kind _) = arg_kind -argKind other_kind = panic "argKind" +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} -Printing -~~~~~~~~ +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#). + +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 ??. + +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. + +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? + + \begin{code} -instance Outputable (GenKind flexi) where - ppr kind = pprKind kind +liftedTypeKind = LiftedTypeKind +unliftedTypeKind = UnliftedTypeKind +openTypeKind = OpenTypeKind +argTypeKind = ArgTypeKind +ubxTupleKind = UbxTupleKind -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] -pprKind (VarKind u _) = char 'k' <> pprUnique u +mkArrowKind :: Kind -> Kind -> Kind +mkArrowKind k1 k2 = k1 `FunKind` k2 -pprParendKind k@(ArrowKind _ _) = parens (pprKind k) -pprParendKind k = pprKind k +mkArrowKinds :: [Kind] -> Kind -> Kind +mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds \end{code} + +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ + +\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} + + +%************************************************************************ +%* * + Pretty printing +%* * +%************************************************************************ + +\begin{code} +instance Outputable KindVar where + ppr (KVar uniq _) = text "k_" <> 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 OpenTypeKind = ptext SLIT("?") +pprKind ArgTypeKind = ptext SLIT("??") +pprKind UbxTupleKind = ptext SLIT("(#)") +pprKind (FunKind k1 k2) = sep [ pprParendKind k1, arrow <+> pprKind k2] +\end{code} + + +