[Agda] Renaming of a module, associated with a record, doesn't hide the original name.

[effectfully]

> default to applying renaming/using/hiding also to the module
> if renaming/using/hiding is given for a module name explicitly, it overrides the default behavior

It has the problem that a term and a module can be unrelated:

t = 0
module t where

Then both the `t's will be imported/renamed/not imported.

But this solution is much better than complicating imports with
aliases. Is it very useful that terms and modules scopes are
separated? Maybe identical names should be allowed only for
records/datas and modules?

On the other hand with separated scopes you can emulate records:

postulate
  A B C : Set

T = A × B × C

module T (t : T) where
  field₁ = proj₁ t
  field₂ = proj₁ (proj₂ t)
  field₃ = proj₂ (proj₂ t)

postulate
  t : T

open T t

Then simulatenous renaming makes sense.