Coersion for SubmonoidClass

Stream: mathlib4

[Nailin Guan]

Is there an reason why we don't have CoeOut A (Submonoid G) when instance [SubmonoidClass A G], same for SubgroupClss. Thank you.

[Edward van de Meent]

I don't know that's possible, as A doesn't get mentioned in the second argument?

[Edward van de Meent]

And there are many classes which might want such an instance

[Nailin Guan]

I already writen it and CI passed:

@[to_additive]
instance (priority := 50) SubmonoidClass.toSubmonoid {A M : Type*} [Monoid M] [SetLike A M]
    [SubmonoidClass A M] : CoeOut A (Submonoid M) :=
  ⟨fun S ↦ ⟨⟨S, MulMemClass.mul_mem⟩, OneMemClass.one_mem S⟩⟩

@[to_additive]
instance (priority := 50) SubgroupClass.toSubgroup {A M : Type*} [Group M] [SetLike A M]
    [SubgroupClass A M] : CoeOut A (Subgroup M) :=
  ⟨fun S ↦ ⟨⟨⟨S, MulMemClass.mul_mem⟩, OneMemClass.one_mem S⟩, InvMemClass.inv_mem⟩⟩

[Edward van de Meent]

do both these instances trigger? there might be an issue because the second argument to CoeOut is a semiOutParam...

[Edward van de Meent]

they do... i guess i don't quite understand what the difference between OutParam and semiOutParam is

[Anne Baanen]

Suppose we have a Class ?X ?Y goal, then:

• if ?Y is a semiOutParam, Lean will start synthesizing instances even if the value for ?Y is not yet known

• if ?Y is marked with an outParam, Lean will start synthesizing instances only if the value for X is known, and always replace ?Y with a new metavariable before starting synthesis

Basically, semiOutParam promises that this value will be determined if the values for the other parameters are known, and outParam requires that this value must be determined by the values for the other parameters.

[Anne Baanen]

One important difference is that outParam means the first instance that works for X is always chosen (and causes an error if Y doesn't unify), and semiOutParam will continue searching if Y doesn't unify.

[Edward van de Meent]

Anne Baanen said:

Basically, semiOutParam promises that this value will be determined if the values for the other parameters are known,

so then the suggested instances are not good design?

[Edward van de Meent]

because there is no way to choose between Subgroup M and Submonoid M?

[Anne Baanen]

Indeed, there is some debate on whether we want these coercions at all: #mathlib4 > too many FunLikes @ 💬

[Anne Baanen]

Most of the coercions for FunLikes use CoeTC which is an implementation detail that we started using in the Lean 4 port and nobody has taken time to replace with the user-facing classes.

[Anne Baanen]

I think in this case CoeOut is okay, since it will find the right instance if we know whether we want a Subgroup or a Submonoid.

[Nailin Guan]

I've opened #22230, see channel PR review for later discussion.