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, 10 insertions, 21 deletions

diff --git a/compiler/GHC/Tc/Utils/Backpack.hs b/compiler/GHC/Tc/Utils/Backpack.hs
index a73c01c90f..f11b900d6e 100644
--- a/compiler/GHC/Tc/Utils/Backpack.hs
+++ b/compiler/GHC/Tc/Utils/Backpack.hs
@@ -27,7 +27,6 @@ import GHC.Types.Fixity (defaultFixity)
 import GHC.Types.Fixity.Env
 import GHC.Types.TypeEnv
 import GHC.Types.Name.Reader
-import GHC.Types.Id
 import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Types.Name.Set
@@ -35,6 +34,7 @@ import GHC.Types.Avail
 import GHC.Types.SrcLoc
 import GHC.Types.SourceFile
 import GHC.Types.Var
+import GHC.Types.Id( idType )
 import GHC.Types.Unique.DSet
 import GHC.Types.Name.Shape
 import GHC.Types.PkgQual
@@ -62,8 +62,6 @@ import GHC.Hs
 
 import GHC.Core.InstEnv
 import GHC.Core.FamInstEnv
-import GHC.Core.Type
-import GHC.Core.Multiplicity
 
 import GHC.IfaceToCore
 import GHC.Iface.Load
@@ -221,32 +219,23 @@ checkHsigIface tcg_env gr sig_iface
 -- (we might conclude the module exports an instance when it doesn't, see
 -- #9422), but we will never refuse to compile something.
 check_inst :: ClsInst -> TcM ()
-check_inst sig_inst = do
+check_inst sig_inst@(ClsInst { is_dfun = dfun_id }) = do
     -- TODO: This could be very well generalized to support instance
     -- declarations in boot files.
     tcg_env <- getGblEnv
     -- NB: Have to tug on the interface, not necessarily
     -- tugged... but it didn't work?
     mapM_ tcLookupImported_maybe (nameSetElemsStable (orphNamesOfClsInst sig_inst))
+
     -- Based off of 'simplifyDeriv'
-    let ty = idType (instanceDFunId sig_inst)
-        -- Based off of tcSplitDFunTy
-        (tvs, theta, pred) =
-           case tcSplitForAllInvisTyVars ty of { (tvs, rho)    ->
-           case splitFunTys rho             of { (theta, pred) ->
-           (tvs, theta, pred) }}
-        origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
-    skol_info <- mkSkolemInfo InstSkol
-    (skol_subst, tvs_skols) <- tcInstSkolTyVars skol_info tvs -- Skolemize
+    let origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
+    (skol_info, tvs_skols, inst_theta, cls, inst_tys) <- tcSkolDFunType (idType dfun_id)
     (tclvl,cts) <- pushTcLevelM $ do
-       wanted <- newWanted origin
-                           (Just TypeLevel)
-                           (substTy skol_subst pred)
-       givens <- forM theta $ \given -> do
+       wanted <- newWanted origin (Just TypeLevel) (mkClassPred cls inst_tys)
+       givens <- forM inst_theta $ \given -> do
            loc <- getCtLocM origin (Just TypeLevel)
-           let given_pred = substTy skol_subst (scaledThing given)
-           new_ev <- newEvVar given_pred
-           return CtGiven { ctev_pred = given_pred
+           new_ev <- newEvVar given
+           return CtGiven { ctev_pred = given
                           -- Doesn't matter, make something up
                           , ctev_evar = new_ev
                           , ctev_loc = loc
@@ -254,7 +243,7 @@ check_inst sig_inst = do
        return $ wanted : givens
     unsolved <- simplifyWantedsTcM cts
 
-    (implic, _) <- buildImplicationFor tclvl (getSkolemInfo skol_info) tvs_skols [] unsolved
+    (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
     reportAllUnsolved (mkImplicWC implic)
 
 -- | For a module @modname@ of type 'HscSource', determine the list