Kind.lhs 11.1 KB
Newer Older
1
%
Gabor Greif's avatar
Gabor Greif committed
2
% (c) The University of Glasgow 2006-2012
3
4
5
%

\begin{code}
6
7
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
Ian Lynagh's avatar
Ian Lynagh committed
8
9
10
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
11
--     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
Ian Lynagh's avatar
Ian Lynagh committed
12
13
-- for details

14
15
module Kind (
        -- * Main data type
16
        SuperKind, Kind, typeKind,
17
18

	-- Kinds
19
	anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind,
20
21
22
        mkArrowKind, mkArrowKinds,

        -- Kind constructors...
dreixel's avatar
dreixel committed
23
        anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
24
        unliftedTypeKindTyCon, constraintKindTyCon,
25
26

        -- Super Kinds
27
	superKind, superKindTyCon, 
28
29
30
31
        
	pprKind, pprParendKind,

        -- ** Deconstructing Kinds
32
        kindAppResult, synTyConResKind,
33
34
35
36
        splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,

        -- ** Predicates on Kinds
        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
37
38
        isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
        isKind, isKindVar,
39
        isSuperKind, isSuperKindTyCon,
batterseapower's avatar
batterseapower committed
40
        isLiftedTypeKindCon, isConstraintKindCon,
dreixel's avatar
dreixel committed
41
        isAnyKind, isAnyKindCon,
42
        okArrowArgKind, okArrowResultKind,
43

44
        isSubOpenTypeKind, isSubOpenTypeKindKey,
45
46
        isSubKind, isSubKindCon, 
        tcIsSubKind, tcIsSubKindCon,
47
        defaultKind, defaultKind_maybe,
dreixel's avatar
dreixel committed
48
49

        -- ** Functions on variables
50
        kiVarsOfKind, kiVarsOfKinds
51
52
53
54
55

       ) where

#include "HsVersions.h"

dreixel's avatar
dreixel committed
56
import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
batterseapower's avatar
batterseapower committed
57

58
59
60
import TypeRep
import TysPrim
import TyCon
dreixel's avatar
dreixel committed
61
import VarSet
62
63
import PrelNames
import Outputable
64
import Maybes( orElse )
65
import Util
66
import FastString
67
68
69
70
71
72
73
74
\end{code}

%************************************************************************
%*									*
	Functions over Kinds		
%*									*
%************************************************************************

75
76
77
78
79
80
81
82
83
84
Note [Kind Constraint and kind *]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The kind Constraint is the kind of classes and other type constraints.
The special thing about types of kind Constraint is that 
 * They are displayed with double arrow:
     f :: Ord a => a -> a
 * They are implicitly instantiated at call sites; so the type inference
   engine inserts an extra argument of type (Ord a) at every call site
   to f.

Gabor Greif's avatar
Gabor Greif committed
85
However, once type inference is over, there is *no* distinction between 
86
87
88
Constraint and *.  Indeed we can have coercions between the two. Consider
   class C a where
     op :: a -> a
Gabor Greif's avatar
Gabor Greif committed
89
For this single-method class we may generate a newtype, which in turn 
90
91
92
93
94
95
96
97
98
generates an axiom witnessing
    Ord a ~ (a -> a)
so on the left we have Constraint, and on the right we have *.
See Trac #7451.

Bottom line: although '*' and 'Constraint' are distinct TyCons, with
distinct uniques, they are treated as equal at all times except 
during type inference.  Hence cmpTc treats them as equal.

99
\begin{code}
dreixel's avatar
dreixel committed
100
-- | Essentially 'funResultTy' on kinds handling pi-types too
101
102
103
104
105
106
kindFunResult :: SDoc -> Kind -> KindOrType -> Kind
kindFunResult _ (FunTy _ res)     _   = res
kindFunResult _ (ForAllTy kv res) arg = substKiWith [kv] [arg] res
#ifdef DEBUG
kindFunResult doc k _ = pprPanic "kindFunResult" (ppr k $$ doc)
#else
Gabor Greif's avatar
Gabor Greif committed
107
-- Without DEBUG, doc becomes an unsed arg, and will be optimised away
108
109
110
111
112
113
kindFunResult _ _ _ = panic "kindFunResult"
#endif

