Little fixes in setoid_rewrite.

- More meaningful argument name for resolve_typeclasses. 
- Try to remove unneeded instance declarations in
Morphisms. 
- Allow the proofs of reflexivity arising from unchanged
arguments in setoid_rewrite to be fullfiled by Morphism instances and
not necessariy because the relation is reflexive (needed by
higher-order morphisms). Use a new "MorphismProxy" class to implement
that efficiently.
- Fix a bug in abstract_generalize not delta-reducing a type where it should.


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

9 files changed, 83 insertions, 59 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 7ec5d3575f..4a848380ef 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -158,7 +158,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses ~onlyargs:false ~all:true env' sigma !isevars;
+  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' sigma !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index b9bda64a9a..ec5af37fe2 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (Evd.evars_of evd) evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (Evd.evars_of evd) evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index d3edb6e3cd..e87eb27dca 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -558,7 +558,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
       isevars:=evd;
       nf_evar (evars_of !isevars) c'
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index df1e45d868..19df941b28 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -653,7 +653,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
       evdref := evd;
       nf_evar (evars_of evd) c'
 
@@ -667,7 +667,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env (evars_of evd) evd in
     let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
@@ -687,7 +687,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c = pretype_gen evdref env lvar kind c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
       if fail_evar then 
-	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~all:false env (evars_of evd) evd in
+	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env (evars_of evd) evd in
 	let c = Evarutil.nf_isevar evd c in
 	  check_evars env Evd.empty evd c;
 	  evd, c
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0450709605..e9a766a92e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -407,10 +407,10 @@ let has_typeclasses evd =
 	&& is_resolvable evi))
     evd false
 
-let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd =
+let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env sigma evd =
   if not (has_typeclasses sigma) then evd
   else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all
+    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs fail
 
 type substitution = (identifier * constr) list
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index d35ee54140..c6763a4213 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -74,7 +74,7 @@ val bool_out : Dyn.t -> bool
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 
-val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_map -> 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
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 922539ddba..685f11d47d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -275,6 +275,9 @@ let filter_pat c =
 
 let morphism_class = 
   lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))))
+
+let morphism_proxy_class = 
+  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.MorphismProxy"))))
     
 let filter c =
   try let morc = constr_of_global (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))) in
@@ -528,6 +531,8 @@ let setoid_refl pars x =
       
 let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl)
 
+let morphism_proxy_type = lazy (constr_of_global (Lazy.force morphism_proxy_class).cl_impl)
+
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
 
@@ -570,16 +575,10 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
 			      t, rel, [t, rel])
   in aux m cstrs
 
-let reflexivity_proof_evar env evars carrier relation x =
+let morphism_proof env evars carrier relation x =
   let goal =
-    mkApp (Lazy.force reflexive_type, [| carrier ; relation |])
-  in
-  let inst = Evarutil.e_new_evar evars env goal in
-    (* try resolve_one_typeclass env goal *)
-    mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
-    (*     with Not_found -> *)
-(*       let meta = Evarutil.new_meta() in *)
-(* 	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *)
+    mkApp (Lazy.force morphism_proxy_type, [| carrier ; relation; x |])
+  in Evarutil.e_new_evar evars env goal
 
 let find_class_proof proof_type proof_method env carrier relation =
   try 
@@ -626,8 +625,8 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
 	let (carrier, relation), sigargs = split_head sigargs in
 	  match y with
 	      None ->
-		let refl_proof = reflexivity_proof_evar env evars carrier relation x in
-		  [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs'
+		let proof = morphism_proof env evars carrier relation x in
+		  [ proof ; x ; x ] @ acc, sigargs, x :: typeargs'
 	    | Some (p, (_, _, _, t')) ->
 		[ p ; t'; x ] @ acc, sigargs, t' :: typeargs')
       ([], sigargs, []) args args'
@@ -936,7 +935,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 (Evd.evars_of !evars) !evars;
+	      evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) ~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
@@ -971,8 +970,9 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 		  else tclIDTAC
 	      in tclTHENLIST [evartac; rewtac] gl
 	    with 
-	      | TypeClassError (_env, UnsatisfiableConstraints _evm) -> 
-		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl
+	      | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> 
+		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints."
+			      ++ Himsg.explain_typeclass_error env e) gl
 	      | Not_found ->
 		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl)
       | None -> 
@@ -1037,10 +1037,10 @@ 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 all =
+let solve_inst debug mode depth env evd onlyargs fail =
   match resolve_typeclass_evars debug (mode, depth) env evd onlyargs with 
     | None -> 
-	if all then 
+	if fail then 
 	  (* Unable to satisfy the constraints. *)
 	  Typeclasses_errors.unsatisfiable_constraints env evd
 	else (* Best effort: do nothing *) evd
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b4e646a079..c3f9c37e9c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1862,14 +1862,17 @@ let abstract_args gl id =
 	   eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
 	*)
 	let aux (prod, ctx, ctxenv, c, args, eqs, refls, finalargs, env) arg =
