[Agda] How does unification work?

[Guillaume Brunerie]

Hi all,

I have a (rather big) example of two terms u and v which each take about 20
seconds and not much memory to fully normalize (the results is about 30 000
lines long), but checking whether reflexivity has type u == v exhaust all
of the memory of my computer (25G). With Agda 2.5.3, the same example does
not take much memory at all, but takes several minutes, much longer than
simply computing both normal forms. The high memory usage is already
present in Agda 2.5.4.1.

I’m trying to shrink the example but I’m wondering if it’s expected that
checking whether two terms are definitionally equal can take much longer
and/or much more memory than normalizing them and comparing the normal
forms.

My naive understanding of the algorithm for checking definitional equality
is as follows (at least for types without eta):
- check whether the two terms are syntactically equal (unless using the
option --no-syntactic-equality), return True if they are
- reduce both terms to weak-head normal form, if the heads differ then
return False, otherwise recursively check definitional equality of the
arguments pairwise.

Is this more or less correct? If we do not have eta, then it seems to me
that in the worst case scenario, checking definitional equality is more or
less as expensive as normalizing both sides, but it shouldn’t be
considerably more expensive.

Is eta the problem, then? Or am I missing something else?

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