Tactic unification vs evarconv in Coq

Question

I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a web search.

I would like to know (with 3 and 4 being optional):

1. In what situations are each of these unification algorithms used?
2. What differences can we observe between the two algorithms?
3. Are there any tricks to force one algorithm over the other as the situation may require?
4. How do both algorithms compare to those of other dependently typed programming languages? I'm most familiar with Agda, but I think any comparison could help me understand the scope of unification in Coq.

Answer 1

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 Metas and not Evars (you still find that node in the internal syntax of terms). Metas 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 Evars, 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.