I'm not sure why the type-classes 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 choice, I'm not sure where, but importing all_ssreflect suffices to obtain it.

Note that [fooType of X] works for other types as well, such as eqType, 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.

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 choice, I'm not sure where, but importing all_ssreflect suffices to obtain it. For the latter, you need to import at least ssreflect.

Note that [fooType of X] works for other types as well, such as eqType, 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.