HB does not interact well with old unification (hence tc)

[CohenCyril]

trafficstars

Example

From HB Require Import structures.
From Coq Require Import Relations Morphisms.

HB.mixin Record hasEquiv A := { equiv : relation A }.
HB.structure Definition Equiv := { A of hasEquiv A }.

HB.mixin Record Equiv_isSetoid A of Equiv A := {
  equivP : Equivalence (@equiv A)
}.
HB.structure Definition Setoid := {A of hasEquiv A & Equiv_isSetoid A}.
#[global] Existing Instance equivP.

HB.mixin Record isFoo A of Setoid A := {}.
HB.structure Definition Foo := {A of isFoo A & Setoid A}.

Lemma not_breaking (A : Setoid.type) : @Equivalence A (@equiv A).
Proof. apply @equivP. Qed.

Lemma not_breaking2 (A : Foo.type) : @Equivalence _ (@equiv A).
Proof. apply @equivP. Qed.

Lemma breaking (A : Foo.type) : @Equivalence A (@equiv A).
Proof.
Set Debug "all".
Set Printing All.
(* Check @equivP. *)
Fail apply @equivP.
Set Typeclasses Debug.
Fail typeclasses eauto.
Succeed refine (@equivP _).
Abort.

cc @robbertkrebbers @gares @fissored

Remark: Foo is the simplification of Ofe in Iris.

[gares]

Lemma breaking (A : Foo.type) : @Equivalence A (@equiv A).
Proof.
Set Debug "all".
Set Printing All.
(*@Equivalence (Foo.sort A) (@equiv (order_Foo__to__order_Equiv A))*)
Check @equivP.
(* : forall s,
@Equivalence
(Equiv.sort
   (Equiv.Pack (Setoid.sort s)
      (Equiv.Class (Setoid.sort s)
         (Setoid.order_hasEquiv_mixin (Setoid.sort s)
            (Setoid.class s)))))
(@equiv
   (Equiv.Pack (Setoid.sort s)
      (Equiv.Class (Setoid.sort s)
         (Setoid.order_hasEquiv_mixin (Setoid.sort s)
            (Setoid.class s)))))
*)
pose proof (H := @equivP).
simpl in H.
(*
H: forall s : Setoid.type,
    @Equivalence (Setoid.sort s)
      (@equiv (Equiv.Pack (Setoid.sort s) (Equiv.Class (Setoid.sort s) (Setoid.order_hasEquiv_mixin (Setoid.sort s) (Setoid.class s)))))
*)
apply H.
(* Fail apply @equivP. *)
Abort.

This is a bug in the old unification. I suspect it overreduces

(Equiv.sort
   (Equiv.Pack (Setoid.sort ?s) ...))

to

match ?s with ...

while evarconv has a piece of code I wrote a long ago to not unfold "stuck" canonical projections (but rather reduce the other side of the unification problem). Indeed if I simplify the lemma statement by hand in the correct way, then legacy unification performs the canonical inference we expect.