# How to provide a countType when using mathcomp?

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 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.

• The notation actually is defined in 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. Apr 13 at 13:36
• Also, technically the mechanism used here is canonical structures, not typeclasses. Apr 13 at 13:41

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.

• But supposedly the type-classes mechanism should be able to pick it up automatically? Apr 13 at 7:46