Recursive `unsafe opaque` declarations are not opaque

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

Recursive unsafe opaque functions are added as definitions to the environment and not as opaques.

Context

Testing recursion stuff

Steps to Reproduce

unsafe opaque val (n : Nat) : Nat := if n = 0 then val n + 1 else 3
unsafe example : val n = if n = 0 then val n + 1 else 3 := rfl

Expected behavior: unsafe opaques are opaque and thus the example fails.

Actual behavior: unsafe opaques behave like unsafe def and thus the example works.

Versions

Lean 4.31.0-nightly-2026-04-16

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 recursive unsafe opaque reproducer in the issue and compare its behavior with the expected opacity semantics on the latest Lean nightly. Trace how recursive unsafe opaque declarations are added to the environment; done means the example no longer succeeds by definitional reduction and regression coverage is added for this case.