Strange failure in typeclass resolution

Using Coq
1

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.

2

As an extra information: the first failure message says simple apply Equivalence_Reflexive failed, but that tactic as-is works on the goal successfully.

3

You need to make the arrows constant transparent as well for unification of typeclasses, while by default it is considered opaque so one can index typeclasses by that constant. predicate uses arrows which models n-ary predicates, so if you can’t unfold arrows Coq cannot unify it with relation.