For logic programming, the standard procedural semantics is based on resolution and, more specifically, full unification, which is sound with respect to the Herbrand equality theory. On the other hand, most Prolog systems implement a form of unification that is sound with respect to the equality theory of rational trees. The advantages are that the unification is more efficient and that the equality theory allows for cyclic terms which have many applications, including, in particular, an efficient representation of grammars. However to really enjoy these benefits, we need to be able to support a flexible system that allows for both the Herbrand and the rational tree equality theory to exist side-by-side in the program. In particular, the system should help the programmer and compiler ensure that the unification at each step is sound for the intended equality theories and that uses of the data-structures are consistent with their cardinality and structure. In this note we discuss what is needed in more detail and show how data-flow analysers can provide this support.