[Agda] Pie in the sky

[Benja Fallenstein]

Hi Samuel,

Glad to see we largely agree after all and even have mostly the same
sensibilities about the design choices! :-)

On Tue, Sep 21, 2010 at 11:57 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> Your proposal for extending instance parameters makes a lot of sense
> and might even work,

Yes, I think that's an acute way of putting it. :)

> but it is clearly a layer above the basic
> instance parameter feature. I would like to focus on implementing the
> basics first.

Agreed, that makes perfect sense. The basic feature is much clearer at
this point and should still be quite useful without these
complications.

Thanks again,
- Benja

> Since we seem to agree on those basics, my question is
> for the gatekeepers of Agda's codebase:
>
> Do the agda gatekeepers have any opposition to a new feature
> introducing "(instance Foo Bar)" as a new form of valid variable name
> and using {instance Foo Bar = instance Foo Bar} instead of {instance
> Foo Bar = _} when a parameter with such a name is omitted?
>
> – Samuel