I expected that if `K : choiceType`

then `{fset K}`

could be interpreted as a `choiceType`

. At least that's what I thought the following line of the `finmap`

library was doing:

```
Canonical fset_choiceType := Eval hnf in ChoiceType {fset K} fset_choiceMixin.
```

However:

```
From mathcomp Require Import all_ssreflect finmap.
Variable K : choiceType.
Variable s : {fset K}.
Variable f : choiceType -> bool.
Fail Check (f s).
(* The command has indeed failed with message:
The term "s" has type "{fset K}" while it is expected to have type
"choiceType". *)
```

More or less by chance I discovered that `Check (f (fset_sub_choiceType s)).`

works, while `Check (f (fset_choiceType s)).`

does not.

I'm confused. What is going on?

Not sure I follow, `s`

is not a choiceType but an element of the type, so indeed Coq can't type that term

`Check (f {fset K}).`

works.

We all get confused by types that are elements of others types often, at least I do :)

You are right, I messed up my example. Should have written `Definition s := {fset K}`

, or used it directly. But over here `Check (f {fset K})`

fails with the same error:

```
The term "{fset K}" has type "Type" while it is expected to have type
"choiceType".
```

I have finmap 1.5.0. Is this possibly a bug?

Actually, with `Variable s : {fset K}`

, both the coercion from `s`

to `Type`

and `{fset K}`

itself are *canonically* choice types, which is not the same has having type `choiceType`

. You can recover the canonical instance using `[choiceType of _]`

, and both `f [choiceType of s]`

and `f [choiceType of {fset K}]`

should work.

Great, that works! But it seems that I don't understand what it means for something to be canonically a `choiceType`

. I thought it meant that if a `choiceType`

was needed to correctly type an expression, then the `choiceType`

instance would be chosen automatically. And in my previous experience with Coq similar things have happened with a number of canonical things. Or maybe it was a coincidence and the inference happened because of other reasons?

the inference did happen because of canonical structures, but there are specific rules

IIUC, for `f : {X : choiceType} -> X -> bool`

, such inference would happen.

but (once you show coercions) this type will be sth like `f : {X : choiceType} -> projectType X -> bool`

(dunno the actual name)

and what Canonical Structure inference does, at its root, is that they solve equations of form `projectType ?X = {fset K}`

by filling in the right `?X`

.

Wait, what is `projectType`

?

But going from `{fset K}`

to `[choiceType of {fset K}]`

is not an equation of that form.

sorry I don’t know the actual name, but I expect sth like `projectType : {choiceType} -> Type`

Oh right, sorry. So it's the coercion from `choiceType`

to `Type`

.

(the name seems `sort`

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/choice.v#L279, but using `Set Printing Coercion`

when printing types using it will be more helpful)

I’m no math-comp expert, but I was pointed to https://hal.inria.fr/hal-00816703v1/document to understand CS basics a while ago, and it has a better version of what I was saying

Yes, the convention is to define the coercion inside a Module (named after the structure) and then call it `sort`

. So there is `Finite.sort`

, `Choice.sort`

etc.

Also, it might be worthwhile to point out the reason why the type is written `{fset T}`

rather than `fset T`

: In order to construct the type of finite sets, one needs not only the type `T`

but indeed its `choiceType`

instance.

The notation `{fset T}`

plays some trickery with phantom types to trigger canonical instance resolution for `T`

, allowing one to write `{fset nat}`

rather than `fset nat_choiceType`

.

FTR there is a, rather terse my bad, explanation of this at page 136 of https://zenodo.org/record/4282710#.X8D4MMIo-8Q

@Enrico Tassi Terse and not exactly margin-respecting :smirk:

My $\LaTeX$ is :pile_of_poo:

Last updated: Jul 25 2024 at 16:02 UTC