<div dir="ltr">Follow up: I had the same issue with another module, but your suspicion got me thinking and as a result I tried removing the module arguments completely and pass in these arguments as functions arguments of the top-level definitions instead and that appears to resolve the issue.<div><br></div><div>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.</div><div><br></div><div>Should I file a bug report about this? (If so, where? On GitHub?)</div><div><br></div><div>For reference:</div><div><br></div><div>The original versions of the modules that had the described issue:</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda">https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda</a><br></div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda">https://github.com/jbracker/polymonad-proofs/blob/d2d678ba008164145e2682a2d6476bde0d3b5abf/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda</a><br></div><div><br></div><div>The changed version without module arguments that compiles:</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda">https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda</a></div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda">https://github.com/jbracker/polymonad-proofs/blob/0f5d25a6553026345d0854a463fef40f2ebfb590/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda</a><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-13 12:20 GMT+01:00 Jan Bracker <span dir="ltr"><<a href="mailto:jan.bracker@googlemail.com" target="_blank">jan.bracker@googlemail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks for your reply!<div><br></div><div>Yes, that is the case. The copied versions now share the definition of "lAssoc" and "rAssoc".</div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">2017-06-13 11:39 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>On 2017-06-13 11:44, Jan Bracker wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I have got around the issue of the compilation possibly not<br>
terminating by simply copying the definition of "fca" and "fca'" into<br>
the module with the holes. Now it takes about 40 seconds to compile.<br>
<br>
Can anybody explain why just importing these definitions from another<br>
module causes this horrible increase in compilation time? I always<br>
thought separating Agda proofs into several modules was the best way<br>
to decrease compilation time.<br>
</blockquote>
<br></span>
When you used two modules you had two definitions of lAssoc/rAssoc. I'm<br>
guessing that, when you copied the definitions of fca and fca', you<br>
arranged things so that they shared the definitions of lAssoc/rAssoc<br>
with the type signature "NaturalTransformation lAssoc rAssoc".<br>
<br>
Agda's convertibility check has a special case for terms that are<br>
syntactically identical. My guess is that this special case was<br>
triggered in the latter case, but not in the former, and that some<br>
reduction was triggered in the former case. (But this is just a guess.)<span class="m_-6766112138392382099HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>
</div></div></blockquote></div><br></div>