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

[Jan Bracker]

I have encountered another case where the compiler appears to go into an
infinite loop:

I tried to postulate a bunch of things, but for some reason when I add one
specific postulate the compiler goes wild with compilation times of 30 or
more minutes without terminating. This is the file that causes this problem:

https://github.com/jbracker/polymonad-proofs/blob/dd41604d6a1e80e640a1a79c2a754fb39f3abe04/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda

The file compiles in under a second, but as soon as you uncomment the
"day-triangle-id" postulate the compiler appears to not terminate anymore.
I tried moving the postulate to a different module and I also tried to add
all of the implicit arguments explicitly so the compiler does not have to
work as hard to infer anything, but both did not solve the issue.

What really baffles me is that these are postulates. I do not understand
why the compiler should ever take any significant amount of time to check
them.

2017-06-21 14:10 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se>:

> On 2017-06-13 14:41, Jan Bracker wrote:
>
>> 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.
>>
>
> The special case that I mentioned only works when terms (including all
> inferred implicit arguments) are syntactically identical. This is a
> brittle condition.
>
> Should I file a bug report about this?
>>
>
> If my guesses are correct, then I wouldn't call this a bug. However, I
> have not verified that they are correct.
>
> (If so, where? On GitHub?)
>>
>
> Yes.
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170623/5812b402/attachment.html>