The following snippet fails typeclass resolution while eauto works with typeclass_instances.

```
From Coq Require Import Relation_Definitions RelationClasses.
Global Open Scope predicate_scope.
Notation "'pred'" := (predicate (Tcons nat Tnil)).
#[local]
Typeclasses Transparent relation binary_relation.
Set Printing Implicit.
Set Typeclasses Debug Verbosity 2.
Goal forall (P : pred), P <∙> P.
Proof.
intros.
Fail reflexivity.
(* Debug: 1.1: simple apply @Equivalence_Reflexive on *)
(* (@Reflexive pred (@predicate_equivalence (Tcons nat Tnil))) failed with: In environment *)
(* P : pred *)
(* Unable to unify "binary_relation pred" with "relation pred". *)
assert (Equivalence (@predicate_equivalence (Tcons nat Tnil))) as _. {
typeclasses eauto.
}
assert (Reflexive (@predicate_equivalence (Tcons nat Tnil))) as _. {
Fail typeclasses eauto.
(* Debug: 1.1: simple apply @Equivalence_Reflexive on *)
(* (@Reflexive pred (@predicate_equivalence (Tcons nat Tnil))) failed with: In environment *)
(* P : pred *)
(* Unable to unify "binary_relation pred" with "relation pred". *)
unify (binary_relation pred) (relation pred).
simple apply @Equivalence_Reflexive.
typeclasses eauto.
}
assert (Reflexive (@predicate_equivalence (Tcons nat Tnil))) as _. {
debug eauto with typeclass_instances.
(* Debug: 1 depth=5 *)
(* Debug: 1.1 depth=4 simple apply @Equivalence_Reflexive *)
(* Debug: 1.1.1 depth=4 simple apply @predicate_equivalence_equivalence *)
}
Abort.
```

It seems that the problem comes from that `typeclasses eauto`

does not know how to unify “binary_relation pred” with “relation pred”, but both `unify`

and `eauto`

clearly do. Is this expected? How do we fix this? I’ve tried to make `binary_relation`

and `relation`

transparent but it doesn’t help.