UselessHiding.agda:11,1-38
Ignoring names in 'hiding' directive: B, module D
when scope checking the declaration
  open M using (A) hiding (B; module D)

———— All done; warnings encountered ————————————————————————

UselessHiding.agda:11,1-38
Ignoring names in 'hiding' directive: B, module D
when scope checking the declaration
  open M using (A) hiding (B; module D)
