[Agda] instance arguments proposal and crash

[Paolo Capriotti]

On Tue, Mar 5, 2013 at 8:35 AM, Dominique Devriese
<dominique.devriese at gmail.com> wrote:
> Anyway, my proposal for Paolo's problem would be to introduce a new
> form of record open command that recursively eta-expands the record in
> the same way as the implicit record patterns and brings in scope its
> contents as let-bindings:
>
> f M G = unit , unit
>   where open IsMonoid {{...}}
>              open recursively Monoid M
>              open recursively Group G

Actually, it is already possible to achieve something like this:
http://hpaste.org/83514.

The idea is that a term of type IsSubtype captures those pairs that I was
expecting the instance argument resolution algorithm to find automatically. The
overloaded module just enables a convenient syntax to bring such terms into
scope.

Paolo