[Agda] Slow type-checking of records

[Nils Anders Danielsson]

On 2016-03-12 00:33, Nils Anders Danielsson wrote:
> I found another problem. I've created a ticket on the bug tracker:
> https://github.com/agda/agda/issues/1901.

This problem has been fixed, and I can now type-check Andreas' old code
on my machine. However, Agda is still slow.

I tried replacing all lambdas in coreAdjunction with pattern-matching
lambdas, and then Agda became roughly ten times faster and used roughly
nine times less memory. This suggests to me that (part of) the problem
is that Agda always reduces lambda applications (as opposed to
applications of pattern-matching lambdas and defined functions), as
pointed out by Andrea.

What can we do about this? I don't want to force users to use
workarounds like copattern matching. Could we for instance add support
for beta-redexes to the internal syntax?

-- 
/NAD