Fix interface of resolve_typeclasses: onlyargs -> with_goals:

by default typeclass resolution is not launched on goal evars.

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

14 files changed, 107 insertions, 104 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 327745616..560b61546 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -323,7 +323,7 @@ let coerce_itf loc env isevars v t c1 =
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~onlyargs:true ~split:true ~fail:false env evd
+    ~with_goals:false ~split:true ~fail:false env evd
 
 (* appliquer le chemin de coercions p à hj *)
 let apply_coercion env sigma p hj typ_cl =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d96f47e3f..0205a52d5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -105,10 +105,8 @@ let interp_elimination_sort = function
 
 let resolve_evars env evdref fail_evar resolve_classes =
   if resolve_classes then
-    (evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
-       ~split:true ~fail:true env !evdref;
-     evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-       ~split:true ~fail:fail_evar env !evdref);
+    (evdref := Typeclasses.resolve_typeclasses ~with_goals:false
+     ~split:true ~fail:fail_evar env !evdref);
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index be335ac91..e6005391d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -451,11 +451,11 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg k =
-  match k with
-      ImplicitArg (ref, (n, id), b) -> true
-    | InternalHole -> true
-    | _ -> false
+let is_implicit_arg k = k <> GoalEvar
+  (* match k with *)
+  (*     ImplicitArg (ref, (n, id), b) -> true *)
+  (*   | InternalHole -> true *)
+  (*   | _ -> false *)
 
 
 (* To embed a boolean for resolvability status.
@@ -500,6 +500,6 @@ let has_typeclasses evd =
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 
-let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
+let resolve_typeclasses ?(with_goals=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses evd) then evd
-  else !solve_instanciations_problem env evd onlyargs split fail
+  else !solve_instanciations_problem env evd with_goals split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 67336b340..b1db243d6 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -80,7 +80,7 @@ val is_implicit_arg : hole_kind -> bool
 val instance_constructor : typeclass -> constr list -> constr option * types
 
 (** Resolvability.
-    Only undefined evars could be marked or checked for resolvability. *)
+    Only undefined evars can be marked or checked for resolvability. *)
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
@@ -89,7 +89,7 @@ val mark_resolvable : evar_info -> evar_info
 val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
+val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 983b9fd61..ce0af6853 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -966,7 +966,7 @@ let check_types env flags (sigma,_,_ as subst) m n =
 
 let try_resolve_typeclasses env evd flags m n =
   if flags.resolve_evars then
-    try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+    try Typeclasses.resolve_typeclasses ~with_goals:false ~split:false
 	  ~fail:true env evd
     with e when Typeclasses_errors.unsatisfiable_exception e ->
       error_cannot_unify env evd (m, n)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 45765805f..3eb665088 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,8 +72,8 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
-      Typeclasses.resolve_typeclasses ~fail:(not with_evars)
-	clenv.env clenv.evd
+      Typeclasses.resolve_typeclasses ~with_goals:true
+        ~fail:(not with_evars) clenv.env clenv.evd
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 68f49d900..37bb96de7 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -162,8 +162,8 @@ module Refinable = struct
   (* spiwack: it is not very fine grain since it solves all typeclasses holes,
       not only those containing the current goal, or a given term. But it
       seems to fit our needs so far. *)
-  let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
-    rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs;
+  let resolve_typeclasses ?with_goals ?split ?(fail=false) () env rdefs _ _ =
+    rdefs:=Typeclasses.resolve_typeclasses ?with_goals ?split ~fail env !rdefs;
     ()
 
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 9219d4a49..d67a6b12f 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -72,7 +72,7 @@ module Refinable : sig
   (* [with_type c typ] constrains term [c] to have type [typ].  *)
   val with_type : Term.constr -> Term.types -> Term.constr sensitive
 
-  val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+  val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
 
 
   (* [constr_of_raw h check_type resolve_classes] is a pretyping function.
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 125ef94dc..24c3a5d9f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -677,24 +677,25 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  docomp evd comps
   in docomp oevd split
 
-let initial_select_evars onlyargs =
-  if onlyargs then
+let initial_select_evars with_goals =
+  if with_goals then
     (fun evd ev evi ->
-      Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd))
-      && Typeclasses.is_class_evar evd evi)
+     Typeclasses.is_class_evar evd evi)
   else
