[Agda] Slow type-checking of records

[Nils Anders Danielsson]

On 2016-03-07 16:50, Andreas Nuyts wrote:
> Oddly, disabling the positivity check doesn't solve the problem.

Agda keeps track of how different arguments are used. This analysis is
run even if the positivity checker is turned off. The analysis can be
quite expensive.

I tried using the -v machinery to see what happens in your case, but I
have trouble type-checking the slow version of your file on my machine.
If you add

   {-# OPTIONS -vtc.pos.tick:100 -vtc.pos.graph:100 -vtc.pos.check:100
               -vtc.pos.record:100 -vtc.pos.args:100 -vtc.pos:25 #-}

to the top of the file, then you can perhaps get some information about
what is going on.

> I have the impression that this behaviour has to do with the fact that
> the objects fwd and bck are themselves records (of the natural
> transformation type _nt→_). Is this normal behaviour or should I file
> a bug?

Andrea Vezzosi once wrote that "I guess the lambda gets always
beta-reduced in the type of the remaining fields, while a defined
function will not be unfolded as much":

   [Agda] agda slow
   Andrea Vezzosi
   Wed Jun 3 22:04:04 CEST 2015
   https://lists.chalmers.se/pipermail/agda/2015/007867.html

If this is the case, then the problem could be that the analysis
mentioned above gets huge terms to process.

-- 
/NAD