Is there any reason why `{fset K}`

, `{fmap K -> V}`

, and `{fsfun K -> V for dflt}`

from finmap library have instances of `choiceType`

, but no `countType`

? Or is it just by accident (or wasn't needed before)?

`countType`

would be more restrictive, no?

I mean, if we have that `K : countType`

then we can derive `{fset K} : countType`

.

I actually implemented the required instances in my project, e.g for `fset`

:

```
Section FSetCount.
Variable (K : countType).
Definition fset_countMixin := Eval hnf in [countMixin of {fset K} by <:].
Canonical fset_countType := Eval hnf in CountType {fset K} fset_countMixin.
End FSetCount.
```

Just what to know if those instances were missing for some reason.

Perhaps, there are some hidden undesirable consequences which I just don't see?

`{fset K}`

has an instance of `finType`

, right? That implies it's a `countType`

as well. Coq doesn't complain about this:

```
Variable K : choiceType.
Variable s : {fset K}.
Check [countType of s].
```

from what I can recall, one can get a `countType`

from a `choiceType`

nearly automatically at any point, and I don't think any `finType`

is involved

But... isn't it possible to have a `choiceType`

that is not countable?

Ana de Almeida Borges said:

`{fset K}`

has an instance of`finType`

, right? That implies it's a`countType`

as well. Coq doesn't complain about this:`Variable K : choiceType. Variable s : {fset K}. Check [countType of s].`

Is `{fset K}`

has an instance of `finType`

though?

One can have an infinite amount of finite sets over some infinite type `K`

.

Still your code snippet confuses me, I can't understand where from `countType`

instance comes.

Ahh, I think in your example `[countType of s]`

actually derives `countType`

for the type of keys of `s`

, which is finite indeed.

```
Variable K : choiceType.
Variable s : {fset K}.
Let T := [countType of s].
Lemma test : Countable.sort T = (s : Type).
Proof. done. Qed.
```

Ok, maybe we are talking about different things and I just didn't read your original post with enough attention. You are asking about the statement `{fset K} : countType`

and not the statement `s : countType`

, is that it?

Yes, I need `countType`

instance for the type of finite sets themselves, not for the type of keys of some particular finite set.

Ok, sorry for the detour then. In that case I don't know, perhaps it was indeed never needed.

I made a PR for this issue https://github.com/math-comp/finmap/pull/87

Everyone interested is welcome to continue the discussion there.

Last updated: Jan 29 2023 at 19:02 UTC