-    (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
+    (fun evd ev evi -> 
+     (snd (Evd.evar_source ev evd) <> Evd.GoalEvar)
+     && Typeclasses.is_class_evar evd evi)
 
-let resolve_typeclass_evars debug m env evd onlyargs split fail =
+let resolve_typeclass_evars debug m env evd with_goals split fail =
   let evd = 
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with _ -> evd
   in
-    resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
+    resolve_all_evars debug m env (initial_select_evars with_goals) evd split fail
 
-let solve_inst debug depth env evd onlyargs split fail =
-  resolve_typeclass_evars debug depth env evd onlyargs split fail
+let solve_inst debug depth env evd with_goals split fail =
+  resolve_typeclass_evars debug depth env evd with_goals split fail
 
 let _ =
   Typeclasses.solve_instanciations_problem :=
diff --git a/tactics/refine.ml b/tactics/refine.ml
index fa023e78e..93c4ea57c 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -389,7 +389,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
 let refine (evd,c) gl =
   let sigma = project gl in
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false (pf_env gl) evd in
   let c = Evarutil.nf_evar evd c in
   let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
   (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index cf05d9d4c..a8de1ba08 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -316,7 +316,8 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
+Program Instance predicate_equivalence_equivalence : 
+  Equivalence (@predicate_equivalence l).
 
   Next Obligation.
     induction l ; firstorder.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9d259eee1..dbabf6160 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -171,8 +171,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   in
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
-  evars := mark_resolvables !evars;
-  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
+  evars := resolve_typeclasses ~with_goals:false ~fail:true env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if abstract then
@@ -232,7 +231,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Pp.dummy_loc, None) :: props), rest
+		       (CHole (Pp.dummy_loc, Some Evd.GoalEvar) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
@@ -242,64 +241,72 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') 
 			     k.cl_props props subst))
       in	  
