Note [Use only the best matching quantified constraint]

Consider (#20582) the ambiguity check for
  (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int

Because of eager expansion of given superclasses, we get
  [G] d1: forall a. Ord (m a)
  [G] d2: forall a. Eq (m a)
  [G] d3: forall a. Semigroup a => Eq (m a)

  [W] {w1}: forall a. Ord (m a)
  [W] {w2}: forall a. Semigroup a => Eq (m a)

The first wanted is solved straightforwardly. But the second wanted
matches *two* local instances: d2 and d3. Our general rule around multiple local
instances is that we refuse to commit to any of them. However, that
means that our type fails the ambiguity check. That's bad: the type
is perfectly fine. (This actually came up in the wild, in the streamly
library.)

The solution is to prefer local instances which are easier to prove, meaning
that they have a weaker precondition. In this case, the empty context
of d2 is a weaker constraint than the "Semigroup a" context of d3, so we prefer
using it when proving w2. This allows us to pass the ambiguity check here.

Our criterion for solving a Wanted by matching local quantified instances is
thus as follows:

  - There is a matching local quantified instance that dominates all others
    matches, in the sense of [When does a quantified instance dominate another?].
    Any such match do, we pick it arbitrarily (the T22223 example below says why).
  - This local quantified instance also dominates all the unifiers, as we
    wouldn't want to commit to a single match when we might have multiple,
    genuinely different matches after further unification takes place.

Some other examples:


  #15244:

    f :: (C g, D g) => ....
    class S g => C g where ...
    class S g => D g where ...
    class (forall a. Eq a => Eq (g a)) => S g where ...

  Here, in f's RHS, there are two identical quantified constraints
  available, one via the superclasses of C and one via the superclasses
  of D. Given that each implies the other, we pick one arbitrarily.


  #22216:

    class Eq a
    class Eq a => Ord a
    class (forall b. Eq b => Eq (f b)) => Eq1 f
    class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f

  Suppose we have

    [G] d1: Ord1 f
    [G] d2: Eq a
    [W] {w}: Eq (f a)

  Superclass expansion of d1 gives us:

    [G] d3 : Eq1 f
    [G] d4 : forall b. Ord b => Ord (f b)

  expanding d4 and d5 gives us, respectively:

    [G] d5 : forall b. Eq  b => Eq (f b)
    [G] d6 : forall b. Ord b => Eq (f b)

  Now we have two matching local instances that we could use when solving the
  Wanted. However, it's obviously silly to use d6, given that d5 provides us with
  as much information, with a strictly weaker precondition. So we pick d5 to solve
  w. If we chose d6, we would get [W] Ord a, which in this case we can't solve.


  #22223:

    [G] forall a b. (Eq a, Ord b) => C a b
    [G] forall a b. (Ord b, Eq a) => C a b
    [W] C x y

  Here we should be free to pick either quantified constraint, as they are
  equivalent up to re-ordering of the constraints in the context.
  See also Note [Do not add duplicate quantified instances]
  in GHC.Tc.Solver.Monad.

Test cases:
  typecheck/should_compile/T20582
  quantified-constraints/T15244
  quantified-constraints/T22216{a,b,c,d,e}
  quantified-constraints/T22223

Historical note: a previous solution was to instead pick the local instance
with the least superclass depth (see Note [Replacement vs keeping]),
but that doesn't work for the example from #22216.