Compilation of `noncomputable` `unsafe` function definition fails

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

Consider the following definition:

axiom foo : Nat

noncomputable unsafe def bar : Nat -> Nat
  | 0 => foo
  | x + 1 => bar x

When running lean, the tool exits with a spurious error message:

Test.lean:3:25: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'foo', and it does not have executable code

If the application that makes the function noncomputable is removed, the program compiles without errors as expected.

noncomputable unsafe def bar : Nat -> Nat
  | 0 => 0
  | x + 1 => bar x

Steps to Reproduce

Run lean on the example.

Expected behavior: The program compiles without errors.

Actual behavior: Compilation fails with a spurious error message.

Versions

Lean version:

Lean 4.18.0-nightly-2025-02-19
Target: x86_64-unknown-linux-gnu

OS version:

22.04.5 LTS (Jammy Jellyfish)

Impact

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

Start by running lean on the minimal Test.lean example with the noncomputable unsafe recursive definition. Compare it with the version whose application is removed, then trace the compiler's handling of the definition and confirm that the original example compiles without the spurious error.