Failed to find LCNF signature for constructor parameter using `match`

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

When a constructor parameter depends on a noncomputable expression and includes a matcher (or more precisely a casesOn-like), the compiler errors with "Failed to find LCNF signature". This is a special case of a more general problem where matchers in constructor parameters cause code duplication and redundant matches.

Context

Discussion with @hargoniX about the underlying issue regarding constructor parameters.

Steps to Reproduce

inductive ManyCases where
  | a
  | b
  | c
  | d
deriving Nonempty

inductive Thing (x : Nat) where
  | myCtor1 (a : Nat)
  | myCtor2 (b : Nat)

@[inline]
def ManyCases.toNat : ManyCases → Nat
  | .a => 3
  | _ => 7

/-- error: Failed to find LCNF signature for Classical.ofNonempty -/
#guard_msgs in
def test : Thing (ManyCases.toNat Classical.ofNonempty) :=
  .myCtor1 1

Expected behavior:
Constructor parameters are irrelevant -- the example should compile without errors.

Actual behavior:
The compiler produces an unhelpful error message "Failed to find LCNF signature".

Versions

Lean 4.33.0, commit 12c859a4d735fbcdb3ebbddb42dcc8619bcc7a7d

Impact

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

Start with the minimal Lean reproducer in the issue and inspect the compiler path that handles constructor parameters containing matchers or casesOn-like expressions. Trace the reported “Failed to find LCNF signature” for Classical.ofNonempty. Done means the reproducer compiles without the error while preserving the expected constructor behavior.