Take benefit of improved name preservation of evars in e2fa65fcc.
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...
Improving error message when one instance-hole is not found.

Still to do:
- Decide between using SeveralInstancesFound or raising an error when
  multiple instances exist.
- Use a proper printer for evars instead of the debugging
  pr_evar_map_filter printer in pr_constraints.