Merge branch 'master' of http://darcs.haskell.org/ghc
[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, constraintKind,
19         mkArrowKind, mkArrowKinds,
20         typeNatKind, typeStringKind,
21
22         -- Kind constructors...
23         anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
24         unliftedTypeKindTyCon, constraintKindTyCon,
25
26         -- Super Kinds
27         superKind, superKindTyCon, 
28         
29         pprKind, pprParendKind,
30
31         -- ** Deconstructing Kinds
32         kindAppResult, synTyConResKind,
33         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
34
35         -- ** Predicates on Kinds
36         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
37         isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
38         isKind, isKindVar,
39         isSuperKind, isSuperKindTyCon,
40         isLiftedTypeKindCon, isConstraintKindCon,
41         isAnyKind, isAnyKindCon,
42         okArrowArgKind, okArrowResultKind,
43
44         isSubOpenTypeKind, 
45         isSubKind, isSubKindCon, 
46         tcIsSubKind, tcIsSubKindCon,
47         defaultKind,
48
49         -- ** Functions on variables
50         kiVarsOfKind, kiVarsOfKinds
51
52        ) where
53
54 #include "HsVersions.h"
55
56 import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
57
58 import TypeRep
59 import TysPrim
60 import TyCon
61 import VarSet
62 import PrelNames
63 import Outputable
64 import Util
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 isOpenTypeKind, isUnliftedTypeKind,
110   isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
111
112 isOpenTypeKindCon, isUnliftedTypeKindCon,
113   isSubOpenTypeKindCon, isConstraintKindCon,
114   isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool
115
116
117 isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
118 isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
119 isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
120 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
121 isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
122
123 isAnyKind (TyConApp tc _) = isAnyKindCon tc
124 isAnyKind _               = False
125
126 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
127 isOpenTypeKind _               = False
128
129 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
130 isUnliftedTypeKind _               = False
131
132 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
133 isConstraintKind _               = False
134
135 isConstraintOrLiftedKind (TyConApp tc _)
136   = isConstraintKindCon tc || isLiftedTypeKindCon tc
137 isConstraintOrLiftedKind _ = False
138
139 returnsConstraintKind :: Kind -> Bool
140 returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
141 returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
142 returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
143 returnsConstraintKind _               = False
144
145 --------------------------------------------
146 --            Kinding for arrow (->)
147 -- Says when a kind is acceptable on lhs or rhs of an arrow
148 --     arg -> res
149
150 okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
151 okArrowArgKindCon kc
152   | isLiftedTypeKindCon   kc = True
153   | isUnliftedTypeKindCon kc = True
154   | isConstraintKindCon   kc = True
155   | otherwise                = False
156
157 okArrowResultKindCon = okArrowArgKindCon
158
159 okArrowArgKind, okArrowResultKind :: Kind -> Bool
160 okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
161 okArrowArgKind    _                = False
162
163 okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
164 okArrowResultKind _                = False
165
166 -----------------------------------------
167 --              Subkinding
168 -- The tc variants are used during type-checking, where we don't want the
169 -- Constraint kind to be a subkind of anything
170 -- After type-checking (in core), Constraint is a subkind of argTypeKind
171 isSubOpenTypeKind :: Kind -> Bool
172 -- ^ True of any sub-kind of OpenTypeKind
173 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
174 isSubOpenTypeKind _                = False
175
176 isSubOpenTypeKindCon kc
177   =  isOpenTypeKindCon   kc
178   || isUnliftedTypeKindCon kc
179   || isLiftedTypeKindCon   kc  
180   || isConstraintKindCon kc   -- Needed for error (Num a) "blah"
181                               -- and so that (Ord a -> Eq a) is well-kinded
182                               -- and so that (# Eq a, Ord b #) is well-kinded
183
184 -- | Is this a kind (i.e. a type-of-types)?
185 isKind :: Kind -> Bool
186 isKind k = isSuperKind (typeKind k)
187
188 isSubKind :: Kind -> Kind -> Bool
189 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
190
191 isSuperKindTyCon :: TyCon -> Bool
192 isSuperKindTyCon tc = tc `hasKey` superKindTyConKey
193
194 isSubKind (FunTy a1 r1) (FunTy a2 r2)
195   = (isSubKind a2 a1) && (isSubKind r1 r2)
196
197 isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
198   | isPromotedTyCon kc1 || isPromotedTyCon kc2
199     -- handles promoted kinds (List *, Nat, etc.)
200   = eqKind k1 k2
201
202   | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
203     -- handles BOX
204   = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 
205              && null k1s && null k2s, 
206              ppr kc1 <+> ppr kc2 )
207     True   -- If one is BOX, the other must be too
208
209   | otherwise = -- handles usual kinds (*, #, (#), etc.)
210                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
211                 kc1 `isSubKindCon` kc2
212
213 isSubKind k1 k2 = eqKind k1 k2
214
215 isSubKindCon :: TyCon -> TyCon -> Bool
216 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
217 isSubKindCon kc1 kc2
218   | kc1 == kc2            = True
219   | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 
220   | otherwise             = False
221
222 -------------------------
223 -- Hack alert: we need a tiny variant for the typechecker
224 -- Reason:     f :: Int -> (a~b)
225 --             g :: forall (c::Constraint). Int -> c
226 -- We want to reject these, even though Constraint is
227 -- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
228 -- *after* the typechecker
229 --   a) So that (Ord a -> Eq a) is a legal type
230 --   b) So that the simplifer can generate (error (Eq a) "urk")
231 --
232 -- Easiest way to reject is simply to make Constraint not
233 -- below OpenTypeKind when type checking
234
235 tcIsSubKind :: Kind -> Kind -> Bool
236 tcIsSubKind k1 k2
237   | isConstraintKind k1 = isConstraintKind k2
238   | otherwise           = isSubKind k1 k2
239
240 tcIsSubKindCon :: TyCon -> TyCon -> Bool
241 tcIsSubKindCon kc1 kc2
242   | isConstraintKindCon kc1 = isConstraintKindCon kc2
243   | otherwise               = isSubKindCon kc1 kc2
244
245 -------------------------
246 defaultKind :: Kind -> Kind
247 -- ^ Used when generalising: default OpenKind and ArgKind to *.
248 -- See "Type#kind_subtyping" for more information on what that means
249
250 -- When we generalise, we make generic type variables whose kind is
251 -- simple (* or *->* etc).  So generic type variables (other than
252 -- built-in constants like 'error') always have simple kinds.  This is important;
253 -- consider
254 --      f x = True
255 -- We want f to get type
256 --      f :: forall (a::*). a -> Bool
257 -- Not 
258 --      f :: forall (a::ArgKind). a -> Bool
259 -- because that would allow a call like (f 3#) as well as (f True),
260 -- and the calling conventions differ.
261 -- This defaulting is done in TcMType.zonkTcTyVarBndr.
262 --
263 -- The test is really whether the kind is strictly above '*'
264 defaultKind (TyConApp kc _args)
265   | isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
266 defaultKind k = k
267
268 -- Returns the free kind variables in a kind
269 kiVarsOfKind :: Kind -> VarSet
270 kiVarsOfKind = tyVarsOfType
271
272 kiVarsOfKinds :: [Kind] -> VarSet
273 kiVarsOfKinds = tyVarsOfTypes
274 \end{code}