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