Fix and simplify DeriveAnyClass's context inference using SubTypePredSpecwip/T20719

As explained in `Note [Gathering and simplifying constraints for DeriveAnyClass]`
in `GHC.Tc.Deriv.Infer`, `DeriveAnyClass` infers instance contexts by emitting
implication constraints. Previously, these implication constraints were
constructed by hand. This is a terribly trick thing to get right, as it
involves a delicate interplay of skolemisation, metavariable instantiation, and
`TcLevel` bumping. Despite much effort, we discovered in #20719 that the
implementation was subtly incorrect, leading to valid programs being rejected.

While we could scrutinize the code that manually constructs implication
constraints and repair it, there is a better, less error-prone way to do
things. After all, the heart of `DeriveAnyClass` is generating code which
fills in each class method with defaults, e.g., `foo = $gdm_foo`. Typechecking
this sort of code is tantamount to calling `tcSubTypeSigma`, as we much ensure
that the type of `$gdm_foo` is a subtype of (i.e., more polymorphic than) the
type of `foo`. As an added bonus, `tcSubTypeSigma` is a battle-tested function
that handles skolemisation, metvariable instantiation, `TcLevel` bumping, and
all other means of tricky bookkeeping correctly.

With this insight, the solution to the problems uncovered in #20719 is simple:
use `tcSubTypeSigma` to check if `$gdm_foo`'s type is a subtype of `foo`'s
type. As a side effect, `tcSubTypeSigma` will emit exactly the implication
constraint that we were attempting to construct by hand previously. Moreover,
it does so correctly, fixing #20719 as a consequence.

This patch implements the solution thusly:

* The `PredSpec` data type (previously named `PredOrigin`) is now split into
  `SimplePredSpec`, which directly stores a `PredType`, and `SubTypePredSpec`,
  which stores the actual and expected types in a subtype check.
  `SubTypePredSpec` is only used for `DeriveAnyClass`; all other deriving
  strategies use `SimplePredSpec`.
* Because `tcSubTypeSigma` manages the finer details of type variable
  instantiation and constraint solving under the hood, there is no longer any
  need to delicately split apart the method type signatures in
  `inferConstraintsAnyclass`. This greatly simplifies the implementation of
  `inferConstraintsAnyclass` and obviates the need to store skolems,
  metavariables, or given constraints in a `ThetaSpec` (previously named
  `ThetaOrigin`). As a bonus, this means that `ThetaSpec` now simply becomes a
  synonym for a list of `PredSpec`s, which is conceptually much simpler than it
  was before.
* In `simplifyDeriv`, each `SubTypePredSpec` results in a call to
  `tcSubTypeSigma`. This is only performed for its side effect of emitting
  an implication constraint, which is fed to the rest of the constraint solving
  machinery in `simplifyDeriv`. I have updated
  `Note [Gathering and simplifying constraints for DeriveAnyClass]` to explain
  this in more detail.

To make the changes in `simplifyDeriv` more manageable, I also performed some
auxiliary refactoring:

* Previously, every iteration of `simplifyDeriv` was skolemising the type
  variables at the start, simplifying, and then performing a reverse
  substitution at the end to un-skolemise the type variables. This is not
  necessary, however, since we can just as well skolemise once at the
  beginning of the `deriving` pipeline and zonk the `TcTyVar`s after
  `simplifyDeriv` is finished. This patch does just that, having been made
  possible by prior work in !7613. I have updated `Note [Overlap and deriving]`
  in `GHC.Tc.Deriv.Infer` to explain this, and I have also left comments on
  the relevant data structures (e.g., `DerivEnv` and `DerivSpec`) to explain
  when things might be `TcTyVar`s or `TyVar`s.
* All of the aforementioned cleanup allowed me to remove an ad hoc
  deriving-related in `checkImplicationInvariants`, as all of the skolems in
  a `tcSubTypeSigma`–produced implication constraint should now be `TcTyVar`
  at the time the implication is created.
* Since `simplifyDeriv` now needs a `SkolemInfo` and `UserTypeCtxt`, I have
  added `ds_skol_info` and `ds_user_ctxt` fields to `DerivSpec` to store these.
  Similarly, I have also added a `denv_skol_info` field to `DerivEnv`, which
  ultimately gets used to initialize the `ds_skol_info` in a `DerivSpec`.

Fixes #20719.

8 files changed, 511 insertions, 275 deletions

diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 39900cb47e..29a58d9c01 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -88,7 +88,7 @@ Overall plan
 3.  Add the derived bindings, generating InstInfos
 -}
 
-data EarlyDerivSpec = InferTheta (DerivSpec [ThetaOrigin])
+data EarlyDerivSpec = InferTheta (DerivSpec ThetaSpec)
                     | GivenTheta (DerivSpec ThetaType)
         -- InferTheta ds => the context for the instance should be inferred
         --      In this case ds_theta is the list of all the sets of
@@ -102,7 +102,7 @@ data EarlyDerivSpec = InferTheta (DerivSpec [ThetaOrigin])
         -- See Note [Inferring the instance context] in GHC.Tc.Deriv.Infer
 
 splitEarlyDerivSpec :: [EarlyDerivSpec]
-                    -> ([DerivSpec [ThetaOrigin]], [DerivSpec ThetaType])
+                    -> ([DerivSpec ThetaSpec], [DerivSpec ThetaType])
 splitEarlyDerivSpec [] = ([],[])
 splitEarlyDerivSpec (InferTheta spec : specs) =
     case splitEarlyDerivSpec specs of (is, gs) -> (spec : is, gs)
@@ -1137,14 +1137,40 @@ mkEqnHelp :: Maybe OverlapMode
 mkEqnHelp overlap_mode tvs cls cls_args deriv_ctxt deriv_strat = do
   is_boot <- tcIsHsBootOrSig
   when is_boot $ bale_out DerivErrBootFileFound
