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

[Andreas Abel]

See my comment on https://github.com/agda/agda/issues/1815

With the semantics you propose, we do not get that

   module M' Gamma = M Gamma

produces an identical copy of M.

On 05.02.2016 09:55, Ulf Norell wrote:
> On Fri, Feb 5, 2016 at 9:13 AM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     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?
>
> Yes.
>
> / Ulf


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