matchLocalInst: do domination analysis

When multiple Given quantified constraints match a Wanted, and there is
a quantified constraint that dominates all others, we now pick it
to solve the Wanted.

See Note [Use only the best matching quantified constraint].

For example:

  [G] d1: forall a b. ( Eq a, Num b, C a b  ) => D a b
  [G] d2: forall a  .                C a Int  => D a Int
  [W] {w}: D a Int

When solving the Wanted, we find that both Givens match, but we pick
the second, because it has a weaker precondition, C a Int, compared
to (Eq a, Num Int, C a Int). We thus say that d2 dominates d1;
see Note [When does a quantified instance dominate another?].

This domination test is done purely in terms of superclass expansion,
in the function GHC.Tc.Solver.Interact.impliedBySCs. We don't attempt
to do a full round of constraint solving; this simple check suffices
for now.

Fixes #22216 and #22223

1 files changed, 14 insertions, 0 deletions

diff --git a/testsuite/tests/quantified-constraints/T22216a.hs b/testsuite/tests/quantified-constraints/T22216a.hs
new file mode 100644
index 0000000000..f8df47d73d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module T22216a where
+
+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
+
+foo :: (Ord a, Ord1 f) => (Eq (f a) => r) -> r
+foo r = r