-	  let (name, ty, arity) = destProd prod in
+	  let (name, _, ty), arity = 
+	    let rel, c = Reductionops.decomp_n_prod env sigma 1 prod in
+	      List.hd rel, c
+	  in
 	  let argty = pf_type_of gl arg in
 	  let liftarg = lift (List.length ctx) arg in
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv ctxenv sigma ty liftargty in
 	    match kind_of_term arg with
 	      | Var _ | Rel _ when convertible -> 
-		    (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, (Anonymous, liftarg, liftarg) :: finalargs, env)
+		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, (Anonymous, liftarg, liftarg) :: finalargs, env)
 	      | _ ->
 		  let name = get_id name in
 		  let decl = (Name name, None, ty) in
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 552ff996ae..e2d3f21c73 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -75,7 +75,7 @@ Arguments Scope Morphism [type_scope signature_scope].
 
 Implicit Arguments Morphism [A].
 
-(** We allow to unfold the relation definition while doing morphism search. *)
+(** We allow to unfold the [relation] definition while doing morphism search. *)
 
 Typeclasses unfold relation.
 
@@ -144,15 +144,7 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] =>
     intuition.
   Qed.
 
-(** The inverse too. *)
-
-Program Instance [ mor : Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
-  inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
-
-  Next Obligation.
-  Proof.
-    apply mor ; auto.
-  Qed.
+(** The [inverse] too, actually the [flip] instance is a bit more general. *) 
 
 Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
   flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
@@ -174,15 +166,15 @@ Program Instance [ Transitive A R ] =>
     transitivity x0...
   Qed.
 
-(** Dually... *)
+(* (** Dually... *) *)
 
-Program Instance [ Transitive A R ] =>
-  trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
+(* Program Instance [ Transitive A R ] => *)
+(*   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *)
   
-  Next Obligation.
-  Proof with auto.
-    apply* trans_contra_co_morphism ; eauto. eauto.
-  Qed.
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     apply* trans_contra_co_morphism ; eauto. eauto. *)
+(*   Qed. *)
 
 (** Morphism declarations for partial applications. *)
 
@@ -229,10 +221,8 @@ Program Instance [ Equivalence A R ] =>
     symmetry...
   Qed.
 
-(** [R] is Reflexive, hence we can build the needed proof. *)
-
-Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ]  =>
-  Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
+(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ]  => *)
+(*   Reflexive_partial_app_morphism : Morphism R' (m x) | 4. *)
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
@@ -245,13 +235,13 @@ Program Instance [ Transitive A R ] =>
     transitivity y...
   Qed.
 
-Program Instance [ Transitive A R ] => 
-  trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
+(* Program Instance [ Transitive A R ] =>  *)
+(*   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *)
 
-  Next Obligation.
-  Proof with auto.
-    transitivity x...
-  Qed.
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     transitivity x... *)
+(*   Qed. *)
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
@@ -266,7 +256,7 @@ Program Instance [ Transitive A R, Symmetric _ R ] =>
     transitivity y... transitivity y0... 
   Qed.
 
-Program Instance [ Equivalence A R ] => 
+Program Instance [ Equivalence A R ] =>
   equiv_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
@@ -294,11 +284,11 @@ Program Instance inverse_iff_impl_id :
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-Instance (A : Type) [ Reflexive B R ] =>
-  eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
-Proof. simpl_relation. Qed.
+(* Instance (A : Type) [ Reflexive B R ] => *)
+(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
+(* Proof. simpl_relation. Qed. *)
 
-Instance (A : Type) [ Reflexive B R' ] => 
+Instance (A : Type) [ Reflexive B R' ] =>
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -322,6 +312,37 @@ Proof.
     assumption.
 Qed.
 
+(** Every element in the carrier of a reflexive relation is a morphism for this relation.
+   We use a proxy class for this case which is used internally to discharge reflexivity constraints.
+   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of 
+   [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
+   to set different priorities in different hint bases and select a particular hint database for
+   resolution of a type class constraint.*) 
+
+Class MorphismProxy A (R : relation A) (m : A) : Prop :=
+  respect_proxy : R m m.
+
+Instance [ Reflexive A R ] (x : A) => 
+  reflexive_morphism_proxy : MorphismProxy A R x | 1.
+Proof. firstorder. Qed.
+
+Instance [ Morphism A R x ] =>
+  morphism_morphism_proxy : MorphismProxy A R x | 2.
+Proof. firstorder. Qed.
+
+(* Instance (A : Type) [ Reflexive B R ] => *)
+(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
+(* Proof. simpl_relation. Qed. *)
+
+Instance [ Reflexive A R ] (x : A) => 
+  reflexive_morphism : Morphism R x | 4.
+Proof. firstorder. Qed.
+
+(** [R] is Reflexive, hence we can build the needed proof. *)
+
+Program Instance [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ]  =>
+  Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
+
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
   relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
 Proof.