4 Kind, mkTypeKind, mkBoxedTypeKind, mkUnboxedTypeKind, mkArrowKind,
5 isSubKindOf, -- Kind -> Kind -> Bool
6 resultKind, -- Kind -> Kind
8 TcKind, mkTcTypeKind, mkTcArrowKind, mkTcVarKind,
9 newKindVar, -- NF_TcM s (TcKind s)
10 newKindVars, -- Int -> NF_TcM s [TcKind s]
11 unifyKind, -- TcKind s -> TcKind s -> TcM s ()
13 kindToTcKind, -- Kind -> TcKind s
14 tcKindToKind -- TcKind s -> NF_TcM s Kind
21 import Unique ( Unique, pprUnique10 )
27 data TcKind s -- Used for kind inference
29 | TcArrowKind (TcKind s) (TcKind s)
30 | TcVarKind Unique (MutableVar s (Maybe (TcKind s)))
32 mkTcTypeKind = TcTypeKind
33 mkTcArrowKind = TcArrowKind
34 mkTcVarKind = TcVarKind
36 newKindVar :: NF_TcM s (TcKind s)
37 newKindVar = tcGetUnique `thenNF_Tc` \ uniq ->
38 tcNewMutVar Nothing `thenNF_Tc` \ box ->
39 returnNF_Tc (TcVarKind uniq box)
41 newKindVars :: Int -> NF_TcM s [TcKind s]
42 newKindVars n = mapNF_Tc (\_->newKindVar) (take n (repeat ()))
49 unifyKind :: TcKind s -> TcKind s -> TcM s ()
51 = tcAddErrCtxtM ctxt (unify_kind kind1 kind2)
53 ctxt = zonkTcKind kind1 `thenNF_Tc` \ kind1' ->
54 zonkTcKind kind2 `thenNF_Tc` \ kind2' ->
55 returnNF_Tc (unifyKindCtxt kind1' kind2')
58 unify_kind TcTypeKind TcTypeKind = returnTc ()
60 unify_kind (TcArrowKind fun1 arg1)
61 (TcArrowKind fun2 arg2)
63 = unify_kind fun1 fun2 `thenTc_`
66 unify_kind (TcVarKind uniq box) kind = unify_var uniq box kind
67 unify_kind kind (TcVarKind uniq box) = unify_var uniq box kind
69 unify_kind kind1 kind2
70 = failTc (kindMisMatchErr kind1 kind2)
73 We could probably do some "shorting out" in unifyVarKind, but
74 I'm not convinced it would save time, and it's a little tricky to get right.
77 unify_var uniq1 box1 kind2
78 = tcReadMutVar box1 `thenNF_Tc` \ maybe_kind1 ->
80 Just kind1 -> unify_kind kind1 kind1
81 Nothing -> unify_unbound_var uniq1 box1 kind2
83 unify_unbound_var uniq1 box1 kind2@(TcVarKind uniq2 box2)
84 | uniq1 == uniq2 -- Binding to self is a no-op
87 | otherwise -- Distinct variables
88 = tcReadMutVar box2 `thenNF_Tc` \ maybe_kind2 ->
90 Just kind2' -> unify_unbound_var uniq1 box1 kind2'
91 Nothing -> tcWriteMutVar box1 (Just kind2) `thenNF_Tc_`
92 -- No need for occurs check here
95 unify_unbound_var uniq1 box1 non_var_kind2
96 = occur_check non_var_kind2 `thenTc_`
97 tcWriteMutVar box1 (Just non_var_kind2) `thenNF_Tc_`
100 occur_check TcTypeKind = returnTc ()
101 occur_check (TcArrowKind fun arg) = occur_check fun `thenTc_` occur_check arg
102 occur_check kind1@(TcVarKind uniq' box)
104 = failTc (kindOccurCheck kind1 non_var_kind2)
106 | otherwise -- Different variable
107 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
109 Nothing -> returnTc ()
110 Just kind -> occur_check kind
113 The "occurs check" is necessary to catch situation like
120 Coercions between TcKind and Kind
123 kindToTcKind :: Kind -> TcKind s
124 kindToTcKind TypeKind = TcTypeKind
125 kindToTcKind BoxedTypeKind = TcTypeKind
126 kindToTcKind UnboxedTypeKind = TcTypeKind
127 kindToTcKind (ArrowKind k1 k2) = TcArrowKind (kindToTcKind k1) (kindToTcKind k2)
130 tcKindToKind :: TcKind s -> NF_TcM s Kind
132 tcKindToKind TcTypeKind
133 = returnNF_Tc TypeKind
135 tcKindToKind (TcArrowKind kind1 kind2)
136 = tcKindToKind kind1 `thenNF_Tc` \ k1 ->
137 tcKindToKind kind2 `thenNF_Tc` \ k2 ->
138 returnNF_Tc (ArrowKind k1 k2)
140 -- Here's where we "default" unbound kinds to BoxedTypeKind
141 tcKindToKind (TcVarKind uniq box)
142 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
144 Nothing -> returnNF_Tc BoxedTypeKind -- Default is kind Type for unbound
145 Just kind -> tcKindToKind kind
147 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
148 -- Removes variables that have now been bound.
149 -- Mainly used just before an error message is printed,
150 -- so that we don't need to follow through bound variables
151 -- during error message construction.
153 zonkTcKind TcTypeKind = returnNF_Tc TcTypeKind
155 zonkTcKind (TcArrowKind kind1 kind2)
156 = zonkTcKind kind1 `thenNF_Tc` \ k1 ->
157 zonkTcKind kind2 `thenNF_Tc` \ k2 ->
158 returnNF_Tc (TcArrowKind k1 k2)
160 zonkTcKind kind@(TcVarKind uniq box)
161 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
163 Nothing -> returnNF_Tc kind
164 Just kind' -> zonkTcKind kind'
169 instance Outputable (TcKind s) where
170 ppr sty kind = ppr_kind sty kind
172 ppr_kind sty TcTypeKind
174 ppr_kind sty (TcArrowKind kind1 kind2)
175 = ppSep [ppr_parend sty kind1, ppStr "->", ppr_kind sty kind2]
176 ppr_kind sty (TcVarKind uniq box)
177 = ppBesides [ppStr "k", pprUnique10 uniq]
179 ppr_parend sty kind@(TcArrowKind _ _) = ppBesides [ppChar '(', ppr_kind sty kind, ppChar ')']
180 ppr_parend sty other_kind = ppr_kind sty other_kind
188 unifyKindCtxt kind1 kind2 sty
189 = ppHang (ppStr "When unifying two kinds") 4
190 (ppSep [ppr sty kind1, ppStr "and", ppr sty kind2])
192 kindOccurCheck kind1 kind2 sty
193 = ppHang (ppStr "Cannot construct the infinite kind:") 4
194 (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
196 ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
197 ppStr "(\"occurs check\")"])
199 kindMisMatchErr kind1 kind2 sty
200 = ppHang (ppStr "Couldn't match the kind") 4
201 (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
203 ppBesides [ppStr "`", ppr sty kind1, ppStr "'"]