Generic Unification

type Equation t = (t,t)
type Equations t = [Equation t]
type Substitution v t = [(v,t)]
The unification function needs three operations on terms: 
class (Show term,Eq var) => Unifiable term var | term -> var where
  topMatch :: Equation term -> Maybe (Equations term)
  isVar :: term -> Maybe var
  subst :: Substitution var term -> term -> term

unify :: (Monad m,Unifiable t v) => Equations t -> m (Substitution v t)
unify = ... -- 19 lines, purely functional implementation
See module Unification.