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.

1 files changed, 94 insertions, 10 deletions

diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst
index 7776a7f833..84276527a3 100644
--- a/docs/users_guide/exts/instances.rst
+++ b/docs/users_guide/exts/instances.rst
@@ -180,18 +180,10 @@ syntactically allowed. Some further various observations about this grammar:
 
 .. _instance-rules:
 .. _instance-termination:
-.. _undecidable-instances:
 
 Instance termination rules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. extension:: UndecidableInstances
-    :shortdesc: Enable undecidable instances.
-
-    :since: 6.8.1
-
-    Permit definition of instances which may lead to type-checker non-termination.
-
 Regardless of :extension:`FlexibleInstances` and :extension:`FlexibleContexts`,
 instance declarations must conform to some rules that ensure that
 instance resolution will terminate. The restrictions can be lifted with
@@ -212,6 +204,9 @@ The rules are these:
       application can in principle expand to a type of arbitrary size,
       and so are rejected out of hand
 
+   If these three conditions hold we say that the constraint ``(C t1 ... tn)`` is
+   **Paterson-smaller** than the instance head.
+
 2. The Coverage Condition. For each functional dependency,
    ⟨tvs⟩\ :sub:`left` ``->`` ⟨tvs⟩\ :sub:`right`, of the class, every
    type variable in S(⟨tvs⟩\ :sub:`right`) must appear in
@@ -318,10 +313,99 @@ indeed the (somewhat strange) definition:
 makes instance inference go into a loop, because it requires the
 constraint ``(Mul a [b] b)``.
 
-The :extension:`UndecidableInstances` extension is also used to lift some of the
-restrictions imposed on type family instances. See
+.. _undecidable-instances:
+
+Undecidable instances and loopy superclasses
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. extension:: UndecidableInstances
+    :shortdesc: Enable undecidable instances.
+
+    :since: 6.8.1
+
+    Permit definition of instances which may lead to type-checker non-termination.
+
+The :extension:`UndecidableInstances` extension  lifts the restrictions on
+on instance declarations described in :ref:`instance-termination`.
+The :extension:`UndecidableInstances` extension also lifts some of the
+restrictions imposed on type family instances; see
 :ref:`type-family-decidability`.
 
+
+With :extension:`UndecidableInstances` it is possible to create a superclass cycle,
+which leads to the program failing to terminate.  To avoid this, GHC imposes
+rules on the way in which superclass constraints are satisfied in an instance
+declaration.  These rules apply even when :extension:`UndecidableInstances` is enabled.
+Consider::
+
+  class C a => D a where ...
+
+  instance Wombat [b] => D [b] where ...
+
+When typechecking this ``instance`` declaration, GHC must ensure that ``D``'s superclass,
+``(C [b])`` is satisfied. We say that ``(C [b])`` is a **Wanted superclass constraint** of the
+instance declaration.
+
+If there is an ``instance blah => C [b]``, which is often the
+case, GHC can use the instance declaration and all is well.  But suppose there is no
+such instance, so GHC can only satisfy the Wanted ``(C [b])`` from the context of the instance,
+namely the Given constraint ``(Wombat [b])``.  Perhaps the declaration of ``Wombat`` looks like this::
+
+  class C a => Wombat a
+
+So the Given ``(Wombat [b])`` has a superclass ``(C [b])``, and it looks as if we can satisfy the
+Wanted ``(C [b])`` constraint from this superclass of ``Wombat``.  But it turns out that
+allowing this can lead to subtle looping dictionaries, and GHC prevents it.
+
+The rule is this: **a Wanted superclass constraint can only be satisfied in one of these three ways:**
+
+.. rst-class:: open
+
+1. *Directly from the context of the instance declaration*.  For example, if the declaration looked like this::
+
+      instance (Wombat [b], C [b]) => D [b] where ...
+
+   we could satisfy the Wanted ``(C [b])`` from the Given ``(C [b])``.
+
+2. *Using another instance declaration*. For example, if we had::
+
+      instance C b => C [b] where ...
+
+   we can satisfy the Wanted superclass constraint ``(C [b])`` using this instance,
+   reducing it to the Wanted constraint ``(C b)`` (which still has to be solved).
+
+3. *Using the immediate superclass of a Given constraint X that is Paterson-smaller than the head of the instance declaration.*
+   The rules for Paterson-smaller are precisely those described in :ref:`instance-rules`:
+
+     - No type variable can occur more often in X than in the instance head.
+
+     - X must have fewer type constructors and variables (taken together and counting repetitions) than the instance head.
+
+     - X must mention no type functions.
+
+Rule (3) is the tricky one.  Here is an example, taken from GHC's own source code::
+
+           class Ord r => UserOfRegs r a where ...
+    (i1)   instance UserOfRegs r a => UserOfRegs r (Maybe a) where
+    (i2)   instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
+
+For ``(i1)`` we can get the ``(Ord r)`` superclass by selection from
+``(UserOfRegs r a)``, since it (i.e. ``UserOfRegs r a``) is Paterson-smaller than the
+head of the instance declaration, namely ``(UserOfRegs r (Maybe a))``.
+
+But for ``(i2)`` that isn't the case: ``(UserOfRegs r CmmReg)`` is not Paterson-smaller
+than the head of the instance ``(UserOfRegs r CmmExpr)``, so we can't use
+the superclasses of the former.  Hence we must instead add an explicit,
+and perhaps surprising, ``(Ord r)`` argument to the instance declaration.
+
+This fix, of simply adding an apparently-redundant constraint to the context
+of an instance declaration, is robust: it always fixes the problem.
+(We considered adding it automatically, but decided that it was better be explicit.)
+
+Fixing this subtle superclass cycle has a long history; if you are interested, read
+``Note [Recursive superclasses]`` and ``Note [Solving superclass constraints]``
+in ``GHC.Tc.TyCl.Instance``.
+
 .. _instance-overlap:
 
 Overlapping instances