5
$\begingroup$

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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – Alexander Gryzlov
    Commented Apr 13, 2022 at 13:36
  • $\begingroup$ Also, technically the mechanism used here is canonical structures, not typeclasses. $\endgroup$
    – Alexander Gryzlov
    Commented Apr 13, 2022 at 13:41
1
$\begingroup$

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.
Improve this answer
$\endgroup$
1
  • $\begingroup$ But supposedly the type-classes mechanism should be able to pick it up automatically? $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Apr 13, 2022 at 7:46

Not the answer you're looking for? Browse other questions tagged or ask your own question.