[Agda] Re: Instance arguments: three more updates

[Dominique Devriese]

> * Introduce a cleaner and more efficient replacement for the
> RecordWithImplicits macro's. The new syntax is
>     module RecordWithImplicits = Record {{...}}
>  and
>     open Record {{...}}
>  and variations with "open module ...", "open ... public" and
> using/renaming/hiding stuff

I forgot to mention: these new module macro's do not cause a type
checking performance degradation for code not using them as the old
"RecordWithImplicits" module did. This is because in the new approach
the modules are only generated when they are requested. This means the
new system has the same performance characteristics as the
corresponding translation in terms of standard module macro's, but it
saves you the trouble of looking up and writing out the record
parameters yourself.

Dominique