stuck `simp` introduces metavariable; combined with `expose`, leads to panic later

Prerequisites

• 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

If simp makes no changes, this can sometimes lead to a declaration with metavariables (-> kernel error). If the declaration is public and exposed, later trying to apply the declaration's equational lemmas leads to a panic.

Using a declaration even after getting a kernel type error before is admittedly a questionable use case, but it might still be worthwhile to understand where the metavariable and panic are coming from, especially because it's somehow related to @[expose].

Reproduction steps

Consider this snippet:

module

/--
error: `simp` made no progress
---
error: (kernel) declaration has metavariables 'f'
-/
#guard_msgs in
@[expose] public def f (_ : Nat) : { xs : Unit // False } := ⟨sorry, by simp⟩

/--
error: unknown metavariable '?_uniq.24'
---
info: PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:450:17: unknown metavariable _uniq.24
backtrace:
PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:450:17: unknown metavariable _uniq.24
backtrace:
PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:450:17: unknown metavariable _uniq.24
backtrace:
---
error: (kernel) declaration has metavariables 'f.eq_1'
---
info: PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:450:17: unknown metavariable _uniq.24
backtrace:
---
warning: declaration uses `sorry`
-/
#guard_msgs in
theorem t : f 0 = sorry := by simp [f]

Expected behavior:

The simp in f's definition should fail. There should be no panics or kernel errors.

Actual behavior:

Defining f fails with a kernel error ("contains metavariables"), but the declaration is nonetheless created. If it's exposed, we get a panic when trying to simplify using f.eq_1.

Versions

Lean 4.30.0-nightly-2026-02-25
Target: x86_64-unknown-linux-gnu

Impact

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

Run the minimal reproduction in the issue and compare the simp and @[expose] behavior. Start at the reported Lean.MetavarContext.getDecl entry point and trace how the metavariable survives the kernel error and reaches the exposed equational lemma. Done means the failing definition is not created with metavariables and later simplification produces no panic or related kernel errors.