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, 10 insertions, 0 deletions

diff --git a/docs/users_guide/9.6.1-notes.rst b/docs/users_guide/9.6.1-notes.rst
index f66ba9e06a..54f4a3fed2 100644
--- a/docs/users_guide/9.6.1-notes.rst
+++ b/docs/users_guide/9.6.1-notes.rst
@@ -68,6 +68,16 @@ Language
   :extension:`TypeData`. This extension permits ``type data`` declarations
   as a more fine-grained alternative to :extension:`DataKinds`.
 
+- GHC now does a better job of solving constraints in the presence of multiple
+  matching quantified constraints. For example, if we want to solve
+  ``C a b Int`` and we have matching quantified constraints: ::
+
+    forall x y z. (Ord x, Enum y, Num z) => C x y z
+    forall u v. (Enum v, Eq u) => C u v Int
+
+  Then GHC will use the second quantified constraint to solve ``C a b Int``,
+  as it has a strictly weaker precondition.
+
 Compiler
 ~~~~~~~~