Refactor the treatment of loopy superclass dictswip/T20666

This patch completely re-engineers how we deal with loopy superclass
dictionaries in instance declarations. It fixes #20666 and #19690

The highlights are

* Recognise that the loopy-superclass business should use precisely
  the Paterson conditions.  This is much much nicer.  See
  Note [Recursive superclasses] in GHC.Tc.TyCl.Instance

* With that in mind, define "Paterson-smaller" in
  Note [Paterson conditions] in GHC.Tc.Validity, and the new
  data type `PatersonSize` in GHC.Tc.Utils.TcType, along with
  functions to compute and compare PatsonSizes

* Use the new PatersonSize stuff when solving superclass constraints
  See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance

* In GHC.Tc.Solver.Monad.lookupInInerts, add a missing call to
  prohibitedSuperClassSolve.  This was the original cause of #20666.

* Treat (TypeError "stuff") as having PatersonSize zero. See
  Note [Paterson size for type family applications] in GHC.Tc.Utils.TcType.

* Treat the head of a Wanted quantified constraint in the same way
  as the superclass of an instance decl; this is what fixes #19690.
  See GHC.Tc.Solver.Canonical Note [Solving a Wanted forall-constraint]
  (Thanks to Matthew Craven for this insight.)

  This entailed refactoring the GivenSc constructor of CtOrigin a bit,
  to say whether it comes from an instance decl or quantified constraint.

* Some refactoring way in which redundant constraints are reported; we
  don't want to complain about the extra, apparently-redundant
  constraints that we must add to an instance decl because of the
  loopy-superclass thing.  I moved some work from GHC.Tc.Errors to
  GHC.Tc.Solver.

* Add a new section to the user manual to describe the loopy
  superclass issue and what rules it follows.

4 files changed, 43 insertions, 42 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T15473.stderr b/testsuite/tests/typecheck/should_compile/T15473.stderr
index 6fdeaa115c..42aeee63c2 100644
--- a/testsuite/tests/typecheck/should_compile/T15473.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15473.stderr
@@ -1,8 +1,9 @@
 
 T15473.hs:11:3: error:
     • Variable ‘a’ occurs more often
-        in the type family application ‘Undefined’
-        than in the instance head ‘LetInterleave xs t ts is y z’
+        in the type-family application ‘Undefined’
+        than in the LHS of the family instance ‘LetInterleave
+                                                  xs t ts is y z’
       (Use UndecidableInstances to permit this)
     • In the equations for closed type family ‘LetInterleave’
       In the type family declaration for ‘LetInterleave’
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index d34792964a..628a78aea6 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -41,12 +41,22 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
         ($) (_ :: [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+        id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
+          where id :: forall a. a -> a
+        head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
+          where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+        last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
+          where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+        fst (_ :: (t0 -> [Integer] -> Integer, b1)) (_ :: t0)
+          where fst :: forall a b. (a, b) -> a
+        snd (_ :: (a2, t0 -> [Integer] -> Integer)) (_ :: t0)
+          where snd :: forall a b. (a, b) -> b
         return (_ :: Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: Integer)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         (>>=) (_ :: [Integer] -> a8) (_ :: a8 -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
                          Monad m =>
@@ -83,16 +93,6 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where (<$) :: forall (f :: * -> *) a b.
                         Functor f =>
                         a -> f b -> f a
-        id (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
-          where id :: forall a. a -> a
-        head (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
-          where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
-        last (_ :: [t0 -> [Integer] -> Integer]) (_ :: t0)
-          where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
-        fst (_ :: (t0 -> [Integer] -> Integer, b1)) (_ :: t0)
-          where fst :: forall a b. (a, b) -> a
-        snd (_ :: (a2, t0 -> [Integer] -> Integer)) (_ :: t0)
-          where snd :: forall a b. (a, b) -> b
         id (_ :: [Integer] -> Integer)
           where id :: forall a. a -> a
         head (_ :: [[Integer] -> Integer])
@@ -117,12 +117,12 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
-          where ($!) :: forall a b. (a -> b) -> a -> b
 
 abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> [Integer] -> Integer
@@ -158,12 +158,22 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
         ($) (_ :: Integer -> [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: Integer -> [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+        id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
+          where id :: forall a. a -> a
+        head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
+          where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+        last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
+          where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
+        fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b1)) (_ :: t0)
+          where fst :: forall a b. (a, b) -> a
+        snd (_ :: (a2, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
+          where snd :: forall a b. (a, b) -> b
         return (_ :: [Integer] -> Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: [Integer] -> Integer)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: Integer -> [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         (>>=) (_ :: Integer -> a8)
               (_ :: a8 -> Integer -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
@@ -203,16 +213,6 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where (<$) :: forall (f :: * -> *) a b.
                         Functor f =>
                         a -> f b -> f a
-        id (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
-          where id :: forall a. a -> a
-        head (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
-          where head :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
-        last (_ :: [t0 -> Integer -> [Integer] -> Integer]) (_ :: t0)
-          where last :: forall a. GHC.Stack.Types.HasCallStack => [a] -> a
-        fst (_ :: (t0 -> Integer -> [Integer] -> Integer, b1)) (_ :: t0)
-          where fst :: forall a b. (a, b) -> a
-        snd (_ :: (a2, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
-          where snd :: forall a b. (a, b) -> b
         id (_ :: Integer -> [Integer] -> Integer)
           where id :: forall a. a -> a
         head (_ :: [Integer -> [Integer] -> Integer])
@@ -239,9 +239,9 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
-          where ($!) :: forall a b. (a -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
index 65e213a21b..44fa618172 100644
--- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
@@ -36,12 +36,12 @@ constraint_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
           where const :: forall a b. a -> b -> a
         ($) (_ :: [a] -> a)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: [a] -> a)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: a)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: a)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: [a] -> a)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         id (_ :: [a] -> a)
           where id :: forall a. a -> a
         head (_ :: [[a] -> a])
diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
index adb5ed75f2..6dc4f2ba0a 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -70,6 +70,11 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
           with ($) @GHC.Types.LiftedRep @[Integer] @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @GHC.Types.LiftedRep @[Integer] @Integer
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         return (_ :: Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
           with return @((->) [Integer]) @Integer
@@ -80,11 +85,6 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
           with pure @((->) [Integer]) @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @GHC.Types.LiftedRep @[Integer] @Integer
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
         j (_ :: [Integer] -> Integer)
           where j :: forall a. a -> a
           with j @([Integer] -> Integer)
@@ -171,6 +171,11 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
           with ($) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: Integer -> [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         return (_ :: [Integer] -> Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
           with return @((->) Integer) @([Integer] -> Integer)
@@ -181,11 +186,6 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
           with pure @((->) Integer) @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: Integer -> [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
         j (_ :: Integer -> [Integer] -> Integer)
           where j :: forall a. a -> a
           with j @(Integer -> [Integer] -> Integer)