shake can incorrectly demote `public meta import` to `meta import`

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

Create a project with following two files:

-- Dep.lean
module

public def helper (n : Nat) : Nat := n + 1

-- Main.lean
module

public meta import Dep

meta section

private def priv (n : Nat) : Nat := helper n  -- private meta helper

public def pub (n : Nat) : Nat := priv n      -- public meta def

end

The body of pub (including priv's body) gets re-exported since it is public, so helper also needs to be accessible to downstream modules, hence the public is required in the import. However:

$ lake build            # succeeds
$ lake shake --fix Main
  remove #[public meta import Dep]
  add #[meta import Dep]
$ lake build            # now FAILS:
error: Main.lean:9:11: Invalid public `meta` definition `pub`, `helper` is not
accessible here; consider adding `public meta import Dep`

Context

Observed in https://github.com/leanprover-community/mathlib4/pull/40343.

Steps to Reproduce

See the Description above.

For a 3-file version that reproduces the issue in mathlib4 (where the --add-public flag that we used suppresses the issue above), as well as Claude Fable's description of the bug see https://github.com/bryangingechen/shake-public-meta-def-demoted.

Expected behavior: shake --fix should not cause breakage.

Actual behavior: the build breaks, see above.

Versions

Present in both v4.32.0 and v4.33.0-rc1.

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start with the two-file reproduction in Dep.lean and Main.lean, then run lake shake --fix Main followed by lake build to observe the demotion of public meta import. Trace shake's import-fixing logic and ensure the command preserves the public meta import when a public meta definition exposes helper. The build should continue to succeed after --fix.