[Agda] Slow type-checking of records

[Nils Anders Danielsson]

On 2016-03-08 13:01, Andreas Nuyts wrote:
> The big (but not huge? Memory usage goes up to about 8GiB of RAM and
> 8GiB of swap) term you see is just the single object defined in the
> file. I don't really know how to interpret the rest.

It seems to me as if the occurrence graph is benign: 51 nodes, each in a
trivial SCC, and 50 edges.

If I turn off the occurrence machinery for this file, then I can get the
code to type-check. I suspect that the construction of the occurrence
graph takes a lot of time. I found some potential sources of quadratic
behaviour in the occurrence machinery, but addressing those wasn't
enough to make your code type-check in a reasonable amount of time on my
machine.

-- 
/NAD