The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Dear coq-club,

I am trying to use the "typeclasses eauto" tactic in combination with
custom hint bases, and I am observing confusing behavior with respect to
hints added using "Hint Resolve".

The snippet below (also attached) illustrates the issue.

Essentially, in many cases, hints registered using "Hint Resolve" seem
to not be picked up. However, adding them instead using "Hint Extern"
and a pattern that exactly matches the conclusion of the lemma makes
them work...

Of course I could turn all my "Hint Resolve" into "Hint Extern" (that
would be a bit tedious), but I'm wondering if there's a reason for this
behavior of "typeclasses eauto". Maybe this is the result of some
subtlety of the tactic I'm not aware of?

Cheers,
Armaël

-------------

Record type : Type := Pack { sort : Type }.
Coercion sort : type >-> Sortclass.

Definition nat_packed := Pack nat.

Parameter R : forall (A : Type), (A -> nat) -> (A -> nat) -> Prop.
Hypothesis R_refl : forall (A : Type) f, R A f f.
Hint Resolve R_refl : myhints.

Goal forall f, R nat_packed f f.
  intro. simple apply R_refl.
Qed. (* ok *)

Goal forall f, R nat_packed f f.
  intro. typeclasses eauto with myhints.
Qed. (* ok *)

Goal R nat_packed (fun x => x) (fun x => x).
  simple apply R_refl.
Qed. (* ok *)

Goal R nat_packed (fun x => x) (fun x => x).
  Fail typeclasses eauto with myhints.
Abort. (* ?? *)

Print HintDb myhints.
(* This seems to replicate the exact pattern that can be found for
[R_refl] in [myhints]... *)
Hint Extern 0 (R _ ?f ?f) => simple apply R_refl : myhints2.

Goal R nat_packed (fun x => x) (fun x => x).
  typeclasses eauto with myhints2.
Qed. (* ??? *)

------------
Record type : Type := Pack { sort : Type }.
Coercion sort : type >-> Sortclass.

Definition nat_packed := Pack nat.

Parameter R : forall (A : Type), (A -> nat) -> (A -> nat) -> Prop.
Hypothesis R_refl : forall (A : Type) f, R A f f.
Hint Resolve R_refl : myhints.

Goal forall f, R nat_packed f f.
  intro. simple apply R_refl.
Qed. (* ok *)

Goal forall f, R nat_packed f f.
  intro. typeclasses eauto with myhints.
Qed. (* ok *)

Goal R nat_packed (fun x => x) (fun x => x).
  simple apply R_refl.
Qed. (* ok *)

Goal R nat_packed (fun x => x) (fun x => x).
  Fail typeclasses eauto with myhints.
Abort. (* ?? *)

Print HintDb myhints.
(* This seems to replicate the exact pattern that can be found for [R_refl] in
   [myhints]... *)
Hint Extern 0 (R _ ?f ?f) => simple apply R_refl : myhints2.

Goal R nat_packed (fun x => x) (fun x => x).
  typeclasses eauto with myhints2.
Qed. (* ??? *)