Optionally (and by default) split typeclasses evars into connected

components and resolving them separately, reporting more precise failures. 
Improve error messages.


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

6 files changed, 111 insertions, 42 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4b078ff30..519aee85d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -258,7 +258,7 @@ let instances r =
   let cl = class_info r in instances_of cl
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
-let solve_instanciations_problem = ref (fun _ _ _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -415,10 +415,10 @@ let has_typeclasses evd =
 	&& is_resolvable evi))
     evd false
 
-let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env evd =
+let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs fail
+    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
 
 type substitution = (identifier * constr) list
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b12a85869..cb867a071 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -79,10 +79,10 @@ val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
 
-val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
-val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref
+val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
 
 type substitution = (identifier * constr) list
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index aed42aa04..72d23946c 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -28,7 +28,7 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs
+    | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -41,10 +41,14 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
 let no_instance env id args = typeclass_error env (NoInstance (id, args))
 
-let unsatisfiable_constraints env evd = 
+let unsatisfiable_constraints env evd ev = 
   let evd = Evd.undefined_evars evd in
-  let ev = List.hd (Evd.dom (Evd.evars_of evd)) in
-  let loc, _ = Evd.evar_source ev evd in
-    raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints evd)))
-
+    match ev with
+    | None ->
+	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
+    | 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)))))
+	    
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index d93a354ec..df196ae4c 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -28,7 +28,7 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs
+    | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -39,6 +39,6 @@ val unbound_method : env -> global_reference -> identifier located -> 'a
 
 val no_instance : env -> identifier located -> constr list -> 'a
 
-val unsatisfiable_constraints : env -> evar_defs -> 'a
+val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 37fe7c3c8..46faee195 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -417,19 +417,81 @@ let has_undefined p oevd evd =
     (evi.evar_body = Evar_empty && p ev evi && 
 	(try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true)))
     (Evd.evars_of evd) false
-    
-let resolve_all_evars debug m env p oevd =
+
+let evars_of_term init c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) -> Intset.add n acc
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec init c
+
+let intersects s t =
+  Intset.exists (fun el -> Intset.mem el t) s
+
+let rec merge_deps deps = function
+  | [] -> [deps]
+  | hd :: tl -> 
+      if intersects deps hd then 
+	merge_deps (Intset.union deps hd) tl
+      else hd :: merge_deps deps tl
+	
+let split_evars evm =
+  Evd.fold (fun ev evi acc ->
+    let deps = evars_of_term (Intset.singleton ev) evi.evar_concl in
+      merge_deps deps acc)
+    evm []
+
+let select_evars evs evm =
+  Evd.fold (fun ev evi acc ->
+    if Intset.mem ev evs then Evd.add acc ev evi else acc)
+    evm Evd.empty
+
+let resolve_all_evars debug m env p oevd do_split fail =
   let oevm = Evd.evars_of oevd in
