Setting `-D Elab.async=false` breaks `backward.privateInPublic`

Prerequisites

(cf. #8746, but it is different and more fatal)

• 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

As title said: Elab.async and backward.privateInPublic are incompatible.

Steps to Reproduce

Code:

-- main.lean
module

set_option backward.privateInPublic true

public class U : Type where
  a : Nat
  h : a = a

private theorem A : 0 = 0 := rfl

public instance : U := ⟨0, A⟩

Compile it use lean main.lean -D Elab.async=false.

Expected behavior:

main.lean:12:27: warning: Private declaration `A` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled.

Disable `backward.privateInPublic.warn` to silence this warning.

Actual behavior:

main.lean:12:27: error(lean.unknownIdentifier): Unknown identifier `A`

Note: A private declaration `A` (from the current module) exists but would need to be public to access here.

Versions

4.30.0-rc2, macOS (reproducible in live):

https://live.lean-lang.org/#codez=LYewJgrgNgpgUHAzjALgfRABxQSxAOwAIAjAQwGMBrAd1ICcwA6TOnAN1JRgEl8AFCMSg5yhFHQjxk6LLgKEAolFLFGpRAE98ogGakoyBJkHDR5ZYkSEAqoQBchACobMMQtQAWMOvEKFS9oQAcpxwfh6BAQC8%2FkasHFxiXiA%2BwIQAgoEADIQxOXYxdDpQRiYihDj4iCik2m4OtgWEgBfkWQA0GYCX5HBAA

Additional Information

Based on the description
https://github.com/leanprover/lean4/blob/aa6fa1cf1a7c7a7161ceeda64c934176abc3595b/src/Lean/CoreM.lean#L35-L46
of this option, it shouldn't affect any correctness.

Start by compiling the provided main.lean example with lean main.lean -D Elab.async=false and compare it with the expected warning. Read the Elab.async option description in src/Lean/CoreM.lean at lines 35-46, then trace the elaboration behavior involved in backward.privateInPublic; done means the reproducible case no longer reports A as an unknown identifier.