[Agda] Slow type-checking of records

[Andrea Vezzosi]

There are two unifiers, one for definitional equality and one for
propositional equality. The latter is the one that has been improved
to better handle eta, and there we're usually talking about records
which are unification variables.

Using copatterns and no-eta should help with dealing with defined
records, so that they do not immediately reduce to their definition.

On Wed, Mar 9, 2016 at 12:25 AM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:
> On Tue, Mar 08, 2016 at 06:32:07PM +0900, Andreas Abel wrote:
>> Folklore suggests that you can improve performance by defining your
>> record values via copattern matching and/or no-eta record types.
>
> At least for the development version, is there still any basis
> to believe the latter? The CHANGELOG says:
>
>  | The new unifier also has eta-equality for record types built-in. This should
>  | avoid unnecessary case splitting on record constructors and improve the
>  | performance of Agda on code that contains deeply nested record patterns (see
>  | issues #473, #635, #1575, #1603, #1613, and #1645).
>
>
> Wolfram
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda