merge
[ghc.git] / compiler / types / Kind.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 {-# OPTIONS -fno-warn-tabs #-}
7 -- The above warning supression flag is a temporary kludge.
8 -- While working on this module you are encouraged to remove it and
9 -- detab the module (please do the detabbing in a separate patch). See
10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
11 -- for details
12
13 module Kind (
14         -- * Main data type
15         Kind, typeKind,
16
17         -- Kinds
18         anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
19         argTypeKind, ubxTupleKind, constraintKind,
20         mkArrowKind, mkArrowKinds,
21
22         -- Kind constructors...
23         anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
24         unliftedTypeKindTyCon, argTypeKindTyCon, ubxTupleKindTyCon,
25         constraintKindTyCon,
26
27         -- Super Kinds
28         tySuperKind, tySuperKindTyCon, 
29         
30         pprKind, pprParendKind,
31
32         -- ** Deconstructing Kinds
33         kindFunResult, kindAppResult, synTyConResKind,
34         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
35
36         -- ** Predicates on Kinds
37         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
38         isUbxTupleKind, isArgTypeKind, isConstraintKind, isKind,
39         isSuperKind, noHashInKind,
40         isLiftedTypeKindCon, isConstraintKindCon,
41         isAnyKind, isAnyKindCon,
42
43         isSubArgTypeKind, tcIsSubArgTypeKind, 
44         isSubOpenTypeKind, tcIsSubOpenTypeKind,
45         isSubKind, tcIsSubKind, defaultKind,
46         isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon,
47
48         -- ** Functions on variables
49         isKiVar, splitKiTyVars, partitionKiTyVars,
50         kiVarsOfKind, kiVarsOfKinds,
51
52         -- ** Promotion related functions
53         promoteType, isPromotableType, isPromotableKind,
54
55        ) where
56
57 #include "HsVersions.h"
58
59 import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
60
61 import TypeRep
62 import TysPrim
63 import TyCon
64 import Var
65 import VarSet
66 import PrelNames
67 import Outputable
68
69 import Data.List ( partition )
70 \end{code}
71
72 %************************************************************************
73 %*                                                                      *
74         Predicates over Kinds
75 %*                                                                      *
76 %************************************************************************
77
78 \begin{code}
79 -------------------
80 -- Lastly we need a few functions on Kinds
81
82 isLiftedTypeKindCon :: TyCon -> Bool
83 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
84
85 -- This checks that its argument does not contain # or (#).
86 -- It is used in tcTyVarBndrs.
87 noHashInKind :: Kind -> Bool
88 noHashInKind (TyVarTy {}) = True
89 noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2
90 noHashInKind (ForAllTy _ ki) = noHashInKind ki
91 noHashInKind (TyConApp kc kis)
92   =  not (kc `hasKey` unliftedTypeKindTyConKey)
93   && not (kc `hasKey` ubxTupleKindTyConKey)
94   && all noHashInKind kis
95 noHashInKind _ = panic "noHashInKind"
96 \end{code}
97
98 %************************************************************************
99 %*                                                                      *
100         Functions over Kinds            
101 %*                                                                      *
102 %************************************************************************
103
104 \begin{code}
105 -- | Essentially 'funResultTy' on kinds handling pi-types too
106 kindFunResult :: Kind -> KindOrType -> Kind
107 kindFunResult (FunTy _ res) _ = res
108 kindFunResult (ForAllTy kv res) arg = substKiWith [kv] [arg] res
109 kindFunResult k _ = pprPanic "kindFunResult" (ppr k)
110
111 kindAppResult :: Kind -> [Type] -> Kind
112 kindAppResult k []     = k
113 kindAppResult k (a:as) = kindAppResult (kindFunResult k a) as
114
115 -- | Essentially 'splitFunTys' on kinds
116 splitKindFunTys :: Kind -> ([Kind],Kind)
117 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
118                               (as, k) -> (a:as, k)
119 splitKindFunTys k = ([], k)
120
121 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
122 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
123 splitKindFunTy_maybe _           = Nothing
124
125 -- | Essentially 'splitFunTysN' on kinds
126 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
127 splitKindFunTysN 0 k           = ([], k)
128 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
129                                    (as, k) -> (a:as, k)
130 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
131
132 -- | Find the result 'Kind' of a type synonym, 
133 -- after applying it to its 'arity' number of type variables
134 -- Actually this function works fine on data types too, 
135 -- but they'd always return '*', so we never need to ask
136 synTyConResKind :: TyCon -> Kind
137 synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
138
139 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
140 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
141   isConstraintKind, isAnyKind :: Kind -> Bool
142
143 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
144   isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon,
145   isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon,
146   isAnyKindCon :: TyCon -> Bool
147
148 isAnyKindCon tc     = tyConUnique tc == anyKindTyConKey
149
150 isAnyKind (TyConApp tc _) = isAnyKindCon tc
151 isAnyKind _               = False
152
153 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
154
155 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
156 isOpenTypeKind _               = False
157
158 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
159
160 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
161 isUbxTupleKind _               = False
162
163 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
164
165 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
166 isArgTypeKind _               = False
167
168 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
169
170 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
171 isUnliftedTypeKind _               = False
172
173 isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
174
175 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
176 isConstraintKind _               = False
177
178
179 -- Subkinding
180 -- The tc variants are used during type-checking, where we don't want the
181 -- Constraint kind to be a subkind of anything
182 -- After type-checking (in core), Constraint is a subkind of argTypeKind
183 isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool
184 -- ^ True of any sub-kind of OpenTypeKind
185 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
186 isSubOpenTypeKind _                = False
187
188 -- ^ True of any sub-kind of OpenTypeKind
189 tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc
190 tcIsSubOpenTypeKind _                = False
191
192 isSubOpenTypeKindCon kc
193   | isSubArgTypeKindCon kc   = True
194   | isUbxTupleKindCon kc     = True
195   | isOpenTypeKindCon kc     = True
196   | otherwise                = False
197
198 tcIsSubOpenTypeKindCon kc
199   | tcIsSubArgTypeKindCon kc = True
200   | isUbxTupleKindCon kc     = True
201   | isOpenTypeKindCon kc     = True
202   | otherwise                = False
203
204 isSubArgTypeKindCon kc
205   | isUnliftedTypeKindCon kc = True
206   | isLiftedTypeKindCon kc   = True
207   | isArgTypeKindCon kc      = True
208   | isConstraintKindCon kc   = True
209   | otherwise                = False
210
211 tcIsSubArgTypeKindCon kc
212   | isConstraintKindCon kc   = False
213   | otherwise                = isSubArgTypeKindCon kc
214
215 isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool
216 -- ^ True of any sub-kind of ArgTypeKind 
217 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
218 isSubArgTypeKind _                = False
219
220 tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc
221 tcIsSubArgTypeKind _                = False
222
223 -- | Is this a super-kind (i.e. a type-of-kinds)?
224 isSuperKind :: Type -> Bool
225 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
226 isSuperKind _                   = False
227
228 -- | Is this a kind (i.e. a type-of-types)?
229 isKind :: Kind -> Bool
230 isKind k = isSuperKind (typeKind k)
231
232 isSubKind, tcIsSubKind :: Kind -> Kind -> Bool
233 isSubKind   = isSubKind' False
234 tcIsSubKind = isSubKind' True
235
236 -- The first argument denotes whether we are in the type-checking phase or not
237 isSubKind' :: Bool -> Kind -> Kind -> Bool
238 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
239
240 isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2)
241   = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2)
242
243 isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
244   | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
245     -- handles promoted kinds (List *, Nat, etc.)
246     = eqKind k1 k2
247
248   | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
249     -- handles BOX
250     = ASSERT2( isSuperKindTyCon kc2 && null k1s && null k2s, ppr kc1 <+> ppr kc2 )
251       True
252
253   | otherwise = -- handles usual kinds (*, #, (#), etc.)
254                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
255                 if duringTc then kc1 `tcIsSubKindCon` kc2
256                 else kc1 `isSubKindCon` kc2
257
258 isSubKind' _duringTc k1 k2 = eqKind k1 k2
259
260 isSubKindCon :: TyCon -> TyCon -> Bool
261 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
262 isSubKindCon kc1 kc2
263   | kc1 == kc2                                             = True
264   | isSubArgTypeKindCon  kc1  && isArgTypeKindCon  kc2     = True
265   | isSubOpenTypeKindCon kc1  && isOpenTypeKindCon kc2     = True
266   | otherwise                                              = False
267
268 tcIsSubKindCon :: TyCon -> TyCon -> Bool
269 tcIsSubKindCon kc1 kc2
270   | kc1 == kc2                                         = True
271   | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False
272   | otherwise                                          = isSubKindCon kc1 kc2
273
274 defaultKind :: Kind -> Kind
275 -- ^ Used when generalising: default OpenKind and ArgKind to *.
276 -- See "Type#kind_subtyping" for more information on what that means
277
278 -- When we generalise, we make generic type variables whose kind is
279 -- simple (* or *->* etc).  So generic type variables (other than
280 -- built-in constants like 'error') always have simple kinds.  This is important;
281 -- consider
282 --      f x = True
283 -- We want f to get type
284 --      f :: forall (a::*). a -> Bool
285 -- Not 
286 --      f :: forall (a::ArgKind). a -> Bool
287 -- because that would allow a call like (f 3#) as well as (f True),
288 -- and the calling conventions differ.
289 -- This defaulting is done in TcMType.zonkTcTyVarBndr.
290 defaultKind k
291   | isSubOpenTypeKind k = liftedTypeKind
292   | otherwise           = k
293
294 splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
295 -- Precondition: kind variables should precede type variables
296 -- Postcondition: appending the two result lists gives the input!
297 splitKiTyVars = span (isSuperKind . tyVarKind)
298
299 partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
300 partitionKiTyVars = partition (isSuperKind . tyVarKind)
301
302 -- Checks if this "type or kind" variable is a kind variable
303 isKiVar :: TyVar -> Bool
304 isKiVar v = isSuperKind (varType v)
305
306 -- Returns the free kind variables in a kind
307 kiVarsOfKind :: Kind -> VarSet
308 kiVarsOfKind = tyVarsOfType
309
310 kiVarsOfKinds :: [Kind] -> VarSet
311 kiVarsOfKinds = tyVarsOfTypes
312
313 -- Datatype promotion
314 isPromotableType :: Type -> Bool
315 isPromotableType = go emptyVarSet
316   where
317     go vars (TyConApp tc tys) = ASSERT( not (isPromotedDataTyCon tc) ) all (go vars) tys
318     go vars (FunTy arg res) = all (go vars) [arg,res]
319     go vars (TyVarTy tvar) = tvar `elemVarSet` vars
320     go vars (ForAllTy tvar ty) = isPromotableTyVar tvar && go (vars `extendVarSet` tvar) ty
321     go _ _ = panic "isPromotableType"  -- argument was not kind-shaped
322
323 isPromotableTyVar :: TyVar -> Bool
324 isPromotableTyVar = isLiftedTypeKind . varType
325
326 -- | Promotes a type to a kind. Assumes the argument is promotable.
327 promoteType :: Type -> Kind
328 promoteType (TyConApp tc tys) = mkTyConApp (mkPromotedTypeTyCon tc) 
329                                            (map promoteType tys)
330   -- T t1 .. tn  ~~>  'T k1 .. kn  where  ti ~~> ki
331 promoteType (FunTy arg res) = mkArrowKind (promoteType arg) (promoteType res)
332   -- t1 -> t2  ~~>  k1 -> k2  where  ti ~~> ki
333 promoteType (TyVarTy tvar) = mkTyVarTy (promoteTyVar tvar)
334   -- a :: *  ~~>  a :: BOX
335 promoteType (ForAllTy tvar ty) = ForAllTy (promoteTyVar tvar) (promoteType ty)
336   -- forall (a :: *). t  ~~> forall (a :: BOX). k  where  t ~~> k
337 promoteType _ = panic "promoteType"  -- argument was not kind-shaped
338
339 promoteTyVar :: TyVar -> KindVar
340 promoteTyVar tvar = mkKindVar (tyVarName tvar) tySuperKind
341
342 -- If kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
343 isPromotableKind :: Kind -> Maybe Int
344 isPromotableKind kind =
345   let (args, res) = splitKindFunTys kind in
346   if all isLiftedTypeKind (res:args)
347   then Just $ length args
348   else Nothing
349
350 {- Note [Promoting a Type to a Kind]
351    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
352 We only promote the followings.
353 - Type variables: a
354 - Fully applied arrow types: tau -> sigma
355 - Fully applied type constructors of kind:
356      n >= 0
357   /-----------\
358   * -> ... -> * -> *
359 - Polymorphic types over type variables of kind star:
360   forall (a::*). tau
361 -}
362 \end{code}