4 Kind, mkTypeKind, mkBoxedTypeKind, mkUnboxedTypeKind, mkArrowKind,
5 hasMoreBoxityInfo, -- 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 tcDefaultKind -- TcKind s -> NF_TcM s Kind
18 import TcMonad hiding ( rnMtoTcM )
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 kind2
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 -- Default all unbound kinds to TcTypeKind, and return the
131 -- corresponding Kind as well.
132 tcDefaultKind :: TcKind s -> NF_TcM s Kind
134 tcDefaultKind TcTypeKind
135 = returnNF_Tc BoxedTypeKind
137 tcDefaultKind (TcArrowKind kind1 kind2)
138 = tcDefaultKind kind1 `thenNF_Tc` \ k1 ->
139 tcDefaultKind kind2 `thenNF_Tc` \ k2 ->
140 returnNF_Tc (ArrowKind k1 k2)
142 -- Here's where we "default" unbound kinds to BoxedTypeKind
143 tcDefaultKind (TcVarKind uniq box)
144 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
146 Just kind -> tcDefaultKind kind
148 Nothing -> -- Default unbound variables to kind Type
149 tcWriteMutVar box (Just TcTypeKind) `thenNF_Tc_`
150 returnNF_Tc BoxedTypeKind
152 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
153 -- Removes variables that have now been bound.
154 -- Mainly used just before an error message is printed,
155 -- so that we don't need to follow through bound variables
156 -- during error message construction.
158 zonkTcKind TcTypeKind = returnNF_Tc TcTypeKind
160 zonkTcKind (TcArrowKind kind1 kind2)
161 = zonkTcKind kind1 `thenNF_Tc` \ k1 ->
162 zonkTcKind kind2 `thenNF_Tc` \ k2 ->
163 returnNF_Tc (TcArrowKind k1 k2)
165 zonkTcKind kind@(TcVarKind uniq box)
166 = tcReadMutVar box `thenNF_Tc` \ maybe_kind ->
168 Nothing -> returnNF_Tc kind
169 Just kind' -> zonkTcKind kind'
174 instance Outputable (TcKind s) where
175 ppr sty kind = ppr_kind sty kind
177 ppr_kind sty TcTypeKind
179 ppr_kind sty (TcArrowKind kind1 kind2)
180 = ppSep [ppr_parend sty kind1, ppStr "->", ppr_kind sty kind2]
181 ppr_kind sty (TcVarKind uniq box)
182 = ppBesides [ppStr "k", pprUnique10 uniq]
184 ppr_parend sty kind@(TcArrowKind _ _) = ppBesides [ppChar '(', ppr_kind sty kind, ppChar ')']
185 ppr_parend sty other_kind = ppr_kind sty other_kind
193 unifyKindCtxt kind1 kind2 sty
194 = ppHang (ppStr "When unifying two kinds") 4
195 (ppSep [ppr sty kind1, ppStr "and", ppr sty kind2])
197 kindOccurCheck kind1 kind2 sty
198 = ppHang (ppStr "Cannot construct the infinite kind:") 4
199 (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
201 ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
202 ppStr "(\"occurs check\")"])
204 kindMisMatchErr kind1 kind2 sty
205 = ppHang (ppStr "Couldn't match the kind") 4
206 (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
208 ppBesides [ppStr "`", ppr sty kind2, ppStr "'"]