[Agda] Slow type-checking of records

[Andreas Nuyts]

Dear All,

I have an Agda file here (part of a library):
https://github.com/anuyts/willow/blob/slowRecords/cat/Groupoids/CoreAdjunction.agda
that contains two encodings of the same element of a record type of 
isomorphisms.

In the encoding that is commented out, I define all four fields within 
the record block. This leads to very slow type-checking (150s, of which 
110s for positivity - I've had longer times too), see
https://github.com/anuyts/willow/blob/slowRecords/cat/Groupoids/CoreAdjunctionProfile.txt
Oddly, disabling the positivity check doesn't solve the problem. Also, 
the file doesn't contain any type definitions, so it seems strange to 
begin with, that positivity-checking would be the problem.
(The postulate 'hole' is there because (it seems) you cannot use the 
profiler from the command line when you have real holes.)

In the encoding that is not commented out, I define the values for the 
fields fwd and bck (on which the types of fields src-id and tgt-id 
depend) seperately and then refer to them in the record block. This 
type-checks all right.

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?

Best regards,

Andreas Nuyts

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm