## Stream: math-comp users

### Topic: Missing coercion from {fset C} to finType

#### Ricardo (Nov 15 2022 at 22:41):

Why is there no coercion from `{fset C}` (given `C : choiceType`) to `finType` in `mathcomp.finmap`?

#### Ricardo (Nov 16 2022 at 00:18):

Wait. I'm not sure there's no coercion. In the following code it coerces in one situation and not in the other.

``````From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module X.
Definition symb (T : finType) (R : rel T) :=
[forall x, forall y, R x y == R y x].
Definition rel0 (T : Type) (_ _ : T) := false.
Variable (C : choiceType) (f : {fset C}).
Set Printing Coercions. Set Printing Implicit.
Check symb (@rel0 f). (* here the coercion works *)
Definition g (T : finType) := tt.
Check g f. (* here it doesn't *)
Check g (@fset_sub_finType C f). (* here no problem again *)
``````

#### Paolo Giarrusso (Nov 16 2022 at 00:21):

The working case is coercing to Type not finType?

#### Ricardo (Nov 16 2022 at 00:22):

The output of `Check symb (@rel0 f)` is

``````@symb (@fset_sub_finType C f)
(@rel0 (@fset_sub_type C f))
: bool
``````

#### Paolo Giarrusso (Nov 16 2022 at 00:22):

rel0 takes a Type, so the coercion is inserted. The only finType is symb's argument, which is not generated by a coercion but by canonical structure inference.

#### Paolo Giarrusso (Nov 16 2022 at 00:24):

does that help / make sense?

#### Paolo Giarrusso (Nov 16 2022 at 00:26):

double-checked and https://github.com/math-comp/finmap/blob/master/finmap.v shows indeed

``````Canonical fset_sub_finType := Eval hnf in FinType fset_sub_type fset_sub_finMixin.
...
Coercion fset_sub_type : finSet >-> predArgType.
``````

#### Paolo Giarrusso (Nov 16 2022 at 00:27):

I guess you'd try `g [finType of f]`, as needed when you need Coq to infer extra structure?

#### Ricardo (Nov 16 2022 at 00:58):

Shouldn't that coercion in the second line help with `g f`?

#### Ricardo (Nov 16 2022 at 00:58):

Or would it have to be `Coercion fset_sub_type : finSet >-> finType` for it to work as I expect?

#### Ricardo (Nov 16 2022 at 01:07):

I was mixing up `fset_sub_type` with `fset_sub_finType`. The former is a coercion in `mathcomp.finmap` but not the latter. If I make `fset_sub_finType` a coercion then `g f` works as expected.

``````Coercion fset_sub_finType : finSet >-> finType.
Check g f. (* no problem *)
``````

Are there good reasons why `fset_sub_finType` isn't made a coercion in `mathcomp.finmap`?

#### Paolo Giarrusso (Nov 16 2022 at 01:11):

I'll leave this to the actual math-comp experts :-)

#### Cyril Cohen (Nov 16 2022 at 08:20):

Ricardo said:

I was mixing up `fset_sub_type` with `fset_sub_finType`. The former is a coercion in `mathcomp.finmap` but not the latter. If I make `fset_sub_finType` a coercion then `g f` works as expected.

``````Coercion fset_sub_finType : finSet >-> finType.
Check g f. (* no problem *)
``````

Are there good reasons why `fset_sub_finType` isn't made a coercion in `mathcomp.finmap`?

That would make sense indeed.

#### Ricardo (Nov 17 2022 at 23:09):

@Cyril Cohen, I see on the github page of `mathcomp.finmap` that you're one of the contributors. Would you like to add this coercion to a possible next release?

#### Cyril Cohen (Nov 18 2022 at 08:52):

Yes, let's do this. Could you open an issue or submit a PR?

#### Ricardo (Nov 18 2022 at 18:48):

I can open an issue. Here it is https://github.com/math-comp/finmap/issues/102

Last updated: Jul 15 2024 at 20:02 UTC