+ c) Flattened type-family equalities must be exposed to the nested
+ constraints. Consider
+ F b ~ alpha, (forall c. F b ~ alpha)
+ Obviously this is soluble with [alpha := F b]. But the
+ unification is only done by solveCTyFunEqs, right at the end of
+ solveWanteds, and if we aren't careful we'll end up with an
+ unsolved goal inside the implication. We need to "push" the
+ as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
+ can be used to solve the inner (F b
+ ~ alpha). See Trac #4935.
+
+ d) There are other cases where interactions between wanteds that can help
+ to solve a constraint. For example
+
+ class C a b | a -> b
+
+ (C Int alpha), (forall d. C d blah => C Int a)
+
+ If we push the (C Int alpha) inwards, as a given, it can produce
+ a fundep (alpha~a) and this can float out again and be used to
+ fix alpha. (In general we can't float class constraints out just
+ in case (C d blah) might help to solve (C Int a).)
+