Mercurial > urweb
changeset 1742:fca4a6d05ac1
More diagnostic information about some type class resolution failures
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 04 May 2012 10:33:04 -0400 |
| parents | d6e233db97c8 |
| children | 1e940643a5f0 |
| files | src/elab_env.sig src/elab_env.sml src/elab_err.sml src/elaborate.sml tests/classFail.ur |
| diffstat | 5 files changed, 31 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sig Fri May 04 10:07:27 2012 -0400 +++ b/src/elab_env.sig Fri May 04 10:33:04 2012 -0400 @@ -73,6 +73,7 @@ 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
--- a/src/elab_env.sml Fri May 04 10:07:27 2012 -0400 +++ b/src/elab_env.sml Fri May 04 10:33:04 2012 -0400 @@ -678,13 +678,18 @@ | 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 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 @@ end in if startsWithUnif c then - NONE + notFound () else case #1 c of TRecord c => @@ -777,21 +782,22 @@ (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 =
--- a/src/elab_err.sml Fri May 04 10:07:27 2012 -0400 +++ b/src/elab_err.sml Fri May 04 10:33:04 2012 -0400 @@ -239,17 +239,10 @@ ("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),
--- a/src/elaborate.sml Fri May 04 10:07:27 2012 -0400 +++ b/src/elaborate.sml Fri May 04 10:33:04 2012 -0400 @@ -4676,7 +4676,13 @@ (!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