Can restrictScalars be a coercion?

Stream: mathlib4

[Martin Winter]

In a recent PR we implemented coercion from a submodule to a pointed cone, which is just restriction to the non-negative scalars. Is there a reason to not have the general restrictScalars as a coercion like this:

instance {p : Submodule R M} : CoeDep (Submodule R M) p (Submodule S M) := ⟨restrictScalars S p⟩

I know from my own code that a lot of statements would become much shorter.
We could then also put @[coe] on restrictScalars for readability.

[Eric Wieser]

Why do you need CoeDep here?

[Eric Wieser]

Martin Winter said:

We could then also put @[coe] on restrictScalars for readability.

This is a bad idea, since the goal view then shows p.restrictScalars S as ↑S p

[Martin Winter]

Eric Wieser said:

Why do you need CoeDep here?

The honest answer is: because I could not make it work with any other Coe variant. It always complains that it cannot find a synthesization order.

[Martin Winter]

Eric Wieser said:

Martin Winter said:

We could then also put @[coe] on restrictScalars for readability.

This is a bad idea, since the goal view then shows p.restrictScalars S as ↑S p

This is already the case for LinearMap.restrictScalars and I always found this to be more readable than the alternative.

[Kevin Buzzard]

Yes I noticed this "weirdness" with LinearMap.restrictScalars recently and after having considered reporting it as an issue I decided it might actually be more helpful to just to leave it as it is and get used to it :-) It's weird but helpful notation :-)