Unification: Added a heuristic to solve problems of the form

?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to
know if it occurs in rigid position or not. Such equations typically
come from matching problems such as "match a return ?T[a] with pair a1
a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the
return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified
with ?A.  This possible dependency is kept since commits r15060-15062.
The heuristic is to restrict ?T so that the dependency is removed,
leading to a behavior similar to the one existing before these commits.

This allows BGsection15.v, from contrib Ssreflect, to compile as it
did before these commits.

Also, removed one function exported without true need in r15061.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 63 insertions, 11 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 2bbdc76cf9..a87b9f5107 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -457,6 +457,9 @@ let list_map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
+let list_map_to_array f l =
+  Array.of_list (List.map f l)
+
 let rec list_smartfilter f l = match l with
     [] -> l
   | h::tl ->
diff --git a/lib/util.mli b/lib/util.mli
index 8f8475afd7..380f58eaba 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -101,6 +101,7 @@ val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
 val list_map4 :
   ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array
 val list_filter_i :
   (int -> 'a -> bool) -> 'a list -> 'a list
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index dc7d10b475..cddfbd5d14 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -743,6 +743,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 ->
       let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in
       solve_refl ~can_drop:true f env evd evk1 args1 args2, true
+  | Evar ev1, Evar ev2 ->
+      solve_evar_evar ~force:true
+        (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       (* and otherwise second-order matching *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 371e37bc83..00501a8931 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -136,6 +136,16 @@ let whd_head_evar_stack sigma c =
 
 let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
+let noccur_evar evd evk c =
+  let rec occur_rec c = match kind_of_term c with
+  | Evar (evk',_ as ev') ->
+      (match safe_evar_value evd ev' with
+       | Some c -> occur_rec c
+       | None -> if evk = evk' then raise Occur)
+  | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; true with Occur -> false
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -704,7 +714,7 @@ let is_unification_pattern_meta env nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l & not (occur_evar evk t) then
+  if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then
     let args = remove_instance_local_defs evd evk (Array.to_list args) in
     let n = List.length args in
     match find_unification_pattern_args env (args @ l) t with
@@ -1078,8 +1088,10 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
 let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
   match res with
-  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
-  | _ -> res
+  | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
+      CannotInvert
+  | _ ->
+      res
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -1320,6 +1332,19 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
   | Rel n -> n <= k || Intset.mem n fv_rels
   | _ -> is_constrainable_in k (ev,fvs) t
 
+let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
+  let filter1 =
+    restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
+  in
+  let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
+  let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
+  let filter2 =
+    restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
+  in
+  let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
+  let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
+  evd,ev1,ev2
+
 exception EvarSolvedOnTheFly of evar_map * constr
 
 let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
@@ -1350,13 +1375,17 @@ let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd ev2 c
 
-let solve_evar_evar f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
   if are_canonical_instances args1 args2 env then
     (* If instances are canonical, we solve the problem in linear time *)
     let sign = evar_filtered_context (Evd.find evd evk2) in
-    let subst = List.map (fun (id,_,_) -> mkVar id) sign in
-    Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd
+    let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in
+    Evd.define evk2 (mkEvar(evk1,id_inst)) evd
   else
+    let evd,ev1,ev2 =
+      (* If an evar occurs in the instance of the other evar and the
+         use of an heuristic is forced, we restrict *)
+      if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
     let aliases = make_alias_map env in
     try solve_evar_evar_l2r f g env evd aliases ev1 ev2
     with CannotProject filter1 ->
@@ -1599,8 +1628,11 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
   match kind_of_term rhs with
   | Evar (evk2,argsv2 as ev2) ->
-      if evk = evk2 then solve_refl conv_algo env evd evk argsv argsv2
-      else solve_evar_evar (evar_define conv_algo) conv_algo env evd ev ev2
+      if evk = evk2 then
+        solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
+      else
+        solve_evar_evar ~force:choose
+          (evar_define conv_algo) conv_algo env evd ev ev2
   | _ ->
   try solve_candidates conv_algo env evd ev rhs
   with NoCandidates ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 59c1c71206..bef5398aab 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -17,9 +17,6 @@ open Evd
 open Environ
 open Reductionops
 
-val restrict_upon_filter :  Evd.evar_map ->
-           Evd.evar -> (constr -> bool) -> constr list -> bool list option
-
 (** {5 This modules provides useful functions for unification modulo evars } *)
 
 (** {6 Metas} *)
@@ -91,6 +88,10 @@ val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 val solve_refl : ?can_drop:bool -> conv_fun -> env ->  evar_map ->
   existential_key -> constr array -> constr array -> evar_map
+val solve_evar_evar : ?force:bool ->
+  (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun ->
+  env ->  evar_map -> existential -> existential -> evar_map
+
 val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
   bool option * existential * constr -> evar_map * bool
 val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 906eb0fc9a..e6088091b1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -367,3 +367,15 @@ Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _))
            (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
 
 End Bigop.
+
+(* Check the use of (at least) an heuristic to solve problems of the form
+   "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can
+   eventually be erased in t *)
+
+Section evar_evar_occur.
+  Variable id : nat -> nat.
+  Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2.
+  Variable g : forall y, id y = 0 /\ id y = 0.
+  (* Still evars in the resulting type, but constraints should be solved *)
+  Check match g _ with conj a b => f _ a b end.
+End evar_evar_occur.