Hi,

What would be the proper way to refer to this canonical in MC2?

```
Canonical seq_sub_finType := Eval hnf in FinType sT (seq_sub_finMixin s).
```

Trying

```
Definition seq_sub_finType {T:eqType} (s:seq T): finType := seq_sub s.
```

gives

```
The term "seq_sub (T:=T) s" has type "Type" while it is expected to have type "finType".
```

even though `HB.about`

reports:

```
HB: seq_sub is canonically equipped with structures:
- SubChoice
choice.Choice
(from "./fintype.v", line 1618)
- SubType
(from "./fintype.v", line 1561)
- SubFinite
fintype.Finite
(from "./fintype.v", line 1620)
- Countable
SubCountable
(from "./fintype.v", line 1619)
- eqtype.Equality
SubEquality
(from "./fintype.v", line 1562)
```

, i.e., claims to be a `finType`

instance.

It does not work because the `finType`

structure comes from the `subType`

structure, so you need `T`

to be itself a `finType`

for the inference to work. Since you can have only one canonical instance for a given structure and subject, you will not be able to declare your own on `seq_sub`

. What you can do is declare an alias for `seq_sub`

and declare the instances you want on your alias.

It took some convincing to make it work, but the following compiles:

```
Definition adhoc_seq_sub := seq_sub.
HB.instance Definition _ (T : eqType) (s : seq T) := Equality.copy (adhoc_seq_sub T s) (seq_sub s).
HB.instance Definition _ (T : eqType) (s : seq T) := isCountable.Build (adhoc_seq_sub T s) (@seq_sub_pickleK T s).
HB.instance Definition _ (T : eqType) (s : seq T) := isFinite.Build (adhoc_seq_sub T s) (@seq_sub_axiom T s).
```

Cyril Cohen has marked this topic as unresolved.

Actually `seq_sub T`

type is a `finType`

if `T`

is a ** choiceType**, not a

`finType`

https://github.com/math-comp/math-comp/blob/27b595cee274ade2fdc4a3a8e80213e3bb07a8bf/mathcomp/ssreflect/fintype.v#L1613-L1627

if you can use a `choiceType`

instead of an `eqType`

in your development I would advise you to rely on `choiceType`

instead. Otherwise `adhoc_seq_sub`

choice will be incompatible with the canonical choice function of the base type.

Last updated: Oct 13 2024 at 01:02 UTC