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