kindAppResult :: SDoc -> Kind -> [Type] -> Kind
kindAppResult _   k []     = k
kindAppResult doc k (a:as) = kindAppResult doc (kindFunResult doc k a) as
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136

-- | Essentially 'splitFunTys' on kinds
splitKindFunTys :: Kind -> ([Kind],Kind)
splitKindFunTys (FunTy a r) = case splitKindFunTys r of
                              (as, k) -> (a:as, k)
splitKindFunTys k = ([], k)

splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
splitKindFunTy_maybe (FunTy a r) = Just (a,r)
splitKindFunTy_maybe _           = Nothing

-- | Essentially 'splitFunTysN' on kinds
splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
splitKindFunTysN 0 k           = ([], k)
splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
                                   (as, k) -> (a:as, k)
splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)

-- | Find the result 'Kind' of a type synonym, 
-- after applying it to its 'arity' number of type variables
-- Actually this function works fine on data types too, 
-- but they'd always return '*', so we never need to ask
synTyConResKind :: TyCon -> Kind
137
138
synTyConResKind tycon = kindAppResult (ptext (sLit "synTyConResKind") <+> ppr tycon)
                                      (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
139
140

-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
141
isOpenTypeKind, isUnliftedTypeKind,
dreixel's avatar
dreixel committed
142
  isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
dreixel's avatar
dreixel committed
143

144
isOpenTypeKindCon, isUnliftedTypeKindCon,
145
  isSubOpenTypeKindCon, isConstraintKindCon,
146
  isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
dreixel's avatar
dreixel committed
147
148


149
150
151
152
153
isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
154
isSuperKindTyCon      tc = tyConUnique tc == superKindTyConKey
dreixel's avatar
dreixel committed
155
156
157

isAnyKind (TyConApp tc _) = isAnyKindCon tc
isAnyKind _               = False
158
159
160
161
162
163
164

isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
isOpenTypeKind _               = False

isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
isUnliftedTypeKind _               = False

batterseapower's avatar
batterseapower committed
165
166
167
isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
isConstraintKind _               = False

dreixel's avatar
dreixel committed
168
169
170
isConstraintOrLiftedKind (TyConApp tc _)
  = isConstraintKindCon tc || isLiftedTypeKindCon tc
isConstraintOrLiftedKind _ = False
dreixel's avatar
dreixel committed
171

172
173
174
175
176
177
returnsConstraintKind :: Kind -> Bool
returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
returnsConstraintKind _               = False

178
179
180
181
182
183
--------------------------------------------
--            Kinding for arrow (->)
-- Says when a kind is acceptable on lhs or rhs of an arrow
--     arg -> res

okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
184
185
okArrowArgKindCon    = isSubOpenTypeKindCon
okArrowResultKindCon = isSubOpenTypeKindCon
186
187
188
189
190
191
192
193
194
195

okArrowArgKind, okArrowResultKind :: Kind -> Bool
okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
okArrowArgKind    _                = False

okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
okArrowResultKind _                = False

-----------------------------------------
--              Subkinding
dreixel's avatar
dreixel committed
196
197
-- The tc variants are used during type-checking, where we don't want the
-- Constraint kind to be a subkind of anything
198
-- After type-checking (in core), Constraint is a subkind of openTypeKind
199

200
isSubOpenTypeKind :: Kind -> Bool
dreixel's avatar
dreixel committed
201
202
203
204
-- ^ True of any sub-kind of OpenTypeKind
isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
isSubOpenTypeKind _                = False

205
206
207
208
209
210
211
212
213
214
215
isSubOpenTypeKindCon kc = isSubOpenTypeKindKey (tyConUnique kc)

isSubOpenTypeKindKey :: Unique -> Bool
isSubOpenTypeKindKey uniq
  =  uniq == openTypeKindTyConKey
  || uniq == unliftedTypeKindTyConKey
  || uniq == liftedTypeKindTyConKey
  || uniq == constraintKindTyConKey  -- Needed for error (Num a) "blah"
                                     -- and so that (Ord a -> Eq a) is well-kinded
                                     -- and so that (# Eq a, Ord b #) is well-kinded
                              	     -- See Note [Kind Constraint and kind *]
216
217
218
219
220

-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)

221
isSubKind :: Kind -> Kind -> Bool
222
-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
223
224
-- Sub-kinding is extremely simple and does not look
-- under arrrows or type constructors
dreixel's avatar
dreixel committed
225

226
227
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
228
isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
229
  | isPromotedTyCon kc1 || isPromotedTyCon kc2
dreixel's avatar
dreixel committed
230
    -- handles promoted kinds (List *, Nat, etc.)
231
  = eqKind k1 k2
dreixel's avatar
dreixel committed
232

233
234
235
  | otherwise -- handles usual kinds (*, #, (#), etc.)
  = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
    kc1 `isSubKindCon` kc2
dreixel's avatar
dreixel committed
236

237
isSubKind k1 k2 = eqKind k1 k2
238
239
240

isSubKindCon :: TyCon -> TyCon -> Bool
-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
241
242
243

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
244
isSubKindCon kc1 kc2
245
246
247
248
249
  | kc1 == kc2              = True
  | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 
  | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
  | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
    -- See Note [Kind Constraint and kind *]
250
  | otherwise               = False
251
252
253
254
255

-------------------------
-- Hack alert: we need a tiny variant for the typechecker
-- Reason:     f :: Int -> (a~b)
--             g :: forall (c::Constraint). Int -> c
256
--             h :: Int => Int
257
258
259
260
261
-- We want to reject these, even though Constraint is
-- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
-- *after* the typechecker
--   a) So that (Ord a -> Eq a) is a legal type
--   b) So that the simplifer can generate (error (Eq a) "urk")
262
263
-- Moreover, after the type checker, Constraint and *
-- are identical; see Note [Kind Constraint and kind *]
264
--
265
-- Easiest way to reject is simply to make Constraint a compliete
266
267
268
269
270
-- below OpenTypeKind when type checking

