The following snippet can't pass type checking.
From mathcomp Require Import choice.
Definition exfn (A:countType) := false.
(* Fail *) Check exfn nat.
Failed with message: The term "nat" has type "Set" while it is expected to have type "countType".
How to instantiate A with nat properly?
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.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.
choice, you just need to import ssreflect for it to work. It's usually a good idea to add From Coq Require Import ssreflect ssrbool ssrfun by default (if you're not importing all_ssreflect), as not doing so will typically result in cryptic errors.
$\endgroup$
Commented
Apr 13, 2022 at 13:36
I see there is a nat_countType in mathcomp.ssreflect.choice:
From mathcomp Require Import choice.
Definition exfn (A:countType) := false.
Check exfn nat_countType.
Variable (x : nat_countType).
Definition y : nat := x + 42.
