summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-04 10:33:04 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-04 10:33:04 -0400
commit581037b5cf9defbcf1412046e1cd1b8fb02d3d43 (patch)
treee52dfe5be4f5e8033c784ee197b5980006771472
parent8b1eaab4e930cb8c23d731c606137e118d9c8d42 (diff)
More diagnostic information about some type class resolution failures
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml26
-rw-r--r--src/elab_err.sml15
-rw-r--r--src/elaborate.sml8
-rw-r--r--tests/classFail.ur3
5 files changed, 31 insertions, 22 deletions
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) = _