[Agda] instance arguments proposal and crash

Paolo Capriotti p.capriotti at gmail.com
Tue Mar 5 17:56:08 CET 2013

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:

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


More information about the Agda mailing list