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

1 files changed, 4 insertions, 4 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b7e0535da..73f251243 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 *)