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

[Nils Anders Danielsson]

On 2017-06-13 11:44, Jan Bracker wrote:
> I have got around the issue of the compilation possibly not
> terminating by simply copying the definition of "fca" and "fca'" into
> the module with the holes. Now it takes about 40 seconds to compile.
> 
> Can anybody explain why just importing these definitions from another
> module causes this horrible increase in compilation time? I always
> thought separating Agda proofs into several modules was the best way
> to decrease compilation time.

When you used two modules you had two definitions of lAssoc/rAssoc. I'm
guessing that, when you copied the definitions of fca and fca', you
arranged things so that they shared the definitions of lAssoc/rAssoc
with the type signature "NaturalTransformation lAssoc rAssoc".

Agda's convertibility check has a special case for terms that are
syntactically identical. My guess is that this special case was
triggered in the latter case, but not in the former, and that some
reduction was triggered in the former case. (But this is just a guess.)

-- 
/NAD