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.

32 files changed, 210 insertions, 94 deletions

diff --git a/testsuite/tests/deriving/should_compile/T14339.hs b/testsuite/tests/deriving/should_compile/T14339.hs
index e2521f2de0..098b6e829a 100644
--- a/testsuite/tests/deriving/should_compile/T14339.hs
+++ b/testsuite/tests/deriving/should_compile/T14339.hs
@@ -5,9 +5,6 @@ module Bug where
 
 import GHC.TypeLits
 
-newtype Baz = Baz Foo
-  deriving Bar
-
 newtype Foo = Foo Int
 
 class Bar a where
@@ -15,3 +12,14 @@ class Bar a where
 
 instance (TypeError (Text "Boo")) => Bar Foo where
   bar = undefined
+
+newtype Baz = Baz Foo
+  deriving Bar
+
+-- Apparently we derive
+--  instance TypeError (Text "Boo") => Bar Baz
+--
+-- Is that really what we want?  It defers the type
+-- error... surely we should use standalone deriving
+-- if that is what we want?
+-- See GHC.Tc.Validity.validDerivPred and #22696.
\ No newline at end of file
diff --git a/testsuite/tests/deriving/should_fail/T21302.hs b/testsuite/tests/deriving/should_fail/T21302.hs
index 16e7cf320d..2e073e6f3c 100644
--- a/testsuite/tests/deriving/should_fail/T21302.hs
+++ b/testsuite/tests/deriving/should_fail/T21302.hs
@@ -10,3 +10,9 @@ type family Assoc a
 data BoxAssoc a = BoxAssoc (Assoc a)
 
 deriving instance c Eq a => Eq (BoxAssoc a)
+
+{-
+[W] Eq (BoxAssoc Int)
+==>
+[W] c0 Eq Int
+-}
diff --git a/testsuite/tests/deriving/should_fail/T8165_fail2.stderr b/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
index c0ceabf920..99e2c5fdbb 100644
--- a/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
+++ b/testsuite/tests/deriving/should_fail/T8165_fail2.stderr
@@ -1,6 +1,6 @@
 
 T8165_fail2.hs:9:12: error:
-    • The type family application ‘T Loop’
-        is no smaller than the instance head ‘T Loop’
+    • The type-family application ‘T Loop’
+        is no smaller than the LHS of the family instance ‘T Loop’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘C Loop’
diff --git a/testsuite/tests/impredicative/T17332.stderr b/testsuite/tests/impredicative/T17332.stderr
index 5fb876b8c5..97c35bf70a 100644
--- a/testsuite/tests/impredicative/T17332.stderr
+++ b/testsuite/tests/impredicative/T17332.stderr
@@ -1,5 +1,7 @@
 
 T17332.hs:13:7: error: [GHC-05617]
-    • Could not solve: ‘a’ arising from a use of ‘MkDict’
+    • Could not solve: ‘a’
+        arising from the head of a quantified constraint
+        arising from a use of ‘MkDict’
     • In the expression: MkDict
       In an equation for ‘aux’: aux = MkDict
diff --git a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
index 500be78a5f..733d90eafc 100644
--- a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
@@ -1,17 +1,18 @@
 
 NotRelaxedExamples.hs:9:15: error:
-    • Illegal nested type family application ‘F1 (F1 Char)’
+    • Illegal nested use of type family ‘F1’
+        in the arguments of the type-family application ‘F1 (F1 Char)’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘F1’
 
 NotRelaxedExamples.hs:10:15: error:
-    • The type family application ‘F2 [x]’
-        is no smaller than the instance head ‘F2 [x]’
+    • The type-family application ‘F2 [x]’
+        is no smaller than the LHS of the family instance ‘F2 [x]’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘F2’
 
 NotRelaxedExamples.hs:11:15: error:
-    • The type family application ‘F3 [Char]’
-        is no smaller than the instance head ‘F3 Bool’
+    • The type-family application ‘F3 [Char]’
+        is no smaller than the LHS of the family instance ‘F3 Bool’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘F3’
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr
index af8acae33a..b6851fe0f6 100644
--- a/testsuite/tests/indexed-types/should_fail/T10817.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr
@@ -1,7 +1,7 @@
 
 T10817.hs:9:3: error:
