I'm not sure why the
type-classes canonical structure mechanism can't figure this out on its own. However, there are two ways of making it explicit:
nat_countType, as mentioned by Pierre, and
[countType of nat].
The latter is a notation defined outside For the latter, you need to import at least
choice, I'm not sure where, but importing
all_ssreflect suffices to obtain it.
[fooType of X] works for other types as well, such as
choiceType, etc. And it works even when
X is not a "base" type. For example,
[countType of nat * nat] works, whereas
"nat*nat"_countType is not a thing.