interpreter error from `import all` + `public import` allowing non-meta private def in public meta def

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

Private non-meta definitions in a module A can be used without immediate error in the bodies of public meta definitions in module B where B has public import A and import all A (and, notably, no meta import of A). The private def's IR is, as expected, not loaded when importing B normally downstream, which causes an interpreter error.

Steps to Reproduce

1. Create three files:

A:

module

def a (n : Nat) := n + 1

B:

module

public import A
import all A

-- No error:
public meta def b (n : Nat) := a n + 1

C:

module

import B

#eval b 5

2. run lake build C (or equivalent) on the command line. (Do not open C in the language server; IR loading differs there, and no error is produced.)

Expected behavior: We have an error at b telling us that it improperly depends on a, and that we must include public meta import A (and maybe meta import all A as well as a matter of principle, even if not strictly necessary?)

Actual behavior:

error: C.lean:5:0: (interpreter) unknown declaration '_private.A.0.a'

Versions

4.34.0-nightly-2026-08-04, macOS

Additional Information

Note that if a were instead from the same module, it would be (correctly) rejected. I suspect that the assignment of IRPhases.all to the imported declaration a in B by getIRPhases (which therefore lets checkMeta treat it as an auxiliary def, look for it in the locally-produced decls, find nothing, and thereby succeed) might be incorrect. Even though the IRPhases of the module itself might be acceptable (we want to load the IR from import all'd modules for execution), I would expect that its declarations should retain their original IRPhases (unless we used meta import all) to make it "as if we were in the same module". (Currently getIRPhases just takes the IRPhases from the module's IRPhases without any questions asked.)

Or, maybe IRPhases is intended to fill a different role primarily (i.e. execution availability and not "reference" availability), and this is correct? I imagine that would mean checkMeta should have some extra branch, e.g. handling the case where getLocalDecl? returns none.

I'm sure there isn't a great need for me to propose solutions here, but I'm curious as to how this should be thought about. :)

Impact

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

Start with the three-file reproducer in A, B, and C, and run lake build C rather than using the language server. Read getIRPhases and checkMeta, focusing on how import all A and the private declaration a are classified. Done means the reproducer reports the invalid dependency at b instead of failing later with an interpreter unknown-declaration error.