Look through type synonyms when deciding if something is a type literal.
[ghc.git] / compiler / types / Kind.lhs
1 %
2 % (c) The University of Glasgow 2006-2012
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
21         -- Kind constructors...
22         anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
23         unliftedTypeKindTyCon, constraintKindTyCon,
24
25         -- Super Kinds
26         superKind, superKindTyCon, 
27         
28         pprKind, pprParendKind,
29
30         -- ** Deconstructing Kinds
31         kindAppResult, synTyConResKind,
32         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
33
34         -- ** Predicates on Kinds
35         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
36         isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
37         isKind, isKindVar,
38         isSuperKind, isSuperKindTyCon,
39         isLiftedTypeKindCon, isConstraintKindCon,
40         isAnyKind, isAnyKindCon,
41         okArrowArgKind, okArrowResultKind,
42
43         isSubOpenTypeKind, 
44         isSubKind, isSubKindCon, 
45         tcIsSubKind, tcIsSubKindCon,
46         defaultKind,
47
48         -- ** Functions on variables
49         kiVarsOfKind, kiVarsOfKinds
50
51        ) where
52
53 #include "HsVersions.h"
54
55 import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
56
57 import TypeRep
58 import TysPrim
59 import TyCon
60 import VarSet
61 import PrelNames
62 import Outputable
63 import Util
64 \end{code}
65
66 %************************************************************************
67 %*                                                                      *
68         Functions over Kinds            
69 %*                                                                      *
70 %************************************************************************
71
72 Note [Kind Constraint and kind *]
73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
74 The kind Constraint is the kind of classes and other type constraints.
75 The special thing about types of kind Constraint is that 
76  * They are displayed with double arrow:
77      f :: Ord a => a -> a
78  * They are implicitly instantiated at call sites; so the type inference
79    engine inserts an extra argument of type (Ord a) at every call site
80    to f.
81
82 However, once type inference is over, there is *no* distinction between 
83 Constraint and *.  Indeed we can have coercions between the two. Consider
84    class C a where
85      op :: a -> a
86 For this single-method class we may generate a newtype, which in turn 
87 generates an axiom witnessing
88     Ord a ~ (a -> a)
89 so on the left we have Constraint, and on the right we have *.
90 See Trac #7451.
91
92 Bottom line: although '*' and 'Constraint' are distinct TyCons, with
93 distinct uniques, they are treated as equal at all times except 
94 during type inference.  Hence cmpTc treats them as equal.
95
96 \begin{code}
97 -- | Essentially 'funResultTy' on kinds handling pi-types too
98 kindFunResult :: Kind -> KindOrType -> Kind
99 kindFunResult (FunTy _ res) _ = res
100 kindFunResult (ForAllTy kv res) arg = substKiWith [kv] [arg] res
101 kindFunResult k _ = pprPanic "kindFunResult" (ppr k)
102
103 kindAppResult :: Kind -> [Type] -> Kind
104 kindAppResult k []     = k
105 kindAppResult k (a:as) = kindAppResult (kindFunResult k a) as
106
107 -- | Essentially 'splitFunTys' on kinds
108 splitKindFunTys :: Kind -> ([Kind],Kind)
109 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
110                               (as, k) -> (a:as, k)
111 splitKindFunTys k = ([], k)
112
113 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
114 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
115 splitKindFunTy_maybe _           = Nothing
116
117 -- | Essentially 'splitFunTysN' on kinds
118 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
119 splitKindFunTysN 0 k           = ([], k)
120 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
121                                    (as, k) -> (a:as, k)
122 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
123
124 -- | Find the result 'Kind' of a type synonym, 
125 -- after applying it to its 'arity' number of type variables
126 -- Actually this function works fine on data types too, 
127 -- but they'd always return '*', so we never need to ask
128 synTyConResKind :: TyCon -> Kind
129 synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
130
131 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
132 isOpenTypeKind, isUnliftedTypeKind,
133   isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
134
135 isOpenTypeKindCon, isUnliftedTypeKindCon,
136   isSubOpenTypeKindCon, isConstraintKindCon,
137   isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
138
139
140 isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
141 isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
142 isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
143 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
144 isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
145 isSuperKindTyCon      tc = tyConUnique tc == superKindTyConKey
146
147 isAnyKind (TyConApp tc _) = isAnyKindCon tc
148 isAnyKind _               = False
149
150 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
151 isOpenTypeKind _               = False
152
153 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
154 isUnliftedTypeKind _               = False
155
156 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
157 isConstraintKind _               = False
158
159 isConstraintOrLiftedKind (TyConApp tc _)
160   = isConstraintKindCon tc || isLiftedTypeKindCon tc
161 isConstraintOrLiftedKind _ = False
162
163 returnsConstraintKind :: Kind -> Bool
164 returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
165 returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
166 returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
167 returnsConstraintKind _               = False
168
169 --------------------------------------------
170 --            Kinding for arrow (->)
171 -- Says when a kind is acceptable on lhs or rhs of an arrow
172 --     arg -> res
173
174 okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
175 okArrowArgKindCon kc
176   | isLiftedTypeKindCon   kc = True
177   | isUnliftedTypeKindCon kc = True
178   | isConstraintKindCon   kc = True
179   | otherwise                = False
180
181 okArrowResultKindCon = okArrowArgKindCon
182
183 okArrowArgKind, okArrowResultKind :: Kind -> Bool
184 okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
185 okArrowArgKind    _                = False
186
187 okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
188 okArrowResultKind _                = False
189
190 -----------------------------------------
191 --              Subkinding
192 -- The tc variants are used during type-checking, where we don't want the
193 -- Constraint kind to be a subkind of anything
194 -- After type-checking (in core), Constraint is a subkind of openTypeKind
195
196 isSubOpenTypeKind :: Kind -> Bool
197 -- ^ True of any sub-kind of OpenTypeKind
198 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
199 isSubOpenTypeKind _                = False
200
201 isSubOpenTypeKindCon kc
202   =  isOpenTypeKindCon   kc
203   || isUnliftedTypeKindCon kc
204   || isLiftedTypeKindCon   kc  
205   || isConstraintKindCon kc   -- Needed for error (Num a) "blah"
206                               -- and so that (Ord a -> Eq a) is well-kinded
207                               -- and so that (# Eq a, Ord b #) is well-kinded
208                               -- See Note [Kind Constraint and kind *]
209
210 -- | Is this a kind (i.e. a type-of-types)?
211 isKind :: Kind -> Bool
212 isKind k = isSuperKind (typeKind k)
213
214 isSubKind :: Kind -> Kind -> Bool
215 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
216 -- Sub-kinding is extremely simple and does not look
217 -- under arrrows or type constructors
218
219 -- If you edit this function, you may need to update the GHC formalism
220 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
221 isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
222   | isPromotedTyCon kc1 || isPromotedTyCon kc2
223     -- handles promoted kinds (List *, Nat, etc.)
224   = eqKind k1 k2
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
235 -- If you edit this function, you may need to update the GHC formalism
236 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
237 isSubKindCon kc1 kc2
238   | kc1 == kc2              = True
239   | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 
240   | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
241   | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
242   | otherwise               = False
243     -- See Note [Kind Constraint and kind *]
244
245 -------------------------
246 -- Hack alert: we need a tiny variant for the typechecker
247 -- Reason:     f :: Int -> (a~b)
248 --             g :: forall (c::Constraint). Int -> c
249 -- We want to reject these, even though Constraint is
250 -- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
251 -- *after* the typechecker
252 --   a) So that (Ord a -> Eq a) is a legal type
253 --   b) So that the simplifer can generate (error (Eq a) "urk")
254 --
255 -- Easiest way to reject is simply to make Constraint not
256 -- below OpenTypeKind when type checking
257
258 tcIsSubKind :: Kind -> Kind -> Bool
259 tcIsSubKind k1 k2
260   | isConstraintKind k1 = isConstraintKind k2
261   | otherwise           = isSubKind k1 k2
262
263 tcIsSubKindCon :: TyCon -> TyCon -> Bool
264 tcIsSubKindCon kc1 kc2
265   | isConstraintKindCon kc1 = isConstraintKindCon kc2
266   | otherwise               = isSubKindCon kc1 kc2
267
268 -------------------------
269 defaultKind :: Kind -> Kind
270 -- ^ Used when generalising: default OpenKind and ArgKind to *.
271 -- See "Type#kind_subtyping" for more information on what that means
272
273 -- When we generalise, we make generic type variables whose kind is
274 -- simple (* or *->* etc).  So generic type variables (other than
275 -- built-in constants like 'error') always have simple kinds.  This is important;
276 -- consider
277 --      f x = True
278 -- We want f to get type
279 --      f :: forall (a::*). a -> Bool
280 -- Not 
281 --      f :: forall (a::ArgKind). a -> Bool
282 -- because that would allow a call like (f 3#) as well as (f True),
283 -- and the calling conventions differ.
284 -- This defaulting is done in TcMType.zonkTcTyVarBndr.
285 --
286 -- The test is really whether the kind is strictly above '*'
287 defaultKind (TyConApp kc _args)
288   | isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
289 defaultKind k = k
290
291 -- Returns the free kind variables in a kind
292 kiVarsOfKind :: Kind -> VarSet
293 kiVarsOfKind = tyVarsOfType
294
295 kiVarsOfKinds :: [Kind] -> VarSet
296 kiVarsOfKinds = tyVarsOfTypes
297 \end{code}