Fix canonical structure resolution which was launched on the results of

eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.

5 files changed, 94 insertions, 31 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index eba0423fe..e27ee84aa 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -159,7 +159,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
       [], c, sk1
     | None ->
       match Stack.strip_n_app nparams sk1 with
-      | Some (params1, c1,extra_args1) -> params1, c1, extra_args1
+      | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
       | _ -> raise Not_found in
   let us2,extra_args2 =
     let l_us = List.length us in
@@ -319,7 +319,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
       let evd, b = 
-	try infer_conv ~pb:pbty ~ts env evd term1 term2 
+	try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 
 	with Univ.UniverseInconsistency _ -> evd, false
       in
 	if b then Some (evd, true)
@@ -333,8 +333,8 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
-        let term1 = apprec_nohdbeta ts env evd term1 in
-        let term2 = apprec_nohdbeta ts env evd term2 in
+        let term1 = apprec_nohdbeta (fst ts) env evd term1 in
+        let term2 = apprec_nohdbeta (fst ts) env evd term2 in
 	let default () = 
           evar_eqappr_x ts env evd pbty
             (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
@@ -389,7 +389,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let c = nf_evar evd c1 in
     let env' = push_rel (na,None,c) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
-      ts env' evd Cst_stack.empty (c'1, Stack.empty) in
+      (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
       (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
@@ -424,7 +424,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       else quick_fail i
     and f3 i =
       switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
-	(whd_betaiota_deltazeta_for_iota_state ts env i cstsM vM)
+	(whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM vM)
     in
     ise_try evd [f1; f2; f3] in
   let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
@@ -458,7 +458,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     let open Pp in
 	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
 		 ++ fnl ()) in
-  match (flex_kind_of_term ts env term1 sk1, flex_kind_of_term ts env term2 sk2) with
+  match (flex_kind_of_term (fst ts) env term1 sk1, flex_kind_of_term (fst ts) env term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
 	  match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
@@ -521,8 +521,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
 	and f2 i =
-          let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
-          and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
+          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
+          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
 	  in evar_eqappr_x ts env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
@@ -533,8 +533,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    [(fun i -> evar_conv_x ts env i CONV c c');
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
+            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
+            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
@@ -549,8 +549,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)]
 	      | None -> UnifFailure (evd, NotSameHead))
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
+            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
+            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in ise_try evd [f1;f2]
 
@@ -564,8 +564,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)]
 	      | None -> UnifFailure (evd, NotSameHead))
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2')
+            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
+            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in ise_try evd [f1;f2]
 
@@ -585,9 +585,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
 	    else UnifFailure (i,NotSameHead)
 	and f2 i =
-	  (try conv_record ts env i
-             (try check_conv_record appr1 appr2
-	      with Not_found -> check_conv_record appr2 appr1)
+	  (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)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f3 i =
           (* heuristic: unfold second argument first, exception made
@@ -603,7 +605,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             | Lambda _ -> assert (match args with [] -> true | _ -> false); true
             | LetIn (_,b,_,c) -> is_unnamed
 	     (fst (whd_betaiota_deltazeta_for_iota_state
-		      ts env i Cst_stack.empty (subst1 b c, args)))
+		      (fst ts) env i Cst_stack.empty (subst1 b c, args)))
 	    | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
 	    | Proj (p, c) -> true
             | Case _ | App _| Cast _ -> assert false in
