<div dir="ltr">Hello,<div><br></div><div>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?</div><div><br></div><div>The modules with holes can be found here:</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/master/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda" target="_blank">https://github.com/jbracker/po<wbr>lymonad-proofs/blob/master/src<wbr>/Theory/Natural/Isomorphism/<wbr>Examples/FunctorCompositionAss<wbr>ociator.agda</a><br></div><div><br></div><div>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:</div><div><br></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)">agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/<wbr>Isomorphism/Examples/<wbr>FunctorCompositionAssociator.<wbr>agda</span><br></span></div><div><br></div><div>If I try to fill the hole on line 44 with the expression "<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">fca {ℓC₀} {ℓC₁} C</span>" 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. </div><div><br></div><div>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.</div><div><br></div><div>"<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">fca</span>" or "<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">functorCompositionAssociator</span>" is imported from</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/master/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda" target="_blank">https://github.com/jbracker/po<wbr>lymonad-proofs/blob/master/src<wbr>/Theory/Natural/Transformation<wbr>/Examples/FunctorCompositionAs<wbr>sociator.agda</a><br></div><div><br></div><div>This module on its own again compiles within a reasonable amount of time (in emacs and while calling agda directly):</div><div><br></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)">agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/<wbr>Transformation/Examples/<wbr>FunctorCompositionAssociator.<wbr>agda</span><br></span></div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>So what is causing this issue and how can I get around it?<br></div><div><br></div><div>Best,</div><div>Jan</div></div>