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

[Jan Bracker]

Hello,

I have a module that compiles in a reasonable amount of time with some
holes in it. If I fill one specific hole using a specific proof from
another module and start compilation it does not appear to terminate (I
have let it running for 50+ minutes and it just fills and empties my RAM
and swap slowly...). Can anyone explain why this happens or how I can get
around this issue?

The modules with holes can be found here:

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

On its own this file (with holes) type checks in a reasonable amount of
time in emacs and if I call Agda directly, as well:

agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Isomorphism/Examples/
FunctorCompositionAssociator.agda

If I try to fill the hole on line 44 with the expression "fca {ℓC₀} {ℓC₁} C"
I experience the possibly non-terminating behavior of the type checker. As
far as I can see that expression exactly matches the type of that hole and
I don't understand why it is not just accepted immediately. As said before
I have let Agda work away at the proof for 50+ minutes without finishing
type checking.

I don't know if this helps at all, but usually when I watch my memory usage
during Agda compilations t just stepwise allocates memory up to a point and
then finishes. With the hole filled in the compilation allocates and
deallocates memory in (2-3 minute) cycles which I have not seen before when
running Agda. I have not measured memory usage I just watched the graph of
memory usage in my system monitor while it was running.

"fca" or "functorCompositionAssociator" is imported from

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

This module on its own again compiles within a reasonable amount of time
(in emacs and while calling agda directly):

agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Transformation/Examples/
FunctorCompositionAssociator.agda

I first encountered this problem using emacs and I have verified that it is
actually an Agda and not an emacs issue by calling Agda on the respective
files directly before and after I replaced the hole with the expression.

I have tested this using Agda 2.5.2 built from the Hackage sources on two
different 64-bit Linux machines (Kubuntu 16.04 & 14.04). The machines have
6 / 8 GB of RAM and that is fully used by the compilation together with 2-3
GB of swap.

So what is causing this issue and how can I get around it?

Best,
Jan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170608/d7811875/attachment.html>