<div dir="ltr"><div>Hi all,</div><div><br></div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>My naive understanding of the algorithm for checking definitional equality is as follows (at least for types without eta):</div><div>- check whether the two terms are syntactically equal (unless using the option --no-syntactic-equality), return True if they are<br></div><div>- reduce both terms to weak-head normal form, if the heads differ then return False, otherwise recursively check definitional equality of the arguments pairwise.</div><div><br></div><div>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.</div><div><br></div><div>Is eta the problem, then? Or am I missing something else?</div><div><br></div><div>Best,</div><div>Guillaume<br></div></div>