[Agda] A quiz: what should the types of these definitions be?

[Andreas Abel]

On 05.02.2016 08:34, Ulf Norell wrote:
> Without cheating, I would expect
>
>    module M Γ where
>      record R Δ
>
> to yield the same types for functions and projections as
>
>    module M where
>      record R Γ Δ

But this means that inside M, there are declarations that do not have 
the module telescope Gamma as a prefix, but the hiding-modified one.

For instance,

   module M (A : Set) where
     record R : Set where
       data D (a : A) : Set where
     open R public
     data E (a : A) : Set

then

   E = M.E Nat

is ok while

   D = M.D Nat

will give a type error?

> On Thu, Feb 4, 2016 at 6:48 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     On 04.02.2016 17:43, Nils Anders Danielsson wrote:
>
>         On 2016-02-04 17:19, Andreas Abel wrote:
>
>             Hi, this is a poll about what you would expect Agda to do
>             about the
>             hiding of parameters if you have definitions inside a
>             parametrized
>             record inside a parametrized module.
>
>
>         I suspect that you're not quite satisfied with the current
>         situation.
>         Let me see if I can guess what you're most annoyed with. Is it
>         the fact
>         that fields and record module definitions are (sometimes) treated
>         differently?
>
>
>     No, frankly, I want to fix a bug, but I do not know the intended
>     semantics.
>
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>


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