summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 14:57:00 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 14:57:00 -0400
commitd1898695cba6c924456d7de4d1b700072310f752 (patch)
tree3a57d1a9c42edb747baa7d2207cb097191044abb /src
parentf87820a0554612aec1fc2965740febef3695b0bd (diff)
Saving proper environments, to use in displaying nested error messages
Diffstat (limited to 'src')
-rw-r--r--src/elab_err.sig20
-rw-r--r--src/elab_err.sml66
-rw-r--r--src/elaborate.sml94
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 := []);