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

[Andreas Abel]

On 10.08.2015 14:45, Nicolas Pouillard wrote:
> On 08/10/2015 10:09 AM, Andreas Abel wrote:
>> 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.
>
> I find this feature useful, for instance to qualify certain
> data-constructors for instance:
>
> ```
>    suc-inj : ∀{x y} → ℕ.suc x ≡ suc y → x ≡ y
> ```

Hopefully, this will still work, as the data type module ℕ will exists 
parallel with the data type ℕ (to the naive user).

>> * 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
>
> I'm in favor of this change though. Some old code which explicitly
> mention both namespaces should still be accepted:
>
> ```
> open M using (module X; X) hiding (module Y; Y)
> ```

This will work, as the explicit instruction for modules X and Y will 
overwrite the (here identical) default instructions derived from the 
instructions for X and Y.

> This way the only non-backward compatible situation requires to hide the
> module:
>
> Before:
>
> ```
> open M using (X)
> ```
>
> After:
>
> ```
> open M using (X) hiding (module X)
> ```

Indeed, if you have need to hide module X, you need to do it explicitly 
in this situation.

Cheers,
Andreas

-- 
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/