Note [Skolemisation en-bloc]

Consider this case:

  topSkolemise  (forall a. Ord a => forall b. Eq b => a->b->b)

We /could/ return just
  (wp, [a], [d:Ord a, forall b. Eq b => a -> b -> b)

But in fact we skolemise "en-bloc", looping around (in `topSkolemise` for
example) to skolemise the (forall b. Eq b =>).  So in fact

  topSkolemise  (forall a. Ord a => forall b. Eq b => a->b->b)
    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
    where
      wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2

This applies regardless of DeepSubsumption.

Why do we do this "en-bloc" loopy thing?  It is /nearly/ just an optimisation.
But not quite!  At the call site of `topSkolemise` (and its cousins) we
use `checkConstraints` to gather constraints and build an implication
constraint.   So skolemising just one level at a time would lead to nested
implication constraints. That is a bit less efficient, but there is /also/ a small
user-visible effect: see Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.
Specifically, consider

   forall a. Eq a => forall b. (a ~ [b]) => blah

If we skolemise en-bloc, the equality (a~[b]) is like a let-binding and we
don't treat it like a GADT pattern match, limiting unification. With nested
implications, the inner one would be treated as having-given-equalities.

This is also relevant when Required foralls are involved; see #24810, and
the loop in `skolemiseRequired`.