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

[Wolfram Kahl]

On Fri, Feb 05, 2016 at 09:55:10AM +0100, Ulf Norell wrote:
> On Fri, Feb 5, 2016 at 9:13 AM, Andreas Abel <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.

Otherwise, with:

    module M Γ where
      record R Δ where
        f : T Γ Δ
    r : R Γ Δ

,  outside of M one would need to write f Γ r,
although Γ can be inferred from r.
I could of course still make Γ implicit:

    module M {Γ} where
      record R Δ where
        f : T Γ Δ

But typically there is other stuff in M that needs Γ as explicit argument ---
I already have very many cases where I need to split parameterised modules
into sequences of modules that alternatingly have such parameters as
implicit and explicit...


Wolfram