# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1336141984 14400
# Node ID fca4a6d05ac1098149380319e4caf78e3951f32f
# Parent  d6e233db97c869d95eaafb3d9d988558ac539608
More diagnostic information about some type class resolution failures

diff -r d6e233db97c8 -r fca4a6d05ac1 src/elab_env.sig
--- 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
diff -r d6e233db97c8 -r fca4a6d05ac1 src/elab_env.sml
--- 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 =
diff -r d6e233db97c8 -r fca4a6d05ac1 src/elab_err.sml
--- 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),
diff -r d6e233db97c8 -r fca4a6d05ac1 src/elaborate.sml
--- 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
diff -r d6e233db97c8 -r fca4a6d05ac1 tests/classFail.ur
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/classFail.ur	Fri May 04 10:33:04 2012 -0400
@@ -0,0 +1,3 @@
+val x = show 7
+val y = show (8, 9)
+val z : (show int * show unit) = _