Quick fix to unification regression #4955.

The commit which caused the regression (5ea2539d4a) looks reasonable.
However, it happens that this commit made that unification started in
the #4955 example to follow a path with problems of the form
"proj ?x == ?x" which clearly are unsolvable (both ?x have the same
instance).

We hack the corresponding very permissive occur-check function so that
it is a bit less permissive.

One day, this occur-check function would have to be rewritten in a
more stricter way.

----------------------------------------------------------------------
Extra comments:

I could list several functions for occur check of evars.

Four of them are too strict in the sense that they do not take into
account occurrences of evars which may disappear by reduction, nor
evars which have instances made in such a way that the occur-check is
solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are:
- Termops.occur_evar for clenv, evar_refiner, tactic unification
  - syntactic check without any normalization, even on defined evars
- Evarutil.occur_evar_upto for refine and the V82 compatibility mode
  - syntactic check without any normalization but inlining of defined evars
- Evarsolve.occur_evar_upto_types for evar_define
  - syntactic check without any normalization but inlining of defined evars
  - occur-check in the type of evars met
  - optimization for not visiting several time the same evar
- Evarsolve.noccur_evar for pattern unification and for inversion of
  substitution (evar/evar or evar/term problems)
  - syntactic check without any normalization but inlining of defined evars
  - occur-check in the type of evars met in arguments of projections
  - occur-check in the type of variables met in arguments of projections
  - optimization for not visiting several time the same evar
  - optimization for not visiting several time the type of the same variable
  - note: to go this way, it seems to me that it should check also in
    all types which are a cut-formula in the expression

One is much too lax:
- Evarconv.occur_rigidly
  - no recursive check except on the types of "forall" and sometimes
    in the arguments of an application
  - note: there is obviously a large room for refinements without
    loosing solutions

2 files changed, 102 insertions, 4 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b7e0535dad..73f2512431 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -97,19 +97,19 @@ let position_problem l2r = function
   | CONV -> None
   | CUMUL -> Some l2r
 
-let occur_rigidly ev evd t = 
+let occur_rigidly (evk,_ as ev) evd t =
   let rec aux t =
     match kind_of_term (whd_evar evd t) with
     | App (f, c) -> if aux f then Array.exists aux c else false
     | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
     | Proj (p, c) -> not (aux c)
-    | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false
+    | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
     | Cast (p, _, _) -> aux p
     | Lambda _ | LetIn _ -> false
     | Const _ -> false
     | Prod (_, b, t) -> ignore(aux b || aux t); true
     | Rel _ | Var _ -> false
-    | Case _ -> false
+    | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
   in try ignore(aux t); false with Occur -> true
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
@@ -478,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	      ise_try evd 
 	        [eta;(* Postpone the use of an heuristic *)
 		 (fun i -> 
-		   if not (occur_rigidly (fst ev) i tR) then
+		   if not (occur_rigidly ev i tR) then
                      let i,tF =
                        if isRel tR || isVar tR then
                          (* Optimization so as to generate candidates *)
diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v
new file mode 100644
index 0000000000..dce1f764c3
--- /dev/null
+++ b/test-suite/bugs/closed/4955.v
@@ -0,0 +1,98 @@
+(* An example involving a first-order unification triggering a cyclic constraint *)
+
+Module A.
+Notation "{ x : A | P }" := (sigT (fun x:A => P)).
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation "p @ q" := (eq_trans p q) (at level 20).
+Notation "p ^" := (eq_sym p) (at level 3).
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) 
+: P y :=
+  match p with eq_refl => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only 
+parsing).
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with eq_refl => eq_refl end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f 
+x) = f y
+  := match p with eq_refl => eq_refl end.
+Axiom transport_compose
+  : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f 
+x)),
+    transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Delimit Scope functor_scope with functor.
+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) }.
+Arguments object_of {C%category D%category} f%functor c%object : rename, simpl 
+nomatch.
+Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] 
+m%morphism : rename, simpl nomatch.
+Section path_functor.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Local Notation path_functor'_T F G
+    := { HO : object_of F = object_of G
+       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) 
+(GO d))
+                   HO
+                   (morphism_of F)
+         = morphism_of G }
+         (only parsing).
+  Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> 
+path_functor'_T F G
+    := fun H'
+       => (ap object_of H';
+             (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
+
+End path_functor.
+End A.
+
+(* A variant of it with more axioms *)
+
+Module B.
+Notation "{ x : A | P }" := (sigT (fun x:A => P)).
+Notation "( x ; y )" := (existT _ x y).
+Notation "p @ q" := (eq_trans p q) (at level 20).
+Notation "p ^" := (eq_sym p) (at level 3).
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only 
+parsing).
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with eq_refl => eq_refl end.
+Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f 
+x) = f y.
+Axiom transport_compose
+  : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f 
+x)),
+    transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+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) }.
+Arguments object_of {C D} f c : rename, simpl nomatch.
+Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch.
+Section path_functor.
+  Variable C D : PreCategory.
+  Local Notation path_functor'_T F G
+    := { HO : object_of F = object_of G
+       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) 
+(GO d))
+                   HO
+                   (morphism_of F)
+         = morphism_of G }.
+  Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> 
+path_functor'_T F G
+    := fun H'
+       => (ap object_of H';
+             (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
+
+End path_functor.
+End B.