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.

5 files changed, 15 insertions, 20 deletions

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’