-    • The type family application ‘F a’
-        is no smaller than the instance head ‘F a’
+    • The type-family application ‘F a’
+        is no smaller than the LHS of the family instance ‘F a’
       (Use UndecidableInstances to permit this)
     • In the default type instance declaration for ‘F’
       In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T13271.stderr b/testsuite/tests/indexed-types/should_fail/T13271.stderr
index 4a8e7ebd20..81af4cbbab 100644
--- a/testsuite/tests/indexed-types/should_fail/T13271.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13271.stderr
@@ -13,10 +13,3 @@ T13271.hs:13:3: error: [GHC-05175]
         X 2 = T2 -- Defined at T13271.hs:13:3
     • In the equations for closed type family ‘X’
       In the type family declaration for ‘X’
-
-T13271.hs:13:3: error:
-    • The type family application ‘(TypeError ...)’
-        is no smaller than the instance head ‘X 2’
-      (Use UndecidableInstances to permit this)
-    • In the equations for closed type family ‘X’
-      In the type family declaration for ‘X’
diff --git a/testsuite/tests/indexed-types/should_fail/T15172.stderr b/testsuite/tests/indexed-types/should_fail/T15172.stderr
index 8c28c5148c..b961109055 100644
--- a/testsuite/tests/indexed-types/should_fail/T15172.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15172.stderr
@@ -1,5 +1,5 @@
 
 T15172.hs:11:10: error:
-    • Illegal nested constraint ‘F a’
+    • Illegal use of type family ‘F’ in the constraint ‘F a’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘C [[a]]’
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
index 4ac7e2537c..2e111b9eff 100644
--- a/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
+++ b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
@@ -1,18 +1,19 @@
 
 TyFamUndec.hs:6:15: error:
     • Variable ‘b’ occurs more often
-        in the type family application ‘T (b, b)’
-        than in the instance head ‘T (a, [b])’
+        in the type-family application ‘T (b, b)’
+        than in the LHS of the family instance ‘T (a, [b])’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘T’
 
 TyFamUndec.hs:7:15: error:
-    • The type family application ‘T (a, Maybe b)’
-        is no smaller than the instance head ‘T (a, Maybe b)’
+    • The type-family application ‘T (a, Maybe b)’
+        is no smaller than the LHS of the family instance ‘T (a, Maybe b)’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘T’
 
 TyFamUndec.hs:8:15: error:
-    • Illegal nested type family application ‘T (a, T b)’
+    • Illegal nested use of type family ‘T’
+        in the arguments of the type-family application ‘T (a, T b)’
       (Use UndecidableInstances to permit this)
     • In the type instance declaration for ‘T’
diff --git a/testsuite/tests/quantified-constraints/T19690.hs b/testsuite/tests/quantified-constraints/T19690.hs
new file mode 100644
index 0000000000..924ad35951
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T19690.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, ConstraintKinds, FlexibleInstances,
+  GADTs, QuantifiedConstraints, TypeApplications, ScopedTypeVariables #-}
+
+module T19690 where
+
+class c => Hold c
+instance c => Hold c
+
+data Dict c = c => Dict
+
+anythingDict :: Dict c
+anythingDict = go
+  where
+    go :: (Hold c => c) => Dict c
+    go = Dict
diff --git a/testsuite/tests/quantified-constraints/T19690.stderr b/testsuite/tests/quantified-constraints/T19690.stderr
new file mode 100644
index 0000000000..38c4dcda64
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T19690.stderr
@@ -0,0 +1,16 @@
+
+T19690.hs:12:16: error: [GHC-05617]
+    • Could not deduce ‘c’
+        arising from the head of a quantified constraint
+        arising from a use of ‘go’
+      from the context: Hold c
+        bound by a quantified context at T19690.hs:12:16-17
+    • In the expression: go
+      In an equation for ‘anythingDict’:
+          anythingDict
+            = go
+            where
+                go :: (Hold c => c) => Dict c
+                go = Dict
+    • Relevant bindings include
+        anythingDict :: Dict c (bound at T19690.hs:12:1)
diff --git a/testsuite/tests/quantified-constraints/T19921.stderr b/testsuite/tests/quantified-constraints/T19921.stderr
index 4ebc2d227f..7284fbdbf7 100644
--- a/testsuite/tests/quantified-constraints/T19921.stderr
+++ b/testsuite/tests/quantified-constraints/T19921.stderr
@@ -1,6 +1,9 @@
 
 T19921.hs:29:8: error: [GHC-05617]
