Cannot use private type in private constructor of public inductive

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

module

structure A where

public inductive B where
  | private foo : A → B

yields

Unknown identifier `A`

Note: A private declaration `A` (from this module) exists but is not accessible in the current context.

Context

I believe that this worked before, but I haven't checked (possibly #9890?)

Expected behavior: The code works without errors

Actual behavior: See above

Versions

nightly-2025-08-24.

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 reproducer from the issue against the Lean nightly release and inspect how the public inductive declaration resolves the private type in its private constructor. Done means the example compiles without the Unknown identifier A error while preserving the intended privacy rules.