  A new hierarchy of "exact" unification types is introduced, motivated by the
study of admissibility for equational classes and non-classical logics. In this
setting, unifiers of identities in an equational class are preordered, not by
instantiation, but rather by inclusion over the corresponding sets of unified
identities. Minimal complete sets of unifiers under this new preordering always
have a smaller or equal cardinality than those provided by the standard
instantiation preordering, and in significant cases a dramatic reduction may be
observed. In particular, the classes of distributive lattices, idempotent
semigroups, and MV-algebras, which all have nullary unification type, have
unitary or finitary exact type. These results are obtained via an algebraic
interpretation of exact unification, inspired by Ghilardi's algebraic approach
to equational unification.
