Why is there no coercion from {fset C}
(given C : choiceType
) to finType
in mathcomp.finmap
?
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 *)
The working case is coercing to Type not finType?
The output of Check symb (@rel0 f)
is
@symb (@fset_sub_finType C f)
(@rel0 (@fset_sub_type C f))
: bool
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.
does that help / make sense?
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.
I guess you'd try g [finType of f]
, as needed when you need Coq to infer extra structure?
Shouldn't that coercion in the second line help with g f
?
Or would it have to be Coercion fset_sub_type : finSet >-> finType
for it to work as I expect?
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
?
I'll leave this to the actual math-comp experts :-)
Ricardo said:
I was mixing up
fset_sub_type
withfset_sub_finType
. The former is a coercion inmathcomp.finmap
but not the latter. If I makefset_sub_finType
a coercion theng 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 inmathcomp.finmap
?
That would make sense indeed.
@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?
Yes, let's do this. Could you open an issue or submit a PR?
I can open an issue. Here it is https://github.com/math-comp/finmap/issues/102
Last updated: Mar 28 2024 at 23:01 UTC