Kind.lhs 5.93 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

\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))
63
  -- INVARIANT: a KindVar can only be instantiated by a SimpleKind
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

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
148
149
150
isOpenTypeKind (KindVar _)   = False	-- This is a conservative answer
					-- It matters in the call to isSubKind in
					-- checkExpectedKind.
151
152
153
154
155
156
157
158
159
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
160
161
isSubKind (FunKind a1 r1) (FunKind a2 r2)   = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
isSubKind k1		  k2		    = False
162
163
164

defaultKind :: Kind -> Kind
-- Used when generalising: default kind '?' and '??' to '*'
165
166
167
168
169
170
171
172
173
174
175
176
-- 
-- 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.
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
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("(#)")
206
pprKind (FunKind k1 k2)  = sep [ pprParendKind k1, arrow <+> pprKind k2]
207
208
209
210
\end{code}