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.

2 files changed, 5 insertions, 6 deletions

diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index bb7315074f..f06f12e89a 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -232,10 +232,8 @@ pprInstances ispecs = vcat (map pprInstance ispecs)
 
 instanceHead :: ClsInst -> ([TyVar], Class, [Type])
 -- Returns the head, using the fresh tyvars from the ClsInst
-instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+instanceHead (ClsInst { is_tvs = tvs, is_cls = cls, is_tys = tys })
    = (tvs, cls, tys)
-   where
-     (_, _, cls, _) = tcSplitDFunTy (idType dfun)
 
 -- | Collects the names of concrete types and type constructors that make
 -- up the head of a class instance. For instance, given `class Foo a b`:
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 3685876fa4..689503ef89 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -31,7 +31,7 @@ module GHC.Core.TyCo.FVs
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
         -- * Free type constructors
-        tyConsOfType,
+        tyConsOfType, tyConsOfTypes,
 
         -- * Free vars with visible/invisible separate
         visVarsOfTypes, visVarsOfType,
@@ -1069,7 +1069,7 @@ tyConsOfType ty
      go ty | Just ty' <- coreView ty = go ty'
      go (TyVarTy {})                = emptyUniqSet
      go (LitTy {})                  = emptyUniqSet
-     go (TyConApp tc tys)           = go_tc tc `unionUniqSets` go_s tys
+     go (TyConApp tc tys)           = go_tc tc `unionUniqSets` tyConsOfTypes tys
      go (AppTy a b)                 = go a `unionUniqSets` go b
      go (FunTy af w a b)            = go w `unionUniqSets`
                                       go a `unionUniqSets` go b
@@ -1108,12 +1108,13 @@ tyConsOfType ty
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
 
-     go_s tys     = foldr (unionUniqSets . go)     emptyUniqSet tys
      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos
 
      go_tc tc = unitUniqSet tc
      go_ax ax = go_tc $ coAxiomTyCon ax
 
+tyConsOfTypes :: [Type] -> UniqSet TyCon
+tyConsOfTypes tys = foldr (unionUniqSets . tyConsOfType) emptyUniqSet tys
 
 {- **********************************************************************
 *                                                                       *