Unfolding fails when code is split up into multiple files

[nad]

The following code is accepted:

module _ where

open import Agda.Builtin.Equality

module M (A : Set₁) where

  opaque

    B : Set₁
    B = A

module N (A : Set₁) where

  open M A public

open N Set

opaque
  unfolding B

  _ : B ≡ Set
  _ = refl

However, if I replace the local modules with modules in separate files (in a certain way), then Agda rejects the code:

module M (A : Set₁) where

opaque

  B : Set₁
  B = A

module N (A : Set₁) where

open import M A public

module _ where

open import Agda.Builtin.Equality

open import N Set

opaque
  unfolding B

  _ : B ≡ Set
  _ = refl

———— Error —————————————————————————————————————————————————
[…]/Bug.agda:11,7-11
B != Set of type Set₁
when checking that the expression refl has type B ≡ Set

———— Warning(s) ————————————————————————————————————————————
[…]/Bug.agda:8,13-14
warning: -W[no]UnfoldTransparentName
The name B, mentioned by an unfolding clause, does not belong to an
opaque block. This has no effect.

I can make the code work again by referring to the underlying definition of B instead of the reexported one:

module _ where

open import Agda.Builtin.Equality

import M

open import N Set

opaque
  unfolding M.B

  _ : B ≡ Set
  _ = refl

I don't think Agda should care if the code is in one or multiple files.