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.

3 files changed, 19 insertions, 5 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’