`csimp` and `macro_inline` cannot be arbitrarily nested

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

def specOr (x y : Bool) : Bool :=
  match x with
  | true  => true
  | false => y

@[macro_inline] def implOr (x y : Bool) : Bool :=
  match x with
  | true  => true
  | false => y

@[csimp] theorem specOr_eq_implOr : specOr = implOr := by
  funext x y; cases x <;> rfl

/-- Macro-inlining this introduces `specOr` after `toDecl` has already run `csimp`. -/
@[macro_inline] def wrapper (x y : Bool) : Bool :=
  specOr x y

def useWrapper (x y : Bool) : Bool :=
  wrapper x y

/-- info: false -/
#guard_msgs in
#eval useWrapper false false

/-- info: true -/
#guard_msgs in
#eval useWrapper true false

Context

This came up as part of #8309, where we want to mark the Decidable instances on And and Or as macro_inline.

Steps to Reproduce

1. Run the above code

Expected behavior: Code succeeds

Actual behavior: useWrapper fails to compile with Failed to find LCNF signature for implOr

Versions

nightly-2026-08-20

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 minimal reproducer against the reported nightly version and inspect the compiler stages named in the issue: macro_inline, csimp, and toDecl. The work is done when arbitrarily nested uses compile successfully and both #guard_msgs evaluations produce the expected false and true results.