Private instance synthesized in a public declaration's type (inside a single module)

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

Private instances are synthesized in public terms.

Context

A similar bug has been reported in https://github.com/leanprover/lean4/issues/9383. However, the fix only seems to have solved the example in the PR, where the private instance is in another module shouldn't even be imported since the example does not use import all. This PR reproduces the same problem in a slightly different situation.

Steps to Reproduce

1. Check out the Lake project in this branch: https://github.com/datokrat/lean-bug-reproductions/tree/bugs1
2. Open Reproductions/PrivateInstance.lean and see an "unknown constant" error message

Here's the code:

module

public class X

private instance : X where

/--
error: Unknown constant `_private.Reproductions.PrivateInstance.0.instX`

Note: A private declaration `instX` exists but is not accessible in the current context.
-/
#guard_msgs in
@[expose]
public def a [LE X] : X := inferInstance

Expected behavior:

The a declaration should produce a "failed to synthesize" error instead of "unknown constant". The private instance should not be visible for the instance synthesizer in public contexts.

Actual behavior:

The private instance is synthesized, which then leads to an "unknown constant" error.

Versions

Lean 4.23.0-nightly-2025-08-11
Target: arm64-apple-darwin23.6.0 macOS

Impact

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

Start by opening Reproductions/PrivateInstance.lean from the linked Lake project and run its minimal reproduction against the reported Lean nightly version. Trace how the private instance is synthesized for the public @[expose] declaration; done means the example reports a failed-to-synthesize error rather than an unknown constant.