Merge branch 'master' into type-nats
[ghc.git] / compiler / types / Kind.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module Kind (
7         -- * Main data type
8         Kind, typeKind,
9
10         -- Kinds
11         liftedTypeKind, unliftedTypeKind, openTypeKind,
12         argTypeKind, ubxTupleKind,
13         mkArrowKind, mkArrowKinds,
14
15         -- Kind constructors...
16         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
17         argTypeKindTyCon, ubxTupleKindTyCon,
18
19         -- Super Kinds
20         tySuperKind, tySuperKindTyCon, 
21         
22         pprKind, pprParendKind,
23
24         -- ** Deconstructing Kinds
25         kindFunResult, kindAppResult, synTyConResKind,
26         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
27
28         -- ** Predicates on Kinds
29         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
30         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
31         isSuperKind, isCoercionKind, 
32         isLiftedTypeKindCon,
33         isNatKind, isNatKindCon,
34
35         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
36         isSubKindCon,
37
38        ) where
39
40 #include "HsVersions.h"
41
42 import TypeRep
43 import TysPrim
44 import TyCon
45 import Var
46 import PrelNames
47 import Outputable
48 \end{code}
49
50 %************************************************************************
51 %*                                                                      *
52         Predicates over Kinds
53 %*                                                                      *
54 %************************************************************************
55
56 \begin{code}
57 isTySuperKind :: SuperKind -> Bool
58 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
59 isTySuperKind _                = False
60
61 -------------------
62 -- Lastly we need a few functions on Kinds
63
64 isLiftedTypeKindCon :: TyCon -> Bool
65 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
66
67 isNatKindCon :: TyCon -> Bool
68 isNatKindCon tc           =  tc `hasKey` natKindTyConKey
69 \end{code}
70
71 %************************************************************************
72 %*                                                                      *
73         The kind of a type
74 %*                                                                      *
75 %************************************************************************
76
77 \begin{code}
78 typeKind :: Type -> Kind
79 typeKind _ty@(TyConApp tc tys) 
80   = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty )
81              -- Assertion checks for unsaturated application of (~)
82              -- See Note [The (~) TyCon] in TysPrim
83     kindAppResult (tyConKind tc) tys
84
85 typeKind (PredTy pred)        = predKind pred
86 typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
87 typeKind (ForAllTy _ ty)      = typeKind ty
88 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
89 typeKind (FunTy _arg res)
90     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
91     --              not unliftedTypKind (#)
92     -- The only things that can be after a function arrow are
93     --   (a) types (of kind openTypeKind or its sub-kinds)
94     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
95     | isTySuperKind k         = k
96     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
97     where
98       k = typeKind res
99 typeKind (LiteralTy x)        = tyLitKind x
100
101 ------------------
102 predKind :: PredType -> Kind
103 predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted
104 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
105 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
106
107 -----------------
108 tyLitKind :: TyLit -> Kind
109 tyLitKind (NumberTyLit _) = natKind
110 \end{code}
111
112 %************************************************************************
113 %*                                                                      *
114         Functions over Kinds            
115 %*                                                                      *
116 %************************************************************************
117
118 \begin{code}
119 -- | Essentially 'funResultTy' on kinds
120 kindFunResult :: Kind -> Kind
121 kindFunResult (FunTy _ res) = res
122 kindFunResult k = pprPanic "kindFunResult" (ppr k)
123
124 kindAppResult :: Kind -> [arg] -> Kind
125 kindAppResult k []     = k
126 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
127
128 -- | Essentially 'splitFunTys' on kinds
129 splitKindFunTys :: Kind -> ([Kind],Kind)
130 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
131                               (as, k) -> (a:as, k)
132 splitKindFunTys k = ([], k)
133
134 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
135 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
136 splitKindFunTy_maybe _           = Nothing
137
138 -- | Essentially 'splitFunTysN' on kinds
139 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
140 splitKindFunTysN 0 k           = ([], k)
141 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
142                                    (as, k) -> (a:as, k)
143 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
144
145 -- | Find the result 'Kind' of a type synonym, 
146 -- after applying it to its 'arity' number of type variables
147 -- Actually this function works fine on data types too, 
148 -- but they'd always return '*', so we never need to ask
149 synTyConResKind :: TyCon -> Kind
150 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
151
152 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
153 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
154 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
155         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
156
157 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
158
159 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
160 isOpenTypeKind _               = False
161
162 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
163
164 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
165 isUbxTupleKind _               = False
166
167 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
168
169 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
170 isArgTypeKind _               = False
171
172 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
173
174 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
175 isUnliftedTypeKind _               = False
176
177 isNatKind :: Kind -> Bool
178 isNatKind (TyConApp tc [])        = isNatKindCon tc
179 isNatKind _                       = False
180
181 isSubOpenTypeKind :: Kind -> Bool
182 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow and Nat)
183 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
184                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
185                                      False
186 isSubOpenTypeKind k | isNatKind k  = False
187 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
188 isSubOpenTypeKind other            = ASSERT( isKind other ) False
189          -- This is a conservative answer
190          -- It matters in the call to isSubKind in
191          -- checkExpectedKind.
192
193 isSubArgTypeKindCon kc
194   | isUnliftedTypeKindCon kc = True
195   | isLiftedTypeKindCon kc   = True
196   | isArgTypeKindCon kc      = True
197   | otherwise                = False
198
199 isSubArgTypeKind :: Kind -> Bool
200 -- ^ True of any sub-kind of ArgTypeKind 
201 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
202 isSubArgTypeKind _                = False
203
204 -- | Is this a super-kind (i.e. a type-of-kinds)?
205 isSuperKind :: Type -> Bool
206 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
207 isSuperKind _                   = False
208
209 -- | Is this a kind (i.e. a type-of-types)?
210 isKind :: Kind -> Bool
211 isKind k = isSuperKind (typeKind k)
212
213 isSubKind :: Kind -> Kind -> Bool
214 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
215 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
216 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
217 isSubKind _             _                     = False
218
219 isSubKindCon :: TyCon -> TyCon -> Bool
220 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
221 isSubKindCon kc1 kc2
222   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
223   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
224   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
225   | isNatKindCon kc1                                       = isNatKindCon kc2
226   | isOpenTypeKindCon kc2                                  = True 
227                            -- we already know kc1 is not a fun, its a TyCon
228   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
229   | otherwise                                              = False
230
231 defaultKind :: Kind -> Kind
232 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
233 -- information on what that means
234
235 -- When we generalise, we make generic type variables whose kind is
236 -- simple (* or *->* etc).  So generic type variables (other than
237 -- built-in constants like 'error') always have simple kinds.  This is important;
238 -- consider
239 --      f x = True
240 -- We want f to get type
241 --      f :: forall (a::*). a -> Bool
242 -- Not 
243 --      f :: forall (a::??). a -> Bool
244 -- because that would allow a call like (f 3#) as well as (f True),
245 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
246 defaultKind k 
247   | isSubOpenTypeKind k = liftedTypeKind
248   | isSubArgTypeKind k  = liftedTypeKind
249   | otherwise        = k
250 \end{code}