2 % (c) The University of Glasgow 2006
11 liftedTypeKind, unliftedTypeKind, openTypeKind,
12 argTypeKind, ubxTupleKind,
13 mkArrowKind, mkArrowKinds,
15 -- Kind constructors...
16 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
17 argTypeKindTyCon, ubxTupleKindTyCon,
20 tySuperKind, tySuperKindTyCon,
22 pprKind, pprParendKind,
24 -- ** Deconstructing Kinds
25 kindFunResult, kindAppResult, synTyConResKind,
26 splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
28 -- ** Predicates on Kinds
29 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
30 isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
31 isSuperKind, isCoercionKind,
34 isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
39 #include "HsVersions.h"
49 %************************************************************************
53 %************************************************************************
56 isTySuperKind :: SuperKind -> Bool
57 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
58 isTySuperKind _ = False
61 -- Lastly we need a few functions on Kinds
63 isLiftedTypeKindCon :: TyCon -> Bool
64 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
67 %************************************************************************
71 %************************************************************************
74 typeKind :: Type -> Kind
75 typeKind (TyConApp tc tys)
76 = kindAppResult (tyConKind tc) tys
78 typeKind (PredTy pred) = predKind pred
79 typeKind (AppTy fun _) = kindFunResult (typeKind fun)
80 typeKind (ForAllTy _ ty) = typeKind ty
81 typeKind (TyVarTy tyvar) = tyVarKind tyvar
82 typeKind (FunTy _arg res)
83 -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
84 -- not unliftedTypKind (#)
85 -- The only things that can be after a function arrow are
86 -- (a) types (of kind openTypeKind or its sub-kinds)
87 -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
89 | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
94 predKind :: PredType -> Kind
95 predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted
96 predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
97 predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
100 %************************************************************************
104 %************************************************************************
107 -- | Essentially 'funResultTy' on kinds
108 kindFunResult :: Kind -> Kind
109 kindFunResult (FunTy _ res) = res
110 kindFunResult k = pprPanic "kindFunResult" (ppr k)
112 kindAppResult :: Kind -> [arg] -> Kind
113 kindAppResult k [] = k
114 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
116 -- | Essentially 'splitFunTys' on kinds
117 splitKindFunTys :: Kind -> ([Kind],Kind)
118 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
120 splitKindFunTys k = ([], k)
122 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
123 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
124 splitKindFunTy_maybe _ = Nothing
126 -- | Essentially 'splitFunTysN' on kinds
127 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
128 splitKindFunTysN 0 k = ([], k)
129 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
131 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
133 -- | Find the result 'Kind' of a type synonym,
134 -- after applying it to its 'arity' number of type variables
135 -- Actually this function works fine on data types too,
136 -- but they'd always return '*', so we never need to ask
137 synTyConResKind :: TyCon -> Kind
138 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
140 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
141 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
142 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
143 isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
145 isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
147 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
148 isOpenTypeKind _ = False
150 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
152 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
153 isUbxTupleKind _ = False
155 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
157 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
158 isArgTypeKind _ = False
160 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
162 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
163 isUnliftedTypeKind _ = False
165 isSubOpenTypeKind :: Kind -> Bool
166 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
167 isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
168 ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
170 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
171 isSubOpenTypeKind other = ASSERT( isKind other ) False
172 -- This is a conservative answer
173 -- It matters in the call to isSubKind in
174 -- checkExpectedKind.
176 isSubArgTypeKindCon kc
177 | isUnliftedTypeKindCon kc = True
178 | isLiftedTypeKindCon kc = True
179 | isArgTypeKindCon kc = True
182 isSubArgTypeKind :: Kind -> Bool
183 -- ^ True of any sub-kind of ArgTypeKind
184 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
185 isSubArgTypeKind _ = False
187 -- | Is this a super-kind (i.e. a type-of-kinds)?
188 isSuperKind :: Type -> Bool
189 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
190 isSuperKind _ = False
192 -- | Is this a kind (i.e. a type-of-types)?
193 isKind :: Kind -> Bool
194 isKind k = isSuperKind (typeKind k)
196 isSubKind :: Kind -> Kind -> Bool
197 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
198 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
199 isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
200 isSubKind _ _ = False
202 isSubKindCon :: TyCon -> TyCon -> Bool
203 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
205 | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
206 | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
207 | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
208 | isOpenTypeKindCon kc2 = True
209 -- we already know kc1 is not a fun, its a TyCon
210 | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
213 defaultKind :: Kind -> Kind
214 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
215 -- information on what that means
217 -- When we generalise, we make generic type variables whose kind is
218 -- simple (* or *->* etc). So generic type variables (other than
219 -- built-in constants like 'error') always have simple kinds. This is important;
222 -- We want f to get type
223 -- f :: forall (a::*). a -> Bool
225 -- f :: forall (a::??). a -> Bool
226 -- because that would allow a call like (f 3#) as well as (f True),
227 --and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
229 | isSubOpenTypeKind k = liftedTypeKind
230 | isSubArgTypeKind k = liftedTypeKind