-  try
-    let rec aux n evd =
-      if has_undefined p oevm evd then
-	if n > 0 then
-	  let evd' = resolve_all_evars_once debug m env p evd in
-	    aux (pred n) evd'
-	else None
-      else Some evd
-    in aux 3 oevd
-  with Not_found -> None
+  let split = if do_split then split_evars (Evd.evars_of (Evd.undefined_evars oevd)) else [Intset.empty] in
+  let p = if do_split then fun comp ev evi -> Intset.mem ev comp && p ev evi else fun _ -> p in
+  let rec aux n p evd =
+    if has_undefined p oevm evd then
+      if n > 0 then
+	let evd' = resolve_all_evars_once debug m env p evd in
+	  aux (pred n) p evd'
+      else None
+    else Some evd
+  in 
+  let rec docomp evd = function
+    | [] -> evd
+    | comp :: comps ->
+	let res = try aux 3 (p comp) evd with Not_found -> None in
+	  match res with
+	  | None -> 
+	      if fail then 
+		(* 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
+		in
+		  Typeclasses_errors.unsatisfiable_constraints env (Evd.evars_reset_evd evm evd) ev
+	      else (* Best effort: do nothing *) oevd
+	  | Some evd' -> docomp evd' comps
+  in docomp oevd split
+
+(* let resolve_all_evars debug m env p oevd = *)
+(*   let oevm = Evd.evars_of oevd in *)
+(*   try *)
+(*     let rec aux n evd = *)
+(*       if has_undefined p oevm evd then *)
+(* 	if n > 0 then *)
+(* 	  let evd' = resolve_all_evars_once debug m env p evd in *)
+(* 	    aux (pred n) evd' *)
+(* 	else None *)
+(*       else Some evd *)
+(*     in aux 3 oevd *)
+(*   with Not_found -> None *)
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "unfold" reference_list(cl) ] -> [
@@ -907,14 +969,14 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars =
   if rest <> [] then error_invalid_occurrence rest;
   eq
     
-let resolve_typeclass_evars d p env evd onlyargs =
+let resolve_typeclass_evars d p env evd onlyargs split fail =
   let pred = 
     if onlyargs then 
       (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) &&
 	class_of_constr evi.Evd.evar_concl <> None)
     else
       (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
-  in resolve_all_evars d p env pred evd
+  in resolve_all_evars d p env pred evd split fail
       
 let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
   let concl, is_hyp = 
@@ -935,7 +997,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
     match eq with  
     | Some (p, (_, _, oldt, newt)) -> 
 	(try 
-	  evars := Typeclasses.resolve_typeclasses env ~fail:true !evars;
+	  evars := Typeclasses.resolve_typeclasses env ~split:false ~fail:true !evars;
 	  let p = Evarutil.nf_isevar !evars p in
 	  let newt = Evarutil.nf_isevar !evars newt in
 	  let undef = Evd.undefined_evars !evars in
@@ -1055,14 +1117,8 @@ ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
 | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
 END
 	
-let solve_inst debug mode depth env evd onlyargs fail =
-  match resolve_typeclass_evars debug (mode, depth) env evd onlyargs with 
-    | None -> 
-	if fail then 
-	  (* Unable to satisfy the constraints. *)
-	  Typeclasses_errors.unsatisfiable_constraints env evd
-	else (* Best effort: do nothing *) evd
-    | Some evd -> evd
+let solve_inst debug mode depth env evd onlyargs split fail =
+  resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail
 
 let _ = 
   Typeclasses.solve_instanciations_problem :=
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3d0691b18..0a35673c1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -286,7 +286,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       strbrk " not in guarded form (should be a constructor," ++
       strbrk " an abstraction, a match, a cofix or a recursive call)"
   in
-  let pvd, pvdt = pr_ljudge_env fixenv vdefj.(i) in
+  let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in
   prt_name i ++ str " is ill-formed." ++ fnl () ++
   pr_ne_context_of (str "In environment") env ++
   st ++ str "." ++ fnl () ++
@@ -505,10 +505,19 @@ let explain_no_instance env (_,id) l =
   str "applied to arguments" ++ spc () ++ 
     prlist_with_sep pr_spc (pr_lconstr_env env) l
 
-let explain_unsatisfiable_constraints env evd =
-  str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
-    Evd.pr_evar_map (Evd.evars_of (Evd.undefined_evars evd))
-
+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
+  | 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:" ++ 
+	    fnl() ++ Evd.pr_evar_map evm 
+	else mt ()
+	
 let explain_mismatched_contexts env c i j = 
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
     hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ 
@@ -519,7 +528,7 @@ let explain_typeclass_error env err =
     | NotAClass c -> explain_not_a_class env c
     | UnboundMethod (cid, id) -> explain_unbound_method env cid id
     | NoInstance (id, l) -> explain_no_instance env id l
-    | UnsatisfiableConstraints evm -> explain_unsatisfiable_constraints env evm
+    | UnsatisfiableConstraints (evd, c) -> explain_unsatisfiable_constraints env evd c
     | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
 	
 (* Refiner errors *)