New approach to deal with evar-evar unification problems in different

types: we downcast the evar in the higher type to the lower type.

Then, we have the freedom to choose the order of instantiation
according to the instances of the evars (e.g. choosing the
instantiation for which pattern-unification is possible, if ever it is
possible in only one way - as shown by an example in contribution
Paco).

This still does not preserve compatibility because it happens that
type classes resolution is crucially dependent on the order of
presentation of the ?n=?p problems. Consider e.g. an example taken
from Containers. Both now and before e2fa65fccb9, one has this asymmetry:

Context `{Helt : OrderedType elt}.
Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h).

--> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y

Context `{Helt : OrderedType elt}.
Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y.

--> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt)

Then, embedding this example within a bigger one which relies on the
?n=?n' resolution order, one can get two incompatible resolution of
the same problem.

To be continued...

3 files changed, 24 insertions, 14 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 940eebbf7e..a6d5e1eac1 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1132,35 +1132,34 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
     if force then ensure_evar_independent g env evd ev1 ev2, None
     else (evd,ev1,ev2),pbty in
   let evi = Evd.find evd evk1 in
+  let evd =
     try 
       (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
 	 The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
       let evienv = Evd.evar_env evi in
-      let ctx, i = Reduction.dest_arity evienv evi.evar_concl in
+      let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in
       let evi2 = Evd.find evd evk2 in
       let evi2env = Evd.evar_env evi2 in
-      let ctx', j = Reduction.dest_arity evi2env evi2.evar_concl in
+      let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in
       let ui, uj = univ_of_sort i, univ_of_sort j in
 	if i == j || Evd.check_eq evd ui uj
 	then (* Shortcut, i = j *) 
-	  solve_evar_evar_aux f g env evd pbty ev1 ev2
-	  (* Avoid looping if postponing happened on previous evar/evar problem *) 
+	  evd
 	else if Evd.check_leq evd ui uj then
-	  solve_evar_evar_aux f g env evd (opp_problem pbty) ev2 ev1
+          let t2 = it_mkProd_or_LetIn (mkSort i) ctx2 in
+          downcast evk2 t2 evd
 	else if Evd.check_leq evd uj ui then
-	  solve_evar_evar_aux f g env evd pbty ev1 ev2
+          let t1 = it_mkProd_or_LetIn (mkSort j) ctx1 in
+          downcast evk1 t1 evd
 	else
 	  let evd, k = Evd.new_sort_variable univ_flexible_alg evd in
-	  let evd, ev3 = 
-	    Evarutil.new_pure_evar (Evd.evar_hyps evi) evd
-	      ~src:evi.evar_source ~filter:evi.evar_filter 
-	      ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) 
-	  in
+          let t1 = it_mkProd_or_LetIn (mkSort k) ctx1 in
+          let t2 = it_mkProd_or_LetIn (mkSort k) ctx2 in
 	  let evd = Evd.set_leq_sort env (Evd.set_leq_sort env evd k i) k j in
-	  let evd = solve_evar_evar_aux f g env evd (opp_problem pbty) (ev3,args1) ev1 in
-          f env evd (opp_problem pbty) ev2 (whd_evar evd (mkEvar (ev3,args1)))
+          downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
-      solve_evar_evar_aux f g env evd pbty ev1 ev2
+      evd in
+  solve_evar_evar_aux f g env evd pbty ev1 ev2
 
 type conv_fun =
   env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d5e3c6715c..9336841436 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -853,6 +853,11 @@ let restrict evk evk' filter ?candidates evd =
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
     defn_evars; evar_names }
 
+let downcast evk ccl evd =
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let evar_info' = { evar_info with evar_concl = ccl } in
+  { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
 let extract_conv_pbs evd p =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index df5269d345..f800a45474 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -243,6 +243,12 @@ val evar_declare :
 
 val restrict : evar -> evar -> Filter.t -> ?candidates:constr list ->
   evar_map -> evar_map
+(** Restrict an undefined evar into a new evar by filtering context and
+    possibly limiting the instances to a set of candidates *)
+
+val downcast : evar -> types -> evar_map -> evar_map
+(** Change the type of an undefined evar to a new type assumed to be a
+    subtype of its current type; subtyping must be ensured by caller *)
 
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an