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

[Jan Bracker]

Thank you, Nils!

I was not aware of "abstract" as a language feature. I will keep it in mind
and I have made all my equivalence proofs abstract. It still takes a
significant amount of time to type check the triangle identity but it
eventually type checks now.

I tried to add the last postulate I need, but even though I now have marked
all of the proofs as abstract the compilation time is again at 30+ minutes
with no end in sight:

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



2017-06-26 15:33 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se>:

> On 2017-06-23 12:42, Jan Bracker wrote:
>
>> 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.
>>
>
> I think Agda has trouble checking that the last equality type that you
> give is well-formed.
>
> I managed to get the code to type-check by adding a large number of
> "abstract" annotations to your code (and postulating a single lemma that
> failed to type-check), see the attached patch. I suggest that you try to
> make all of your "proofs" abstract.
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170627/cc92f09f/attachment.html>