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

[effectfully]

Thanks for the link. I posted some thoughts there.
Also, the problem is stated incorrectly in my previous post — there is
no ambiguity in `R.field', which is a counterintuitive behaviour of a
counterituitive feature:

module RM where
  record R : Set where
    field t : ⊤
open RM renaming (module R to DummyR)

module R where
  open DummyR public

typechecks : R -> ⊤
typechecks = R.t

While

module R r where
  open DummyR r public

doesn't : R -> ⊤
doesn't = R.t