summaryrefslogtreecommitdiff
path: root/src/elab_err.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-23 11:23:31 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-23 11:23:31 -0500
commit867a11af44827af8974250e6dbb5e96b6268b44f (patch)
treefcdcc73abd3ef7b68fe8a02e5b11901e0fec5c92 /src/elab_err.sml
parent17ecbd235ad9b7692dfc029329fb13103eb55d9c (diff)
Recursive record unification errors, for more detail
Diffstat (limited to 'src/elab_err.sml')
-rw-r--r--src/elab_err.sml23
1 files changed, 13 insertions, 10 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 7d5e6be8..a03bc096 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -118,7 +118,7 @@ datatype cunify_error =
| CIncompatible of con * con
| CExplicitness of con * con
| CKindof of kind * con * string
- | CRecordFailure of con * con * (con * con * con) option
+ | CRecordFailure of con * con * (con * con * con * cunify_error option) option
| TooLifty of ErrorMsg.span * ErrorMsg.span
| TooUnify of con * con
| TooDeep
@@ -147,15 +147,18 @@ fun cunifyError env err =
[("Kind", p_kind env k),
("Con", p_con env c)]
| CRecordFailure (c1, c2, fo) =>
- eprefaces "Can't unify record constructors"
- (("Summary 1", p_con env c1)
- :: ("Summary 2", p_con env c2)
- :: (case fo of
- NONE => []
- | SOME (nm, t1, t2) =>
- [("Field", p_con env nm),
- ("Value 1", p_con env t1),
- ("Value 2", p_con env t2)]))
+ (eprefaces "Can't unify record constructors"
+ (("Summary 1", p_con env c1)
+ :: ("Summary 2", p_con env c2)
+ :: (case fo of
+ NONE => []
+ | SOME (nm, t1, t2, _) =>
+ [("Field", p_con env nm),
+ ("Value 1", p_con env t1),
+ ("Value 2", p_con env t2)]));
+ case fo of
+ SOME (_, _, _, SOME err') => cunifyError env err'
+ | _ => ())
| TooLifty (loc1, loc2) =>
(ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])