Default MessageData

Stream: lean4

[Damiano Testa]

The Inhabited instance for MessageData is derived from docs#MessageData.ofGoal, which in turn uses the default MVarId, which is Name.anonymous. This causes confusion when trying to log the default MessageData.

import Lean.Elab.Command

run_cmd -- [error when printing message: unknown goal [anonymous]]
  Lean.logInfo default

run_cmd -- [error when printing message: unknown goal [anonymous]]
  Lean.logInfo <| m!"Interesting message" ++ default ++ m!" and more interesting stuff here."

If, instead, the default instance was m!"", then there would be no issues above.

[Aaron Liu]

Should we make it something distinctive (like docs#Lean.instInhabitedExpr does .const `_inhabitedExprDummy []) to aid debugging?

[Eric Wieser]

m!"" would match Inhabited for String

[Thomas Murrills]

Aaron Liu said:

Should we make it something distinctive (like docs#Lean.instInhabitedExpr does .const `_inhabitedExprDummy []) to aid debugging?

Debugging-wise, ideally we have this for Format and String too imo, with differences so that it’s easy to tell which type it’s coming from (e.g. m!"<default MessageData>")!

[Thomas Murrills]

Not sure if this would introduce any costs with these types being so basic and widely used, though.

[Eric Wieser]

Why do we care about the value of default in the first place? Does it ever get used?

[Eric Wieser]

My guess is that the main place it matters is for panic!, where I'd perhaps argue a separate panicValue would make the intent clearer

[Damiano Testa]

I found out about this, because I was writing a long match statement, and I pre-filled in the various branches with default, just to get something that compiled. I then proceeded to fill in the various values with meaningful messages, but left one out. It took me quite a while to debug what was the issue, though, since I was getting no output at all from the log, except that there was an error with printing some goal.

[Damiano Testa]

So, indeed, in the end, there are no defaults left in my code, but some better default would have given me an easier time when debugging what went wrong.

[Aaron Liu]

in that case I would use sorry

[Damiano Testa]

Sure, I could have also used m!"".

[Damiano Testa]

But I did not and there was no indication that what I was doing would give me such a hard time!

[Thomas Murrills]

Eric Wieser said:

My guess is that the main place it matters is for panic!, where I'd perhaps argue a separate panicValue would make the intent clearer

I agree this is the main place it matters, but I'd be reluctant to create an edge case where we indicate something panicked, when in fact e.g. someone (or something else) had just left a default somewhere, thus sending people on a wild goose chase... :sweat_smile:

[Eric Wieser]

To be clear, my suggestion is to have separate Inhabited and PanicValue classes, perhaps with a low-priority instance inferring one from the other

[Thomas Murrills]

Oh, sorry, I misinterpreted. I like that!