m!"{expr}" doesn't work as of 4.9.0-rc1

[llllvvuu]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

As of 4.9.0-rc1, specifically the change to MessageData.ofExpr in 9f6bbfa, the following no longer works:

import Lean

def main : IO Unit := do
  let foo := Lean.mkConst `foo
  let bar ← m!"{foo}".toString
  IO.println s!"Expr: {foo}"
  IO.println s!"MessageData: {bar}"

#eval main

Feel free to close if this is intended behavior.

If not, MessageData.ofExpr (and similar functions) could be changed back to something like this:.

def ofExpr (e : Expr) : MessageData :=
  .ofLazy (fun ctx? => do
            let msg ← ofFormatWithInfos <$> match ctx? with
              | .none => pure (format (toString e))
              | .some ctx => ppExprWithInfos ctx e
            return Dynamic.mk msg)
          (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)

Context

Batteries' lake exe runLinter is now printing "(invalid MessageData.lazy, missing context)" which is showing up in Batteries and Mathlib CI.

leanprover-community/batteries#838

Steps to Reproduce

Try the above code in 4.9.0-rc1 vs 4.8.0.

Expected behavior: Prints "MessageData: foo"

Actual behavior: Prints "MessageData: (invalid MessageData.lazy, missing context)"

Versions

4.9.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I didn't expect much petty printing of expressions without a context, as how else would you show local variables. But for closed expressions and in particular global names it does make sense. Recovering the previous functionality in ofExpr is reasonable, do you want to prepare a PR for that?