Now I understand why Constraint is a sub-kind of ArgKind!
[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         SuperKind, 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         superKind, superKindTyCon, 
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, isKindVar,
40         isSuperKind, isSuperKindTyCon,
41         isLiftedTypeKindCon, isConstraintKindCon,
42         isAnyKind, isAnyKindCon,
43         okArrowArgKind, okArrowResultKind,
44
45         isSubArgTypeKind, isSubOpenTypeKind, 
46         isSubKind, isSubKindCon, 
47         tcIsSubKind, tcIsSubKindCon,
48         defaultKind,
49
50         -- ** Functions on variables
51         kiVarsOfKind, kiVarsOfKinds
52
53        ) where
54
55 #include "HsVersions.h"
56
57 import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
58
59 import TypeRep
60 import TysPrim
61 import TyCon
62 import VarSet
63 import PrelNames
64 import Outputable
65 \end{code}
66
67 %************************************************************************
68 %*                                                                      *
69         Functions over Kinds            
70 %*                                                                      *
71 %************************************************************************
72
73 \begin{code}
74 -- | Essentially 'funResultTy' on kinds handling pi-types too
75 kindFunResult :: Kind -> KindOrType -> Kind
76 kindFunResult (FunTy _ res) _ = res
77 kindFunResult (ForAllTy kv res) arg = substKiWith [kv] [arg] res
78 kindFunResult k _ = pprPanic "kindFunResult" (ppr k)
79
80 kindAppResult :: Kind -> [Type] -> Kind
81 kindAppResult k []     = k
82 kindAppResult k (a:as) = kindAppResult (kindFunResult k a) as
83
84 -- | Essentially 'splitFunTys' on kinds
85 splitKindFunTys :: Kind -> ([Kind],Kind)
86 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
87                               (as, k) -> (a:as, k)
88 splitKindFunTys k = ([], k)
89
90 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
91 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
92 splitKindFunTy_maybe _           = Nothing
93
94 -- | Essentially 'splitFunTysN' on kinds
95 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
96 splitKindFunTysN 0 k           = ([], k)
97 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
98                                    (as, k) -> (a:as, k)
99 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
100
101 -- | Find the result 'Kind' of a type synonym, 
102 -- after applying it to its 'arity' number of type variables
103 -- Actually this function works fine on data types too, 
104 -- but they'd always return '*', so we never need to ask
105 synTyConResKind :: TyCon -> Kind
106 synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
107
108 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
109 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
110   isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
111
112 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
113   isUnliftedTypeKindCon, isSubArgTypeKindCon, 
114   isSubOpenTypeKindCon, isConstraintKindCon,
115   isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool
116
117
118 isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
119 isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
120 isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
121 isUbxTupleKindCon     tc = tyConUnique tc == ubxTupleKindTyConKey
122 isArgTypeKindCon      tc = tyConUnique tc == argTypeKindTyConKey
123 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
124 isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
125
126 isAnyKind (TyConApp tc _) = isAnyKindCon tc
127 isAnyKind _               = False
128
129 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
130 isOpenTypeKind _               = False
131
132 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
133 isUbxTupleKind _               = False
134
135 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
136 isArgTypeKind _               = False
137
138 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
139 isUnliftedTypeKind _               = False
140
141 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
142 isConstraintKind _               = False
143
144 isConstraintOrLiftedKind (TyConApp tc _)
145   = isConstraintKindCon tc || isLiftedTypeKindCon tc
146 isConstraintOrLiftedKind _ = False
147
148 --------------------------------------------
149 --            Kinding for arrow (->)
150 -- Says when a kind is acceptable on lhs or rhs of an arrow
151 --     arg -> res
152
153 okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
154 okArrowArgKindCon kc
155   | isLiftedTypeKindCon   kc = True
156   | isUnliftedTypeKindCon kc = True
157   | isConstraintKindCon   kc = True
158   | otherwise                = False
159
160 okArrowResultKindCon kc
161   | okArrowArgKindCon kc = True
162   | isUbxTupleKindCon kc = True
163   | otherwise            = False
164
165 okArrowArgKind, okArrowResultKind :: Kind -> Bool
166 okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
167 okArrowArgKind    _                = False
168
169 okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
170 okArrowResultKind _                = False
171
172 -----------------------------------------
173 --              Subkinding
174 -- The tc variants are used during type-checking, where we don't want the
175 -- Constraint kind to be a subkind of anything
176 -- After type-checking (in core), Constraint is a subkind of argTypeKind
177 isSubOpenTypeKind :: Kind -> Bool
178 -- ^ True of any sub-kind of OpenTypeKind
179 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
180 isSubOpenTypeKind _                = False
181
182 isSubOpenTypeKindCon kc
183   =  isSubArgTypeKindCon kc
184   || isUbxTupleKindCon   kc
185   || isOpenTypeKindCon   kc
186
187 isSubArgTypeKindCon kc
188   =  isUnliftedTypeKindCon kc
189   || isLiftedTypeKindCon   kc  
190   || isArgTypeKindCon      kc     
191   || isConstraintKindCon kc   -- Needed for error (Num a) "blah"
192                               -- and so that (Ord a -> Eq a) is well-kinded
193                               -- and so that (# Eq a, Ord b #) is well-kinded
194
195 isSubArgTypeKind :: Kind -> Bool
196 -- ^ True of any sub-kind of ArgTypeKind 
197 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
198 isSubArgTypeKind _                = False
199
200 -- | Is this a kind (i.e. a type-of-types)?
201 isKind :: Kind -> Bool
202 isKind k = isSuperKind (typeKind k)
203
204 isSubKind :: Kind -> Kind -> Bool
205 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
206
207 isSuperKindTyCon :: TyCon -> Bool
208 isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
209
210 isSubKind (FunTy a1 r1) (FunTy a2 r2)
211   = (isSubKind a2 a1) && (isSubKind r1 r2)
212
213 isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
214   | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
215     -- handles promoted kinds (List *, Nat, etc.)
216   = eqKind k1 k2
217
218   | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
219     -- handles BOX
220   = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
221              && null k1s && null k2s, 
222              ppr kc1 <+> ppr kc2 )
223     True   -- If one is BOX, the other must be too
224
225   | otherwise = -- handles usual kinds (*, #, (#), etc.)
226                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
227                 kc1 `isSubKindCon` kc2
228
229 isSubKind k1 k2 = eqKind k1 k2
230
231 isSubKindCon :: TyCon -> TyCon -> Bool
232 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
233 isSubKindCon kc1 kc2
234   | kc1 == kc2            = True
235   | isArgTypeKindCon  kc2 = isSubArgTypeKindCon  kc1
236   | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 
237   | otherwise             = False
238
239 -------------------------
240 -- Hack alert: we need a tiny variant for the typechecker
241 -- Reason:     f :: Int -> (a~b)
242 --             g :: forall (c::Constraint). Int -> c
243 -- We want to reject these, even though Constraint is
244 -- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
245 -- *after* the typechecker
246 --   a) So that (Ord a -> Eq a) is a legal type
247 --   b) So that the simplifer can generate (error (Eq a) "urk")
248 --
249 -- Easiest way to reject is simply to make Constraint not
250 -- below OpenTypeKind when type checking
251
252 tcIsSubKind :: Kind -> Kind -> Bool
253 tcIsSubKind k1 k2
254   | isConstraintKind k1 = isConstraintKind k2
255   | otherwise           = isSubKind k1 k2
256
257 tcIsSubKindCon :: TyCon -> TyCon -> Bool
258 tcIsSubKindCon kc1 kc2
259   | isConstraintKindCon kc1 = isConstraintKindCon kc2
260   | otherwise               = isSubKindCon kc1 kc2
261
262 -------------------------
263 defaultKind :: Kind -> Kind
264 -- ^ Used when generalising: default OpenKind and ArgKind to *.
265 -- See "Type#kind_subtyping" for more information on what that means
266
267 -- When we generalise, we make generic type variables whose kind is
268 -- simple (* or *->* etc).  So generic type variables (other than
269 -- built-in constants like 'error') always have simple kinds.  This is important;
270 -- consider
271 --      f x = True
272 -- We want f to get type
273 --      f :: forall (a::*). a -> Bool
274 -- Not 
275 --      f :: forall (a::ArgKind). a -> Bool
276 -- because that would allow a call like (f 3#) as well as (f True),
277 -- and the calling conventions differ.
278 -- This defaulting is done in TcMType.zonkTcTyVarBndr.
279 defaultKind k
280   | isSubOpenTypeKind k = liftedTypeKind
281   | otherwise           = k
282
283 -- Returns the free kind variables in a kind
284 kiVarsOfKind :: Kind -> VarSet
285 kiVarsOfKind = tyVarsOfType
286
287 kiVarsOfKinds :: [Kind] -> VarSet
288 kiVarsOfKinds = tyVarsOfTypes
289 \end{code}