+We perform the substitutions in two steps:
+
+ Step A: Substitute variable equalities into the right-hand sides of all
+ other equalities (but wanted only into wanteds) and into class and IP
+ constraints (again wanteds only into wanteds).
+
+ Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
+ 'alpha' is a skolem flexible (i.e., not free in the environment),
+ into the right-hand sides of all wanted variable equalities and into
+ both sides of all wanted family equalities.
+
+ Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
+ alpha' into the right-hand sides of all wanted variable equalities
+ and into both sides of all wanted family equalities.
+
+In inference mode, we do not substitute into variable equalities in Steps B & C.
+
+The treatment of flexibles in wanteds is quite subtle. We absolutely want to
+substitute variable equalities first; e.g., consider
+
+ F s ~ alpha, alpha ~ t
+
+If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
+This would be bad as `F s' is less useful, eg, as an argument to a class
+constraint.
+
+The restriction on substituting locals is necessary due to examples, such as
+
+ F delta ~ alpha, F alpha ~ delta,
+
+where `alpha' is a skolem flexible and `delta' a environment flexible. We need
+to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
+we may wrongly claim to having performed an improvement, which can lead to
+non-termination of the combined class-family solver.
+
+We do also substitute flexibles, as in `alpha ~ t' into class constraints.
+When `alpha' is later instantiated, we'd get the same effect, but in the
+meantime the class constraint would miss some information, which would be a
+problem in an integrated equality-class solver.
+
+NB:
+* Given that we apply the substitution corresponding to a single equality
+ exhaustively, before turning to the next, and because we eliminate recursive
+ equalities, all opportunities for subtitution will have been exhausted after
+ we have considered each equality once.