+      let term, termtype =
+	match subst with
+	| None -> let termtype = it_mkProd_or_LetIn cty ctx in
+	    None, termtype
+	| Some (Inl subst) ->
+	  let subst = List.fold_left2
+	    (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+	    [] subst (k.cl_props @ snd k.cl_context)
+	  in
+	  let app, ty_constr = instance_constructor k subst in
+	  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+	  let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
+	    Some term, termtype
+	| Some (Inr (def, subst)) ->
+	  let termtype = it_mkProd_or_LetIn cty ctx in
+	  let term = Termops.it_mkLambda_or_LetIn def ctx in
+	    Some term, termtype
+      in
+      let _ = 
 	evars := Evarutil.nf_evar_map !evars;
-	let term, termtype =
-	  match subst with
-	  | None -> let termtype = it_mkProd_or_LetIn cty ctx in
-	      None, termtype
-	  | Some (Inl subst) ->
-	      let subst = List.fold_left2
-		(fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
-		[] subst (k.cl_props @ snd k.cl_context)
+	evars := Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true
+          env !evars;
+	(* Try resolving fields that are typeclasses automatically. *)
+	evars := Typeclasses.resolve_typeclasses ~with_goals:true ~fail:false
+	  env !evars
+      in
+      let termtype = Evarutil.nf_evar !evars termtype in
+      let _ = (* Check that the type is free of evars now. *)
+	Evarutil.check_evars env Evd.empty !evars termtype
+      in
+      let term = Option.map (Evarutil.nf_evar !evars) term in
+      let evm = undefined_evars !evars in
+	if Evd.is_empty evm && term <> None then
+	  declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
+	else begin
+	  let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	    if Flags.is_program_mode () then
+	      let hook vis gr =
+		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
 	      in
-	      let app, ty_constr = instance_constructor k subst in
-	      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	      let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-		Some term, termtype
-	  | Some (Inr (def, subst)) ->
-	      let termtype = it_mkProd_or_LetIn cty ctx in
-	      let term = Termops.it_mkLambda_or_LetIn def ctx in
-		Some term, termtype
-	in
-	let termtype = Evarutil.nf_evar !evars termtype in
-	let term = Option.map (Evarutil.nf_evar !evars) term in
-	let evm = undefined_evars !evars in
-	  Evarutil.check_evars env Evd.empty !evars termtype;
-	  if Evd.is_empty evm && term <> None then
-	    declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
-	  else begin
-	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
-	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	      if Flags.is_program_mode () then
-		let hook vis gr =
-		  let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-		    Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-		    Typeclasses.declare_instance pri (not global) (ConstRef cst)
-		in
-		let obls, constr, typ =
-		  match term with 
-		  | Some t -> 
-		      let obls, _, constr, typ = 
-			Obligations.eterm_obligations env id !evars 0 t termtype
-		      in obls, Some constr, typ
-		  | None -> [||], None, termtype
-		in
-		  ignore (Obligations.add_definition id ?term:constr
-			    typ ~kind:(Global,Instance) ~hook obls);
-		  id
-	      else
-		(Flags.silently 
-		   (fun () ->
-		      Lemmas.start_proof id kind termtype
-			(fun _ -> instance_hook k pri global imps ?hook);
-		      if term <> None then 
-			Pfedit.by (!refine_ref (evm, Option.get term))
-		      else if Flags.is_auto_intros () then
-			Pfedit.by (Refiner.tclDO len Tactics.intro);
-		      (match tac with Some tac -> Pfedit.by tac | None -> ())) ();
-		 Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
-		 id)
-	  end)
+	      let obls, constr, typ =
+		match term with 
+		| Some t -> 
+		  let obls, _, constr, typ = 
+		    Obligations.eterm_obligations env id !evars 0 t termtype
+		  in obls, Some constr, typ
+		| None -> [||], None, termtype
+	      in
+		ignore (Obligations.add_definition id ?term:constr
+			typ ~kind:(Global,Instance) ~hook obls);
+		id
+	    else
+	      (Flags.silently 
+	       (fun () ->
+		Lemmas.start_proof id kind termtype
+		(fun _ -> instance_hook k pri global imps ?hook);
+		if term <> None then 
+		  Pfedit.by (!refine_ref (evm, Option.get term))
+		else if Flags.is_auto_intros () then
+		  Pfedit.by (Refiner.tclDO len Tactics.intro);
+		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+	       Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+	       id)
+	end)
 	
 let named_of_rel_context l =
   let acc, ctx =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8bb875ffb..13139557a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -282,8 +282,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
 
   (* Instantiate evars and check all are resolved *)
   let evd = consider_remaining_unif_problems env_params !evdref in
-  let evd = Typeclasses.mark_resolvables evd in
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env_params evd in
   let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
@@ -768,7 +767,7 @@ let interp_recursive isfix fixl notations =
   (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
   List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
   if not (List.mem None fixdefs) then begin
@@ -876,7 +875,7 @@ let do_program_recursive fixkind fixl ntns =
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instanciated *)
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
     (* Solve remaining evars *)
   let rec collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a0bffd4fb..051eb3062 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -389,16 +389,13 @@ let explain_unsolvability = function
       strbrk " (several distinct possible instances found)"
 
 let explain_typeclass_resolution env evi k =
-  match k with
-  | GoalEvar | InternalHole | ImplicitArg _ ->
-      (match Typeclasses.class_of_constr evi.evar_concl with
-      | Some c ->
-	  let env = Evd.evar_env evi in
-	    fnl () ++ str "Could not find an instance for " ++
-	      pr_lconstr_env env evi.evar_concl ++
-	      pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
-      | None -> mt())
-  | _ -> mt()
+  match Typeclasses.class_of_constr evi.evar_concl with
+  | Some c ->
+    let env = Evd.evar_env evi in
+      fnl () ++ str "Could not find an instance for " ++
+      pr_lconstr_env env evi.evar_concl ++
+      pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
+  | None -> mt()
 
 let explain_unsolvable_implicit env evi k explain =
   str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++