diff src/elab_err.sml @ 1306:3a845f2ce9e9

:::_ 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
line wrap: on
line diff
--- a/src/elab_err.sml	Sun Oct 10 15:54:51 2010 -0400
+++ b/src/elab_err.sml	Sun Oct 10 20:33:10 2010 -0400
@@ -121,6 +121,7 @@
        | 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 @@
         (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