Blaisorblade is right, these papers are about a third algorithm, available via the UniCoq plugin, which is a cleaner, documented, and almost backward compatible, version of evarconv.ml
. It is still slower, last time we checked (not algorithmically, it was due to simpler data structures IIRC) so we could not replace evarconv.ml
with it.
I think we need Matthieu to know exactly the differences. From far away, also in time, unification.ml
used Meta
s and not Evar
s (you still find that node in the internal syntax of terms). Meta
s are not assigned a type and don't track which bound variables are in scope. This is a funny beast for a type theoretic system. Indeed you can't possibly implement HO unification in a sound way with them. evarconv.ml
is based on Evar
s, which do have a type and an explicit substitution to make reduction and instantiation commute. So evarconv.ml
definitely makes more sense than unification.ml
, but, coding style on the side, it has still a few downsides, in particular it may suspend/resume hard unification (sub) problems in unpredictable ways.
All SSReflect tactics use evarconv.ml
since I can remember. Most of the vanilla tactics were progressively ported to evarconv.ml
as well, with the notable exception of apply
which is still "in progress" (there is a series of PRs called "unifall", not all merged).
I don't think you can compare unification in isolation. It is used inside elaboration (say, type inference). IIRC Agda has an algorithm based on accumulating (unification) constraints during typing, and then solving them in a "good" order. Lean used to have a similar approach (it is described in a paper) but that part of the system got rewritten. In Coq, pretyping.ml
does solve unification problems via evarconv.ml
eagerly, with some exceptions in which the problem is postponed (since it is too loosely constrained to hint to a single solution) and eventually resumed when made more constrained by some related Evar
assignment or when the client forcibly asks for a solution, not necessarily the only one.