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, 1 insertions, 30 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 61caa2e456..c22ab6a2e5 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -391,7 +391,7 @@ reportImplic ctxt implic@(Implic { ic_skols  = tvs
 
 warnRedundantConstraints :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [EvVar] -> TcM ()
 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
-warnRedundantConstraints ctxt env info ev_vars
+warnRedundantConstraints ctxt env info redundant_evs
  | null redundant_evs
  = return ()
 
@@ -423,18 +423,6 @@ warnRedundantConstraints ctxt env info ev_vars
                 []
           ; reportDiagnostic msg }
 
-   redundant_evs =
-       filterOut is_type_error $
-       case info of -- See Note [Redundant constraints in instance decls]
-         InstSkol -> filterOut (improving . idType) ev_vars
-         _        -> ev_vars
-
-   -- See #15232
-   is_type_error = isJust . userTypeError_maybe . idType
-
-   improving pred -- (transSuperClasses p) does not include p
-     = any isImprovementPred (pred : transSuperClasses pred)
-
 reportBadTelescope :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [TcTyVar] -> TcM ()
 reportBadTelescope ctxt env (ForAllSkol telescope) skols
   = do { msg <- mkErrorReport
@@ -449,23 +437,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols
 reportBadTelescope _ _ skol_info skols
   = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols)
 
-{- Note [Redundant constraints in instance decls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For instance declarations, we don't report unused givens if
-they can give rise to improvement.  Example (#10100):
-    class Add a b ab | a b -> ab, a ab -> b
-    instance Add Zero b b
-    instance Add a b ab => Add (Succ a) b (Succ ab)
-The context (Add a b ab) for the instance is clearly unused in terms
-of evidence, since the dictionary has no fields.  But it is still
-needed!  With the context, a wanted constraint
-   Add (Succ Zero) beta (Succ Zero)
-we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
-But without the context we won't find beta := Zero.
-
-This only matters in instance declarations..
--}
-
 -- | Should we completely ignore this constraint in error reporting?
 -- It *must* be the case that any constraint for which this returns True
 -- somehow causes an error to be reported elsewhere.