a re-implementation of exprUnify that avoids Fix.
(merge from fixpoint branch)