`Failed to find LCNF signature` reported to users where v4.20 gave the `noncomputable` hint

Prerequisites

• Check that your issue is not already filed
• 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

Description

The new compiler surfaces the internal message Failed to find LCNF signature for X in situations where the previous compiler gave the actionable failed to compile definition, consider marking it as 'noncomputable' because it depends on 'X'. The user has done nothing unusual in at least one of the triggers.

Steps to Reproduce

1. #eval sizeOf on anything but Nat:

#eval sizeOf (5 : Nat)   -- 5
#eval sizeOf [1, 2, 3]   -- error: Failed to find LCNF signature for List._sizeOf_inst
#eval sizeOf (some 1)    -- error: Failed to find LCNF signature for Option._sizeOf_inst
#eval sizeOf "ab"        -- error: Failed to find LCNF signature for String._sizeOf_inst
#eval sizeOf (1, 2)      -- error: Failed to find LCNF signature for Prod._sizeOf_inst

Same for user-defined structures and inductives (P._sizeOf_inst, T._sizeOf_inst).

On v4.20.0 the same lines give failed to compile definition, consider marking it as 'noncomputable' because it depends on 'List._sizeOf_inst', and it does not have executable code. (That toolchain also emits a stray (interpreter) unknown declaration '_eval', but the primary message is the useful one.)

2. A definition depending on a kernel-rejected function:

unsafe def bad (n : Nat) : Nat := n
def risky (n : Nat) : Nat := bad n          -- (kernel) invalid declaration, as expected
def risky2 (n : Nat) : Nat := risky n + 1   -- error: Failed to find LCNF signature for risky

The second error is a consequence of the first, which was already reported; the message doesn't say so and names an internal structure instead. (When risky is 0-ary rather than a function, this same shape panics instead — that is #15033.)

Expected behavior: either the noncomputable hint the old compiler produced, or an error that names the real cause (risky was rejected / List._sizeOf_inst has no executable code).

Actual behavior: Failed to find LCNF signature for ….

Versions

• Lean 4.35.0-nightly-2026-09-04, arm64-apple-darwin24.6.0 macOS
• Lean 4.33.1 (stable) — same
• Lean 4.20.0 — old messages, as described

macOS 26.5.2, arm64.

Additional Information

#14378 reports the same message from a different trigger (a match on a constructor parameter). #10573 / #10944 dealt with realization of _sizeOf_inst for user inductives; the built-in types above still fail, so if that fix was meant to cover #eval sizeOf it has not.

Investigation assisted by Claude; repros run and checked manually.

Impact

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

Run the listed #eval sizeOf and risky/risky2 reproductions on the current compiler and compare their diagnostics with Lean 4.20.0. Trace the compiler path that reports Failed to find LCNF signature and determine whether it can retain the actionable noncomputable hint or expose the rejected declaration; done means these cases report the real cause rather than the internal LCNF message.