From 802fc606ff18c261eb591d7ae6dbb99fe9c48af9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 4 May 2012 10:33:04 -0400 Subject: More diagnostic information about some type class resolution failures --- src/elab_env.sig | 1 + src/elab_env.sml | 26 ++++++++++++++++---------- src/elab_err.sml | 15 ++++----------- src/elaborate.sml | 8 +++++++- tests/classFail.ur | 3 +++ 5 files changed, 31 insertions(+), 22 deletions(-) create mode 100644 tests/classFail.ur diff --git a/src/elab_env.sig b/src/elab_env.sig index 662d7071..e0c589c4 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -73,6 +73,7 @@ signature ELAB_ENV = sig val isClass : env -> Elab.con -> bool val resolveClass : (Elab.con -> Elab.con) -> (Elab.con * Elab.con -> bool) -> env -> Elab.con -> Elab.exp option + val resolveFailureCause : unit -> Elab.con option val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list val pushERel : env -> string -> Elab.con -> env diff --git a/src/elab_env.sml b/src/elab_env.sml index ed96782e..bf0808f5 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -678,13 +678,18 @@ fun startsWithUnif c = | SOME x => hasUnif x end +val cause = ref (NONE : con option) +fun resolveFailureCause () = !cause + fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = let - fun resolve c = + fun resolve firstLevel c = let + fun notFound () = (if firstLevel then () else cause := SOME c; NONE) + fun doHead f = case CM.find (#classes env, f) of - NONE => NONE + NONE => notFound () | SOME class => let val loc = #2 c @@ -722,13 +727,13 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = fun tryRules rules = case rules of - [] => NONE + [] => notFound () | (nRs, cs, c', e) :: rules' => case tryUnify hnorm nRs (c, c') of NONE => tryRules rules' | SOME rs => let - val eos = map (resolve o unifySubst rs) cs + val eos = map (resolve false o unifySubst rs) cs in if List.exists (not o Option.isSome) eos orelse not (equate ()) @@ -759,7 +764,7 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = end in if startsWithUnif c then - NONE + notFound () else case #1 c of TRecord c => @@ -777,21 +782,22 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) | _ => t in - case resolve t of - NONE => NONE + case resolve false t of + NONE => notFound () | SOME e => resolver (xts, (x, e, t) :: acc) end in resolver (xts, []) end - | _ => NONE) + | _ => notFound ()) | _ => case class_head_in c of SOME f => doHead f - | _ => NONE + | _ => notFound () end in - resolve + cause := NONE; + resolve true end fun pushERel (env : env) x t = diff --git a/src/elab_err.sml b/src/elab_err.sml index f21ddce0..0e04cf51 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -239,17 +239,10 @@ fun expError env err = ("Type", p_con env c)]) co) | Unresolvable (loc, c) => (ErrorMsg.errorAt loc "Can't resolve type class instance"; - eprefaces' [("Class constraint", p_con env c)(*, - ("Class database", p_list (fn (c, rules) => - box [P.p_con env c, - PD.string ":", - space, - p_list (fn (c, e) => - box [p_exp env e, - PD.string ":", - space, - P.p_con env c]) rules]) - (E.listClasses env))*)]) + eprefaces' ([("Class constraint", p_con env c)] + @ (case E.resolveFailureCause () of + NONE => [] + | SOME c' => [("Reduced to unresolvable", p_con env c')]))) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff --git a/src/elaborate.sml b/src/elaborate.sml index f098b580..5799d6bb 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4676,7 +4676,13 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = (!delayedUnifs);*) end | TypeClass (env, c, r, loc) => - expError env (Unresolvable (loc, c))) + let + val c = normClassKey env c + in + case resolveClass env c of + SOME _ => raise Fail "Type class resolution succeeded unexpectedly" + | NONE => expError env (Unresolvable (loc, c)) + end) gs) end in diff --git a/tests/classFail.ur b/tests/classFail.ur new file mode 100644 index 00000000..dd7b66e9 --- /dev/null +++ b/tests/classFail.ur @@ -0,0 +1,3 @@ +val x = show 7 +val y = show (8, 9) +val z : (show int * show unit) = _ -- cgit v1.2.3