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