Fix bug #3505.

When w_unifying primitive projection applications, force
the unification of types of the projected records to recover instances
for the parameters (evarconv does this automatically by unifying evar
instances with their expected type).

2 files changed, 50 insertions, 8 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9737b9feb..d89cde1ae 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -676,14 +676,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| Proj (p1,c1), Proj (p2,c2) ->
 	    if eq_constant p1 p2 then
 	      try 
-	        let c1, c2, substn = 
-		   if isCast c1 && isCast c2 then
-		     let (c1,_,tc1) = destCast c1 in
-		     let (c2,_,tc2) = destCast c2 in
-		       c1, c2, unirec_rec curenvnb CONV true false substn tc1 tc2
-		   else c1, c2, substn
-		in
-		  unirec_rec curenvnb CONV true wt substn c1 c2
+		let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in
+		  try (* Force unification of the types to fill in parameters *)
+		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
+		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
+		      unirec_rec curenvnb CONV true false substn ty1 ty2
+		  with RetypeError _ -> substn
 	      with ex when precatchable_exception ex ->
 	        unify_not_same_head curenvnb pb b wt substn cM cN
 	    else
diff --git a/test-suite/bugs/closed/3505.v b/test-suite/bugs/closed/3505.v
new file mode 100644
index 000000000..2695bc796
--- /dev/null
+++ b/test-suite/bugs/closed/3505.v
@@ -0,0 +1,44 @@
+(* File reduced by coq-bug-finder from original input, then from 7421 lines to 6082 lines, then from 5860 lines to 5369 lines, then from 5300 lines to 165 lines, then from 111 lines to 38 lines *)
+Set Implicit Arguments.
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+    identity : forall x, morphism x x }.
+Bind Scope category_scope with PreCategory.
+Local Notation "1" := (identity _ _) : morphism_scope.
+Local Open Scope morphism_scope.
+Definition prod (C D : PreCategory) : PreCategory
+  := @Build_PreCategory
+       (C * D)%type
+       (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)
+       (fun x => (identity _ (fst x), identity _ (snd x))).
+Local Infix "*" := prod : category_scope.
+Module NonPrim.
+  Record Functor (C D : PreCategory) :=
+    { object_of :> C -> D;
+      morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
+      identity_of : forall x, morphism_of _ _ (identity _ x) = identity _ (object_of x) }.
+  Notation "F '_1' m" := (morphism_of F _ _ m) (at level 10, no associativity) : morphism_scope.
+  Goal forall C1 C2 D (F : Functor (C1 * C2) D) x, F _1 (1, 1) = identity _ (F x).
+  Proof.
+    intros.
+    rewrite identity_of.
+    reflexivity.
+  Qed.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record Functor (C D : PreCategory) :=
+    { object_of :> C -> D;
+      morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
+      identity_of : forall x, morphism_of _ _ (identity _ x) = identity _ (object_of x) }.
+  Notation "F '_1' m" := (morphism_of F _ _ m) (at level 10, no associativity) : morphism_scope.
+  Goal forall C1 C2 D (F : Functor (C1 * C2) D) x, F _1 (1, 1) = identity _ (F x).
+  Proof.
+    intros.
+    rewrite identity_of. (* Toplevel input, characters 0-20:
+Error:
+Found no subterm matching "morphism_of ?192 ?193 ?193 (identity ?190 ?193)" in the current goal. *)
+    reflexivity.
+  Qed.
+End Prim.