finite_countable Hint Immediate in typeclass_instances is broken
The use of Hint Immediate finite_countable : typeclass_instances
seems to get triggered when it really shouldn't:
From stdpp Require Import gmap.
From stdpp Require finite.
Definition addr: Type := (nat * nat).
(* this is failing because (l:finite.Finite addr), which makes no sense! *)
Fail Definition foo l (m: gmap addr nat) : unit := l.
(* we can fix this situation by making the hint a regular [Hint Resolve] *)
Remove Hints finite.finite_countable : typeclass_instances.
Hint Resolve finite.finite_countable : typeclass_instances.
Definition foo l (m: gmap addr nat) : unit := l.
In particular it looks like it uses an assumption l : ?T
and resolves T
.