simp attribute + unknown identifiers = internal exception #3 / PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:448:17: unknown metavariable

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

The code below produces a PANIC at the first @[simp] and an internal exception #3 at the second one.

Context

set_option autoImplicit false

structure Foo where
  foo := 37

variable {G : Foo}
def Foo.bar {U : Type} (f : Nat → Nat) := G.foo = G.foo

variable (C : G.bar baz)
include C

@[simp]
theorem quux : G.foo ↔ G.foo :=
  sorry

@[simp]
theorem eggs : true :=
  sorry

Steps to Reproduce

1. Move the cursor to either simp

Expected behavior:: Probably some unknown identifier error depending on where the "real" error is occuring, but alternatively some error about metavariables without a backtrace if that's appropriate.

Actual behavior: : Observe a backtrace at the first one, and an internal exception at the second

Versions

[Output of #version or #eval Lean.versionString] 4.27.0-rc1
[OS version, if not using live.lean-lang.org.] macOS

Additional Information

Impact

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

Start by running the self-contained reproducer with Lean 4.27.0-rc1 and moving the cursor to each simp attribute. Inspect the reported panic at Lean.MetavarContext.getDecl and the internal exception from the second simp. Done means the snippet reports an appropriate unknown-identifier or metavariable error without a backtrace or internal exception.