<div dir="ltr"><div><div><div><div><div>Dear all,<br><br></div>For some time now, I&#39;ve been working on implementing a new unification algorithm to be used by Agda&#39;s case splitting algorithm. I originally started working on this because of issues <a href="https://github.com/agda/agda/issues/1406" target="_blank">https://github.com/agda/agda/issues/1406</a>, <a href="https://github.com/agda/agda/issues/1408" target="_blank">https://github.com/agda/agda/issues/1408</a>, <a href="https://github.com/agda/agda/issues/1427" target="_blank">https://github.com/agda/agda/issues/1427</a>, and <a href="https://github.com/agda/agda/issues/1435" target="_blank">https://github.com/agda/agda/issues/1435</a>. You may also remember my presentation at AIM XXI (see <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXI" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXI</a>). My implementation has changed a lot since then, but the basic theory is still the same.<br><br></div>I&#39;m writing this mail because I&#39;ve come to a point where I think it makes sense to integrate my work into the main Agda repository. You can find the current status of the new unifier at <a href="https://github.com/jespercockx/agda/tree/unification" target="_blank">https://github.com/jespercockx/agda/tree/unification</a>.<br><br></div><div>The basic idea of the new unifier is to manipulate an explicit unification state, consisting of a telescope of free variables, a telescope of equations, and left- and right-hand sides of each equation. The algorithm itself consists of two components: a strategy for suggesting which unification rule to apply where, and the unifier trying all these suggestions in turn until one succeeds. At each step, the current substitution is updated, resulting in the final substitution once the unification succeeds. Please don&#39;t hesitate to ask me if you want to know more about the theory. You can also (hopefully) expect a paper about it in the next few months.<br></div><div><br></div><div>In addition to fixing the issue with injective type constructors, my unifier also handles eta rules for records in a better way than the current unifier. Because can perform on-demand eta expansion of record variables, it solves most 
problems with the eager eta-expansion of implicit record patterns. This is related to issues <a href="https://github.com/agda/agda/issues/473" target="_blank">https://github.com/agda/agda/issues/473</a>, <a href="https://github.com/agda/agda/issues/635">https://github.com/agda/agda/issues/635</a>,  <a href="https://github.com/agda/agda/issues/1603">https://github.com/agda/agda/issues/1603</a>, <a href="https://github.com/agda/agda/issues/1608">https://github.com/agda/agda/issues/1608</a>, and <a href="https://github.com/agda/agda/issues/1613">https://github.com/agda/agda/issues/1613</a>. In order to make Agda handle dot patterns more robustly (see <a href="https://github.com/agda/agda/issues/1608">https://github.com/agda/agda/issues/1608</a>), I also had to add a check that checks whether the dot patterns written by the user are compatible with the dot patterns computed by the unifier. This is done by the function checkLeftoverDotPatterns in <span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">TypeChecking/Rules/LHS.hs.
            <br><br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">There is a small number of test cases that still fail with my new unifier, I would appreciate your feedback on these:<br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">- There are a few testcases that shouldn&#39;t work but are currently accepted, these are Issue292.agda, Issue1427.agda, and Issue1435.agda (only D-elim-c₁-helper doesn&#39;t work, the rest does).<br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">- A number of testcases require the solution of metavariables during unification, these are IndexInference.agda, Issue199.agda, Issue314.agda, Issue501.agda, and SizedBTree.agda (only old-style sized types fail). In my opinion, the case splitting algorithm should never instantiate metavariables, since this results in non-unique solutions that depend on the order of the constructors (see <a href="https://github.com/agda/agda/issues/1653">https://github.com/agda/agda/issues/1653</a>). However, if I get outvoted on this matter, it should be easy enough to add.<br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">- SetDetection.agda: The second example in this testcase needs a better way to generalize datatype indices when --without-K is enabled, i.e. the &quot;reverse unification rules&quot; I talked about at AIM XXI. This is still work in progress, but the current version seems to do the job well enough in most cases.<br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">- Issue473-1606.agda: This needs a modification of my checkLeftoverDotPatterns function to handle &#39;with&#39; clauses. Since I&#39;m not familiar with the implementation of &#39;with&#39;, I was hoping Andreas (or someone else) could give me a hint here.<br><br></span></div><div><span class="" title="src/full/Agda/TypeChecking/Rules/LHS.hs">I haven&#39;t put much effort yet in optimizing the unifier, so I expect that it may be slower than the current unifier in some cases. On the other hand, it should handle code with deeply-nested records more efficiently because of the on-demand eta expansion. On the standard library, my unifier actually performs a tiny bit faster, but the result isn&#39;t really significant (less than 1 sec). I&#39;m very interested to see how it performs on other people&#39;s code bases.<br></span></div><div></div><div><br></div><div>Implementation-wise, this is quite a large patch (~1500 insertions and ~1600 deletions). At the moment, I have just smashed everything in one big commit, but I could try to extract some logical sub-commits from it if there is demand for that.<br><br></div><div>I would appreciate your feedback on my work, and I&#39;d be glad to answer any questions about the theory or the implementation.<br><br></div><div>Cheers,<br></div><div>Jesper<br></div></div></div></div>