From c12e158ad85da9d5e78026997ef6ca969c8ad3a6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 19:32:23 +0200
Subject: Fixing a missing constraint in consider_remaining_unif_constraints.

---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0d261f7f87..d82d555f84 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1130,7 +1130,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in
       Success (solve_refl ~can_drop:true f env evd
                  (position_problem true pbty) evk1 args1 args2)
-  | Evar ev1, Evar ev2 ->
+  | Evar ev1, Evar ev2 when app_empty ->
       Success (solve_evar_evar ~force:true
         (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
         (position_problem true pbty) ev1 ev2)
-- 
cgit v1.2.3


From fa1cb4a55262a1dced369ae6556265b968f4b9a3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 19:35:16 +0200
Subject: Fixing to #3209 (Not_found due to an occur-check cycle).

The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
---
 pretyping/evarsolve.ml        |  8 +++++
 test-suite/bugs/closed/3209.v | 75 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 test-suite/bugs/closed/3209.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4084ee579a..4a99246bba 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -600,7 +600,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
  * substitution u1..uq.
  *)
 
+exception MorePreciseOccurCheckNeeeded
+
 let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+  if Evd.is_defined evd evk1 then
+      (* Some circularity somewhere (see e.g. #3209) *)
+      raise MorePreciseOccurCheckNeeeded;
+  let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -1542,6 +1548,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
         add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+    | MorePreciseOccurCheckNeeeded ->
+        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
diff --git a/test-suite/bugs/closed/3209.v b/test-suite/bugs/closed/3209.v
new file mode 100644
index 0000000000..855058b011
--- /dev/null
+++ b/test-suite/bugs/closed/3209.v
@@ -0,0 +1,75 @@
+(* Avoiding some occur-check *)
+
+(* 1. Original example *)
+
+Inductive eqT {A} (x : A) : A -> Type :=
+  reflT : eqT x x.
+Definition Bi_inv (A B : Type) (f : (A -> B)) :=
+  sigT (fun (g : B -> A) =>
+          sigT (fun (h : B -> A) =>
+                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
+                          forall a : A, eqT (h (f a)) a))).
+Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
+
+Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
+Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
+  sigT_rect (fun _ => TEquiv A B)
+            (fun (f : TEquiv A B -> eqT A B) H =>
+               sigT_rect _ (* (fun _ => TEquiv A B) *)
+                         (fun g _ => g e)
+                         H)
+            (UA A B).
+
+(* 2. Alternative example by Guillaume *)
+
+Inductive foo (A : Prop) : Prop := Foo : foo A.
+Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop.
+
+(* This used to fail with a Not_found, we fail more graciously but a
+   heuristic could be implemented, e.g. in some smart occur-check
+   function, to find a solution of then form ?P := fun _ => ?P' *)
+
+Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)).
+
+(* This works and tells which solution we could have inferred *)
+
+Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)).
+
+(* For the record, here is the trace in the failing example:
+
+In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables
+
+e:?T |- ?A : Prop
+e:?T |- ?P : foo ?A -> Prop
+e:?T |- ?A' : Type
+
+with constraints
+
+?A' == ?A
+?A' == ?T -> ?P (Foo ?A)
+
+To type (g e), unification first defines
+
+?A := forall x:?B, ?P'{e:=e,x:=x}
+with ?T <= ?B
+and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x}))
+
+Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is
+not a pattern and we define a new
+
+e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop
+
+for some ?B' and ?P''', together with
+
+?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P')
+?P@{e} := ?P''{e:=e,x:=e}
+
+Moreover, ?B' and ?P''' have to satisfy
+
+?B'@{e:=e,x:=e} == ?B@{e:=e}
+?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x}
+
+and this leads to define ?P' which was the initial existential
+variable to define.
+*)
+
-- 
cgit v1.2.3


From 317ae3b327d201530730ed2cce5f44e8763814d4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 17:37:15 +0200
Subject: Removing output test for module qualification.

I do not know how to provide a proper test in 8.5, as the location on my
machine appears in the error printed when loading the file. Adding a Fail
on the End command does not help much either, because it simply does not
print anything.

Do not merge this commit in 8.6, we still want a test there.
---
 test-suite/output/qualification.out |  3 ---
 test-suite/output/qualification.v   | 19 -------------------
 2 files changed, 22 deletions(-)
 delete mode 100644 test-suite/output/qualification.out
 delete mode 100644 test-suite/output/qualification.v

diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
deleted file mode 100644
index 3cf3c2d8fb..0000000000
--- a/test-suite/output/qualification.out
+++ /dev/null
@@ -1,3 +0,0 @@
-File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
-Error: Signature components for label test do not match: expected type
-"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
deleted file mode 100644
index d39097e2dd..0000000000
--- a/test-suite/output/qualification.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Module Type T1.
-  Parameter t : Type.
-End T1.
-
-Module Type T2.
-  Declare Module M : T1.
-  Parameter t : Type.
-  Parameter test : t = M.t.
-End T2.
-
-Module M1 <: T1.
-  Definition t : Type := bool.
-End M1.
-
-Module M2 <: T2.
-  Module M := M1.
-  Definition t : Type := nat.
-  Lemma test : t = t. Proof. reflexivity. Qed.
-End M2.
-- 
cgit v1.2.3