Saving proper environments, to use in displaying nested error messages

3 files changed, 90 insertions, 90 deletions

diff --git a/src/elab_err.sig b/src/elab_err.sig
index 14133d08..b5e3d64d 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -43,7 +43,7 @@ signature ELAB_ERR = sig
              UnboundCon of ErrorMsg.span * string
            | UnboundDatatype of ErrorMsg.span * string
            | UnboundStrInCon of ErrorMsg.span * string
-           | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
+           | WrongKind of Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error
            | DuplicateField of ErrorMsg.span * string
            | ProjBounds of Elab.con * int
            | ProjMismatch of Elab.con * Elab.kind
@@ -51,12 +51,12 @@ signature ELAB_ERR = sig
     val conError : ElabEnv.env -> con_error -> unit
 
     datatype cunify_error =
-             CKind of Elab.kind * Elab.kind * kunify_error
+             CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
            | COccursCheckFailed of Elab.con * Elab.con
            | CIncompatible of Elab.con * Elab.con
            | CExplicitness of Elab.con * Elab.con
            | CKindof of Elab.kind * Elab.con * string
-           | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option
+           | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option
            | TooLifty of ErrorMsg.span * ErrorMsg.span
            | TooUnify of Elab.con * Elab.con
            | TooDeep
@@ -67,12 +67,12 @@ signature ELAB_ERR = sig
     datatype exp_error =
              UnboundExp of ErrorMsg.span * string
            | UnboundStrInExp of ErrorMsg.span * string
-           | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
+           | Unify of Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error
            | Unif of string * ErrorMsg.span * Elab.con
            | WrongForm of string * Elab.exp * Elab.con
            | IncompatibleCons of Elab.con * Elab.con
            | DuplicatePatternVariable of ErrorMsg.span * string
-           | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
+           | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.env * cunify_error
            | UnboundConstructor of ErrorMsg.span * string list * string
            | PatHasArg of ErrorMsg.span
            | PatHasNoArg of ErrorMsg.span
@@ -94,13 +94,13 @@ signature ELAB_ERR = sig
     datatype sgn_error =
              UnboundSgn of ErrorMsg.span * string
            | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
-           | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
-           | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+           | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error
+           | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error
            | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
-                                       * (Elab.con * Elab.con * cunify_error) option
+                                       * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option
            | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
            | UnWhereable of Elab.sgn * string
-           | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
+           | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
            | NotIncludable of Elab.sgn
            | DuplicateCon of ErrorMsg.span * string
            | DuplicateVal of ErrorMsg.span * string
@@ -115,7 +115,7 @@ signature ELAB_ERR = sig
            | NotFunctor of Elab.sgn
            | FunctorRebind of ErrorMsg.span
            | UnOpenable of Elab.sgn
-           | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+           | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error)
            | DuplicateConstructor of string * ErrorMsg.span
            | NotDatatype of ErrorMsg.span
 
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 1951d971..f21ddce0 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2010, 2012, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -72,7 +72,7 @@ datatype con_error =
          UnboundCon of ErrorMsg.span * string
        | UnboundDatatype of ErrorMsg.span * string
        | UnboundStrInCon of ErrorMsg.span * string
-       | WrongKind of con * kind * kind * kunify_error
+       | WrongKind of con * kind * kind * E.env * kunify_error
        | DuplicateField of ErrorMsg.span * string
        | ProjBounds of con * int
        | ProjMismatch of con * kind