@@ -611,7 +613,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    let applicative_stack = fst (Stack.strip_app sk2') in
 	    is_unnamed
 	      (fst (whd_betaiota_deltazeta_for_iota_state
-		      ts env i Cst_stack.empty (v2, applicative_stack))) in
+		      (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 
@@ -619,12 +621,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    && (not (Stack.not_purely_applicative sk1')) then
 	    evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
 	      (whd_betaiota_deltazeta_for_iota_state
-		 ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1'))
+		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1'))
 	      (appr2,csts2)
 	  else
 	    evar_eqappr_x ts env i pbty (appr1,csts1)
 	      (whd_betaiota_deltazeta_for_iota_state
-		 ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2'))
+		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2'))
 	in
 	ise_try evd [f1; f2; f3]
     end
@@ -644,24 +646,28 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     | MaybeFlexible (v1,sk1), Rigid ->
 	let f3 i =
-	  (try conv_record ts env i (check_conv_record appr1 appr2)
+	  (try 
+	     if not (snd ts) then raise Not_found
+	     else conv_record ts env i (check_conv_record appr1 appr2)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty
 	    (whd_betaiota_deltazeta_for_iota_state
-	       ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+	       (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	    (appr2,csts2)
 	in
 	  ise_try evd [f3; f4]
 
     | Rigid, MaybeFlexible (v2,sk2) ->
 	let f3 i =
-	  (try conv_record ts env i (check_conv_record appr2 appr1)
+	  (try
+	     if not (snd ts) then raise Not_found
+	     else conv_record ts env i (check_conv_record appr2 appr1)
            with Not_found -> UnifFailure (i,NoCanonicalStructure))
 	and f4 i =
 	  evar_eqappr_x ts env i pbty (appr1,csts1)
 	    (whd_betaiota_deltazeta_for_iota_state
-	       ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+	       (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	  ise_try evd [f3; f4]
 
@@ -797,7 +803,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
 	     let term = Stack.zip (term2,sk2) in 
 	       List.map (fun p -> mkProj (p, term)) (Array.to_list projs)
 	   in
-	     exact_ise_stack2 env evd (evar_conv_x ts) l1' 
+	     exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' 
 	       (Stack.append_app_list l2' Stack.empty)
 	 with 
 	 | Invalid_argument _ ->
@@ -805,6 +811,8 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
 	   UnifFailure(evd,NotSameHead))
     | _ -> UnifFailure (evd,NotSameHead)
 
+let evar_conv_x ts = evar_conv_x (ts, true)
+
 (* Profiling *)
 let evar_conv_x =
   if Flags.profile then
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 500bb5430..12cf7d0b7 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -63,7 +63,7 @@ val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
 (* For debugging *)
 val evar_conv_x : transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
-val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
   env -> evar_map ->
     conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
       Evarsolve.unification_result
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 494138541..66aa85ecd 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -308,9 +308,6 @@ let declare_canonical_structure ref =
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (Refmap.find proj !object_table)
 
-  (* let cst, u' = destConst cs.o_DEF in *)
-  (*   { cs with o_DEF = mkConstU (cst, u) } *)
-
 let is_open_canonical_projection env sigma (c,args) =
   try
     let ref = global_of_constr c in
diff --git a/test-suite/bugs/closed/3665.v b/test-suite/bugs/closed/3665.v
new file mode 100644
index 000000000..f6a13596c
--- /dev/null
+++ b/test-suite/bugs/closed/3665.v
@@ -0,0 +1,33 @@
+(* File reduced by coq-bug-finder from original input, then from 5449 lines to 44 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
+   coqtop version trunk (September 2014) *)
+Set Primitive Projections.
+
+Axiom IsHSet : Type -> Type.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+
+Module withdefault.
+Canonical Structure default_HSet := fun T P => (@BuildhSet T P).
+Goal forall (z : hSet) (T0 : Type -> Type),
+       (forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
+       forall x0 : setT z, Set.
+  clear; intros z T H.
+  Set Debug Unification.
+  Fail refine (H _ _). (* Timeout! *)
+Abort.
+End withdefault.
+
+Module withnondefault.
+Variable T0 : Type -> Type.
+Variable T0hset: forall A, IsHSet (T0 A).
+
+Canonical Structure nondefault_HSet := fun A =>(@BuildhSet (T0 A) (T0hset A)).
+Canonical Structure default_HSet := fun A P =>(@BuildhSet A P).
+Goal forall (z : hSet) (T0 : Type -> Type),
+       (forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
+       forall x0 : setT z, Set.
+  clear; intros z T H.
+  Set Debug Unification.
+  Fail refine (H _ _). (* Timeout! *)
+Abort.
+End withnondefault.
diff --git a/test-suite/bugs/closed/3667.v b/test-suite/bugs/closed/3667.v
new file mode 100644
index 000000000..e0d0e4486
--- /dev/null
+++ b/test-suite/bugs/closed/3667.v
@@ -0,0 +1,25 @@
+
+Set Primitive Projections.
+Axiom ap10 : forall {A B} {f g:A->B} (h:f=g) x, f x = g x.
+Axiom IsHSet : Type -> Type.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+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) }.
+Set Implicit Arguments.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  { components_of :> forall c, morphism D (F c) (G c);
+    commutes : forall s d (m : morphism C s d), components_of s = components_of s }.
+Definition set_cat : PreCategory.
+  exact ((@Build_PreCategory hSet
+                             (fun x y => x -> y))).
+Defined.
+Goal forall (A : PreCategory) (F : Functor A set_cat)
+            (a : A) (x : F a), x = x.
+  intros. 
+  pose (fun c d m => ap10 (commutes x c d m)).
+
+