From 867a11af44827af8974250e6dbb5e96b6268b44f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Dec 2010 11:23:31 -0500 Subject: Recursive record unification errors, for more detail --- src/elab_err.sml | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) (limited to 'src/elab_err.sml') 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))]) -- cgit v1.2.3