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

[Andreas Abel]

See

   https://code.google.com/p/agda/issues/detail?id=836

for a bit of discussion of the "double qualify" feature...  (and 
contribute if you like).

Cheers,
Andreas

On 06.08.2015 21:27, effectfully wrote:
>> 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?
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/