simp fails to finish after reaching `True`, inside a `match`

Stream: lean4

[Scott Morrison]

This is a bug, right?

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

[Scott Morrison]

Assuming this is a bug, this is getting in the way of changing the default for decide. :-)

[Sebastian Ullrich]

Yes, 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))]

[Scott Morrison]

Okay, I made an issue at https://github.com/leanprover/lean4/issues/2173.