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

[effectfully]

> If you change the record R to a plain module, you will not get the described behavior.

Which is precisely what I want. Say I have

module M₁ where
module M₂ where

module RM where
  record R : Set where
    open M₁
    open M₂
open RM renaming (module R to DummyR)

module R where
  open DummyR public
  open M₁ public
  open M₂ public

module R₁ where
  open DummyR public
  open M₁ public

module R₂ where
  open DummyR public
  open M₂ public

Now I can define values of type `R' and open records as usual, but
there is also more control on what to open and how. This example is
artificial, but in my real code this trick is very useful. However
with the current behaviour R.field refers to both the module and the
record, which seems counterintuitive to me, because modules are about
scope and type constructors are just terms. Could you explain why it
is needed to double qualify things like that?