4 Kind, mkTypeKind, mkBoxedTypeKind, mkUnboxedTypeKind, mkArrowKind,
5 hasMoreBoxityInfo, -- Kind -> Kind -> Bool
6 resultKind, -- Kind -> Kind
9 newKindVar, -- NF_TcM s (TcKind s)
10 newKindVars, -- Int -> NF_TcM s [TcKind s]
11 unifyKind, -- TcKind s -> TcKind s -> TcM s ()
12 unifyKinds, -- [TcKind s] -> [TcKind s] -> TcM s ()
14 kindToTcKind, -- Kind -> TcKind s
15 tcDefaultKind -- TcKind s -> NF_TcM s Kind
18 #include "HsVersions.h"
23 import Unique ( Unique, pprUnique10 )
24 import Util ( nOfThem, panic )
30 type TcKind s = GenKind (TcRef s (TcMaybe s))
31 data TcMaybe s = Unbound
32 | BoundTo (TcKind s) -- Always ArrowKind or BoxedTypeKind
34 newKindVar :: NF_TcM s (TcKind s)
35 newKindVar = tcGetUnique `thenNF_Tc` \ uniq ->
36 tcNewMutVar Unbound `thenNF_Tc` \ box ->
37 returnNF_Tc (VarKind uniq box)
39 newKindVars :: Int -> NF_TcM s [TcKind s]
40 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
47 unifyKinds :: [TcKind s] -> [TcKind s] -> TcM s ()
48 unifyKinds [] [] = returnTc ()
49 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
51 unifyKinds _ _ = panic "unifyKinds: length mis-match"
53 unifyKind :: TcKind s -- Expected
58 = tcAddErrCtxtM ctxt (unify_kind kind1 kind2)
60 ctxt = zonkTcKind kind1 `thenNF_Tc` \ kind1' ->
61 zonkTcKind kind2 `thenNF_Tc` \ kind2' ->
62 returnNF_Tc (unifyKindCtxt kind1' kind2')
65 -- TypeKind expected => the actual can be boxed or unboxed
66 unify_kind TypeKind TypeKind = returnTc ()
67 unify_kind TypeKind BoxedTypeKind = returnTc ()
68 unify_kind TypeKind UnboxedTypeKind = returnTc ()
70 unify_kind BoxedTypeKind BoxedTypeKind = returnTc ()
71 unify_kind UnboxedTypeKind UnboxedTypeKind = returnTc ()
73 unify_kind (ArrowKind fun1 arg1)
76 = unify_kind fun1 fun2 `thenTc_`
79 unify_kind kind1@(VarKind uniq box) kind2 = unify_var False kind1 uniq box kind2
80 unify_kind kind1 kind2@(VarKind uniq box) = unify_var True kind2 uniq box kind1
82 unify_kind kind1 kind2
83 = failWithTc (kindMisMatchErr kind1 kind2)
86 We could probably do some "shorting out" in unifyVarKind, but
87 I'm not convinced it would save time, and it's a little tricky to get right.
90 unify_var swap_vars kind1 uniq1 box1 kind2
91 = tcReadMutVar box1 `thenNF_Tc` \ maybe_kind1 ->
93 Unbound -> unify_unbound_var False kind1 uniq1 box1 kind2
94 BoundTo TypeKind -> unify_unbound_var True kind1 uniq1 box1 kind2
95 -- *** NB: BoundTo TypeKind is a kind of un-bound
96 -- It can get refined to BoundTo UnboxedTypeKind or BoxedTypeKind
98 BoundTo kind1' | swap_vars -> unify_kind kind2 kind1'
99 | otherwise -> unify_kind kind1' kind2
100 -- Keep them the right way round, so that
101 -- the asymettric boxed/unboxed stuff works
104 unify_unbound_var type_kind kind1 uniq1 box1 kind2@(VarKind uniq2 box2)
105 | uniq1 == uniq2 -- Binding to self is a no-op
108 | otherwise -- Distinct variables
109 = tcReadMutVar box2 `thenNF_Tc` \ maybe_kind2 ->
111 BoundTo kind2' -> unify_unbound_var type_kind kind1 uniq1 box1 kind2'
112 Unbound -> tcWriteMutVar box2 (BoundTo kind1) `thenNF_Tc_`
113 -- No need for occurs check here
114 -- Kind1 is an unbound variable, or BoundToTypeKind
117 -- If the variable was originally bound to TypeKind, we succeed
118 -- unless the thing its bound to is an arrow.
119 unify_unbound_var True kind1 uniq1 box1 kind2@(ArrowKind k1 k2)
120 = failWithTc (kindMisMatchErr kind1 kind2)
122 unify_unbound_var type_kind kind1 uniq1 box1 non_var_or_arrow_kind2
123 = occur_check non_var_or_arrow_kind2 `thenTc_`
124 tcWriteMutVar box1 (BoundTo non_var_or_arrow_kind2) `thenNF_Tc_`
127 occur_check TypeKind = returnTc ()
128 occur_check UnboxedTypeKind = returnTc ()
129 occur_check BoxedTypeKind = returnTc ()
130 occur_check (ArrowKind fun arg) = occur_check fun `thenTc_` occur_check arg
131 occur_check kind@(VarKind uniq' box)
133 = failWithTc (kindOccurCheck kind non_var_or_arrow_kind2)
135 | otherwise -- Different variable
136 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
138 Unbound -> returnTc ()
139 BoundTo kind' -> occur_check kind'
142 The "occurs check" is necessary to catch situation like
149 Coercions between TcKind and Kind.
152 -- This strange function is forced on us by the type system
153 kindToTcKind :: Kind -> TcKind s
154 kindToTcKind TypeKind = TypeKind
155 kindToTcKind BoxedTypeKind = BoxedTypeKind
156 kindToTcKind UnboxedTypeKind = UnboxedTypeKind
157 kindToTcKind (ArrowKind k1 k2) = ArrowKind (kindToTcKind k1) (kindToTcKind k2)
160 -- Default all unbound kinds to TcTypeKind, and return the
161 -- corresponding Kind as well.
162 tcDefaultKind :: TcKind s -> NF_TcM s Kind
164 tcDefaultKind TypeKind = returnNF_Tc TypeKind
165 tcDefaultKind BoxedTypeKind = returnNF_Tc BoxedTypeKind
166 tcDefaultKind UnboxedTypeKind = returnNF_Tc UnboxedTypeKind
168 tcDefaultKind (ArrowKind kind1 kind2)
169 = tcDefaultKind kind1 `thenNF_Tc` \ k1 ->
170 tcDefaultKind kind2 `thenNF_Tc` \ k2 ->
171 returnNF_Tc (ArrowKind k1 k2)
173 -- Here's where we "default" unbound kinds to BoxedTypeKind
174 tcDefaultKind (VarKind uniq box)
175 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
177 BoundTo TypeKind -> bind_to_boxed
178 Unbound -> bind_to_boxed
179 BoundTo kind -> tcDefaultKind kind
181 -- Default unbound variables to kind BoxedTypeKind
182 bind_to_boxed = tcWriteMutVar box (BoundTo BoxedTypeKind) `thenNF_Tc_`
183 returnNF_Tc BoxedTypeKind
187 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
188 -- Removes variables that have now been bound.
189 -- Mainly used just before an error message is printed,
190 -- so that we don't need to follow through bound variables
191 -- during error message construction.
193 zonkTcKind TypeKind = returnNF_Tc TypeKind
194 zonkTcKind BoxedTypeKind = returnNF_Tc BoxedTypeKind
195 zonkTcKind UnboxedTypeKind = returnNF_Tc UnboxedTypeKind
197 zonkTcKind (ArrowKind kind1 kind2)
198 = zonkTcKind kind1 `thenNF_Tc` \ k1 ->
199 zonkTcKind kind2 `thenNF_Tc` \ k2 ->
200 returnNF_Tc (ArrowKind k1 k2)
202 zonkTcKind kind@(VarKind uniq box)
203 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
205 Unbound -> returnNF_Tc kind
206 BoundTo kind' -> zonkTcKind kind'
213 unifyKindCtxt kind1 kind2
214 = vcat [ptext SLIT("Expected:") <+> ppr kind1,
215 ptext SLIT("Found: ") <+> ppr kind2]
217 kindOccurCheck kind1 kind2
218 = hang (ptext SLIT("Cannot construct the infinite kind:")) 4
219 (sep [ppr kind1, equals, ppr kind1, ptext SLIT("(\"occurs check\")")])
221 kindMisMatchErr kind1 kind2
222 = hang (ptext SLIT("Couldn't match the kind")) 4
224 ptext SLIT("against"),