[Agda] Slow type-checking of records

[Wolfram Kahl]

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