[Agda] Possibly infinite/exponential compilation time by just calling a certain function

[Jan Bracker]

Thanks for your reply!

Yes, that is the case. The copied versions now share the definition of
"lAssoc" and "rAssoc".

2017-06-13 11:39 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se>:

> On 2017-06-13 11:44, Jan Bracker wrote:
>
>> I have got around the issue of the compilation possibly not
>> terminating by simply copying the definition of "fca" and "fca'" into
>> the module with the holes. Now it takes about 40 seconds to compile.
>>
>> Can anybody explain why just importing these definitions from another
>> module causes this horrible increase in compilation time? I always
>> thought separating Agda proofs into several modules was the best way
>> to decrease compilation time.
>>
>
> When you used two modules you had two definitions of lAssoc/rAssoc. I'm
> guessing that, when you copied the definitions of fca and fca', you
> arranged things so that they shared the definitions of lAssoc/rAssoc
> with the type signature "NaturalTransformation lAssoc rAssoc".
>
> Agda's convertibility check has a special case for terms that are
> syntactically identical. My guess is that this special case was
> triggered in the latter case, but not in the former, and that some
> reduction was triggered in the former case. (But this is just a guess.)
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170613/1bdb13e1/attachment.html>