<div dir="ltr">I have encountered another case where the compiler appears to go into an infinite loop:<div><br></div><div>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:</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/dd41604d6a1e80e640a1a79c2a754fb39f3abe04/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda">https://github.com/jbracker/polymonad-proofs/blob/dd41604d6a1e80e640a1a79c2a754fb39f3abe04/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda</a><br></div><div><br></div><div>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.</div><div><br></div><div>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.</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-21 14:10 GMT+01:00 Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2017-06-13 14:41, Jan Bracker wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I like using module arguments, because they are very useful when all<br>
of the definitions work with the same input. But this experience<br>
discourages me from using them somewhat, because there apparently seem<br>
to be some issues with them in the compiler.<br>
</blockquote>
<br></span>
The special case that I mentioned only works when terms (including all<br>
inferred implicit arguments) are syntactically identical. This is a<br>
brittle condition.<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Should I file a bug report about this?<br>
</blockquote>
<br></span>
If my guesses are correct, then I wouldn't call this a bug. However, I<br>
have not verified that they are correct.<span class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(If so, where? On GitHub?)<br>
</blockquote>
<br></span>
Yes.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>