%
-% (c) The GRASP/AQUA Project, Glasgow University, 1998
+% (c) The University of Glasgow 2006
%
\begin{code}
module Kind (
- Kind(..), SimpleKind,
- openTypeKind, liftedTypeKind, unliftedTypeKind,
- argTypeKind, ubxTupleKind,
+ -- * Main data type
+ Kind, typeKind,
- isLiftedTypeKind, isUnliftedTypeKind,
- 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
- # [UnliftedTypeKind] 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 -- ?
- | 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
-unliftedTypeKind = UnliftedTypeKind
-openTypeKind = OpenTypeKind
-argTypeKind = ArgTypeKind
-ubxTupleKind = UbxTupleKind
+isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
-mkArrowKind :: Kind -> Kind -> Kind
-mkArrowKind k1 k2 = k1 `FunKind` k2
+isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
+isUnliftedTypeKind _ = False
-mkArrowKinds :: [Kind] -> Kind -> Kind
-mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
-\end{code}
+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.
-%************************************************************************
-%* *
- 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)
+isSubArgTypeKindCon kc
+ | isUnliftedTypeKindCon kc = True
+ | isLiftedTypeKindCon kc = True
+ | isArgTypeKindCon kc = True
+ | otherwise = False
-isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
-isLiftedTypeKind LiftedTypeKind = True
-isLiftedTypeKind other = False
+isSubArgTypeKind :: Kind -> Bool
+-- ^ True of any sub-kind of ArgTypeKind
+isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
+isSubArgTypeKind _ = False
-isUnliftedTypeKind UnliftedTypeKind = True
-isUnliftedTypeKind other = False
+-- | Is this a super-kind (i.e. a type-of-kinds)?
+isSuperKind :: Type -> Bool
+isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
+isSuperKind _ = 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 (KindVar _) = False -- This is a conservative answer
- -- It matters in the call to isSubKind in
- -- checkExpectedKind.
-isOpenTypeKind other = True
+-- | 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 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;
-- 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 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 OpenTypeKind = ptext SLIT("?")
-pprKind ArgTypeKind = ptext SLIT("??")
-pprKind UbxTupleKind = ptext SLIT("(#)")
-pprKind (FunKind k1 k2) = sep [ pprParendKind k1, arrow <+> pprKind k2]
-
-\end{code}
+defaultKind k
+ | isSubOpenTypeKind k = liftedTypeKind
+ | isSubArgTypeKind k = liftedTypeKind
+ | otherwise = k
+\end{code}
\ No newline at end of file
projects / ghc-hetmet.git / blobdiff