Usage of realizable constant `foo.eq_1` in privately imported module makes it private

[datokrat]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] 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

I have a situation where a module contains a public, exposed declaration x. Its equation x.eq_1 is public, but if a module imports another module privately that uses x.eq_1, then x.eq_1 is suddenly only available in the private context.

This suggests to me a problem with the handling of realizable constants.

Context

The problem occurred when I simped away instMonadLiftTOfMonadLift in some iterator module that was only privately imported into Std.Do.Triple.SpecLemmas but tried to assign the spec attribute to instMonadLiftTOfMonadLift.eq_1, which then failed because the constant was not in the public environment.

See https://github.com/leanprover/lean4/pull/10653; this PR uses the workaround of publicly importing the offending module into Std.Do.Triple.SpecLemmas.

Steps to Reproduce

1. Check out the Lake project in this branch: https://github.com/datokrat/lean-bug-reproductions/tree/bugs4
2. Open Reproductions/Basic.lean and observe that Lean complains that instX.eq_1 is not available in the public scope. (In fact, it even panics.)

Reproductions/A.lean:

module

public class X

@[expose]
public def x : X where

Reproductions/B.lean:

module

public import Reproductions.A

public theorem t : x = x := by
  simp only [x]

Reproductions/Basic.lean:

module

public import Reproductions.A
import Reproductions.B

-- `x` has an exposed body:
/--
info: @[expose] def x : X :=
{ }
-/
#guard_msgs in
#print x

@[expose]
public def aa := x.eq_1

Either removing import Reproductions.B or making it a public import eliminates the error.

Expected behavior:

The additional import should have no effect on the visibility of x.eq_1. It should always be publicly available.

Actual behavior:

x.eq_1 is considered private in Basic.lean and using it in the public scope causes a panic.

Versions

Lean 4.25.0-nightly-2025-10-01
Target: arm64-apple-darwin23.6.0 macOS

Impact

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

[nomeata]

Is this really specific to instances, or can you reproduce it using normal definitions?

The intended design is that the equational theorems are visible whenever the body of the corresponding definition is visible. Is this still the case here?

[datokrat]

Just checked and it's not specific to instances, I just forgot to minimize that part. I updated the MWE to illustrate this and to demonstrate that in Basic.lean, x has a visible body but x.eq_1 cannot be used.