/
Kind.lhs
235 lines (191 loc) · 8.31 KB
/
Kind.lhs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
%
% (c) The University of Glasgow 2006
%
\begin{code}
module Kind (
-- * Main data type
Kind, typeKind,
-- Kinds
liftedTypeKind, unliftedTypeKind, openTypeKind,
argTypeKind, ubxTupleKind,
mkArrowKind, mkArrowKinds,
-- Kind constructors...
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
argTypeKindTyCon, ubxTupleKindTyCon,
-- Super Kinds
tySuperKind, tySuperKindTyCon,
pprKind, pprParendKind,
-- ** Deconstructing Kinds
kindFunResult, kindAppResult, synTyConResKind,
splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
-- ** Predicates on Kinds
isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
isSuperKind, isCoercionKind,
isLiftedTypeKindCon,
isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
isSubKindCon,
) where
#include "HsVersions.h"
import TypeRep
import TysPrim
import TyCon
import Var
import PrelNames
import Outputable
\end{code}
%************************************************************************
%* *
Predicates over Kinds
%* *
%************************************************************************
\begin{code}
isTySuperKind :: SuperKind -> Bool
isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
isTySuperKind _ = False
-------------------
-- Lastly we need a few functions on Kinds
isLiftedTypeKindCon :: TyCon -> Bool
isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
\end{code}
%************************************************************************
%* *
The kind of a type
%* *
%************************************************************************
\begin{code}
typeKind :: Type -> Kind
typeKind _ty@(TyConApp tc tys)
= ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty )
-- Assertion checks for unsaturated application of (~)
-- See Note [The (~) TyCon] in TysPrim
kindAppResult (tyConKind tc) tys
typeKind (PredTy pred) = predKind pred
typeKind (AppTy fun _) = kindFunResult (typeKind fun)
typeKind (ForAllTy _ ty) = typeKind ty
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (FunTy _arg res)
-- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*),
-- not unliftedTypKind (#)
-- The only things that can be after a function arrow are
-- (a) types (of kind openTypeKind or its sub-kinds)
-- (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
| isTySuperKind k = k
| otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind
where
k = typeKind res
------------------
predKind :: PredType -> Kind
predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted
predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
predKind (IParam {}) = liftedTypeKind -- always represented by lifted types
\end{code}
%************************************************************************
%* *
Functions over Kinds
%* *
%************************************************************************
\begin{code}
-- | Essentially 'funResultTy' on kinds
kindFunResult :: Kind -> Kind
kindFunResult (FunTy _ res) = res
kindFunResult k = pprPanic "kindFunResult" (ppr k)
kindAppResult :: Kind -> [arg] -> Kind
kindAppResult k [] = k
kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
-- | 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
synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool
isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey
isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
isOpenTypeKind _ = False
isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
isUbxTupleKind _ = False
isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
isArgTypeKind _ = False
isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
isUnliftedTypeKind _ = False
isSubOpenTypeKind :: Kind -> Bool
-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
False
isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
isSubOpenTypeKind other = ASSERT( isKind other ) False
-- This is a conservative answer
-- It matters in the call to isSubKind in
-- checkExpectedKind.
isSubArgTypeKindCon kc
| isUnliftedTypeKindCon kc = True
| isLiftedTypeKindCon kc = True
| isArgTypeKindCon kc = True
| otherwise = False
isSubArgTypeKind :: Kind -> Bool
-- ^ True of any sub-kind of ArgTypeKind
isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
isSubArgTypeKind _ = False
-- | Is this a super-kind (i.e. a type-of-kinds)?
isSuperKind :: Type -> Bool
isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
isSuperKind _ = False
-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)
isSubKind :: Kind -> Kind -> Bool
-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
isSubKind _ _ = False
isSubKindCon :: TyCon -> TyCon -> Bool
-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
isSubKindCon kc1 kc2
| isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True
| isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
| isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True
| isOpenTypeKindCon kc2 = True
-- we already know kc1 is not a fun, its a TyCon
| isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True
| otherwise = False
defaultKind :: Kind -> Kind
-- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
-- information on what that means
-- 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
-- f :: forall (a::??). a -> Bool
-- because that would allow a call like (f 3#) as well as (f True),
--and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr.
defaultKind k
| isSubOpenTypeKind k = liftedTypeKind
| isSubArgTypeKind k = liftedTypeKind
| otherwise = k
\end{code}