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

[Jan Bracker]

Follow up: I had the same issue with another module, but your suspicion got
me thinking and as a result I tried removing the module arguments
completely and pass in these arguments as functions arguments of the
top-level definitions instead and that appears to resolve the issue.

I like using module arguments, because they are very useful when all of the
definitions work with the same input. But this experience discourages me
from using them somewhat, because there apparently seem to be some issues
with them in the compiler.

Should I file a bug report about this? (If so, where? On GitHub?)

For reference:

The original versions of the modules that had the described issue:

https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda

https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda

The changed version without module arguments that compiles:

https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda

https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda

2017-06-13 12:20 GMT+01:00 Jan Bracker <jan.bracker at googlemail.com>:

> 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/bf52f0c9/attachment.html>