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

[Nicolas Pouillard]

So +1

On 08/11/2015 07:54 PM, Andreas Abel wrote:
> 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
>

-- 
Best regards,
-- NP