Kind.lhs 5.78 KB
Newer Older
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
%
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%

\begin{code}
module Kind (
	Kind(..), KindVar(..), SimpleKind,
	openTypeKind, liftedTypeKind, unliftedTypeKind, 
	argTypeKind, ubxTupleKind,

	isLiftedTypeKind, isUnliftedTypeKind, 
	isArgTypeKind, isOpenTypeKind,
	mkArrowKind, mkArrowKinds,

        isSubKind, defaultKind, 
	kindFunResult, splitKindFunTys, mkKindVar,

	pprKind, pprParendKind
     ) where

#include "HsVersions.h"

import Unique	( Unique )
import Outputable
import DATA_IOREF
\end{code}

Kinds
~~~~~
There's a little subtyping at the kind level:  

		 ?
		/ \
	       /   \
	      ??   (#)
	     /  \
            *   #

where	*    [LiftedTypeKind]   means boxed type
	#    [UnliftedTypeKind] means unboxed type
	(#)  [UbxTupleKind]     means unboxed tuple
	??   [ArgTypeKind]      is the lub of *,#
	?    [OpenTypeKind]	means any type at all

In particular:

47
	error :: forall a:?. String -> a
48
	(->)  :: ?? -> ? -> *
49
	(\(x::t) -> ...)	Here t::?? (i.e. not unboxed tuple)
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

\begin{code}
data Kind 
  = LiftedTypeKind 	-- *
  | OpenTypeKind	-- ?
  | UnliftedTypeKind	-- #
  | UbxTupleKind	-- (##)
  | ArgTypeKind		-- ??
  | FunKind Kind Kind	-- k1 -> k2
  | KindVar KindVar
  deriving( Eq )

data KindVar = KVar Unique (IORef (Maybe SimpleKind))
  -- INVARIANT: a KindVar can only be instantaited by a SimpleKind

type SimpleKind = Kind	
  -- A SimpleKind has no ? or # kinds in it:
  -- sk ::= * | sk1 -> sk2 | kvar

instance Eq KindVar where
  (KVar u1 _) == (KVar u2 _) = u1 == u2

mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar
mkKindVar = KVar
\end{code}

Kind inference
~~~~~~~~~~~~~~
During kind inference, a kind variable unifies only with 
a "simple kind", sk
	sk ::= * | sk1 -> sk2
For example 
	data T a = MkT a (T Int#)
fails.  We give T the kind (k -> *), and the kind variable k won't unify
with # (the kind of Int#).

Type inference
~~~~~~~~~~~~~~
When creating a fresh internal type variable, we give it a kind to express 
constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x, 
with kind ??.  

During unification we only bind an internal type variable to a type
whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.

When unifying two internal type variables, we collect their kind constraints by
finding the GLB of the two.  Since the partial order is a tree, they only
have a glb if one is a sub-kind of the other.  In that case, we bind the
less-informative one to the more informative one.  Neat, eh?


\begin{code}
liftedTypeKind   = LiftedTypeKind
unliftedTypeKind = UnliftedTypeKind
openTypeKind     = OpenTypeKind
argTypeKind      = ArgTypeKind
ubxTupleKind	 = UbxTupleKind

mkArrowKind :: Kind -> Kind -> Kind
mkArrowKind k1 k2 = k1 `FunKind` k2

mkArrowKinds :: [Kind] -> Kind -> Kind
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
\end{code}

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

\begin{code}
kindFunResult :: Kind -> Kind
kindFunResult (FunKind _ k) = k
kindFunResult k = pprPanic "kindFunResult" (ppr k)

splitKindFunTys :: Kind -> ([Kind],Kind)
splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of
				    (as, r) -> (k1:as, r)
splitKindFunTys k = ([], k)

isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
isLiftedTypeKind LiftedTypeKind = True
isLiftedTypeKind other		= False

isUnliftedTypeKind UnliftedTypeKind = True
isUnliftedTypeKind other	    = False

isArgTypeKind :: Kind -> Bool
-- True of any sub-kind of ArgTypeKind 
isArgTypeKind LiftedTypeKind   = True
isArgTypeKind UnliftedTypeKind = True
isArgTypeKind ArgTypeKind      = True
isArgTypeKind other	       = False

isOpenTypeKind :: Kind -> Bool
-- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
isOpenTypeKind (FunKind _ _) = False
isOpenTypeKind other	     = True

isSubKind :: Kind -> Kind -> Bool
-- (k1 `isSubKind` k2) checks that k1 <: k2
isSubKind LiftedTypeKind   LiftedTypeKind   = True
isSubKind UnliftedTypeKind UnliftedTypeKind = True
isSubKind UbxTupleKind     UbxTupleKind     = True
isSubKind k1 		   OpenTypeKind     = isOpenTypeKind k1
isSubKind k1 		   ArgTypeKind      = isArgTypeKind k1
isSubKind (FunKind a1 r1) (FunKind a2 r2)
  = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
isSubKind k1 k2 = False

defaultKind :: Kind -> Kind
-- Used when generalising: default kind '?' and '??' to '*'
163
164
165
166
167
168
169
170
171
172
173
174
-- 
-- 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.
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
defaultKind OpenTypeKind = LiftedTypeKind
defaultKind ArgTypeKind  = LiftedTypeKind
defaultKind kind	 = kind
\end{code}


%************************************************************************
%*									*
		Pretty printing
%*									*
%************************************************************************

\begin{code}
instance Outputable KindVar where
  ppr (KVar uniq _) = text "k_" <> ppr uniq

instance Outputable Kind where
  ppr k = pprKind k

pprParendKind :: Kind -> SDoc
pprParendKind k@(FunKind _ _) = parens (pprKind k)
pprParendKind k		      = pprKind k

pprKind (KindVar v)      = ppr v
pprKind LiftedTypeKind   = ptext SLIT("*")
pprKind UnliftedTypeKind = ptext SLIT("#")
pprKind OpenTypeKind     = ptext SLIT("?")
pprKind ArgTypeKind      = ptext SLIT("??")
pprKind UbxTupleKind     = ptext SLIT("(#)")
204
pprKind (FunKind k1 k2)  = sep [ pprParendKind k1, arrow <+> pprKind k2]
205
206
207
208
\end{code}