-    • Could not deduce ‘r’ arising from a use of ‘Dict’
+    • Could not deduce ‘r’
+        arising from the head of a quantified constraint
+        arising from the head of a quantified constraint
+        arising from a use of ‘Dict’
       from the context: (x \/ y) \/ z
         bound by a quantified context at T19921.hs:29:8-11
       or from: (x ⇒ r, (y \/ z) ⇒ r)
diff --git a/testsuite/tests/quantified-constraints/T21006.stderr b/testsuite/tests/quantified-constraints/T21006.stderr
index 1abacf8eb5..7eb7c88a07 100644
--- a/testsuite/tests/quantified-constraints/T21006.stderr
+++ b/testsuite/tests/quantified-constraints/T21006.stderr
@@ -1,6 +1,7 @@
 
 T21006.hs:14:10: error: [GHC-05617]
     • Could not deduce ‘c’
+        arising from the head of a quantified constraint
         arising from the superclasses of an instance declaration
       from the context: (Determines b, Determines c)
         bound by a quantified context at T21006.hs:14:10-15
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index fba21ff79d..b3d0eb920f 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -40,3 +40,4 @@ test('T22216c', normal, compile, [''])
 test('T22216d', normal, compile, [''])
 test('T22216e', normal, compile, [''])
 test('T22223', normal, compile, [''])
+test('T19690', normal, compile_fail, [''])
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)
diff --git a/testsuite/tests/typecheck/should_fail/T14884.stderr b/testsuite/tests/typecheck/should_fail/T14884.stderr
index 30e1ffbbfc..5ce38cdecb 100644
--- a/testsuite/tests/typecheck/should_fail/T14884.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14884.stderr
@@ -18,6 +18,10 @@ T14884.hs:4:5: error: [GHC-88464]
           with foldMap @[] @(IO ()) @Char
           (imported from ‘Prelude’ at T14884.hs:1:8-13
            (and originally defined in ‘Data.Foldable’))
