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

[Andreas Abel]

Maybe it is worth continuing the discussion on the Agda list, if we talk 
about changes to the Agda language.

Here is a proposal:

* Remove qualification by data/record type name.

* default to applying renaming/using/hiding also to the module

   E.g.,

     open M1 using (N)
     open M2 hiding (O)
     open M3 renaming (P to Q)

   will be what was

     open M1 using (N; module N)
     open M2 hiding (O; module O)
     open M3 renaming (P to Q; module P to Q)

* if renaming/using/hiding is given for a module name explicitly, it 
overrides the default behavior

   E.g.,

     open M4 using (N) hiding (module N)
     open M5 hiding (O) using (module O)

   will be what was

     open M4 using (N)
     open M5 hiding (O)

Cheers,
Andreas


 > effectfully wrote on https://github.com/agda/agda/issues/836 :

Say I have

open import Data.Unit.Base

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

module M₁ where
module M₂ where

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

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

Then "the default opening" (open R r) brings `M₁' and `M₂' in scope, while
(open R₁ r) brings only `M₁'. However (C-c C-d R.t) gives

Ambiguous name R.t. It could refer to any one of
   .rec.R._.t
   DummyR.t

It seems like there aren't many use cases for this double qualification, 
while
the behaviour is definitely counterintuitive. I think, modules are about
scope and type constructors are just terms.

However writing

open import Function.Equivalence using (Equivalence; module Equivalence)

is not nice either. But if I want to entirely hide some data type or record
(for example to be able to declare a data type with the same name), I 
have to
write

open import Function.Equivalence hiding (Equivalence; module Equivalence)

So there is some inconsistence between behaviours of `using' and `hiding'.

Maybe it's worth adding an alias for (Name; module Name)?


On 08.08.15 6:10 PM, effectfully wrote:
> 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
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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