@@ -85,12 +85,12 @@ fun conError env err =
         ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
       | UnboundStrInCon (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound structure " ^ s)
-      | WrongKind (c, k1, k2, kerr) =>
+      | WrongKind (c, k1, k2, env', kerr) =>
         (ErrorMsg.errorAt (#2 c) "Wrong kind";
          eprefaces' [("Constructor", p_con env c),
                      ("Have kind", p_kind env k1),
                      ("Need kind", p_kind env k2)];
-         kunifyError env kerr)
+         kunifyError env' kerr)
       | DuplicateField (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
       | ProjBounds (c, n) =>
@@ -103,24 +103,24 @@ fun conError env err =
                      ("Kind", p_kind env k)])
 
 datatype cunify_error =
-         CKind of kind * kind * kunify_error
+         CKind of kind * kind * E.env * kunify_error
        | COccursCheckFailed of con * con
        | CIncompatible of con * con
        | CExplicitness of con * con
        | CKindof of kind * con * string
-       | CRecordFailure of con * con * (con * con * con * cunify_error option) option
+       | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option
        | TooLifty of ErrorMsg.span * ErrorMsg.span
        | TooUnify of con * con
        | TooDeep
        | CScope of con * con
 
-fun cunifyError env err =
+fun cunifyError env err : unit =
     case err of
-        CKind (k1, k2, kerr) =>
+        CKind (k1, k2, env', kerr) =>
         (eprefaces "Kind unification failure"
                    [("Have", p_kind env k1),
                     ("Need", p_kind env k2)];
-         kunifyError env kerr)
+         kunifyError env' kerr)
       | COccursCheckFailed (c1, c2) =>
         eprefaces "Constructor occurs check failed"
                   [("Have", p_con env c1),
@@ -148,7 +148,7 @@ fun cunifyError env err =
                              ("Value 1", p_con env t1),
                              ("Value 2", p_con env t2)]));
          case fo of
-             SOME (_, _, _, SOME err') => cunifyError env err'
+             SOME (_, _, _, SOME (env', err')) => cunifyError env' err'
            | _ => ())
       | TooLifty (loc1, loc2) =>
         (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
@@ -166,12 +166,12 @@ fun cunifyError env err =
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string
      | UnboundStrInExp of ErrorMsg.span * string
-     | Unify of exp * con * con * cunify_error
+     | Unify of exp * con * con * E.env * cunify_error
      | Unif of string * ErrorMsg.span * con
      | WrongForm of string * exp * con
      | IncompatibleCons of con * con
      | DuplicatePatternVariable of ErrorMsg.span * string
-     | PatUnify of pat * con * con * cunify_error
+     | PatUnify of pat * con * con * E.env * cunify_error
      | UnboundConstructor of ErrorMsg.span * string list * string
      | PatHasArg of ErrorMsg.span
      | PatHasNoArg of ErrorMsg.span
@@ -197,12 +197,12 @@ fun expError env err =
         ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
       | UnboundStrInExp (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound structure " ^ s)
-      | Unify (e, c1, c2, uerr) =>
+      | Unify (e, c1, c2, env', uerr) =>
         (ErrorMsg.errorAt (#2 e) "Unification failure";
          eprefaces' [("Expression", p_exp env e),
                      ("Have con", p_con env c1),
                      ("Need con", p_con env c2)];
-         cunifyError env uerr)
+         cunifyError env' uerr)
       | Unif (action, loc, c) =>
         (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
          eprefaces' [("Con", p_con env c)])
@@ -216,12 +216,12 @@ fun expError env err =
                      ("Need", p_con env c2)])
       | DuplicatePatternVariable (loc, s) =>
         ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
-      | PatUnify (p, c1, c2, uerr) =>
+      | PatUnify (p, c1, c2, env', uerr) =>
         (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
          eprefaces' [("Pattern", p_pat env p),
                      ("Have con", p_con env c1),
                      ("Need con", p_con env c2)];
-         cunifyError env uerr)
+         cunifyError env' uerr)
       | UnboundConstructor (loc, ms, s) =>
         ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
       | PatHasArg loc =>
@@ -329,13 +329,13 @@ fun declError env err =
 datatype sgn_error =
          UnboundSgn of ErrorMsg.span * string
        | UnmatchedSgi of ErrorMsg.span * sgn_item
-       | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error
-       | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error
+       | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error
+       | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error
        | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
-                                   * (con * con * cunify_error) option
+                                   * (con * con * E.env * cunify_error) option
        | SgnWrongForm of ErrorMsg.span * sgn * sgn
        | UnWhereable of sgn * string
-       | WhereWrongKind of kind * kind * kunify_error
+       | WhereWrongKind of kind * kind * E.env * kunify_error
        | NotIncludable of sgn
        | DuplicateCon of ErrorMsg.span * string
        | DuplicateVal of ErrorMsg.span * string
@@ -353,29 +353,29 @@ fun sgnError env err =
       | UnmatchedSgi (loc, sgi) =>
         (ErrorMsg.errorAt loc "Unmatched signature item";
          eprefaces' [("Item", p_sgn_item env sgi)])
-      | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) =>
+      | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) =>
         (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2),
                      ("Kind 1", p_kind env k1),
                      ("Kind 2", p_kind env k2)];
