Broken CommRing

Stream: mathlib4

[Patrick Massot]

I’m trying to bump MIL and it seems the algebraic hierarchy is broken. The following code used to work, but now complains I should define nsmul and zsmul. This seems to be a pretty serious regression.

[Patrick Massot]

And the explanation we have there in MIL is exactly about how nice it is to not have to define those…

[Matthew Ballard]

#6262

[Patrick Massot]

Thanks. This is extremely sad :cry:

[Patrick Massot]

I really feels like we are making the life of users worse because of performance issues we don’t understand well enough.

[Matthew Ballard]

The performance benefits were secondary there. Having Lean silently insert data when you are not absolutely sure it is the data you want was the problem.

[Patrick Massot]

I really don’t know what to write in MIL now, except for apologizing.

[Patrick Massot]

The cases where you don’t want those default values are extremely rare, right?

[Matthew Ballard]

To me there were not rare enough. I would like something equally ergonomic but with some notification it is happening.

[Matthew Ballard]

I suggested a code action for (semi-)default values there

[Patrick Massot]

It is really super super painful to me to throw away the chapter of MIL where I proudly explained how the community managed to make that non-painful.

[Eric Wieser]

I wonder if we can use nsmul := by exact_nsmulRec_and_warn in the type definition

[Patrick Massot]

I don’t see the difference if it means people have to fill in the field to get rid of the warning.

[Patrick Massot]

This is a really sad day for Mathlib.

[Eric Wieser]

Patrick Massot said:

I really don’t know what to write in MIL now, except for apologizing.

Indeed, I think the best you can do with mathlib master is

-- let's assume we don't care about `Module` instances for now
nsmul := nsmulRec; zsmul := zsmulRec

(perhaps with some more apologetic wording)

[Patrick Massot]

I already added such a line telling people to ignore those lines. But we have a whole chapter about algebraic hierarchies where I was explaining how the defaut value mechanism allowed to get the best of both worlds.

[Eric Wieser]

I think the key thing is that we really do want these nsmul :=s in Mathlib, and we don't currently have a way to allow downstream users to skip them

[Floris van Doorn]

I agree with Patrick that this is sad. I was very happy that the lightbulb since a few months has the "find minimal structure skeleton" command, which is really convenient for beginners, and now we're making it less convenient for beginners again.

[Patrick Massot]

If this is only for Mathlib then it should be a Mathlib linter, right?

[Eric Wieser]

Yes, but writing such a linter is much harder than removing the default.

[Eric Wieser]

Patrick Massot said:

I don’t see the difference if it means people have to fill in the field to get rid of the warning.

The warning could be disabled (or enabled) with an option, just like linter errors

(again, I agree a linter is better, but this mechanism is easier and presumably better than what we have right now)

[Patrick Massot]

Eric Wieser said:

I wonder if we can use nsmul := by exact_nsmulRec_and_warn in the type definition

Would you be happy with a PR implementing this suggestion? The tactic would emit the warning only if the current file is within Mathlib.

[Eric Wieser]

Yes, definitely; I was going to try one on my commute home anyway

[Patrick Massot]

Ok, maybe I should grade some exams and let you have fun during your commute.

[Jireh Loreaux]

Yeah, I really think we need the old behavior, possibly with a warning (but even that I'm not entirely keen on). For instance, at some point (in the hopefully not too distant future), we'll have ppow and psmul too. It really would be terrible to have to provide all those fields for new users.

[Eric Wieser]

Here's a prototype:

register_option linter.structureDiamondDefaults : Bool := {
  defValue := true
  descr := "Linter to check if structure fields that are often implicated in typeclass diamonds are using implciit default values." }

elab "exact_with_diamond_warning" tgt:name default:name msg:str: tactic => do
  -- stupid games because `ident` isn't allowed in the syntax parser (lean4#3328)
  let tgt' := Lean.mkIdent tgt.getName
  let default' := Lean.mkIdent default.getName
  -- TODO: use "Try this" somehow, but we don't have the position info we need
  let stx ← `(whereStructField| $tgt' := $default' )
  Lean.Linter.logLintIf linter.structureDiamondDefaults
    tgt
    (m!"Using default value {stx}, which may {msg.getString}." ++
    m!"If you are sure this is not an issue, write {stx} explicitly")
  Lean.Elab.Tactic.evalTactic <| ← `(tactic| exact $default')

[Eric Wieser]

#12608

[Eric Wieser]

Regarding MIL and

Thanks to these default values, most instances would be constructed exactly as with our previous definitions. But in the special case of ℤ we will be able to provide specific values.

I think this suggests that zsmul is only there to make things right for the instance on ℤ itself. While this is certainly a convenient thing to be able to say at this point in MIL, in mathlib it's fairly rare to have types where the default zsmul is actually fine.

[Eric Wieser]

Probably the earliest motivating example that conceivably could end up in MIL comes from working with vectors of complex numbers, and wanting to be able to "multiply" them by complex / real / rational / int / nat scalars. Obviously you don't want to write 5 scalar multiply functions, and so you write instance [SMul R Complex] : Smul R ComplexVec and now run into trouble when R = Int.

[Yuyang Zhao]

Does #9154 not work with autoParam? Is there a way to write it as an optParam? Or we can just write something in the warning......

[Patrick Massot]

Eric Wieser said:

#12608

This doesn’t build yet.

[Yury G. Kudryashov]

Should we have ofCore constructors instead of default values?