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?

$\endgroup$

2 Answers 2

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.

$\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$ Apr 13 at 13:36
  • $\begingroup$ Also, technically the mechanism used here is canonical structures, not typeclasses. $\endgroup$ Apr 13 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.
$\endgroup$
1
  • $\begingroup$ But supposedly the type-classes mechanism should be able to pick it up automatically? $\endgroup$ Apr 13 at 7:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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