-         kunifyError env kerr)
-      | SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) =>
+         kunifyError env' kerr)
+      | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) =>
         (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2),
                      ("Con 1", p_con env c1),
                      ("Con 2", p_con env c2)];
-         cunifyError env cerr)
+         cunifyError env' cerr)
       | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
         (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
          eprefaces' [("Have", p_sgn_item env sgi1),
                      ("Need", p_sgn_item env sgi2)];
-         Option.app (fn (c1, c2, ue) =>
+         Option.app (fn (c1, c2, env', ue) =>
                         (eprefaces "Unification error"
-                                   [("Con 1", p_con env c1),
-                                    ("Con 2", p_con env c2)];
-                         cunifyError env ue)) cerro)
+                                   [("Con 1", p_con env' c1),
+                                    ("Con 2", p_con env' c2)];
+                         cunifyError env' ue)) cerro)
       | SgnWrongForm (loc, sgn1, sgn2) =>
         (ErrorMsg.errorAt loc "Incompatible signatures:";
          eprefaces' [("Sig 1", p_sgn env sgn1),
@@ -384,11 +384,11 @@ fun sgnError env err =
         (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
          eprefaces' [("Signature", p_sgn env sgn),
                      ("Field", PD.string x)])
-      | WhereWrongKind (k1, k2, kerr) =>
+      | WhereWrongKind (k1, k2, env', kerr) =>
         (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
          eprefaces' [("Have", p_kind env k1),
                      ("Need", p_kind env k2)];
-         kunifyError env kerr)
+         kunifyError env' kerr)
       | NotIncludable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
          eprefaces' [("Signature", p_sgn env sgn)])
@@ -409,7 +409,7 @@ datatype str_error =
        | NotFunctor of sgn
        | FunctorRebind of ErrorMsg.span
        | UnOpenable of sgn
-       | NotType of ErrorMsg.span * kind * (kind * kind * kunify_error)
+       | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error)
        | DuplicateConstructor of string * ErrorMsg.span
        | NotDatatype of ErrorMsg.span
 
@@ -425,12 +425,12 @@ fun strError env err =
       | UnOpenable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
          eprefaces' [("Signature", p_sgn env sgn)])
-      | NotType (loc, k, (k1, k2, ue)) =>
+      | NotType (loc, k, (k1, k2, env', ue)) =>
         (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
          eprefaces' [("Kind", p_kind env k),
                      ("Subkind 1", p_kind env k1),
                      ("Subkind 2", p_kind env k2)];
-         kunifyError env ue)
+         kunifyError env' ue)
       | DuplicateConstructor (x, loc) =>
         ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
       | NotDatatype loc =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a11787a9..1923390a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -86,11 +86,11 @@
 
  and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
 
- exception KUnify' of kunify_error
+ exception KUnify' of E.env * kunify_error
 
  fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
      let
-         fun err f = raise KUnify' (f (k1All, k2All))
+         fun err f = raise KUnify' (env, f (k1All, k2All))
      in
          case (k1, k2) of
              (L'.KType, L'.KType) => ()
@@ -179,16 +179,16 @@
            | _ => err KIncompatible
      end
 
- exception KUnify of L'.kind * L'.kind * kunify_error
+ exception KUnify of L'.kind * L'.kind * E.env * kunify_error
 
  fun unifyKinds env k1 k2 =
      unifyKinds' env k1 k2
-     handle KUnify' err => raise KUnify (k1, k2, err)
+     handle KUnify' (env', err) => raise KUnify (k1, k2, env', err)
 
  fun checkKind env c k1 k2 =
      unifyKinds env k1 k2
-     handle KUnify (k1, k2, err) =>
-            conError env (WrongKind (c, k1, k2, err))
+     handle KUnify (k1, k2, env', err) =>
+            conError env (WrongKind (c, k1, k2, env', err))
 
  val dummy = ErrorMsg.dummySpan
 
@@ -563,7 +563,7 @@
                    con = fn L'.CUnif (_, _, _, _, r') => r = r'
                           | _ => false}
 
- exception CUnify' of cunify_error
+ exception CUnify' of E.env * cunify_error
 
  type record_summary = {
       fields : (L'.con * L'.con) list,
@@ -589,7 +589,7 @@
 
  fun p_summary env s = p_con env (summaryToCon s)
 
- exception CUnify of L'.con * L'.con * cunify_error
+ exception CUnify of L'.con * L'.con * E.env * cunify_error
 
  fun kindof env (c, loc) =
      case c of
@@ -618,7 +618,7 @@
          (case hnormKind (kindof env c) of
               (L'.KArrow (_, k), _) => k
             | (L'.KError, _) => kerror
-            | k => raise CUnify' (CKindof (k, c, "arrow")))
+            | k => raise CUnify' (env, CKindof (k, c, "arrow")))
        | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
 
 
@@ -653,7 +653,7 @@
                        r := L'.KKnown k;
                        k
                    end)
-            | k => raise CUnify' (CKindof (k, c, "tuple")))
+            | k => raise CUnify' (env, CKindof (k, c, "tuple")))
 
        | L'.CError => kerror
        | L'.CUnif (_, _, k, _, _) => k
@@ -662,7 +662,7 @@
        | L'.CKApp (c, k) =>
          (case hnormKind (kindof env c) of
               (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
-            | k => raise CUnify' (CKindof (k, c, "kapp")))
+            | k => raise CUnify' (env, CKindof (k, c, "kapp")))
        | L'.TKFun _ => ktype
 
  exception GuessFailure
@@ -758,7 +758,7 @@
                      r := L'.KKnown (L'.KRecord k, #2 c);
                      k
                  end
-               | k => raise CUnify' (CKindof (k, c, "record"))
+               | k => raise CUnify' (env, CKindof (k, c, "record"))
 
          val k1 = rkindof c1
          val k2 = rkindof c2
@@ -987,10 +987,10 @@
                                  findPointwise fs1
                              else
                                  SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE)
-                                                    handle CUnify (_, _, err) => (reducedSummaries := NONE;
-                                                                                  SOME err))
+                                                    handle CUnify (_, _, env', err) => (reducedSummaries := NONE;
+                                                                                        SOME (env', err)))
              in
-                 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
+                 raise CUnify' (env, CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
              end
 
          fun default () = if !mayDelay then
@@ -1009,7 +1009,7 @@
               in
                   if occursCon r c then
                       (reducedSummaries := NONE;
-                       raise CUnify' (COccursCheckFailed (cr, c)))
+                       raise CUnify' (env, COccursCheckFailed (cr, c)))
                   else
                       let
                           val sq = squish nl c
@@ -1027,7 +1027,7 @@
               in
                   if occursCon r c then
                       (reducedSummaries := NONE;
-                       raise CUnify' (COccursCheckFailed (cr, c)))
+                       raise CUnify' (env, COccursCheckFailed (cr, c)))
                   else
                       let
                           val sq = squish nl c
@@ -1119,7 +1119,7 @@
 
  and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) =
      let
-         fun err f = raise CUnify' (f (c1All, c2All))
+         fun err f = raise CUnify' (env, f (c1All, c2All))
 
          fun projSpecial1 (c1, n1, onFail) =
              let
@@ -1344,18 +1344,18 @@
 
  and unifyCons env loc c1 c2 =
      unifyCons' env loc c1 c2
-     handle CUnify' err => raise CUnify (c1, c2, err)
-          | KUnify args => raise CUnify (c1, c2, CKind args)
+     handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
+          | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
 
  fun checkCon env e c1 c2 =
      unifyCons env (#2 e) c1 c2
-     handle CUnify (c1, c2, err) =>
-            expError env (Unify (e, c1, c2, err))
+     handle CUnify (c1, c2, env', err) =>
+            expError env (Unify (e, c1, c2, env', err))
 
  fun checkPatCon env p c1 c2 =
      unifyCons env (#2 p) c1 c2
-     handle CUnify (c1, c2, err) =>
-            expError env (PatUnify (p, c1, c2, err))
+     handle CUnify (c1, c2, env', err) =>
+            expError env (PatUnify (p, c1, c2, env', err))
 
  fun primType env p =
      case p of
@@ -2579,7 +2579,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
              val (env', n) = E.pushENamed env x c'
          in
              (unifyKinds env ck ktype
-              handle KUnify ue => strError env (NotType (loc, ck, ue)));
+              handle KUnify arg => strError env (NotType (loc, ck, arg)));
 
              ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
          end
@@ -3056,9 +3056,9 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                          if x = x' then
                                              let
                                                  val () = unifyKinds env k1 k2
-                                                     handle KUnify (k1, k2, err) =>
+                                                     handle KUnify (k1, k2, env', err) =>
                                                             sgnError env (SgiWrongKind (loc, sgi1All, k1,
-                                                                                        sgi2All, k2, err))
+                                                                                        sgi2All, k2, env', err))
                                                  val env = E.pushCNamedAs env x n1 k1 co1
                                              in
                                                  SOME (if n1 = n2 then
@@ -3125,9 +3125,9 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                              in
                                                  (unifyCons env loc c1 c2;
                                                   good ())
-                                                 handle CUnify (c1, c2, err) =>
+                                                 handle CUnify (c1, c2, env', err) =>
                                                         (sgnError env (SgiWrongCon (loc, sgi1All, c1,
-                                                                                    sgi2All, c2, err));
+                                                                                    sgi2All, c2, env', err));
                                                          good ())
                                              end
                                          else
@@ -3251,8 +3251,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                          in
                                              (unifyCons env loc t1 t2;
                                               good ())
-                                             handle CUnify (c1, c2, err) =>
-                                                    (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
+                                             handle CUnify (c1, c2, env', err) =>
+                                                    (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err));
                                                      good ())
                                          end
                                      else
@@ -3272,8 +3272,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                                           ("c2'", p_con env (sub2 c2))];*)
                                           unifyCons env loc c1 (sub2 c2);
                                           SOME env)
-                                         handle CUnify (c1, c2, err) =>
-                                                (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
+                                         handle CUnify (c1, c2, env', err) =>
+                                                (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err));
                                                  SOME env)
                                      else
                                          NONE
@@ -3340,9 +3340,9 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                          if x = x' then
                                              let
                                                  val () = unifyKinds env k1 k2
-                                                     handle KUnify (k1, k2, err) =>
+                                                     handle KUnify (k1, k2, env', err) =>
                                                             sgnError env (SgiWrongKind (loc, sgi1All, k1,
-                                                                                        sgi2All, k2, err))
+                                                                                        sgi2All, k2, env', err))
 
                                                  val env = E.pushCNamedAs env x n1 k1 co
                                              in
@@ -3367,9 +3367,9 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                          if x = x' then
                                              let
                                                  val () = unifyKinds env k1 k2
-                                                     handle KUnify (k1, k2, err) =>
+                                                     handle KUnify (k1, k2, env', err) =>
                                                             sgnError env (SgiWrongKind (loc, sgi1All, k1,
-                                                                                        sgi2All, k2, err))
+                                                                                        sgi2All, k2, env', err))
 
                                                  val c2 = sub2 c2
 
@@ -3387,9 +3387,9 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
                                              in
                                                  (unifyCons env loc c1 c2;
                                                   good ())
-                                                 handle CUnify (c1, c2, err) =>
+                                                 handle CUnify (c1, c2, env', err) =>
                                                         (sgnError env (SgiWrongCon (loc, sgi1All, c1,
-                                                                                    sgi2All, c2, err));
+                                                                                    sgi2All, c2, env', err));
                                                          good ())
                                              end
                                          else
@@ -4630,14 +4630,14 @@ fun elabFile basis topStr topSgn env file =
         else
             (app (fn (loc, env, k, s1, s2) =>
                      unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
-                     handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
-                                            cunifyError env err;
-                                            case !reducedSummaries of
-                                                NONE => ()
-                                              | SOME (s1, s2) =>
-                                                (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
-                                                 eprefaces' [("Have", s1),
-                                                             ("Need", s2)])))
+                     handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification";
+                                                    cunifyError env' err;
+                                                    case !reducedSummaries of
+                                                        NONE => ()
+                                                      | SOME (s1, s2) =>
+                                                        (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
+                                                         eprefaces' [("Have", s1),
+                                                                     ("Need", s2)])))
                  (!delayedUnifs);
              delayedUnifs := []);