Mercurial > urweb

comparison src/elab_err.sml @ 1306:3a845f2ce9e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
:::_ notation; switch to TooDeep error message
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 20:33:10 -0400
parents c7b9a33c26c8
children e525ad571e15
comparison
equal deleted inserted replaced
1305:a6fc03d28170 1306:3a845f2ce9e9
119 | CExplicitness of con * con 119 | CExplicitness of con * con
120 | CKindof of kind * con * string 120 | CKindof of kind * con * string
121 | CRecordFailure of con * con * (con * con * con) option 121 | CRecordFailure of con * con * (con * con * con) option
122 | TooLifty of ErrorMsg.span * ErrorMsg.span 122 | TooLifty of ErrorMsg.span * ErrorMsg.span
123 | TooUnify of con * con 123 | TooUnify of con * con
124 | TooDeep
124 125
125 fun cunifyError env err = 126 fun cunifyError env err =
126 case err of 127 case err of
127 CKind (k1, k2, kerr) => 128 CKind (k1, k2, kerr) =>
128 (eprefaces "Kind unification failure" 129 (eprefaces "Kind unification failure"
160 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) 161 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
161 | TooUnify (c1, c2) => 162 | TooUnify (c1, c2) =>
162 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; 163 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
163 eprefaces' [("Replacement", p_con env c1), 164 eprefaces' [("Replacement", p_con env c1),
164 ("Body", p_con env c2)]) 165 ("Body", p_con env c2)])
166 | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
165 167
166 datatype exp_error = 168 datatype exp_error =
167 UnboundExp of ErrorMsg.span * string 169 UnboundExp of ErrorMsg.span * string
168 | UnboundStrInExp of ErrorMsg.span * string 170 | UnboundStrInExp of ErrorMsg.span * string
169 | Unify of exp * con * con * cunify_error 171 | Unify of exp * con * con * cunify_error