+        id :: forall a. a -> a
+          with id @(String -> IO ())
+          (imported from ‘Prelude’ at T14884.hs:1:8-13
+           (and originally defined in ‘GHC.Base’))
         ($) :: forall a b. (a -> b) -> a -> b
           with ($) @GHC.Types.LiftedRep @String @(IO ())
           (imported from ‘Prelude’ at T14884.hs:1:8-13
@@ -26,10 +30,6 @@ T14884.hs:4:5: error: [GHC-88464]
           with ($!) @GHC.Types.LiftedRep @String @(IO ())
           (imported from ‘Prelude’ at T14884.hs:1:8-13
            (and originally defined in ‘GHC.Base’))
-        id :: forall a. a -> a
-          with id @(String -> IO ())
-          (imported from ‘Prelude’ at T14884.hs:1:8-13
-           (and originally defined in ‘GHC.Base’))
 
 T14884.hs:4:7: error: [GHC-39999]
     • Ambiguous type variable ‘a0’ arising from a use of ‘print’
@@ -40,7 +40,7 @@ T14884.hs:4:7: error: [GHC-39999]
           -- Defined in ‘Data.Either’
         instance Show Ordering -- Defined in ‘GHC.Show’
         ...plus 26 others
-        ...plus 28 instances involving out-of-scope types
+        ...plus 29 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the first argument of ‘_’, namely ‘print’
       In the expression: _ print "abc"
diff --git a/testsuite/tests/typecheck/should_fail/T15552a.stderr b/testsuite/tests/typecheck/should_fail/T15552a.stderr
index f7a6094d9e..af168c8d08 100644
--- a/testsuite/tests/typecheck/should_fail/T15552a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15552a.stderr
@@ -1,21 +1,24 @@
 
 T15552a.hs:26:9: error:
-    • Illegal nested type family application ‘GetEntryOfVal
-                                                (FirstEntryOfVal v kvs)’
+    • Illegal nested use of type family ‘FirstEntryOfVal’
+        in the arguments of the type-family application ‘GetEntryOfVal
+                                                           (FirstEntryOfVal v kvs)’
       (Use UndecidableInstances to permit this)
     • In the equations for closed type family ‘FirstEntryOfVal’
       In the type family declaration for ‘FirstEntryOfVal’
 
 T15552a.hs:26:9: error:
-    • Illegal nested type family application ‘EntryOfValKey
-                                                (FirstEntryOfVal v kvs)’
+    • Illegal nested use of type family ‘FirstEntryOfVal’
+        in the arguments of the type-family application ‘EntryOfValKey
+                                                           (FirstEntryOfVal v kvs)’
       (Use UndecidableInstances to permit this)
     • In the equations for closed type family ‘FirstEntryOfVal’
       In the type family declaration for ‘FirstEntryOfVal’
 
 T15552a.hs:26:9: error:
-    • Illegal nested type family application ‘EntryOfValKey
-                                                (FirstEntryOfVal v kvs)’
+    • Illegal nested use of type family ‘FirstEntryOfVal’
+        in the arguments of the type-family application ‘EntryOfValKey
+                                                           (FirstEntryOfVal v kvs)’
       (Use UndecidableInstances to permit this)
     • In the equations for closed type family ‘FirstEntryOfVal’
       In the type family declaration for ‘FirstEntryOfVal’
diff --git a/testsuite/tests/typecheck/should_fail/T15801.stderr b/testsuite/tests/typecheck/should_fail/T15801.stderr
index 9c7cdabeef..922fae41a7 100644
--- a/testsuite/tests/typecheck/should_fail/T15801.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15801.stderr
@@ -2,5 +2,6 @@
 T15801.hs:52:10: error: [GHC-18872]
     • Couldn't match representation of type: UnOp op_a -> UnOp b
                                with that of: op_a --> b
+        arising from the head of a quantified constraint
         arising from the superclasses of an instance declaration
     • In the instance declaration for ‘OpRíki (Op (*))’
diff --git a/testsuite/tests/typecheck/should_fail/T20666.hs b/testsuite/tests/typecheck/should_fail/T20666.hs
new file mode 100644
index 0000000000..279c8f4b7d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+type family T t
+type family S s
+
+class Show (T c) => C1 c
+class Show (T (S d)) => D d
+instance (D d, c ~ S d) => C1 c
+ -- this one fails in GHC 9.2
+
+class Show (T c) => C2 c
+instance (D d, c ~ S d, c' ~ c) => C2 c'
+ -- This one succeeded because it went via lookupInInerts.
+ -- It should fail, just like the one above.
diff --git a/testsuite/tests/typecheck/should_fail/T20666.stderr b/testsuite/tests/typecheck/should_fail/T20666.stderr
new file mode 100644
index 0000000000..bc2aad5497
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666.stderr
@@ -0,0 +1,20 @@
+
+T20666.hs:13:10: error: [GHC-39999]
+    • Could not deduce ‘Show (T c)’
+        arising from the superclasses of an instance declaration
+      from the context: (D d, c ~ S d)
+        bound by the instance declaration at T20666.hs:13:10-31
+      Possible fix:
+        If the constraint looks soluble from a superclass of the instance context,
+        read 'Undecidable instances and loopy superclasses' in the user manual
+    • In the instance declaration for ‘C1 c’
+
+T20666.hs:17:10: error: [GHC-39999]
+    • Could not deduce ‘Show (T c)’
+        arising from the superclasses of an instance declaration
+      from the context: (D d, c ~ S d, c' ~ c)
+        bound by the instance declaration at T20666.hs:17:10-40
+      Possible fix:
+        If the constraint looks soluble from a superclass of the instance context,
+        read 'Undecidable instances and loopy superclasses' in the user manual
+    • In the instance declaration for ‘C2 c'’
diff --git a/testsuite/tests/typecheck/should_fail/T20666a.hs b/testsuite/tests/typecheck/should_fail/T20666a.hs
new file mode 100644
index 0000000000..b1e4d2c174
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T20666a where
+
+type family F a
+
+class Eq (F a) => D a
+class Eq (F a) => C a
+
+instance D [a] => C [a]
+
diff --git a/testsuite/tests/typecheck/should_fail/T20666a.stderr b/testsuite/tests/typecheck/should_fail/T20666a.stderr
new file mode 100644
index 0000000000..4192b88807
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20666a.stderr
@@ -0,0 +1,10 @@
+
+T20666a.hs:11:10: error: [GHC-39999]
+    • Could not deduce ‘Eq (F [a])’
+        arising from the superclasses of an instance declaration
+      from the context: D [a]
+        bound by the instance declaration at T20666a.hs:11:10-23
+      Possible fix:
+        If the constraint looks soluble from a superclass of the instance context,
+        read 'Undecidable instances and loopy superclasses' in the user manual
+    • In the instance declaration for ‘C [a]’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index b15a50b228..61514e725b 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -667,3 +667,5 @@ test('T21530a', normal, compile_fail, [''])
 test('T21530b', normal, compile_fail, [''])
 test('T22570', normal, compile_fail, [''])
 test('T22645', normal, compile_fail, [''])
+test('T20666', normal, compile_fail, [''])
+test('T20666a', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/fd-loop.stderr b/testsuite/tests/typecheck/should_fail/fd-loop.stderr
index 86a70f5b76..a9320c009a 100644
--- a/testsuite/tests/typecheck/should_fail/fd-loop.stderr
+++ b/testsuite/tests/typecheck/should_fail/fd-loop.stderr
@@ -1,6 +1,6 @@
 
 fd-loop.hs:12:10: error:
-    • Variable ‘b’ occurs more often
-        in the constraint ‘C a b’ than in the instance head ‘Eq (T a)’
+    • The constraint ‘C a b’
+        is no smaller than the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail108.stderr b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
index 4096ad36c6..2c7db0dd71 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail108.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
@@ -1,7 +1,6 @@
 
 tcfail108.hs:7:10: error:
-    • Variable ‘f’ occurs more often
-        in the constraint ‘Eq (f (Rec f))’
-        than in the instance head ‘Eq (Rec f)’
+    • The constraint ‘Eq (f (Rec f))’
+        is no smaller than the instance head ‘Eq (Rec f)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (Rec f)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.hs b/testsuite/tests/typecheck/should_fail/tcfail133.hs
index 4aded61a27..a892fbca7d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.hs
@@ -60,11 +60,13 @@ instance Number n
       => Add (n:@Zero) One (n:@One)
 instance AddDigit n One r'
       => Add (n:@One) One (r':@Zero)
-instance (Number n1, Digit d1, Number n2, Digit n2
-         ,Add n1 n2 nr', AddDigit (d1:@nr') d2 r)
+instance ( Number n1, Digit d1, Number n2, Digit n2
+         , Add n1 n2 nr', AddDigit (d1:@nr') d2 r
+         , Number r)  -- Added when fixing #20666
+                      -- Because (AddDigit (d1:@nr') d2 r) is not
+                      -- Paterson-smaller than the instance head
       => Add (n1:@d1) (n2:@d2) r
 
-
 foo = show $ add (One:@Zero) (One:@One)
 
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.stderr b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
index 5b2a8944e5..ff2a76fec7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
@@ -2,7 +2,7 @@
 tcfail133.hs:2:61: warning: [-Wdeprecated-flags (in -Wdefault)]
     -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 
-tcfail133.hs:68:7: error: [GHC-39999]
+tcfail133.hs:70:7: error: [GHC-39999]
     • Ambiguous type variable ‘a0’ arising from a use of ‘show’
       prevents the constraint ‘(Show a0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘a0’ should be.
@@ -11,14 +11,14 @@ tcfail133.hs:68:7: error: [GHC-39999]
         instance (Number a, Digit b, Show a, Show b) => Show (a :@ b)
           -- Defined at tcfail133.hs:11:54
         ...plus 28 others
-        ...plus 12 instances involving out-of-scope types
+        ...plus 13 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the first argument of ‘($)’, namely ‘show’
       In the expression: show $ add (One :@ Zero) (One :@ One)
       In an equation for ‘foo’:
           foo = show $ add (One :@ Zero) (One :@ One)
 
-tcfail133.hs:68:14: error: [GHC-39999]
+tcfail133.hs:70:14: error: [GHC-39999]
     • No instance for ‘AddDigit (Zero :@ (One :@ One)) One a0’
         arising from a use of ‘add’
     • In the second argument of ‘($)’, namely
diff --git a/testsuite/tests/typecheck/should_fail/tcfail154.stderr b/testsuite/tests/typecheck/should_fail/tcfail154.stderr
index a4bda5998e..0fdf2e135b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail154.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail154.stderr
@@ -1,6 +1,6 @@
 
 tcfail154.hs:13:10: error:
-    • Variable ‘a’ occurs more often
-        in the constraint ‘C a a’ than in the instance head ‘Eq (T a)’
+    • The constraint ‘C a a’
+        is no smaller than the instance head ‘Eq (T a)’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail214.stderr b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
index 83fa344834..d0b153725e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail214.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
@@ -1,5 +1,5 @@
 
 tcfail214.hs:9:10: error:
-    • Illegal nested constraint ‘F a’
+    • Illegal use of type family ‘F’ in the constraint ‘F a’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘C [a]’