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...

1 files changed, 5 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d5e3c6715..933684143 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 =