Better typeclass error messages, always giving the full set of

unsatisfiable constraints.
Add a resolution call in tacinterp before trying the default tactic.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 55 insertions, 23 deletions

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 72d23946cb..0907760189 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -49,6 +49,7 @@ let unsatisfiable_constraints env evd ev =
     | Some ev ->
 	let evi = Evd.find (Evd.evars_of evd) ev in
 	let loc, kind = Evd.evar_source ev evd in
-	  raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
+	  raise (Stdpp.Exc_located (loc, TypeClassError
+	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
 	    
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 46faee195d..ad627c8418 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -469,11 +469,14 @@ let resolve_all_evars debug m env p oevd do_split fail =
 		(* Unable to satisfy the constraints. *)
 		let evm = Evd.evars_of evd in
 		let evm = if do_split then select_evars comp evm else evm in
-		let ev = Evd.fold 
-		  (fun ev evi acc -> 
-		    if acc = None then
-		      if class_of_constr evi.evar_concl <> None then Some ev else None 
-		    else acc) evm None
+		let _, ev = Evd.fold 
+		  (fun ev evi (b,acc) -> 
+		    (* focus on one instance if only one was searched for *)
+		    if class_of_constr evi.evar_concl <> None then
+		      if not b then
+			true, Some ev 
+		      else b, None
+		    else b, acc) evm (false, None)
 		in
 		  Typeclasses_errors.unsatisfiable_constraints env (Evd.evars_reset_evd evm evd) ev
 	      else (* Best effort: do nothing *) oevd
@@ -1654,18 +1657,32 @@ TACTIC EXTEND try_classes
   [ "try_classes" tactic(t) ] -> [ try_classes (snd t) ]
 END
 
-(* let lift_monad env t = *)
-(*   match kind_of_term t with *)
-(*     | Rel n -> t *)
-(*     | Var id -> t *)
-(*     | App (f, args) -> *)
-(* 	let args' =  *)
-(* 	  List.fold_right *)
-(* 	    (fun arg acc -> *)
-(* 	      let ty = Typing.type_of env arg in *)
-(* 	      let arg' = lift_monad t in *)
-(* 		monad_bind arg'  *)
-(* 		  (mkLambda (Name (id_of_string "x"),  *)
-			    
-			    
+open Rawterm
+
+let constrexpr = Pcoq.Tactic.open_constr
+type 'a constr_expr_argtype = (open_constr_expr, 'a) Genarg.abstract_argument_type
+
+let (wit_constrexpr : Genarg.tlevel constr_expr_argtype),
+  (globwit_constrexpr : Genarg.glevel constr_expr_argtype),
+  (rawwit_const_expr : Genarg.rlevel constr_expr_argtype) =
+  Genarg.create_arg "constrexpr"
 			    
+open Environ
+open Refiner
+
+TACTIC EXTEND apply_typeclasses
+   [ "app" raw(t) ] -> [ fun gl ->
+     let nprod = nb_prod (pf_concl gl) in
+     let env = pf_env gl in
+     let evars = ref (create_evar_defs (project gl)) in
+     let j = Pretyping.Default.understand_judgment_tcc evars env t in
+     let n = nb_prod j.uj_type - nprod in
+       if n<0 then error "Apply_tc: theorem has not enough premisses.";
+       Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !evars))
+	 (fun gl ->
+	   let clause = make_clenv_binding_apply gl (Some n) (j.uj_val,j.uj_type) NoBindings in
+	   let cl' = evar_clenv_unique_resolver true ~flags:default_unify_flags clause gl in
+	   let evd' = Typeclasses.resolve_typeclasses cl'.env ~fail:true cl'.evd in
+	     Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl
+   ]
+END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 309aef8076..836427c432 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1408,7 +1408,7 @@ let solvable_by_tactic env evi (ev,args) src =
   | _ -> raise Exit
 
 let solve_remaining_evars env initial_sigma evd c =
-  let evdref = ref evd in
+  let evdref = ref (Typeclasses.resolve_typeclasses ~fail:true env evd) in
   let rec proc_rec c =
     match kind_of_term (Reductionops.whd_evar (evars_of !evdref) c) with
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 787e43c15d..dc9b624fbf 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -507,16 +507,30 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++ 
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
+let pr_constraints env evm =
+  let l = Evd.to_list evm in
+  let (ev, evi) = List.hd l in
+    if List.for_all (fun (ev', evi') ->
+      eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
+    then
+      let pe = pr_ne_context_of (str "In environment:") (mt ()) 
+	(reset_with_named_context evi.evar_hyps env) in
+	pe ++ fnl () ++ 
+	  prlist_with_sep (fun () -> fnl ()) 
+	  (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
+    else
+      pr_evar_map evm
+      
 let explain_unsatisfiable_constraints env evd constr =
   let evm = Evd.evars_of evd in
   match constr with
   | None ->
       str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
-	Evd.pr_evar_map evm
+	pr_constraints env evm
   | Some (evi, k) -> 
       explain_unsolvable_implicit env evi k None ++ fnl () ++
 	if List.length (Evd.to_list evm) > 1 then
-	  str"With the following typeclass constraints:" ++ 
+	  str"With the following meta variables:" ++ 
 	    fnl() ++ Evd.pr_evar_map evm 
 	else mt ()