tcIsSubKind :: Kind -> Kind -> Bool
tcIsSubKind k1 k2
  | isConstraintKind k1 = isConstraintKind k2
271
  | isConstraintKind k2 = isConstraintKind k1
272
  | otherwise           = isSubKind k1 k2
273

dreixel's avatar
dreixel committed
274
275
tcIsSubKindCon :: TyCon -> TyCon -> Bool
tcIsSubKindCon kc1 kc2
276
  | isConstraintKindCon kc1 = isConstraintKindCon kc2
277
  | isConstraintKindCon kc2 = isConstraintKindCon kc1
278
  | otherwise               = isSubKindCon kc1 kc2
dreixel's avatar
dreixel committed
279

280
-------------------------
281
282
defaultKind       :: Kind -> Kind
defaultKind_maybe :: Kind -> Maybe Kind
283
-- ^ Used when generalising: default OpenKind and ArgKind to *.
dreixel's avatar
dreixel committed
284
-- See "Type#kind_subtyping" for more information on what that means
285
286
287
288
289
290
291
292
293

-- When we generalise, we make generic type variables whose kind is
-- simple (* or *->* etc).  So generic type variables (other than
-- built-in constants like 'error') always have simple kinds.  This is important;
-- consider
--	f x = True
-- We want f to get type
--	f :: forall (a::*). a -> Bool
-- Not 
294
--	f :: forall (a::ArgKind). a -> Bool
295
-- because that would allow a call like (f 3#) as well as (f True),
dreixel's avatar
dreixel committed
296
297
-- and the calling conventions differ.
-- This defaulting is done in TcMType.zonkTcTyVarBndr.
298
299
--
-- The test is really whether the kind is strictly above '*'
300
301
302
303
304
defaultKind_maybe (TyConApp kc _args)
  | isOpenTypeKindCon kc = ASSERT( null _args ) Just liftedTypeKind
defaultKind_maybe _      = Nothing

defaultKind k = defaultKind_maybe k `orElse` k
dreixel's avatar
dreixel committed
305
306
307
308
309
310
311
312

-- Returns the free kind variables in a kind
kiVarsOfKind :: Kind -> VarSet
kiVarsOfKind = tyVarsOfType

kiVarsOfKinds :: [Kind] -> VarSet
kiVarsOfKinds = tyVarsOfTypes
\end{code}