unused argument causes `noncomputable` error

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 error lean.dependsOnNoncomputable is thrown on definitions where the offending noncomputable dependency is only passed as arguments to a definition whose compiled code does not use those arguments.

Context

I encountered this error after upgrading my Setoid theorems from an earlier version of Lean. See also #14084.

Steps to Reproduce

structure Wrap (α : Type) : Type where
  prop : α → Prop

set_option trace.compiler.ir.result true
/--
trace: [Compiler.IR] [result]
    def myFun (x_1 : @& tobj) : tagged :=
      let x_2 : tagged := ctor_0[Wrap.mk];
      ret x_2
    def myFun._boxed (x_1 : tobj) : tagged :=
      let x_2 : tagged := myFun x_1;
      dec x_1;
      ret x_2
-/
#guard_msgs in
def myFun (n : Nat) : Wrap Nat := Wrap.mk (· = n)
/--
trace: [Compiler.IR] [result]
    def notDependsOnChoice (x_1 : @& tobj) : tagged :=
      let x_2 : tagged := ctor_0[Wrap.mk];
      ret x_2
    def notDependsOnChoice._boxed (x_1 : tobj) : tagged :=
      let x_2 : tagged := notDependsOnChoice x_1;
      dec x_1;
      ret x_2
-/
#guard_msgs in
def notDependsOnChoice (n : Nat) : Wrap Nat := myFun (n + 1)
def dependsOnChoice (n : Nat) : Wrap Nat := myFun (Classical.choice ⟨n + 1⟩)

Expected behavior: The argument to myFun is not used in the generated IR, so since Classical.choice only appears as an argument to myFun, it should be ignored by the noncomputable checker and dependsOnChoice should be accepted. In fact the generated IR notDependsOnChoice doesn't use its argument either.

Actual behavior: I get an "error: Classical.choice not supported by code generator; consider marking definition as noncomputable" on dependsOnChoice.

Versions

This is a regression from v4.28.0.

I tested versions v4.33.0, v4.32.0, v.4.31.0, ..., v4.17.0. dependsOnChoice works on v4.17.0 up to v4.28.0, and fails on v4.29.0 and above. In the versions where it works, the generated IR was identical to that of notDependsOnChoice.

Target: x86_64-w64-windows-gnu Windows

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 reproducer in the issue and inspect the traced compiler IR for myFun, notDependsOnChoice, and dependsOnChoice. Compare the noncomputable-checker behavior between v4.28.0 and v4.29.0; done when the reproducer is accepted without the error while preserving the argument-free generated IR.