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

0 files changed, 0 insertions, 0 deletions