Note [pickQuantifiablePreds]

When pickQuantifiablePreds is called we have decided what type
variables to quantify over, `qtvs`. The only quesion is: which of the
unsolved candidate predicates should we quantify over?  Call them
`picked_theta`.

Note that will leave behind a residual implication
     forall qtvs. picked_theta => unsolved_constraints
For the members of unsolved_constraints that we select for picked_theta
it is easy to solve, by identity.  For the others we just hope that
we can solve them.

So which of the candidates should we pick to quantify over?  It's pretty easy:

* Never pick a constraint that doesn't mention any of the quantified
  variables `qtvs`.  Picking such a constraint essentially moves the solving of
  the constraint from this function definition to call sites.  But because the
  constraint mentions no quantified variables, call sites have no advantage
  over the definition site. Well, not quite: there could be new constraints
  brought into scope by a pattern-match against a constrained (e.g. GADT)
  constructor.  Example

        data T a where { T1 :: T1 Bool; ... }

        f :: forall a. a -> T a -> blah
        f x t = let g y = x&&y    -- This needs a~Bool
              in case t of
                    T1 -> g True
                    ....

  At g's call site we have `a~Bool`, so we /could/ infer
       g :: forall . (a~Bool) => Bool -> Bool  -- qtvs = {}

  This is all very contrived, and probably just postponse type errors to
  the call site.  If that's what you want, write a type signature.

* Implicit parameters is an exception to the "no quantified vars"
  rule (see Note [Inheriting implicit parameters]) so we can't actually
  simply test this case first.

* Finally, we may need to "box" equality predicates: if we want to quantify
  over `a ~# b`, we actually quantify over the boxed version, `a ~ b`.
  See Note [Lift equality constraints when quantifying].

Notice that we do /not/ consult -XFlexibleContexts here.  For example,
we allow `pickQuantifiablePreds` to quantify over a constraint like
`Num [a]`; then if we don't have `-XFlexibleContexts` we'll get an
error from `checkValidType` but (critically) it includes the helpful
suggestion of adding `-XFlexibleContexts`.  See #10608, #10351.