summaryrefslogtreecommitdiff
path: root/src/elab_err.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 20:33:10 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 20:33:10 -0400
commit4e608544ebe87dd991d53ded5267f14f5df93b8b (patch)
tree4de957d9837f39c79ebc56b5ac2935e31a28d0b5 /src/elab_err.sml
parent42d55420b84994ee61c0a4645d21d275dbbea2cd (diff)
:::_ notation; switch to TooDeep error message
Diffstat (limited to 'src/elab_err.sml')
-rw-r--r--src/elab_err.sml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml
index f8a16294..7d5e6be8 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -121,6 +121,7 @@ datatype cunify_error =
| CRecordFailure of con * con * (con * con * con) option
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of con * con
+ | TooDeep
fun cunifyError env err =
case err of
@@ -162,6 +163,7 @@ fun cunifyError env err =
(ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
eprefaces' [("Replacement", p_con env c1),
("Body", p_con env c2)])
+ | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
datatype exp_error =
UnboundExp of ErrorMsg.span * string