Two fixes in unification (bugs #3782 and #3709)

- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.

5 files changed, 123 insertions, 33 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b1f201995..80cb63165 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -112,7 +112,7 @@ let occur_rigidly ev evd t =
     | Case _ -> false
   in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
 
-(* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
+(* [check_conv_record env sigma (t1,l1) (t2,l2)] tries to decompose the problem
    (t1 l1) = (t2 l2) into a problem
 
      l1 = params1@c1::extra_args1
@@ -132,7 +132,7 @@ let occur_rigidly ev evd t =
    object c in structure R (since, if c1 were not an evar, the
    projection would have been reduced) *)
 
-let check_conv_record (t1,sk1) (t2,sk2) =
+let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let (proji, u), arg = Universes.global_app_of_constr t1 in
   let canon_s,sk2_effective =
     try
@@ -156,7 +156,11 @@ let check_conv_record (t1,sk1) (t2,sk2) =
   let params1, c1, extra_args1 =
     match arg with
     | Some c -> (* A primitive projection applied to c *)
-      [], c, sk1
+      let ty = Retyping.get_type_of ~lax:true env sigma c in
+      let (i,u), ind_args = 
+	try Inductiveops.find_mrectype env sigma ty 
+	with _ -> raise Not_found
+      in Stack.append_app_list ind_args Stack.empty, c, sk1
     | None ->
       match Stack.strip_n_app nparams sk1 with
       | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
@@ -612,8 +616,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  (try 
 	     if not (snd ts) then raise Not_found
 	     else conv_record ts env i
-               (try check_conv_record appr1 appr2
-		with Not_found -> check_conv_record appr2 appr1)
+               (try check_conv_record env i appr1 appr2
+		with Not_found -> check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f3 i =
           (* heuristic: unfold second argument first, exception made
@@ -672,7 +676,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	let f3 i =
 	  (try 
 	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record appr1 appr2)
+	     else conv_record ts env i (check_conv_record env i appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty
@@ -686,7 +690,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	let f3 i =
 	  (try
 	     if not (snd ts) then raise Not_found
-	     else conv_record ts env i (check_conv_record appr2 appr1)
+	     else conv_record ts env i (check_conv_record env i appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty (appr1,csts1)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index f3363e358..f559db253 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -42,7 +42,8 @@ val check_problems_are_solved : env -> evar_map -> unit
 
 (** Check if a canonical structure is applicable *)
 
-val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
+val check_conv_record : env -> evar_map -> 
+  constr * types Stack.t -> constr * types Stack.t ->
   Univ.universe_context_set * (constr * constr) 
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * types Stack.t) *
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a53240a1c..3c89bf27a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -732,8 +732,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cN with
-	     | App(f2,l2) when isMeta f2 || isEvar f2 ->
-	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | App(f2,l2) when
+		 (isMeta f2 && use_metas_pattern_unification flags nb l2
+		  || use_evars_pattern_unification flags && isAllowedEvar flags f2) ->
+	       unify_app_pattern false curenvnb pb opt substn cM f1 l1 cN f2 l2
 	     | _ -> raise ex)
 
 	| _, App (f2, l2) when flags.modulo_eta && 
@@ -744,8 +746,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	       Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2'
 	   with ex when precatchable_exception ex ->
 	     match kind_of_term cM with
-	     | App(f1,l1) when isMeta f1 || isEvar f1 ->
-	       unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	     | App(f1,l1) when 
+		 (isMeta f1 && use_metas_pattern_unification flags nb l1
+		  || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
+	       unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2
 	     | _ -> raise ex)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
@@ -761,30 +765,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| App (f1,l1), _ when 
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
             || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
-            (match
-                is_unification_pattern curenvnb sigma f1 (Array.to_list l1) cN
-             with
-             | None ->
-                 (match kind_of_term cN with
-                 | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
-                 | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN cN [||]
-                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
-             | Some l ->
-                 solve_pattern_eqn_array curenvnb f1 l cN substn)
+	  unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN cN [||]
 
 	| _, App (f2,l2) when
 	    (isMeta f2 && use_metas_pattern_unification flags nb l2
             || use_evars_pattern_unification flags && isAllowedEvar flags f2) ->
-            (match
-                is_unification_pattern curenvnb sigma f2 (Array.to_list l2) cM
-             with
-             | None ->
-                 (match kind_of_term cM with
-                 | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
-                 | Proj _ -> unify_app curenvnb pb opt substn cM cM [||] cN f2 l2
-                 | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
-             | Some l ->
-	         solve_pattern_eqn_array curenvnb f2 l cM substn)
+	  unify_app_pattern false curenvnb pb opt substn cM cM [||] cN f2 l2
 
 	| App (f1,l1), App (f2,l2) ->
 	  unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
@@ -798,6 +784,19 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| _ ->
           unify_not_same_head curenvnb pb opt substn cM cN
 
+  and unify_app_pattern dir curenvnb pb opt substn cM f1 l1 cN f2 l2 =
+    let f, l, t = if dir then f1, l1, cN else f2, l2, cM in
+      match is_unification_pattern curenvnb sigma f (Array.to_list l) t with
+      | None ->
+	(match kind_of_term t with
+	| App (f',l') -> 
+	  if dir then unify_app curenvnb pb opt substn cM f1 l1 t f' l'
+	  else unify_app curenvnb pb opt substn t f' l' cN f2 l2
+	| Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+	| _ -> unify_not_same_head curenvnb pb opt substn cM cN)
+      | Some l ->
+	solve_pattern_eqn_array curenvnb f l t substn
+
   and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
     try
       let needs_expansion p c' = 
@@ -963,7 +962,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 
   and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
     let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
-      try Evarconv.check_conv_record f1l1 f2l2
+      try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
     if Reductionops.Stack.compare_shape ts ts1 then
diff --git a/test-suite/bugs/closed/3709.v b/test-suite/bugs/closed/3709.v
new file mode 100644
index 000000000..7f01be7ab
--- /dev/null
+++ b/test-suite/bugs/closed/3709.v
@@ -0,0 +1,23 @@
+Module NonPrim.
+  Unset Primitive Projections.
+  Record hProp := hp { hproptype :> Type }.
+  Goal forall (h : (Type -> hProp) -> (Type -> hProp)) k f,
+         (forall y, h y = y) ->
+         h (fun b : Type => {| hproptype := f b |}) = k.
+  Proof.
+    intros h k f H.
+    etransitivity.
+    apply H.
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record hProp := hp { hproptype :> Type }.
+  Goal forall (h : (Type -> hProp) -> (Type -> hProp)) k f,
+         (forall y, h y = y) ->
+         h (fun b : Type => {| hproptype := f b |}) = k.
+  Proof.
+    intros h k f H.
+    etransitivity.
+    apply H.
diff --git a/test-suite/bugs/closed/3782.v b/test-suite/bugs/closed/3782.v
new file mode 100644
index 000000000..08d456fc6
--- /dev/null
+++ b/test-suite/bugs/closed/3782.v
@@ -0,0 +1,63 @@
+(* File reduced by coq-bug-finder from original input, then from 2674 lines to 136 lines, then from 115 lines to 61 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 28 2014 14:33:38 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,(no branch) (53bfe9cf58a3c40e6eb7120d25c1633a9cea3126) *)
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+Record Equiv A B := { equiv_fun : A -> B ; equiv_isequiv : IsEquiv equiv_fun }.
+Arguments equiv_fun {A B} _ _.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Set Printing Coercions.
+Set Printing Implicit.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record TruncType (n : nat) := { trunctype_type :> Type }.
+  Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
+  Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
+          @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
+  forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
+    intros isiso_isequiv' mc md e e'.
+    (pose (@isiso_isequiv'
+             _ _
+             (e
+              : (Build_TruncType 0 md) ->
+                (Build_TruncType 0 mc))
+             e') as i || fail "too early"); clear i.
+    pose (@isiso_isequiv'
+            _ _ _
+            e').
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record TruncType (n : nat) := { trunctype_type :> Type }.
+  Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
+  Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
+          @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
+  forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
+    intros isiso_isequiv' mc md e e'.
+    (pose (@isiso_isequiv'
+             _ _
+             (e
+              : (Build_TruncType 0 md) ->
+                (Build_TruncType 0 mc))
+             e') as i || fail "too early"); clear i.
+    Set Printing Existential Instances.
+    Set Debug Unification.
+    pose (@isiso_isequiv'
+            _ _ _
+            e'). (* Toplevel input, characters 48-50:
+Error:
+In environment
+isiso_isequiv' : forall (s d : TruncType 0)
+                   (m : trunctype_type 0 s -> trunctype_type 0 d),
+                 @IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type
+mc : Type
+md : Type
+e : md -> mc
+e' : @IsEquiv md mc e
+The term "e'" has type "@IsEquiv md mc e" while it is expected to have type
+ "@IsEquiv (trunctype_type 0 ?t) (trunctype_type 0 ?t0) ?t1".
+                  *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file