+
+  let pred = mkClassPred cls cls_args
+  skol_info <- mkSkolemInfo (DerivSkol pred)
+  (tvs', cls_args', deriv_strat') <-
+    skolemise_when_inferring_context skol_info deriv_ctxt
+  let deriv_env = DerivEnv
+                    { denv_overlap_mode = overlap_mode
+                    , denv_tvs          = tvs'
+                    , denv_cls          = cls
+                    , denv_inst_tys     = cls_args'
+                    , denv_ctxt         = deriv_ctxt
+                    , denv_skol_info    = skol_info
+                    , denv_strat        = deriv_strat' }
   runReaderT mk_eqn deriv_env
   where
-    deriv_env = DerivEnv { denv_overlap_mode = overlap_mode
-                         , denv_tvs          = tvs
-                         , denv_cls          = cls
-                         , denv_inst_tys     = cls_args
-                         , denv_ctxt         = deriv_ctxt
-                         , denv_strat        = deriv_strat }
+    skolemise_when_inferring_context ::
+         SkolemInfo -> DerivContext
+      -> TcM ([TcTyVar], [TcType], Maybe (DerivStrategy GhcTc))
+    skolemise_when_inferring_context skol_info deriv_ctxt =
+      case deriv_ctxt of
+        -- In order to infer an instance context, we must later make use of
+        -- the constraint solving machinery, which expects TcTyVars rather
+        -- than TyVars. We skolemise the type variables with non-overlappable
+        -- (vanilla) skolems.
+        -- See Note [Overlap and deriving] in GHC.Tc.Deriv.Infer.
+        InferContext{} -> do
+          (skol_subst, tvs') <- tcInstSkolTyVars skol_info tvs
+          let cls_args'    = substTys skol_subst cls_args
+              deriv_strat' = fmap (mapDerivStrategy (substTy skol_subst))
+                                  deriv_strat
+          pure (tvs', cls_args', deriv_strat')
+        -- If the instance context is supplied, we don't need to skolemise
+        -- at all.
+        SupplyContext{} -> pure (tvs, cls_args, deriv_strat)
 
     bale_out =
       failWithTc . TcRnCannotDeriveInstance cls cls_args deriv_strat NoGeneralizedNewtypeDeriving
@@ -1308,7 +1334,9 @@ mk_eqn_from_mechanism mechanism
                 , denv_tvs          = tvs
                 , denv_cls          = cls
                 , denv_inst_tys     = inst_tys
-                , denv_ctxt         = deriv_ctxt } <- ask
+                , denv_ctxt         = deriv_ctxt
+                , denv_skol_info    = skol_info } <- ask
+       user_ctxt <- askDerivUserTypeCtxt
        doDerivInstErrorChecks1 mechanism
        loc       <- lift getSrcSpanM
        dfun_name <- lift $ newDFunName cls inst_tys loc
@@ -1321,6 +1349,8 @@ mk_eqn_from_mechanism mechanism
                    , ds_name = dfun_name, ds_tvs = tvs'
                    , ds_cls = cls, ds_tys = inst_tys'
                    , ds_theta = inferred_constraints
+                   , ds_skol_info = skol_info
+                   , ds_user_ctxt = user_ctxt
                    , ds_overlap = overlap_mode
                    , ds_standalone_wildcard = wildcard
                    , ds_mechanism = mechanism' } }
@@ -1331,6 +1361,8 @@ mk_eqn_from_mechanism mechanism
                    , ds_name = dfun_name, ds_tvs = tvs
                    , ds_cls = cls, ds_tys = inst_tys
                    , ds_theta = theta
+                   , ds_skol_info = skol_info
+                   , ds_user_ctxt = user_ctxt
                    , ds_overlap = overlap_mode
                    , ds_standalone_wildcard = Nothing
                    , ds_mechanism = mechanism }
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 3f8893460b..5bacc4fb30 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -39,7 +39,7 @@ module GHC.Tc.Deriv.Generate (
 
         getPossibleDataCons,
         DerivInstTys(..), buildDataConInstArgEnv,
-        derivDataConInstArgTys, substDerivInstTys
+        derivDataConInstArgTys, substDerivInstTys, zonkDerivInstTys
     ) where
 
 import GHC.Prelude
@@ -65,6 +65,7 @@ import GHC.Types.SrcLoc
 import GHC.Core.TyCon
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Zonk
 import GHC.Tc.Validity ( checkValidCoAxBranch )
 import GHC.Core.Coercion.Axiom ( coAxiomSingleBranch )
 import GHC.Builtin.Types.Prim
@@ -2694,6 +2695,12 @@ getPossibleDataCons tycon tycon_args = filter isPossible $ tyConDataCons tycon
 -- @dit_cls_tys ++ ['mkTyConApp' dit_tc dit_tc_args]@. Other parts of the
 -- instance declaration can be found in the 'DerivEnv'. For example, the @Cls@
 -- in the example above corresponds to the 'denv_cls' field of 'DerivEnv'.
+--
+-- Similarly, the type variables that appear in a 'DerivInstTys' value are the
+-- same type variables as the 'denv_tvs' in the parent 'DerivEnv'. Accordingly,
+-- if we are inferring an instance context, the type variables will be 'TcTyVar'
+-- skolems. Otherwise, they will be ordinary 'TyVar's.
+-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer".
 data DerivInstTys = DerivInstTys
   { dit_cls_tys     :: [Type]
     -- ^ Other arguments to the class except the last
@@ -2771,6 +2778,26 @@ substDerivInstTys subst
     tc_args'     = substTys subst tc_args
     rep_tc_args' = substTys subst rep_tc_args
 
+-- | Zonk the 'TcTyVar's in a 'DerivInstTys' value to 'TyVar's.
+-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType".
+--
+-- This is only used in the final zonking step when inferring
+-- the context for a derived instance.
+-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer".
+zonkDerivInstTys :: ZonkEnv -> DerivInstTys -> TcM DerivInstTys
+zonkDerivInstTys ze dit@(DerivInstTys { dit_cls_tys = cls_tys
+                                      , dit_tc_args = tc_args
+                                      , dit_rep_tc = rep_tc
+                                      , dit_rep_tc_args = rep_tc_args }) = do
+  cls_tys'     <- zonkTcTypesToTypesX ze cls_tys
+  tc_args'     <- zonkTcTypesToTypesX ze tc_args
+  rep_tc_args' <- zonkTcTypesToTypesX ze rep_tc_args
+  pure dit{ dit_cls_tys         = cls_tys'
+          , dit_tc_args         = tc_args'
+          , dit_rep_tc_args     = rep_tc_args'
+          , dit_dc_inst_arg_env = buildDataConInstArgEnv rep_tc rep_tc_args'
+          }
+
 {-
 Note [Auxiliary binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index 3b2d3f80dd..94a00ce52b 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -21,7 +21,6 @@ import GHC.Types.Basic
 import GHC.Core.Class
 import GHC.Core.DataCon
 import GHC.Utils.Error
-import GHC.Tc.Utils.Instantiate
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
@@ -44,7 +43,7 @@ import GHC.Core.Type
 import GHC.Tc.Solver
 import GHC.Tc.Solver.Monad ( runTcS )
 import GHC.Tc.Validity (validDerivPred)
-import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints)
+import GHC.Tc.Utils.Unify (buildImplicationFor)
 import GHC.Builtin.Types (typeToTypeKind)
 import GHC.Core.Unify (tcUnifyTy)
 import GHC.Utils.Misc
@@ -60,7 +59,7 @@ import Data.Maybe
 ----------------------
 
 inferConstraints :: DerivSpecMechanism
-                 -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism)
+                 -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
 -- inferConstraints figures out the constraints needed for the
 -- instance declaration generated by a 'deriving' clause on a
 -- data type declaration. It also returns the new in-scope type
@@ -81,7 +80,7 @@ inferConstraints mechanism
                   , denv_cls      = main_cls
                   , denv_inst_tys = inst_tys } <- ask
        ; wildcard <- isStandaloneWildcardDeriv
-       ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism)
+       ; let infer_constraints :: DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
              infer_constraints =
                case mechanism of
                  DerivSpecStock{dsm_stock_dit = dit}
@@ -106,8 +105,8 @@ inferConstraints mechanism
              -- this rule is stock deriving. See
              -- Note [Inferring the instance context].
              infer_constraints_simple
-               :: DerivM [ThetaOrigin]
-               -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism)
+               :: DerivM ThetaSpec
+               -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
              infer_constraints_simple infer_thetas = do
                thetas <- infer_thetas
                pure (thetas, tvs, inst_tys, mechanism)
@@ -116,10 +115,10 @@ inferConstraints mechanism
              -- See Note [Superclasses of derived instance]
              cls_tvs  = classTyVars main_cls
              sc_constraints = assertPpr (equalLength cls_tvs inst_tys)
-                                        (ppr main_cls <+> ppr inst_tys)
-                              [ mkThetaOrigin (mkDerivOrigin wildcard)
-                                              TypeLevel [] [] [] $
-                                substTheta cls_subst (classSCTheta main_cls) ]
+                                        (ppr main_cls <+> ppr inst_tys) $
+                              mkDirectThetaSpec
+                                (mkDerivOrigin wildcard) TypeLevel
+                                (substTheta cls_subst (classSCTheta main_cls))
              cls_subst = assert (equalLength cls_tvs inst_tys) $
                          zipTvSubst cls_tvs inst_tys
 
@@ -138,7 +137,7 @@ inferConstraints mechanism
 --
 -- > data Foo = MkFoo Int Char deriving Show
 --
--- We would infer the following constraints ('ThetaOrigin's):
+-- We would infer the following constraints ('ThetaSpec's):
 --
 -- > (Show Int, Show Char)
 --
@@ -156,7 +155,7 @@ inferConstraints mechanism
 -- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@.
 -- See Note [Inferring the instance context].
 inferConstraintsStock :: DerivInstTys
-                      -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivInstTys)
+                      -> DerivM (ThetaSpec, [TyVar], [TcType], DerivInstTys)
 inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                                         , dit_tc          = tc
                                         , dit_tc_args     = tc_args
@@ -179,8 +178,8 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
            con_arg_constraints
              :: (CtOrigin -> TypeOrKind
                           -> Type
-                          -> [([PredOrigin], Maybe TCvSubst)])
-             -> ([ThetaOrigin], [TyVar], [TcType], DerivInstTys)
+                          -> [(ThetaSpec, Maybe TCvSubst)])
+             -> (ThetaSpec, [TyVar], [TcType], DerivInstTys)
            con_arg_constraints get_arg_constraints
              = let -- Constraints from the fields of each data constructor.
                    (predss, mbSubsts) = unzip
@@ -220,13 +219,14 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                    unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
                                              && not (v `isInScope` subst)) tvs
                    (subst', _)  = substTyVarBndrs subst unmapped_tvs
-                   stupid_theta_origin = mkThetaOrigin deriv_origin TypeLevel [] [] [] $
-                                         substTheta subst' stupid_theta
-                   preds'       = map (substPredOrigin subst') preds
+                   stupid_theta_origin = mkDirectThetaSpec
+                                           deriv_origin TypeLevel
+                                           (substTheta subst' stupid_theta)
+                   preds'       = map (substPredSpec subst') preds
                    inst_tys'    = substTys subst' inst_tys
                    dit'         = substDerivInstTys subst' dit
                    tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
