sig
  exception CannotUnify of Positions.position * MultiEquation.crterm *
              MultiEquation.crterm
  val unify :
    ?tracer:(MultiEquation.variable -> MultiEquation.variable -> unit) ->
    Positions.position ->
    (MultiEquation.variable -> unit) ->
    MultiEquation.variable -> MultiEquation.variable -> unit
end