Fix bugs #3484 and #3546.

The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).

3 files changed, 67 insertions, 10 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 29d721577f..aee7be9816 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -395,7 +395,12 @@ let oracle_order env cf1 cf2 =
       match cf2 with
       | None -> Some true
       | Some k2 ->
-          Some (Conv_oracle.oracle_order (Environ.oracle env) false (translate_key k1) (translate_key k2))
+	match k1, k2 with
+	| IsProj (p, _), IsKey (ConstKey (p',_)) when eq_constant p p' -> Some false
+	| IsKey (ConstKey (p,_)), IsProj (p', _) when eq_constant p p' -> Some true
+	| _ ->
+          Some (Conv_oracle.oracle_order (Environ.oracle env) false
+		  (translate_key k1) (translate_key k2))
 
 let is_rigid_head flags t =
   match kind_of_term t with
@@ -574,15 +579,23 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
 
 	(* For records *)
-	| App (f, l1), _ when flags.modulo_eta && is_eta_constructor_app env f l1 ->
-	  let l1', l2' = eta_constructor_app env f l1 cN in
-	   Array.fold_left2 
-	     (unirec_rec curenvnb CONV true wt) substn l1' l2'
-
-	| _, App (f, l2) when flags.modulo_eta && is_eta_constructor_app env f l2 ->
-	  let l2', l1' = eta_constructor_app env f l2 cM in
-	   Array.fold_left2 
-	     (unirec_rec curenvnb CONV true wt) substn l1' l2'
+	| App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app env f1 l1 ->
+	  (try let l1', l2' = eta_constructor_app env f1 l1 cN in
+		 Array.fold_left2 
+		   (unirec_rec curenvnb CONV true wt) substn l1' l2'
+	   with ex when precatchable_exception ex -> 
+	     (match kind_of_term cN with
+             | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
+             | _ -> unify_not_same_head curenvnb pb b wt substn cM cN))
+
+	| _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app env f2 l2 ->
+	  (try let l2', l1' = eta_constructor_app env f2 l2 cM in
+		 Array.fold_left2 
+		   (unirec_rec curenvnb CONV true wt) substn l1' l2'
+	   with ex when precatchable_exception ex -> 
+	     (match kind_of_term cM with
+             | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
+             | _ -> unify_not_same_head curenvnb pb b wt substn cM cN))
 	   
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             (try 
diff --git a/test-suite/bugs/closed/3484.v b/test-suite/bugs/closed/3484.v
new file mode 100644
index 0000000000..3070a4128c
--- /dev/null
+++ b/test-suite/bugs/closed/3484.v
@@ -0,0 +1,27 @@
+(* File reduced by coq-bug-finder from original input, then from 14259 lines to 305 lines, then from 237 lines to 120 lines, then from 100 lines to 30 lines *)
+Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT (A : Type) (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Notation "{ x : A & P }" := (@sigT A (fun x : A => P)) : type_scope.
+Notation pr1 := (@projT1 _ _).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
+Goal forall (T : Type) (H :  { g : T & g = g }) (x : T), projT1 H = projT1 (existT (fun g : T => g = g) x idpath).
+Proof.
+  intros.
+  let y := match goal with |- projT1 ?x = projT1 ?y => constr:(y) end in
+  apply (@ap _ _ pr1 _ y).
+  Undo.
+  Unset Printing Notations.
+  apply (ap pr1). admit. 
+Defined.
+
+(* Toplevel input, characters 22-28:
+Error:
+In environment
+T : Type
+H : sigT T (fun g : T => paths g g)
+x : T
+Unable to unify "paths (@projT1 ?24 ?23 ?25) (@projT1 ?24 ?23 ?26)" with
+ "paths (projT1 H) (projT1 {| projT1 := x; projT2 := idpath |})". *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3546.v b/test-suite/bugs/closed/3546.v
new file mode 100644
index 0000000000..55d718bd03
--- /dev/null
+++ b/test-suite/bugs/closed/3546.v
@@ -0,0 +1,17 @@
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Arguments pair {_ _} _ _.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y.
+Admitted.
+Goal forall x y z w : Set, (x, y) = (z, w).
+Proof.
+  intros.
+  apply ap11. (* Toplevel input, characters 21-25:
+Error: In environment
+x : Set
+y : Set
+z : Set
+w : Set
+Unable to unify "?31 ?191 = ?32 ?192" with "(x, y) = (z, w)".
+ *)