mdata bug affecting interaction of simp and match

[semorrison]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Running simp (config := {decide := false}) inside a branch of a match statement will often leave an unsolved goal True.
This behaviour has been hidden by the default decide := true, which subsequently closes the True.

Steps to Reproduce

example : 0 = 0 := by
  simp (config := {decide := false}) -- Works fine.

example (n : Nat) : 0 = 0 := by
  match n with
  | 0 => simp (config := {decide := false}) -- Fails: unsolved goal `True`
  | _ => simp

example (n : Nat) : 0 = 0 := by
  match n with
  | 0 => simp (config := {decide := true}) -- this is the default, so masks the problem?
  | _ => simp

Expected behavior:
All three examples to work.

Actual behavior:
The second example fails in the 0 branch, with unsolved goal True.

@Kha says "this looks like an mdata bug. pp.raw + trace_state uncovers the difference."

⊢ Eq.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))

n : Nat
⊢ [mdata noImplicitLambda:1 Eq.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))]

Reproduces how often:

Always.

Versions

Lean (version 4.0.0-nightly-2023-03-17, commit 8650804, Release)

Additional Information

Reported on zulip.

[gebner]

Here are some other related failures:

example : True := by
  have : True := ⟨⟩
  simp (config := {decide := false}) -- unsolved goals

example : True := by
  let x : True := ⟨⟩
  simp (config := {decide := false}) -- unsolved goals

example : True := by
  suffices True by simp (config := {decide := false}) -- unsolved goals
  constructor