Agda: Missing does-not-export warning for `open` directive for parametrised module

[gallais]

Minimised test case from a question on the Agda mailing list by @mechvel

module usingbug where

module A (X : Set₁) where
 Y = X

 Z = X

module B (X : Set₁) where

  open A X using (Y)

open B Set renaming (Y to Y')

[andreasabel]

MWE:

module _ where

module M (A : Set₁) where
  private X = A

open M Set using (X)

Only "works" if the module M Set is not named.

UPDATE: The internal decomposition of the last line into module _ = M Set using (X); open _ leads me to this example:

module _ where

module M where
  private X = Set

module N = M using (X)

Thus, the warnings are missing when the import directive is applied to the created module rather than to the open statement.
It seems to be allowed to mention and rename private things in a module when making a copy. Is this reasonable? Is this useful, what would be the use case? (The only way to use a module is for qualification and opening; both do not permit referring to private contents.)

The relevant call to applyImportDirectiveM (which throw the warnings) is here:
https://github.com/agda/agda/blob/f95313eb004c29b6d9cf85d60bd3b9691486bd55/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs#L264-L266
Cf. the resp. call when opening:
https://github.com/agda/agda/blob/f95313eb004c29b6d9cf85d60bd3b9691486bd55/src/full/Agda/Syntax/Scope/Monad.hs#L941-L944
The difference is that for opening, we restrictPrivate.

There are two options how to proceed:

1. Forbid mentioning private things in import directives in general.
2. Remember in the specific case of open M args that the import directive, albeit applied to the module, may not mention private things because the module is only created (namelessly) to be opened immediately.

[andreasabel]

The behavior changed in 2.5.1 (tested 2.5.1.1). Agda 2.4.2.6 reports:

The module N doesn't export the following: X
when scope checking the declaration
  module N = M using (X)

The release notes of 2.5.1 do not mention a language change towards allowing this.

Thus, this is probably a unwanted regression and we should go for option 1.