default_instance porting notes

Stream: mathlib4

[Johan Commelin]

I am looking at Mathlib/LinearAlgebra/Quotient/Defs.lean, and it contains the following (roughly L120-190)

-- Porting note: should this be marked as a `@[default_instance]`?
/-- Shortcut to help the elaborator in the common case. -/
instance instSMul : SMul R (M ⧸ P) :=
  Quotient.instSMul' P

-- 8<   8<  8<    <<snip>>

-- Porting note: should this be marked as a `@[default_instance]`?
instance mulAction (P : Submodule R M) : MulAction R (M ⧸ P) :=
  Quotient.mulAction' P

-- 8<   8<  8<    <<snip>>

-- Porting note: should this be marked as a `@[default_instance]`?
instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
  Quotient.smulZeroClass' P

-- 8<   8<  8<    <<snip>>

-- Porting note: should this be marked as a `@[default_instance]`?
instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
  Quotient.distribSMul' P

-- 8<   8<  8<    <<snip>>

-- Porting note: should this be marked as a `@[default_instance]`?
instance distribMulAction (P : Submodule R M) : DistribMulAction R (M ⧸ P) :=
  Quotient.distribMulAction' P

-- 8<   8<  8<    <<snip>>

-- Porting note: should this be marked as a `@[default_instance]`?
instance module (P : Submodule R M) : Module R (M ⧸ P) :=
  Quotient.module' P

[Johan Commelin]

My inclination is that the answer to all these questions is: "no".

[Johan Commelin]

But before I remove these porting notes, I would be happy to hear from e.g. @Eric Wieser or @Kyle Miller .

[Kevin Buzzard]

My personal feeling about these instances is that they shouldn't even be global let alone default

[Kevin Buzzard]

Oh sorry I take that back, the ones I don't like are when S acts on M then it acts on M/P where P is a sub-R-module, these ones are ok

[Eric Wieser]

Can you track down the PR they were added in to see if there was discussion at the time?

[Johan Commelin]

#2286 and #mathlib4 > LinearAlgebra.Quotient !4#2286

No discussion at the time.

[Johan Commelin]

I claim these should be removed: #23818

[Kyle Miller]

@Johan Commelin I agree, these should not be @[default_instance]. Doing so could cause modules with unspecified types to specialize to be quotient modules (if they work as default instances at all)