Cannot recurse through type with a private constructor

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

Defining type with nested recursion where the type recurred through has a private constructor causes a "constant already been declared" kernel error. It appears that the private constructor the elaborator generates for the nested inductive is clashing with the existing private constructor for the type.

Steps to Reproduce

structure Box (α : Type u) where
  private mk ::
    private val : α -- this `private` is not needed to produce the error

/--
error: (kernel) constant has already been declared '_private.«external:file:///lean-nightly/lean-nightly.lean».0.Box.mk'
-/
#guard_msgs in 
structure Rec where
  box? : Option (Box Rec)

Expected behavior:

Lean to succeed in creating type Rec.

Actual behavior:

It is impossible to define type Rec due to this error.

Versions

Lean 4.25.0-nightly-2025-10-13
(Bug has existed since at least v4.22.0.)

Impact

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

Start by running the minimal nested-recursion example from the issue and inspect the elaborator and kernel handling of generated private constructors. Trace why the nested Rec declaration produces a private Box.mk collision; done means the example succeeds without a constant-already-declared error.