--- | A very simple unification engine; used by GArrowTikZ
-module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve, occurs)
+-- | A very simple finite-sized-term unification engine; used by GArrowTikZ
+module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve)
+--
+-- | Terminology: a value of type @t@ (for which an instance
+-- @Unifiable t@ exists) is "fully resolved" with respect to some
+-- value of type @Unifier t@ if no @UVar@ which occurs in the
+-- @t@-value is a key in the unifier map.
+--