-               in ( [stupid_theta_origin, mkThetaOriginFromPreds preds']
+               in ( stupid_theta_origin ++ preds'
                   , tvs', inst_tys', dit' )
 
            is_generic  = main_cls `hasKey` genClassKey
@@ -236,13 +236,13 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                           || is_generic1
 
            get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
-                                -> [([PredOrigin], Maybe TCvSubst)]
+                                -> [(ThetaSpec, Maybe TCvSubst)]
            get_gen1_constraints functor_cls orig t_or_k ty
               = mk_functor_like_constraints orig t_or_k functor_cls $
                 get_gen1_constrained_tys last_tv ty
 
            get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
-                                   -> [([PredOrigin], Maybe TCvSubst)]
+                                   -> [(ThetaSpec, Maybe TCvSubst)]
            get_std_constrained_tys orig t_or_k ty
                | is_functor_like
                = mk_functor_like_constraints orig t_or_k main_cls $
@@ -253,7 +253,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
 
            mk_functor_like_constraints :: CtOrigin -> TypeOrKind
                                        -> Class -> [Type]
-                                       -> [([PredOrigin], Maybe TCvSubst)]
+                                       -> [(ThetaSpec, Maybe TCvSubst)]
            -- 'cls' is usually main_cls (Functor or Traversable etc), but if
            -- main_cls = Generic1, then 'cls' can be Functor; see
            -- get_gen1_constraints
@@ -268,8 +268,12 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
            mk_functor_like_constraints orig t_or_k cls
               = map $ \ty -> let ki = tcTypeKind ty in
                              ( [ mk_cls_pred orig t_or_k cls ty
-                               , mkPredOrigin orig KindLevel
-                                   (mkPrimEqPred ki typeToTypeKind) ]
+                               , SimplePredSpec
+                                   { sps_pred = mkPrimEqPred ki typeToTypeKind
+                                   , sps_origin = orig
+                                   , sps_type_or_kind = KindLevel
+                                   }
+                               ]
                              , tcUnifyTy ki typeToTypeKind
                              )
 
@@ -284,9 +288,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
            -- Reason: when the IF holds, we generate a method
            --             dataCast2 f = gcast2 f
            --         and we need the Data constraints to typecheck the method
-           extra_constraints = [mkThetaOriginFromPreds constrs]
-             where
-               constrs
+           extra_constraints
                  | main_cls `hasKey` dataClassKey
                  , all (isLiftedTypeKind . tcTypeKind) rep_tc_args
                  = [ mk_cls_pred deriv_origin t_or_k main_cls ty
@@ -296,7 +298,11 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
 
            mk_cls_pred orig t_or_k cls ty
                 -- Don't forget to apply to cls_tys' too
-              = mkPredOrigin orig t_or_k (mkClassPred cls (cls_tys' ++ [ty]))
+              = SimplePredSpec
+                  { sps_pred = mkClassPred cls (cls_tys' ++ [ty])
+                  , sps_origin = orig
+                  , sps_type_or_kind = t_or_k
+                  }
            cls_tys' | is_generic1 = []
                       -- In the awkward Generic1 case, cls_tys' should be
                       -- empty, since we are applying the class Functor.
@@ -337,36 +343,32 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
 -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
 -- for an explanation of how these constraints are used to determine the
 -- derived instance context.
-inferConstraintsAnyclass :: DerivM [ThetaOrigin]
+inferConstraintsAnyclass :: DerivM ThetaSpec
 inferConstraintsAnyclass
-  = do { DerivEnv { denv_cls      = cls
-                  , denv_inst_tys = inst_tys } <- ask
-       ; wildcard <- isStandaloneWildcardDeriv
-
+  = do { DerivEnv { denv_cls       = cls
+                  , denv_inst_tys  = inst_tys } <- ask
        ; let gen_dms = [ (sel_id, dm_ty)
                        | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
+       ; wildcard <- isStandaloneWildcardDeriv
 
-             cls_tvs = classTyVars cls
-
-             do_one_meth :: (Id, Type) -> TcM ThetaOrigin
+       ; let meth_pred :: (Id, Type) -> PredSpec
                -- (Id,Type) are the selector Id and the generic default method type
                -- NB: the latter is /not/ quantified over the class variables
                -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
-             do_one_meth (sel_id, gen_dm_ty)
-               = do { let (sel_tvs, _cls_pred, meth_ty)
-                                   = tcSplitMethodTy (varType sel_id)
-                          meth_ty' = substTyWith sel_tvs inst_tys meth_ty
-                          (meth_tvs, meth_theta, meth_tau)
-                                   = tcSplitNestedSigmaTys meth_ty'
-
-                          gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
-                          (dm_tvs, dm_theta, dm_tau)
-                                     = tcSplitNestedSigmaTys gen_dm_ty'
-                          tau_eq     = mkPrimEqPred meth_tau dm_tau
-                    ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel
-                                meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
-
-       ; lift $ mapM do_one_meth gen_dms }
+             meth_pred (sel_id, gen_dm_ty)
+               = let (sel_tvs, _cls_pred, meth_ty) = tcSplitMethodTy (varType sel_id)
+                     meth_ty'   = substTyWith sel_tvs inst_tys meth_ty
+                     gen_dm_ty' = substTyWith sel_tvs inst_tys gen_dm_ty in
+                 -- This is the only place where a SubTypePredSpec is
+                 -- constructed instead of a SimplePredSpec. See
+                 -- Note [Gathering and simplifying constraints for DeriveAnyClass]
+                 -- for a more in-depth explanation.
+                 SubTypePredSpec { stps_ty_actual = gen_dm_ty'
+                                 , stps_ty_expected = meth_ty'
+                                 , stps_origin = mkDerivOrigin wildcard
+                                 }
+
+       ; pure $ map meth_pred gen_dms }
 
 -- Like 'inferConstraints', but used only for @GeneralizedNewtypeDeriving@ and
 -- @DerivingVia@. Since both strategies generate code involving 'coerce', the
@@ -375,11 +377,11 @@ inferConstraintsAnyclass
 --
 -- > newtype Age = MkAge Int deriving newtype Num
 --
--- We would infer the following constraints ('ThetaOrigin's):
+-- We would infer the following constraints ('ThetaSpec'):
 --
 -- > (Num Int, Coercible Age Int)
 inferConstraintsCoerceBased :: [Type] -> Type
-                            -> DerivM [ThetaOrigin]
+                            -> DerivM ThetaSpec
 inferConstraintsCoerceBased cls_tys rep_ty = do
   DerivEnv { denv_tvs      = tvs
            , denv_cls      = cls
@@ -391,7 +393,10 @@ inferConstraintsCoerceBased cls_tys rep_ty = do
       -- (for DerivingVia).
       rep_tys ty  = cls_tys ++ [ty]
       rep_pred ty = mkClassPred cls (rep_tys ty)
-      rep_pred_o ty = mkPredOrigin deriv_origin TypeLevel (rep_pred ty)
+      rep_pred_o ty = SimplePredSpec { sps_pred = rep_pred ty
+                                     , sps_origin = deriv_origin
+                                     , sps_type_or_kind = TypeLevel
+                                     }
               -- rep_pred is the representation dictionary, from where
               -- we are going to get all the methods for the final
               -- dictionary
@@ -401,23 +406,23 @@ inferConstraintsCoerceBased cls_tys rep_ty = do
       -- If there are no methods, we don't need any constraints
       -- Otherwise we need (C rep_ty), for the representation methods,
       -- and constraints to coerce each individual method
-      meth_preds :: Type -> [PredOrigin]
+      meth_preds :: Type -> ThetaSpec
       meth_preds ty
         | null meths = [] -- No methods => no constraints
                           -- (#12814)
         | otherwise = rep_pred_o ty : coercible_constraints ty
       meths = classMethods cls
       coercible_constraints ty
-        = [ mkPredOrigin (DerivOriginCoerce meth t1 t2 sa_wildcard)
-                         TypeLevel (mkReprPrimEqPred t1 t2)
+        = [ SimplePredSpec
+              { sps_pred = mkReprPrimEqPred t1 t2
+              , sps_origin = DerivOriginCoerce meth t1 t2 sa_wildcard
+              , sps_type_or_kind = TypeLevel
+              }
           | meth <- meths
           , let (Pair t1 t2) = mkCoerceClassMethEqn cls tvs
                                        inst_tys ty meth ]
 
-      all_thetas :: Type -> [ThetaOrigin]
-      all_thetas ty = [mkThetaOriginFromPreds $ meth_preds ty]
-
-  pure (all_thetas rep_ty)
+  pure (meth_preds rep_ty)
 
 {- Note [Inferring the instance context]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -631,7 +636,7 @@ See also Note [nonDetCmpType nondeterminism]
 -}
 
 
-simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
+simplifyInstanceContexts :: [DerivSpec ThetaSpec]
                          -> TcM [DerivSpec ThetaType]
 -- Used only for deriving clauses or standalone deriving with an
 -- extra-constraints wildcard (InferContext)
@@ -641,7 +646,10 @@ simplifyInstanceContexts [] = return []
 
 simplifyInstanceContexts infer_specs
   = do  { traceTc "simplifyInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
-        ; iterate_deriv 1 initial_solutions }
+        ; final_specs <- iterate_deriv 1 initial_solutions
+          -- After simplification finishes, zonk the TcTyVars as described
+          -- in Note [Overlap and deriving].
+        ; traverse zonkDerivSpec final_specs }
   where
     ------------------------------------------------------------------
         -- The initial solutions for the equations claim that each
@@ -682,12 +690,13 @@ simplifyInstanceContexts infer_specs
        -- See Note [Deterministic simplifyInstanceContexts]
     canSolution = map (sortBy nonDetCmpType)
     ------------------------------------------------------------------
-    gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
+    gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType
     gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
-                 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
+                 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs
+                 , ds_skol_info = skol_info, ds_user_ctxt = user_ctxt })
       = setSrcSpan loc  $
         addErrCtxt (derivInstCtxt the_pred) $
-        do { theta <- simplifyDeriv the_pred tyvars deriv_rhs
+        do { theta <- simplifyDeriv skol_info user_ctxt tyvars deriv_rhs
                 -- checkValidInstance tyvars theta clas inst_tys
                 -- Not necessary; see Note [Exotic derived instance contexts]
 
@@ -713,78 +722,27 @@ derivInstCtxt pred
 
 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
 -- as possible. Fail if not possible.
-simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
-                          -- deriving.  Only used for SkolemInfo.
-              -> [TyVar]  -- ^ The tyvars bound by @inst_ty@.
-              -> [ThetaOrigin] -- ^ Given and wanted constraints
+simplifyDeriv :: SkolemInfo -- ^ The 'SkolemInfo' used to skolemise the
+                            -- 'TcTyVar' arguments
+              -> UserTypeCtxt -- ^ Used to inform error messages as to whether
+                              -- we are in a @deriving@ clause or a standalone
+                              -- @deriving@ declaration
+              -> [TcTyVar]  -- ^ The tyvars bound by @inst_ty@.
+              -> ThetaSpec -- ^ The constraints to solve and simplify
               -> TcM ThetaType -- ^ Needed constraints (after simplification),
                                -- i.e. @['PredType']@.
-simplifyDeriv pred tvs thetas
-  = do { skol_info <- mkSkolemInfo (DerivSkol pred)
-       ; (skol_subst, tvs_skols) <- tcInstSkolTyVars skol_info tvs -- Skolemize
-                -- The constraint solving machinery
-                -- expects *TcTyVars* not TyVars.
-                -- We use *non-overlappable* (vanilla) skolems
-                -- See Note [Overlap and deriving]
-
-       ; let skol_set  = mkVarSet tvs_skols
-             doc = text "deriving" <+> parens (ppr pred)
-
-             mk_given_ev :: PredType -> TcM EvVar
-             mk_given_ev given =
-               let given_pred = substTy skol_subst given
-               in newEvVar given_pred
-
-             emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM ()
-             emit_wanted_constraints metas_to_be preds
-               = do { -- We instantiate metas_to_be with fresh meta type
-                      -- variables. Currently, these can only be type variables
-                      -- quantified in generic default type signatures.
-                      -- See Note [Gathering and simplifying constraints for
-                      -- DeriveAnyClass]
-                      (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be
-
-                    -- Now make a constraint for each of the instantiated predicates
-                    ; let wanted_subst = skol_subst `unionTCvSubst` meta_subst
-                          mk_wanted_ct (PredOrigin wanted orig t_or_k)
-                            = do { ev <- newWanted orig (Just t_or_k) $
-                                         substTyUnchecked wanted_subst wanted
-                                 ; return (mkNonCanonical ev) }
-                    ; cts <- mapM mk_wanted_ct preds
-
-                    -- And emit them into the monad
-                    ; emitSimples (listToCts cts) }
-
-             -- Create the implications we need to solve. For stock and newtype
-             -- deriving, these implication constraints will be simple class
-             -- constraints like (C a, Ord b).
-             -- But with DeriveAnyClass, we make an implication constraint.
-             -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
-             mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
-             mk_wanteds (ThetaOrigin { to_anyclass_skols  = ac_skols
-                                     , to_anyclass_metas  = ac_metas
-                                     , to_anyclass_givens = ac_givens
-                                     , to_wanted_origins  = preds })
-               = do { ac_given_evs <- mapM mk_given_ev ac_givens
-                    ; (_, wanteds)
-                        <- captureConstraints $
-                           checkConstraints (getSkolemInfo skol_info) ac_skols ac_given_evs $
-                              -- The checkConstraints bumps the TcLevel, and
-                              -- wraps the wanted constraints in an implication,
-                              -- when (but only when) necessary
-                           emit_wanted_constraints ac_metas preds
-                    ; pure wanteds }
+simplifyDeriv skol_info user_ctxt tvs theta
+  = do { let skol_set = mkVarSet tvs
 
        -- See [STEP DAC BUILD]
        -- Generate the implication constraints, one for each method, to solve
        -- with the skolemized variables.  Start "one level down" because
-       -- we are going to wrap the result in an implication with tvs_skols,
+       -- we are going to wrap the result in an implication with tvs,
        -- in step [DAC RESIDUAL]
-       ; (tc_lvl, wanteds) <- pushTcLevelM $
-                              mapM mk_wanteds thetas
+       ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt theta
 
        ; traceTc "simplifyDeriv inputs" $
-         vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
+         vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanteds, ppr skol_info ]
 
        -- See [STEP DAC SOLVE]
        -- Simplify the constraints, starting at the same level at which
@@ -792,8 +750,7 @@ simplifyDeriv pred tvs thetas
        -- simplifyInfer)
        ; (solved_wanteds, _) <- setTcLevel tc_lvl $
                                 runTcS            $
-                                solveWanteds      $
-                                unionsWC wanteds
+                                solveWanteds wanteds
 
        -- It's not yet zonked!  Obviously zonk it before peering at it
        ; solved_wanteds <- zonkWC solved_wanteds
@@ -817,7 +774,7 @@ simplifyDeriv pred tvs thetas
                where p = ctPred ct
 
        ; traceTc "simplifyDeriv outputs" $
-         vcat [ ppr tvs_skols, ppr residual_simple, ppr good ]
+         vcat [ ppr tvs, ppr residual_simple, ppr good ]
 
        -- Return the good unsolved constraints (unskolemizing on the way out.)
        ; let min_theta = mkMinimalBySCs id (bagToList good)
@@ -827,8 +784,6 @@ simplifyDeriv pred tvs thetas
              -- constraints.
              -- See Note [Gathering and simplifying constraints for
              --           DeriveAnyClass]
-             subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
-                          -- The reverse substitution (sigh)
 
        -- See [STEP DAC RESIDUAL]
        -- Ensure that min_theta is enough to solve /all/ the constraints in
@@ -837,7 +792,7 @@ simplifyDeriv pred tvs thetas
        --    forall tvs. min_theta => solved_wanteds
        ; min_theta_vars <- mapM newEvVar min_theta
        ; (leftover_implic, _)
-           <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) tvs_skols
+           <- buildImplicationFor tc_lvl (getSkolemInfo skol_info) tvs
                                   min_theta_vars solved_wanteds
        -- This call to simplifyTop is purely for error reporting
        -- See Note [Error reporting for deriving clauses]
@@ -845,7 +800,7 @@ simplifyDeriv pred tvs thetas
        -- in this line of code.
        ; simplifyTopImplic leftover_implic
 
-       ; return (substTheta subst_skol min_theta) }
+       ; return min_theta }
 
 {-
 Note [Overlap and deriving]
@@ -869,9 +824,20 @@ of a function
 and we want to infer
    f :: Show [a] => a -> String
 
-BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
-             the context for the derived instance.
-             Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+As a result, we use vanilla, non-overlappable skolems when inferring the
+context for the derived instances. Hence, we instantiate the type variables
+using tcInstSkolTyVars, not tcInstSuperSkolTyVars.
+
+We do this skolemisation in GHC.Tc.Deriv.mkEqnHelp, a function which occurs
+very early in the deriving pipeline, so that by the time GHC needs to infer the
+instance context, all of the types in the computed DerivSpec have been
+skolemised appropriately. After the instance context inference has completed,
+GHC zonks the TcTyVars in the DerivSpec to ensure that types like
+a[sk:1] do not appear in -ddump-deriv output.
+
+All of this is only needed when inferring an instance context, i.e., the
+InferContext case. For the SupplyContext case, we don't bother skolemising
+at all.
 
 Note [Gathering and simplifying constraints for DeriveAnyClass]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -902,7 +868,7 @@ definition for these generic default methods
   $gdm_bar x y = show x ++ show (range (y,y))
 
 (and similarly for baz).  Now consider a 'deriving' clause
-  data Maybe s = ... deriving Foo
+  data Maybe s = ... deriving anyclass Foo
 
 This derives an instance of the form:
   instance (CX) => Foo (Maybe s) where
@@ -911,14 +877,34 @@ This derives an instance of the form:
 
 Now it is GHC's job to fill in a suitable instance context (CX).  If
 GHC were typechecking the binding
-   bar = $gdm bar
+   bar = $gdm_bar
 it would
    * skolemise the expected type of bar
    * instantiate the type of $gdm_bar with meta-type variables
    * build an implication constraint
 
 [STEP DAC BUILD]
-So that's what we do.  We build the constraint (call it C1)
+So that's what we do. Fortunately, there is already functionality within GHC
+to that does all of the above—namely, tcSubTypeSigma. In the example above,
+we want to use tcSubTypeSigma to check the following subtyping relation:
+
+     forall c. (Show a, Ix c) => Maybe s -> c -> String -- actual type
+  <= forall b.         (Ix b) => Maybe s -> b -> String -- expected type
+
+That is, we check that the type of $gdm_bar (the actual type) is more
+polymorphic than the type of bar (the expected type). We use SubTypePredSpec,
+a special form of PredSpec that is only used by DeriveAnyClass, to store
+the actual and expected types.
+
+(Aside: having a separate SubTypePredSpec is not strictly necessary, as we
+could theoretically construct this implication constraint by hand and store it
+in a SimplePredSpec. In fact, GHC used to do this. However, this is easier
+said than done, and there were numerous subtle bugs that resulted from getting
+this step wrong, such as #20719. Ultimately, we decided that special-casing a
+PredSpec specifically for DeriveAnyClass was worth it.)
+
+tcSubTypeSigma will ultimately spit out an implication constraint, which will
+look something like this (call it C1):
 
    forall[2] b. Ix b => (Show (Maybe s), Ix cc,
                         Maybe s -> b -> String
@@ -929,14 +915,31 @@ Here:
   going to wrap it in a forall[1] in [STEP DAC RESIDUAL]
 
 * The 'b' comes from the quantified type variable in the expected type
-  of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
-  variable that comes from instantiating the quantified type variable 'c' in
-  $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
-
-* The (Ix b) constraint comes from the context of bar's type
-  (i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
-  constraints come from the context of $gdm_bar's type
-  (i.e., 'to_anyclass_givens' in 'ThetaOrigin').
+  of bar. The 'cc' is a unification variable that comes from instantiating the
+  quantified type variable 'c' in $gdm_bar's type. The finer details of
+  skolemisation and metavariable instantiation are handled behind the scenes
+  by tcSubTypeSigma.
+
+* It is important that `b` be distinct from `cc`. In this example, this is
+  clearly the case, but it is not always so obvious when the type variables are
+  hidden behind type synonyms. Suppose the example were written like this,
+  for example:
+
+    type Method a = forall b. Ix b => a -> b -> String
+    class Foo a where
+      bar :: Method a
+      default bar :: Show a => Method a
+      bar = ...
+
+  Both method signatures quantify a `b` once the `Method` type synonym is
+  expanded. To ensure that GHC doesn't confuse the two `b`s during
+  typechecking, tcSubTypeSigma instantiates the `b` in the original signature
+  with a fresh skolem and the `b` in the default signature with a fresh
+  unification variable. Doing so prevents #20719 from happening.
+
+* The (Ix b) constraint comes from the context of bar's type. The
+  (Show (Maybe s)) and (Ix cc) constraints come from the context of $gdm_bar's
+  type.
 
 * The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
   comes from marrying up the instantiated type of $gdm_bar with the specified
@@ -948,7 +951,7 @@ unification variable for each iteration of simplifyDeriv. If we re-use the same
 unification variable across multiple iterations, then bad things can happen,
 such as #14933.
 
-Similarly for 'baz', giving the constraint C2
+Similarly for 'baz', tcSubTypeSigma gives the constraint C2
 
    forall[2]. Eq (Maybe s) => (Ord a, Show a,
                               Maybe s -> Maybe s -> Bool
diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs
index d25db38be0..aa89f94c4b 100644
--- a/compiler/GHC/Tc/Deriv/Utils.hs
+++ b/compiler/GHC/Tc/Deriv/Utils.hs
@@ -10,13 +10,15 @@
 -- | Error-checking and other utilities for @deriving@ clauses or declarations.
 module GHC.Tc.Deriv.Utils (
         DerivM, DerivEnv(..),
-        DerivSpec(..), pprDerivSpec, setDerivSpecTheta,
+        DerivSpec(..), pprDerivSpec, setDerivSpecTheta, zonkDerivSpec,
         DerivSpecMechanism(..), derivSpecMechanismToStrategy, isDerivSpecStock,
-        isDerivSpecNewtype, isDerivSpecAnyClass, isDerivSpecVia,
+        isDerivSpecNewtype, isDerivSpecAnyClass,
+        isDerivSpecVia, zonkDerivSpecMechanism,
         DerivContext(..), OriginativeDerivStatus(..), StockGenFns(..),
-        isStandaloneDeriv, isStandaloneWildcardDeriv, mkDerivOrigin,
-        PredOrigin(..), ThetaOrigin(..), mkPredOrigin,
-        mkThetaOrigin, mkThetaOriginFromPreds, substPredOrigin,
+        isStandaloneDeriv, isStandaloneWildcardDeriv,
+        askDerivUserTypeCtxt, mkDerivOrigin,
+        PredSpec(..), ThetaSpec,
+        mkDirectThetaSpec, substPredSpec, captureThetaSpecConstraints,
         checkOriginativeSideConditions, hasStockDeriving,
         std_class_via_coercible, non_coercible_class,
         newDerivClsInst, extendLocalInstEnv
@@ -47,9 +49,12 @@ import GHC.Tc.Deriv.Generate
 import GHC.Tc.Deriv.Functor
 import GHC.Tc.Deriv.Generics
 import GHC.Tc.Errors.Types
+import GHC.Tc.Types.Constraint (WantedConstraints, mkNonCanonical)
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Unify (tcSubTypeSigma)
+import GHC.Tc.Utils.Zonk
 import GHC.Builtin.Names.TH (liftClassKey)
 import GHC.Core.TyCon
 import GHC.Core.Type
@@ -57,6 +62,7 @@ import GHC.Utils.Misc
 import GHC.Types.Var.Set
 
 import Control.Monad.Trans.Reader
+import Data.Foldable (traverse_)
 import Data.Maybe
 import qualified GHC.LanguageExtensions as LangExt
 import GHC.Data.List.SetOps (assocMaybe)
@@ -84,6 +90,16 @@ isStandaloneWildcardDeriv = asks (go . denv_ctxt)
     go (InferContext wildcard) = isJust wildcard
     go (SupplyContext {})      = False
 
+-- | Return 'InstDeclCtxt' if processing with a standalone @deriving@
+-- declaration or 'DerivClauseCtxt' if processing a @deriving@ clause.
+askDerivUserTypeCtxt :: DerivM UserTypeCtxt
+askDerivUserTypeCtxt = asks (go . denv_ctxt)
+  where
+    go :: DerivContext -> UserTypeCtxt
+    go (SupplyContext {})     = InstDeclCtxt True
+    go (InferContext Just{})  = InstDeclCtxt True
+    go (InferContext Nothing) = DerivClauseCtxt
+
 -- | @'mkDerivOrigin' wc@ returns 'StandAloneDerivOrigin' if @wc@ is 'True',
 -- and 'DerivClauseOrigin' if @wc@ is 'False'. Useful for error-reporting.
 mkDerivOrigin :: Bool -> CtOrigin
@@ -98,7 +114,13 @@ data DerivEnv = DerivEnv
   { denv_overlap_mode :: Maybe OverlapMode
     -- ^ Is this an overlapping instance?
   , denv_tvs          :: [TyVar]
-    -- ^ Universally quantified type variables in the instance
+    -- ^ Universally quantified type variables in the instance. If the
+    --   @denv_ctxt@ is 'InferContext', these will be 'TcTyVar' skolems.
+    --   If the @denv_ctxt@ is 'SupplyContext', these will be ordinary 'TyVar's.
+    --   See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer".
+    --
+    --   All type variables that appear in the 'denv_inst_tys', 'denv_ctxt',
+    --   'denv_skol_info', and 'denv_strat' should come from 'denv_tvs'.
   , denv_cls          :: Class
     -- ^ Class for which we need to derive an instance
   , denv_inst_tys     :: [Type]
@@ -109,6 +131,9 @@ data DerivEnv = DerivEnv
     --   'InferContext' for @deriving@ clauses, or for standalone deriving that
     --   uses a wildcard constraint.
     --   See @Note [Inferring the instance context]@.
+  , denv_skol_info    :: SkolemInfo
+    -- ^ The 'SkolemInfo' used to skolemise the @denv_tvs@ in the case where
+    --   the 'denv_ctxt' is 'InferContext'.
   , denv_strat        :: Maybe (DerivStrategy GhcTc)
     -- ^ 'Just' if user requests a particular deriving strategy.
     --   Otherwise, 'Nothing'.
@@ -120,6 +145,7 @@ instance Outputable DerivEnv where
                 , denv_cls          = cls
                 , denv_inst_tys     = inst_tys
                 , denv_ctxt         = ctxt
+                , denv_skol_info    = skol_info
                 , denv_strat        = mb_strat })
     = hang (text "DerivEnv")
          2 (vcat [ text "denv_overlap_mode" <+> ppr overlap_mode
@@ -127,6 +153,7 @@ instance Outputable DerivEnv where
                  , text "denv_cls"          <+> ppr cls
                  , text "denv_inst_tys"     <+> ppr inst_tys
                  , text "denv_ctxt"         <+> ppr ctxt
+                 , text "denv_skol_info"    <+> ppr skol_info
                  , text "denv_strat"        <+> ppr mb_strat ])
 
 data DerivSpec theta = DS { ds_loc                 :: SrcSpan
@@ -135,6 +162,8 @@ data DerivSpec theta = DS { ds_loc                 :: SrcSpan
                           , ds_theta               :: theta
                           , ds_cls                 :: Class
                           , ds_tys                 :: [Type]
+                          , ds_skol_info           :: SkolemInfo
+                          , ds_user_ctxt           :: UserTypeCtxt
                           , ds_overlap             :: Maybe OverlapMode
                           , ds_standalone_wildcard :: Maybe SrcSpan
                               -- See Note [Inferring the instance context]
@@ -143,11 +172,20 @@ data DerivSpec theta = DS { ds_loc                 :: SrcSpan
         -- This spec implies a dfun declaration of the form
         --       df :: forall tvs. theta => C tys
         -- The Name is the name for the DFun we'll build
-        -- The tyvars bind all the variables in the theta
+        -- The tyvars bind all the variables in the rest of the DerivSpec.
+        -- If we are inferring an instance context, the tyvars will be TcTyVar
+        -- skolems. After the instance context inference is over, the tyvars
+        -- will be zonked to TyVars. See
+        -- Note [Overlap and deriving] in GHC.Tc.Deriv.Infer.
 
         -- the theta is either the given and final theta, in standalone deriving,
         -- or the not-yet-simplified list of constraints together with their origin
 
+        -- The ds_skol_info is the SkolemInfo that was used to skolemise the
+        -- TcTyVars (if we are inferring an instance context). The ds_user_ctxt
+        -- is the UserTypeCtxt that allows error messages to know if we are in
+        -- a deriving clause or a standalone deriving declaration.
+
         -- ds_mechanism specifies the means by which GHC derives the instance.
         -- See Note [Deriving strategies] in GHC.Tc.Deriv
 
@@ -165,7 +203,7 @@ Example:
 
 pprDerivSpec :: Outputable theta => DerivSpec theta -> SDoc
 pprDerivSpec (DS { ds_loc = l, ds_name = n, ds_tvs = tvs, ds_cls = c,
-                   ds_tys = tys, ds_theta = rhs,
+                   ds_tys = tys, ds_theta = rhs, ds_skol_info = skol_info,
                    ds_standalone_wildcard = wildcard, ds_mechanism = mech })
   = hang (text "DerivSpec")
        2 (vcat [ text "ds_loc                  =" <+> ppr l
@@ -174,6 +212,7 @@ pprDerivSpec (DS { ds_loc = l, ds_name = n, ds_tvs = tvs, ds_cls = c,
                , text "ds_cls                  =" <+> ppr c
                , text "ds_tys                  =" <+> ppr tys
                , text "ds_theta                =" <+> ppr rhs
+               , text "ds_skol_info            =" <+> ppr skol_info
                , text "ds_standalone_wildcard  =" <+> ppr wildcard
                , text "ds_mechanism            =" <+> ppr mech ])
 
@@ -184,6 +223,24 @@ instance Outputable theta => Outputable (DerivSpec theta) where
 setDerivSpecTheta :: theta' -> DerivSpec theta -> DerivSpec theta'
 setDerivSpecTheta theta ds = ds{ds_theta = theta}
 
+-- | Zonk the 'TcTyVar's in a 'DerivSpec' to 'TyVar's.
+-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType".
+--
+-- This is only used in the final zonking step when inferring
+-- the context for a derived instance.
+-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer".
+zonkDerivSpec :: DerivSpec ThetaType -> TcM (DerivSpec ThetaType)
+zonkDerivSpec ds@(DS { ds_tvs = tvs, ds_theta = theta
+                     , ds_tys = tys, ds_mechanism = mechanism
+                     }) = do
+  (ze, tvs') <- zonkTyBndrs tvs
+  theta'     <- zonkTcTypesToTypesX ze theta
+  tys'       <- zonkTcTypesToTypesX ze tys
+  mechanism' <- zonkDerivSpecMechanism ze mechanism
+  pure ds{ ds_tvs = tvs', ds_theta = theta'
+         , ds_tys = tys', ds_mechanism = mechanism'
+         }
+
 -- | What action to take in order to derive a class instance.
 -- See @Note [DerivEnv and DerivSpecMechanism]@, as well as
 -- @Note [Deriving strategies]@ in "GHC.Tc.Deriv".
@@ -243,6 +300,44 @@ isDerivSpecAnyClass _                 = False
 isDerivSpecVia (DerivSpecVia{}) = True
 isDerivSpecVia _                = False
 
+-- | Zonk the 'TcTyVar's in a 'DerivSpecMechanism' to 'TyVar's.
+-- See @Note [What is zonking?]@ in "GHC.Tc.Utils.TcMType".
+--
+-- This is only used in the final zonking step when inferring
+-- the context for a derived instance.
+-- See @Note [Overlap and deriving]@ in "GHC.Tc.Deriv.Infer".
+zonkDerivSpecMechanism :: ZonkEnv -> DerivSpecMechanism -> TcM DerivSpecMechanism
+zonkDerivSpecMechanism ze mechanism =
+  case mechanism of
+    DerivSpecStock { dsm_stock_dit     = dit
+                   , dsm_stock_gen_fns = gen_fns
+                   } -> do
+      dit' <- zonkDerivInstTys ze dit
+      pure $ DerivSpecStock { dsm_stock_dit     = dit'
+                            , dsm_stock_gen_fns = gen_fns
+                            }
+    DerivSpecNewtype { dsm_newtype_dit    = dit
+                     , dsm_newtype_rep_ty = rep_ty
+                     } -> do
+      dit'    <- zonkDerivInstTys ze dit
+      rep_ty' <- zonkTcTypeToTypeX ze rep_ty
+      pure $ DerivSpecNewtype { dsm_newtype_dit    = dit'
+                              , dsm_newtype_rep_ty = rep_ty'
+                              }
+    DerivSpecAnyClass ->
+      pure DerivSpecAnyClass
+    DerivSpecVia { dsm_via_cls_tys = cls_tys
+                 , dsm_via_inst_ty = inst_ty
+                 , dsm_via_ty      = via_ty
+                 } -> do
+      cls_tys' <- zonkTcTypesToTypesX ze cls_tys
+      inst_ty' <- zonkTcTypeToTypeX ze inst_ty
+      via_ty'  <- zonkTcTypeToTypeX ze via_ty
+      pure $ DerivSpecVia { dsm_via_cls_tys = cls_tys'
+                          , dsm_via_inst_ty = inst_ty'
+                          , dsm_via_ty      = via_ty'
+                          }
+
 instance Outputable DerivSpecMechanism where
   ppr (DerivSpecStock{dsm_stock_dit = dit})
     = hang (text "DerivSpecStock")
@@ -446,34 +541,43 @@ data StockGenFns = StockGenFns
 -- otherwise knows how to generate code for (possibly requiring the use of a
 -- language extension), such as Eq, Ord, Ix, Data, Generic, etc.)
 
--- | A 'PredType' annotated with the origin of the constraint 'CtOrigin',
--- and whether or the constraint deals in types or kinds.
-data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind
+-- | A 'PredSpec' specifies a constraint to emitted when inferring the
+-- instance context for a derived instance in 'GHC.Tc.Deriv.simplifyInfer'.
+data PredSpec
+  = -- | An ordinary 'PredSpec' that directly stores a 'PredType', which
+    -- will be emitted as a wanted constraint in the constraint solving
+    -- machinery. This is the simple case, as there are no skolems,
+    -- metavariables, or given constraints involved.
+    SimplePredSpec
+      { sps_pred :: TcPredType
+        -- ^ The constraint to emit as a wanted
+      , sps_origin :: CtOrigin
+        -- ^ The origin of the constraint
+      , sps_type_or_kind :: TypeOrKind
+        -- ^ Whether the constraint is a type or kind
+      }
+  | -- | A special 'PredSpec' that is only used by @DeriveAnyClass@. This
+    -- will check if @stps_ty_actual@ is a subtype of (i.e., more polymorphic
+    -- than) @stps_ty_expected@ in the constraint solving machinery, emitting an
+    -- implication constraint as a side effect. For more details on how this
+    -- works, see @Note [Gathering and simplifying constraints for DeriveAnyClass]@
+    -- in "GHC.Tc.Deriv.Infer".
+    SubTypePredSpec
+      { stps_ty_actual :: TcSigmaType
+        -- ^ The actual type. In the context of @DeriveAnyClass@, this is the
+        -- default method type signature.
+      , stps_ty_expected :: TcSigmaType
+        -- ^ The expected type. In the context of @DeriveAnyClass@, this is the
+        -- original method type signature.
+      , stps_origin :: CtOrigin
+        -- ^ The origin of the constraint
+      }
 
--- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') to
--- simplify when inferring a derived instance's context. These are used in all
--- deriving strategies, but in the particular case of @DeriveAnyClass@, we
--- need extra information. In particular, we need:
---
--- * 'to_anyclass_skols', the list of type variables bound by a class method's
---   regular type signature, which should be rigid.
---
--- * 'to_anyclass_metas', the list of type variables bound by a class method's
---   default type signature. These can be unified as necessary.
---
--- * 'to_anyclass_givens', the list of constraints from a class method's
---   regular type signature, which can be used to help solve constraints
---   in the 'to_wanted_origins'.
---
--- (Note that 'to_wanted_origins' will likely contain type variables from the
--- derived type class or data type, neither of which will appear in
--- 'to_anyclass_skols' or 'to_anyclass_metas'.)
---
--- For all other deriving strategies, it is always the case that
--- 'to_anyclass_skols', 'to_anyclass_metas', and 'to_anyclass_givens' are
--- empty.
---
--- Here is an example to illustrate this:
+-- | A list of 'PredSpec' constraints to simplify when inferring a
+-- derived instance's context. For the @stock@, @newtype@, and @via@ deriving
+-- strategies, these will consist of 'SimplePredSpec's, and for
+-- @DeriveAnyClass@, these will consist of 'SubTypePredSpec's. Here is an
+-- example to illustrate the latter:
 --
 -- @
 -- class Foo a where
@@ -488,75 +592,119 @@ data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind
 -- data Quux q = Quux deriving anyclass Foo
 -- @
 --
--- Then it would generate two 'ThetaOrigin's, one for each method:
+-- Then it would generate two 'SubTypePredSpec's, one for each method:
 --
 -- @
--- [ ThetaOrigin { to_anyclass_skols  = [b]
---               , to_anyclass_metas  = [y]
---               , to_anyclass_givens = [Ix b]
---               , to_wanted_origins  = [ Show (Quux q), Ix y
---                                      , (Quux q -> b -> String) ~
---                                        (Quux q -> y -> String)
---                                      ] }
--- , ThetaOrigin { to_anyclass_skols  = []
---               , to_anyclass_metas  = []
---               , to_anyclass_givens = [Eq (Quux q)]
---               , to_wanted_origins  = [ Ord (Quux q)
---                                      , (Quux q -> Quux q -> Bool) ~
---                                        (Quux q -> Quux q -> Bool)
---                                      ] }
+-- [ SubTypePredSpec
+--     { stps_ty_actual   = forall y. (Show (Quux q), Ix y) => Quux q -> y -> String
+--     , stps_ty_expected = forall b.                (Ix b) => Quux q -> b -> String
+--     , stps_ty_origin   = DerivClauseCtxt
+--     }
+-- , SubTypePredSpec
+--     { stps_ty_actual   = Ord (Quux q) => Quux q -> Quux q -> Bool
+--     , stps_ty_expected = Eq  (Quux q) => Quux q -> Quux q -> Bool
+--     , stps_ty_origin   = DerivClauseCtxt
+--     }
 -- ]
 -- @
 --
 -- (Note that the type variable @q@ is bound by the data type @Quux@, and thus
--- it appears in neither 'to_anyclass_skols' nor 'to_anyclass_metas'.)
+-- appears free in the 'stps_ty_actual's and 'stps_ty_expected's.)
 --
 -- See @Note [Gathering and simplifying constraints for DeriveAnyClass]@
--- in "GHC.Tc.Deriv.Infer" for an explanation of how 'to_wanted_origins' are
--- determined in @DeriveAnyClass@, as well as how 'to_anyclass_skols',
--- 'to_anyclass_metas', and 'to_anyclass_givens' are used.
-data ThetaOrigin
-  = ThetaOrigin { to_anyclass_skols  :: [TyVar]
-                , to_anyclass_metas  :: [TyVar]
-                , to_anyclass_givens :: ThetaType
-                , to_wanted_origins  :: [PredOrigin] }
-
-instance Outputable PredOrigin where
-  ppr (PredOrigin ty _ _) = ppr ty -- The origin is not so interesting when debugging
-
-instance Outputable ThetaOrigin where
-  ppr (ThetaOrigin { to_anyclass_skols  = ac_skols
-                   , to_anyclass_metas  = ac_metas
-                   , to_anyclass_givens = ac_givens
-                   , to_wanted_origins  = wanted_origins })
-    = hang (text "ThetaOrigin")
-         2 (vcat [ text "to_anyclass_skols  =" <+> ppr ac_skols
-                 , text "to_anyclass_metas  =" <+> ppr ac_metas
-                 , text "to_anyclass_givens =" <+> ppr ac_givens
-                 , text "to_wanted_origins  =" <+> ppr wanted_origins ])
-
-mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin
-mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k
-
-mkThetaOrigin :: CtOrigin -> TypeOrKind
-              -> [TyVar] -> [TyVar] -> ThetaType -> ThetaType
-              -> ThetaOrigin
-mkThetaOrigin origin t_or_k skols metas givens wanteds
-  = ThetaOrigin { to_anyclass_skols  = skols
-                , to_anyclass_metas  = metas
-                , to_anyclass_givens = givens
-                , to_wanted_origins  = map (mkPredOrigin origin t_or_k) wanteds }
-
--- A common case where the ThetaOrigin only contains wanted constraints, with
--- no givens or locally scoped type variables.
-mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin
-mkThetaOriginFromPreds origins
-  = ThetaOrigin { to_anyclass_skols = [], to_anyclass_metas = []
-                , to_anyclass_givens = [], to_wanted_origins = origins }
-
-substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
-substPredOrigin subst (PredOrigin pred origin t_or_k)
-  = PredOrigin (substTy subst pred) origin t_or_k
+-- in "GHC.Tc.Deriv.Infer" for an explanation of how these 'SubTypePredSpec's
+-- are used to compute implication constraints.
+type ThetaSpec = [PredSpec]
+
+instance Outputable PredSpec where
+  ppr (SimplePredSpec{sps_pred = ty}) =
+    hang (text "SimplePredSpec")
+       2 (vcat [ text "sps_pred" <+> ppr ty ])
+  ppr (SubTypePredSpec { stps_ty_actual = ty_actual
+                       , stps_ty_expected = ty_expected }) =
+    hang (text "SubTypePredSpec")
+       2 (vcat [ text "stps_ty_actual"   <+> ppr ty_actual
+               , text "stps_ty_expected" <+> ppr ty_expected
+               ])
+
+-- | Build a list of 'SimplePredSpec's, using the supplied 'CtOrigin' and
+-- 'TypeOrKind' values for each 'PredType'.
+mkDirectThetaSpec :: CtOrigin -> TypeOrKind -> ThetaType -> ThetaSpec
+mkDirectThetaSpec origin t_or_k =
+  map (\p -> SimplePredSpec
+               { sps_pred = p
+               , sps_origin = origin
+               , sps_type_or_kind = t_or_k
+               })
+
+substPredSpec :: HasCallStack => TCvSubst -> PredSpec -> PredSpec
+substPredSpec subst ps =
+  case ps of
+    SimplePredSpec { sps_pred = pred
+                   , sps_origin = origin
+                   , sps_type_or_kind = t_or_k
+                   }
+      -> SimplePredSpec { sps_pred = substTy subst pred
+                        , sps_origin = origin
+                        , sps_type_or_kind = t_or_k
+                        }
+
+    SubTypePredSpec { stps_ty_actual = ty_actual
+                    , stps_ty_expected = ty_expected
+                    , stps_origin = origin
+                    }
+      -> SubTypePredSpec { stps_ty_actual = substTy subst ty_actual
+                         , stps_ty_expected = substTy subst ty_expected
+                         , stps_origin = origin
+                         }
+
+-- | Capture wanted constraints from a 'ThetaSpec'.
+captureThetaSpecConstraints ::
+     UserTypeCtxt -- ^ Used to inform error messages as to whether
+                  -- we are in a @deriving@ clause or a standalone
+                  -- @deriving@ declaration
+  -> ThetaSpec    -- ^ The specs from which constraints will be created
+  -> TcM (TcLevel, WantedConstraints)
+captureThetaSpecConstraints user_ctxt theta =
+  pushTcLevelM $ mk_wanteds theta
+  where
+    -- Create the constraints we need to solve. For stock and newtype
+    -- deriving, these constraints will be simple wanted constraints
+    -- like (C a, Ord b).
+    -- But with DeriveAnyClass, we make an implication constraint.
+    -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
+    -- in GHC.Tc.Deriv.Infer.
+    mk_wanteds :: ThetaSpec -> TcM WantedConstraints
+    mk_wanteds preds
+      = do { (_, wanteds) <- captureConstraints $
+                             traverse_ emit_constraints preds
+           ; pure wanteds }
+
+    -- Emit the appropriate constraints depending on what sort of
+    -- PredSpec we are dealing with.
+    emit_constraints :: PredSpec -> TcM ()
+    emit_constraints ps =
+      case ps of
+        -- For constraints like (C a, Ord b), emit the
+        -- constraints directly as simple wanted constraints.
+        SimplePredSpec { sps_pred = wanted
+                       , sps_origin = orig
+                       , sps_type_or_kind = t_or_k
+                       } -> do
+          ev <- newWanted orig (Just t_or_k) wanted
+          emitSimple (mkNonCanonical ev)
+
+        -- For DeriveAnyClass, check if ty_actual is a subtype of
+        -- ty_expected, which emits an implication constraint as a
+        -- side effect. See
+        -- Note [Gathering and simplifying constraints for DeriveAnyClass].
+        -- in GHC.Tc.Deriv.Infer.
+        SubTypePredSpec { stps_ty_actual   = ty_actual
+                        , stps_ty_expected = ty_expected
+                        , stps_origin      = orig
+                        } -> do
+          _ <- tcSubTypeSigma orig user_ctxt ty_actual ty_expected
+          return ()
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 2db40c7f7c..f5a1c6ab17 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -121,7 +121,6 @@ import GHC.Data.Bag
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Utils.Constants (debugIsOn)
-import GHC.Utils.Trace
 
 import Data.Coerce
 import Data.Monoid ( Endo(..) )
@@ -1539,9 +1538,7 @@ check_implic implic@(Implic { ic_tclvl = lvl
 
     check :: TcTyVar -> Maybe SDoc
     check tv | not (isTcTyVar tv)
-             = pprTrace "checkImplicationInvariants: not TcTyVar" (ppr tv) Nothing
-               -- Happens in 'deriving' code so I am punting for now
-               -- Just (ppr tv <+> text "is not a TcTyVar")
+             = Just (ppr tv <+> text "is not a TcTyVar")
              | otherwise
              = check_details tv (tcTyVarDetails tv)
 
diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr
index 6db596396d..655fb282a7 100644
--- a/testsuite/tests/deriving/should_compile/T14578.stderr
+++ b/testsuite/tests/deriving/should_compile/T14578.stderr
@@ -9,18 +9,19 @@ Derived class instances:
     GHC.Base.sconcat ::
       GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes ::
-      forall (b :: *).
-      GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
+      forall (b :: *). GHC.Real.Integral b =>
+                       b -> T14578.Wat f g a -> T14578.Wat f g a
     (GHC.Base.<>)
       = GHC.Prim.coerce
           @(T14578.App (Data.Functor.Compose.Compose f g) a
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
           ((GHC.Base.<>) @(T14578.App (Data.Functor.Compose.Compose f g) a))
     GHC.Base.sconcat
       = GHC.Prim.coerce
-          @(GHC.Base.NonEmpty (T14578.App (Data.Functor.Compose.Compose f g) a)
+          @(GHC.Base.NonEmpty
+              (T14578.App (Data.Functor.Compose.Compose f g) a)
             -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
           (GHC.Base.sconcat
@@ -29,7 +30,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(b
             -> T14578.App (Data.Functor.Compose.Compose f g) a
-               -> T14578.App (Data.Functor.Compose.Compose f g) a)
+            -> T14578.App (Data.Functor.Compose.Compose f g) a)
           @(b -> T14578.Wat f g a -> T14578.Wat f g a)
           (GHC.Base.stimes
              @(T14578.App (Data.Functor.Compose.Compose f g) a))
@@ -37,8 +38,8 @@ Derived class instances:
   instance GHC.Base.Functor f =>
            GHC.Base.Functor (T14578.App f) where
     GHC.Base.fmap ::
-      forall (a :: *) (b :: *).
-      (a -> b) -> T14578.App f a -> T14578.App f b
+      forall (a :: *) (b :: *). (a -> b)
+                                -> T14578.App f a -> T14578.App f b
     (GHC.Base.<$) ::
       forall (a :: *) (b :: *). a -> T14578.App f b -> T14578.App f a
     GHC.Base.fmap
@@ -54,17 +55,17 @@ Derived class instances:
            GHC.Base.Applicative (T14578.App f) where
     GHC.Base.pure :: forall (a :: *). a -> T14578.App f a
     (GHC.Base.<*>) ::
-      forall (a :: *) (b :: *).
-      T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b
+      forall (a :: *) (b :: *). T14578.App f (a -> b)
+                                -> T14578.App f a -> T14578.App f b
     GHC.Base.liftA2 ::
-      forall (a :: *) (b :: *) (c :: *).
-      (a -> b -> c) -> T14578.App f a -> T14578.App f b -> T14578.App f c
+      forall (a :: *) (b :: *) (c :: *). (a -> b -> c)
+                                         -> T14578.App f a -> T14578.App f b -> T14578.App f c
     (GHC.Base.*>) ::
-      forall (a :: *) (b :: *).
-      T14578.App f a -> T14578.App f b -> T14578.App f b
+      forall (a :: *) (b :: *). T14578.App f a
+                                -> T14578.App f b -> T14578.App f b
     (GHC.Base.<*) ::
-      forall (a :: *) (b :: *).
-      T14578.App f a -> T14578.App f b -> T14578.App f a
+      forall (a :: *) (b :: *). T14578.App f a
+                                -> T14578.App f b -> T14578.App f a
     GHC.Base.pure
       = GHC.Prim.coerce
           @(a -> f a) @(a -> T14578.App f a) (GHC.Base.pure @f)
diff --git a/testsuite/tests/deriving/should_compile/T20719.hs b/testsuite/tests/deriving/should_compile/T20719.hs
new file mode 100644
index 0000000000..c2c4a4f282
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T20719.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE DerivingStrategies, DeriveAnyClass, DefaultSignatures #-}
+
+module T20719 where
+
+import Data.Proxy
+
+type Method a = forall b . Eq b => Proxy (a, b)
+
+class Class a where
+  method1         :: Method a
+  default method1 :: Method a
+  method1 = Proxy
+
+  method2         :: Method a
+  default method2 :: forall b . Eq b => Proxy (a, b)
+  method2 = Proxy
+
+  method3         :: forall b . Eq b => Proxy (a, b)
+  default method3 :: Method a
+  method3 = Proxy
+
+  method4         :: forall b . Eq b => Proxy (a, b)
+  default method4 :: forall b . Eq b => Proxy (a, b)
+  method4 = Proxy
+
+data Data
+  deriving anyclass Class
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 05f9e87dcb..c5edb5275f 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -137,4 +137,5 @@ test('T20496', multiline_grep_errmsg(r"rnd\n( .*\n)*"), compile, ['-ddump-tc-tra
 test('T20375', normal, compile, [''])
 test('T20387', normal, compile, [''])
 test('T20501', normal, compile, [''])
+test('T20719', normal, compile, [''])
 test('T20994', normal, compile, [''])