Mercurial > urweb

comparison src/elab_err.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents c37d8341940a
children d6c45026240d
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
61 ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) 61 ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
62 62
63 datatype kunify_error = 63 datatype kunify_error =
64 KOccursCheckFailed of kind * kind 64 KOccursCheckFailed of kind * kind
65 | KIncompatible of kind * kind 65 | KIncompatible of kind * kind
66 | KScope of kind * kind
66 67
67 fun kunifyError env err = 68 fun kunifyError env err =
68 case err of 69 case err of
69 KOccursCheckFailed (k1, k2) => 70 KOccursCheckFailed (k1, k2) =>
70 eprefaces "Kind occurs check failed" 71 eprefaces "Kind occurs check failed"
72 ("Kind 2", p_kind env k2)] 73 ("Kind 2", p_kind env k2)]
73 | KIncompatible (k1, k2) => 74 | KIncompatible (k1, k2) =>
74 eprefaces "Incompatible kinds" 75 eprefaces "Incompatible kinds"
75 [("Kind 1", p_kind env k1), 76 [("Kind 1", p_kind env k1),
76 ("Kind 2", p_kind env k2)] 77 ("Kind 2", p_kind env k2)]
77 78 | KScope (k1, k2) =>
79 eprefaces "Scoping prevents kind unification"
80 [("Kind 1", p_kind env k1),
81 ("Kind 2", p_kind env k2)]
78 82
79 fun p_con env c = P.p_con env (simplCon env c) 83 fun p_con env c = P.p_con env (simplCon env c)
80 84
81 datatype con_error = 85 datatype con_error =
82 UnboundCon of ErrorMsg.span * string 86 UnboundCon of ErrorMsg.span * string
120 | CKindof of kind * con * string 124 | CKindof of kind * con * string
121 | CRecordFailure of con * con * (con * con * con * cunify_error option) option 125 | CRecordFailure of con * con * (con * con * con * cunify_error option) option
122 | TooLifty of ErrorMsg.span * ErrorMsg.span 126 | TooLifty of ErrorMsg.span * ErrorMsg.span
123 | TooUnify of con * con 127 | TooUnify of con * con
124 | TooDeep 128 | TooDeep
129 | CScope of con * con
125 130
126 fun cunifyError env err = 131 fun cunifyError env err =
127 case err of 132 case err of
128 CKind (k1, k2, kerr) => 133 CKind (k1, k2, kerr) =>
129 (eprefaces "Kind unification failure" 134 (eprefaces "Kind unification failure"
165 | TooUnify (c1, c2) => 170 | TooUnify (c1, c2) =>
166 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; 171 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
167 eprefaces' [("Replacement", p_con env c1), 172 eprefaces' [("Replacement", p_con env c1),
168 ("Body", p_con env c2)]) 173 ("Body", p_con env c2)])
169 | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting" 174 | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
175 | CScope (c1, c2) =>
176 eprefaces "Scoping prevents constructor unification"
177 [("Have", p_con env c1),
178 ("Need", p_con env c2)]
170 179
171 datatype exp_error = 180 datatype exp_error =
172 UnboundExp of ErrorMsg.span * string 181 UnboundExp of ErrorMsg.span * string
173 | UnboundStrInExp of ErrorMsg.span * string 182 | UnboundStrInExp of ErrorMsg.span * string
174 | Unify of exp * con * con * cunify_error 183 | Unify of exp * con * con * cunify_error