%
-% (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,
- isUnboxedKind, isTypeKind,
- notArrowKind
- ) where
+ pprKind, pprParendKind
+ ) where
-IMP_Ubiq(){-uitous-}
+#include "HsVersions.h"
-import Util ( panic, assertPanic )
---import Outputable ( Outputable(..) )
-import Pretty
+import Unique ( Unique )
+import Outputable
+import DATA_IOREF
\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
+Kinds
+~~~~~
+There's a little subtyping at the kind level:
+
+ ?
+ / \
+ / \
+ ?? (#)
+ / \
+ * #
-mkArrowKind = ArrowKind
-mkTypeKind = TypeKind
-mkUnboxedTypeKind = UnboxedTypeKind
-mkBoxedTypeKind = BoxedTypeKind
+where * [LiftedTypeKind] means boxed type
+ # [UnliftedTypeKind] means unboxed type
+ (#) [UbxTupleKind] means unboxed tuple
+ ?? [ArgTypeKind] is the lub of *,#
+ ? [OpenTypeKind] means any type at all
-isTypeKind :: Kind -> Bool
-isTypeKind TypeKind = True
-isTypeKind other = False
+In particular:
+
+ error :: forall a:?. String -> a
+ (->) :: ?? -> ? -> *
+ (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple)
+
+\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}
-isUnboxedKind :: Kind -> Bool
-isUnboxedKind UnboxedTypeKind = True
-isUnboxedKind 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 = 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 = ppStr "*"
-pprKind BoxedTypeKind = ppStr "*b"
-pprKind UnboxedTypeKind = ppStr "*u"
-pprKind (ArrowKind k1 k2) = ppSep [pprKind_parend k1, ppStr "->", pprKind k2]
-pprKind_parend k@(ArrowKind _ _) = ppBesides [ppLparen, pprKind k, ppRparen]
-pprKind_parend k = pprKind k
-\end{code}