This module provides a Herbrand solver as a monad transformer.
The constraints offered are Either (Unify t) (Constraint m)
where m is the transformed solver. Hence, both unification
and the underlying solver's constraints are available.
The terms offered are L t1 where t1 is the Herbrand solver's
terms and R t2 where t2 are the underlying solver's types.