Diamond import (plain + public meta import) causes lcAny compilation-type mismatch error.

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

Importing the same module both plainly (import) and via public meta import in the same file triggers a Compilation failed, locally inferred compilation type ... differs from type lcAny error on a fully concrete, non-generic declaration. The message suggests adding @[expose], but the flagged type is a structure.

Context

Found while upgrading a project from Lean 4.29.1 to 4.31.0: a public meta import was added to fix a "not accessible here" meta-visibility error, and that broke an unrelated declaration elsewhere in the same file with this message. The repro below isolates the pattern with no project-specific code.

Steps to reproduce

lean-toolchain:

leanprover/lean4:v4.31.0

lakefile.toml:

name = "minimize"
defaultTargets = ["Minimize"]

[[lean_lib]]
name = "Minimize"

Minimize/Bundle.lean:

module
public structure Bundle where
  Ident : Type

Minimize.lean:

module
import Minimize.Bundle
public meta import Minimize.Bundle

abbrev Expression : Bundle := { Ident := Nat }

structure Container where
  f : List Expression.Ident

def v : Container := ⟨[]⟩

Run lake build.

Actual behavior

error: Minimize.lean:10:4: Compilation failed, locally inferred compilation type
  Nat
differs from type
  lcAny
that would be inferred in other modules. This usually means that a type `def` involved with the mentioned declarations needs to be `@[expose]`d. This is a current compiler limitation for `module`s that may be lifted in the future.

Reported on the f : List Expression.Ident field of Container (line 10). Removing either import line makes it disappear; only the combination of both triggers it.

Expected behavior

The build should succeed.

Version

Lean (version 4.31.0, x86_64-unknown-linux-gnu, commit 68218e876d2a38b1985b8590fff244a83c321783, Release)

Lean Nightly changes

Also reproduces on leanprover/lean4-nightly:nightly-2026-07-26 (Lean 4.34.0-nightly, commit b4fb9a75e9e1cfc8d936ee6a574a8b537662698b). On this nightly the error additionally fires one declaration earlier, on abbrev Expression : Bundle := { Ident := Nat } (line 7):

error: Minimize.lean:7:0: Compilation failed, locally inferred compilation type
  List Nat
differs from type
  List lcAny
that would be inferred in other modules. This usually means that a type `def` involved with the mentioned declarations needs to be `@[expose]`d. This is a current compiler limitation for `module`s that may be lifted in the future.

in addition to the original error on Container (line 10).

Impact

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

Start with the minimal files Minimize/Bundle.lean and Minimize.lean, then run lake build using the reported Lean toolchain or nightly version. Investigate how the plain import and public meta import affect compilation-type inference for Expression and Container; done means the reproducer builds without the lcAny mismatch.