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.

2 files changed, 83 insertions, 0 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4084ee579..4a99246bb 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 000000000..855058b01
--- /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.
+*)
+