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