Refactor DeriveAnyClass's instance context inference

Summary:
Currently, `DeriveAnyClass` has two glaring flaws:

* It only works on classes whose argument is of kind `*` or `* -> *` (#9821).
* The way it infers constraints makes no sense. It basically co-opts the
  algorithms used to infer contexts for `Eq` (for `*`-kinded arguments) or
  `Functor` (for `(* -> *)`-kinded arguments). This tends to produce overly
  constrained instances, which in extreme cases can lead to legitimate things
  failing to typecheck (#12594). Or even worse, it can trigger GHC panics
  (#12144 and #12423).

This completely reworks the way `DeriveAnyClass` infers constraints to fix
these two issues. It now uses the type signatures of the derived class's
methods to infer constraints (and to simplify them). A high-level description
of how this works is included in the GHC users' guide, and more technical notes
on what is going on can be found as comments (and a Note) in `TcDerivInfer`.

Fixes #9821, #12144, #12423, #12594.

Test Plan: ./validate

Reviewers: dfeuer, goldfire, simonpj, austin, bgamari

Subscribers: dfeuer, thomie

Differential Revision: https://phabricator.haskell.org/D2961

21 files changed, 579 insertions, 191 deletions

diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index a6ddb81d80..00869c4f4b 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -80,12 +80,12 @@ Overall plan
 3.  Add the derived bindings, generating InstInfos
 -}
 
-data EarlyDerivSpec = InferTheta (DerivSpec ThetaOrigin)
+data EarlyDerivSpec = InferTheta (DerivSpec [ThetaOrigin])
                     | GivenTheta (DerivSpec ThetaType)
         -- InferTheta ds => the context for the instance should be inferred
-        --      In this case ds_theta is the list of all the constraints
-        --      needed, such as (Eq [a], Eq a), together with a suitable CtLoc
-        --      to get good error messages.
+        --      In this case ds_theta is the list of all the sets of
+        --      constraints needed, such as (Eq [a], Eq a), together with a
+        --      suitable CtLoc to get good error messages.
         --      The inference process is to reduce this to a
         --      simpler form (e.g. Eq a)
         --
@@ -97,7 +97,8 @@ earlyDSLoc :: EarlyDerivSpec -> SrcSpan
 earlyDSLoc (InferTheta spec) = ds_loc spec
 earlyDSLoc (GivenTheta spec) = ds_loc spec
 
-splitEarlyDerivSpec :: [EarlyDerivSpec] -> ([DerivSpec ThetaOrigin], [DerivSpec ThetaType])
+splitEarlyDerivSpec :: [EarlyDerivSpec]
+                    -> ([DerivSpec [ThetaOrigin]], [DerivSpec ThetaType])
 splitEarlyDerivSpec [] = ([],[])
 splitEarlyDerivSpec (InferTheta spec : specs) =
     case splitEarlyDerivSpec specs of (is, gs) -> (spec : is, gs)
@@ -980,8 +981,7 @@ mkDataTypeEqn dflags overlap_mode tvs cls cls_tys
   = case deriv_strat of
       Just StockStrategy    -> mk_eqn_stock dflags mtheta cls cls_tys rep_tc
                                 go_for_it bale_out
-      Just AnyclassStrategy -> mk_eqn_anyclass dflags rep_tc cls
-                                go_for_it bale_out
+      Just AnyclassStrategy -> mk_eqn_anyclass dflags go_for_it bale_out
       -- GeneralizedNewtypeDeriving makes no sense for non-newtypes
       Just NewtypeStrategy  -> bale_out gndNonNewtypeErr
       -- Lacking a user-requested deriving strategy, we will try to pick
@@ -1010,8 +1010,7 @@ mk_data_eqn overlap_mode tvs cls cls_tys tycon tc_args rep_tc rep_tc_args
        dfun_name            <- newDFunName' cls tycon
        case mtheta of
         Nothing -> -- Infer context
-          inferConstraints tvs cls cls_tys
-                           inst_ty rep_tc rep_tc_args
+          inferConstraints tvs cls cls_tys inst_ty rep_tc rep_tc_args mechanism
             $ \inferred_constraints tvs' inst_tys' ->
             return $ InferTheta $ DS
                    { ds_loc = loc
@@ -1052,14 +1051,14 @@ mk_eqn_stock' cls go_for_it
         Nothing ->
           pprPanic "mk_eqn_stock': Not a stock class!" (ppr cls)
 
-mk_eqn_anyclass :: DynFlags -> TyCon -> Class
+mk_eqn_anyclass :: DynFlags
                 -> (DerivSpecMechanism -> TcRn EarlyDerivSpec)
                 -> (SDoc -> TcRn EarlyDerivSpec)
                 -> TcRn EarlyDerivSpec
-mk_eqn_anyclass dflags rep_tc cls go_for_it bale_out
-  = case canDeriveAnyClass dflags rep_tc cls of
-        Nothing  -> go_for_it DerivSpecAnyClass
-        Just msg -> bale_out msg
+mk_eqn_anyclass dflags go_for_it bale_out
+  = case canDeriveAnyClass dflags of
+        IsValid      -> go_for_it DerivSpecAnyClass
+        NotValid msg -> bale_out msg
 
 mk_eqn_no_mechanism :: DynFlags -> TyCon -> DerivContext
                     -> Class -> [Type] -> TyCon
@@ -1103,8 +1102,7 @@ mkNewTypeEqn dflags overlap_mode tvs
     case deriv_strat of
       Just StockStrategy    -> mk_eqn_stock dflags mtheta cls cls_tys rep_tycon
                                  go_for_it_other bale_out
-      Just AnyclassStrategy -> mk_eqn_anyclass dflags rep_tycon cls
-                                 go_for_it_other bale_out
+      Just AnyclassStrategy -> mk_eqn_anyclass dflags go_for_it_other bale_out
       Just NewtypeStrategy  ->
         -- Since the user explicitly asked for GeneralizedNewtypeDeriving, we
         -- don't need to perform all of the checks we normally would, such as
@@ -1170,7 +1168,7 @@ mkNewTypeEqn dflags overlap_mode tvs
         deriveAnyClass    = xopt LangExt.DeriveAnyClass             dflags
         go_for_it_gnd     = do
           traceTc "newtype deriving:" $
-            ppr tycon <+> ppr rep_tys <+> ppr all_preds
+            ppr tycon <+> ppr rep_tys <+> ppr all_thetas
           let mechanism = DerivSpecNewtype rep_inst_ty
           doDerivInstErrorChecks1 cls cls_tys tycon tc_args rep_tycon mtheta
                                   strat_used mechanism
@@ -1190,7 +1188,7 @@ mkNewTypeEqn dflags overlap_mode tvs
                , ds_name = dfun_name, ds_tvs = dfun_tvs
                , ds_cls = cls, ds_tys = inst_tys
                , ds_tc = rep_tycon
-               , ds_theta = all_preds
+               , ds_theta = all_thetas
                , ds_overlap = overlap_mode
                , ds_mechanism = mechanism }
         go_for_it_other = mk_data_eqn overlap_mode tvs cls cls_tys tycon
@@ -1258,12 +1256,12 @@ mkNewTypeEqn dflags overlap_mode tvs
 
         -- Next we figure out what superclass dictionaries to use
         -- See Note [Newtype deriving superclasses] above
-        sc_theta   :: [PredOrigin]
+        sc_preds   :: [PredOrigin]
         cls_tyvars = classTyVars cls
         dfun_tvs   = tyCoVarsOfTypesWellScoped inst_tys
         inst_ty    = mkTyConApp tycon tc_args
         inst_tys   = cls_tys ++ [inst_ty]
-        sc_theta   = mkThetaOrigin DerivOrigin TypeLevel $
+        sc_preds   = map (mkPredOrigin DerivOrigin TypeLevel) $
                      substTheta (zipTvSubst cls_tyvars inst_tys) $
                      classSCTheta cls
 
@@ -1271,9 +1269,9 @@ mkNewTypeEqn dflags overlap_mode tvs
         -- 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_theta :: [PredOrigin]
+        meth_preds :: [PredOrigin]
         meths = classMethods cls
-        meth_theta | null meths = [] -- No methods => no constraints
+        meth_preds | null meths = [] -- No methods => no constraints
                                      -- (Trac #12814)
                    | otherwise = rep_pred_o : coercible_constraints
         coercible_constraints
@@ -1283,8 +1281,8 @@ mkNewTypeEqn dflags overlap_mode tvs
             , let (Pair t1 t2) = mkCoerceClassMethEqn cls dfun_tvs
                                          inst_tys rep_inst_ty meth ]
 
-        all_preds :: [PredOrigin]
-        all_preds = meth_theta ++ sc_theta
+        all_thetas :: [ThetaOrigin]
+        all_thetas = [mkThetaOriginFromPreds $ meth_preds ++ sc_preds]
 
         -------------------------------------------------------------------
         --  Figuring out whether we can only do this newtype-deriving thing
@@ -1627,7 +1625,9 @@ genDerivStuff mechanism loc clas tycon inst_tys tyvars
             mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env
         dflags <- getDynFlags
         tyfam_insts <-
-          ASSERT2( isNothing (canDeriveAnyClass dflags tycon clas)
+          -- canDeriveAnyClass should ensure that this code can't be reached
+          -- unless -XDeriveAnyClass is enabled.
+          ASSERT2( isValid (canDeriveAnyClass dflags)
                  , ppr "genDerivStuff: bad derived class" <+> ppr clas )
           mapM (tcATDefault False loc mini_subst emptyNameSet)
                (classATItems clas)
diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index 109e6347e7..52a4daf4a5 100644
--- a/compiler/typecheck/TcDerivInfer.hs
+++ b/compiler/typecheck/TcDerivInfer.hs
@@ -13,16 +13,17 @@ module TcDerivInfer (inferConstraints, simplifyInstanceContexts) where
 #include "HsVersions.h"
 
 import Bag
+import BasicTypes
 import Class
 import DataCon
-import DynFlags
+-- import DynFlags
 import ErrUtils
 import Inst
 import Outputable
 import PrelNames
 import TcDerivUtils
 import TcEnv
-import TcErrors (reportAllUnsolved)
+-- import TcErrors (reportAllUnsolved)
 import TcGenFunctor
 import TcGenGenerics
 import TcMType
@@ -33,8 +34,10 @@ import Type
 import TcSimplify
 import TcValidity (validDerivPred)
 import TcUnify (buildImplicationFor)
-import Unify (tcUnifyTy)
+import Unify (tcMatchTy, tcUnifyTy)
 import Util
+import Var
+import VarEnv
 import VarSet
 
 import Control.Monad
@@ -44,8 +47,8 @@ import Data.Maybe
 ----------------------
 
 inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
-                 -> TyCon -> [TcType]
-                 -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
+                 -> TyCon -> [TcType] -> DerivSpecMechanism
+                 -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
                  -> TcM a
 -- inferConstraints figures out the constraints needed for the
 -- instance declaration generated by a 'deriving' clause on a
@@ -62,30 +65,37 @@ inferConstraints :: [TyVar] -> Class -> [TcType] -> TcType
 -- Generate a sufficiently large set of constraints that typechecking the
 -- generated method definitions should succeed.   This set will be simplified
 -- before being used in the instance declaration
-inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
-  | is_generic                        -- Generic constraints are easy
-  = mkTheta [] tvs inst_tys
+inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args
+                 mechanism thing
+  | is_generic && not is_anyclass     -- Generic constraints are easy
+  = thing [mkThetaOriginFromPreds []] tvs inst_tys
 
-  | is_generic1                       -- Generic1 needs Functor
+  | is_generic1 && not is_anyclass    -- Generic1 needs Functor
   = ASSERT( length rep_tc_tvs > 0 )   -- See Note [Getting base classes]
     ASSERT( length cls_tys   == 1 )   -- Generic1 has a single kind variable
     do { functorClass <- tcLookupClass functorClassName
-       ; con_arg_constraints (get_gen1_constraints functorClass) mkTheta }
+       ; con_arg_constraints (get_gen1_constraints functorClass) thing }
 
   | otherwise  -- The others are a bit more complicated
-  = ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
+  = -- See the comment with all_rep_tc_args for an explanation of
+    -- this assertion
+    ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
            , ppr main_cls <+> ppr rep_tc
              $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
-    con_arg_constraints get_std_constrained_tys
-      $ \arg_constraints tvs' inst_tys' ->
+    infer_constraints $ \arg_constraints tvs' inst_tys' ->
       do { traceTc "inferConstraints" $ vcat
                 [ ppr main_cls <+> ppr inst_tys'
                 , ppr arg_constraints
                 ]
-         ; mkTheta (stupid_constraints ++ extra_constraints
+         ; thing (stupid_constraints ++ extra_constraints
                      ++ sc_constraints ++ arg_constraints)
-                   tvs' inst_tys' }
+                 tvs' inst_tys' }
   where
+    is_anyclass = isDerivSpecAnyClass mechanism
+    infer_constraints
+      | is_anyclass = inferConstraintsDAC main_cls tvs inst_tys
+      | otherwise   = con_arg_constraints get_std_constrained_tys
+
     tc_binders = tyConBinders rep_tc
     choose_level bndr
       | isNamedTyConBinder bndr = KindLevel
@@ -96,10 +106,10 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
        -- Constraints arising from the arguments of each constructor
     con_arg_constraints :: (CtOrigin -> TypeOrKind
                                      -> Type
-                                     -> [(ThetaOrigin, Maybe TCvSubst)])
-                        -> (ThetaOrigin -> [TyVar] -> [TcType] -> TcM a)
+                                     -> [([PredOrigin], Maybe TCvSubst)])
+                        -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
                         -> TcM a
-    con_arg_constraints get_arg_constraints mkTheta
+    con_arg_constraints get_arg_constraints thing
       = let (predss, mbSubsts) = unzip
               [ preds_and_mbSubst
               | data_con <- tyConDataCons rep_tc
@@ -122,29 +132,25 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
             unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
                                       && not (v `isInScope` subst)) tvs
             (subst', _)  = mapAccumL substTyVarBndr subst unmapped_tvs
-            preds'       = substThetaOrigin subst' preds
+            preds'       = map (substPredOrigin subst') preds
             inst_tys'    = substTys subst' inst_tys
             tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
-        in mkTheta preds' tvs' inst_tys'
+        in thing [mkThetaOriginFromPreds preds'] tvs' inst_tys'
 
     is_generic  = main_cls `hasKey` genClassKey
     is_generic1 = main_cls `hasKey` gen1ClassKey
     -- is_functor_like: see Note [Inferring the instance context]
     is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
-                   || is_generic1 -- Technically, Generic1 requires a type of
-                                  -- kind (k -> *), not (* -> *), but we still
-                                  -- label it "functor-like" to make sure
-                                  -- all_rep_tc_args has all the necessary type
-                                  -- variables it needs to function.
+                   || is_generic1
 
     get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
-                         -> [(ThetaOrigin, Maybe TCvSubst)]
+                         -> [([PredOrigin], 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
-                            -> [(ThetaOrigin, Maybe TCvSubst)]
+                            -> [([PredOrigin], Maybe TCvSubst)]
     get_std_constrained_tys orig t_or_k ty
         | is_functor_like = mk_functor_like_constraints orig t_or_k main_cls $
                             deepSubtypesContaining last_tv ty
@@ -153,7 +159,7 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
 
     mk_functor_like_constraints :: CtOrigin -> TypeOrKind
                                 -> Class -> [Type]
-                                -> [(ThetaOrigin, Maybe TCvSubst)]
+                                -> [([PredOrigin], 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
     --
@@ -173,23 +179,31 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
 
     rep_tc_tvs      = tyConTyVars rep_tc
     last_tv         = last rep_tc_tvs
-    all_rep_tc_args | is_functor_like = rep_tc_args ++ [mkTyVarTy last_tv]
-                    | otherwise       = rep_tc_args
+    -- When we first gather up the constraints to solve, most of them contain
+    -- rep_tc_tvs, i.e., the type variables from the derived datatype's type
+    -- constructor. We don't want these type variables to appear in the final
+    -- instance declaration, so we must substitute each type variable with its
+    -- counterpart in the derived instance. rep_tc_args lists each of these
+    -- counterpart types in the same order as the type variables.
+    all_rep_tc_args = rep_tc_args ++ map mkTyVarTy
+                                     (drop (length rep_tc_args) rep_tc_tvs)
 
         -- Constraints arising from superclasses
         -- See Note [Superclasses of derived instance]
     cls_tvs  = classTyVars main_cls
     inst_tys = cls_tys ++ [inst_ty]
     sc_constraints = ASSERT2( equalLength cls_tvs inst_tys, ppr main_cls <+> ppr rep_tc)
-                     mkThetaOrigin DerivOrigin TypeLevel $
-                     substTheta cls_subst (classSCTheta main_cls)
+                     [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+                       substTheta cls_subst (classSCTheta main_cls) ]
     cls_subst = ASSERT( equalLength cls_tvs inst_tys )
                 zipTvSubst cls_tvs inst_tys
 
         -- Stupid constraints
-    stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $
-                         substTheta tc_subst (tyConStupidTheta rep_tc)
-    tc_subst = ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
+    stupid_constraints = [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+                           substTheta tc_subst (tyConStupidTheta rep_tc) ]
+    tc_subst = -- See the comment with all_rep_tc_args for an explanation of
+               -- this assertion
+               ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
                zipTvSubst rep_tc_tvs all_rep_tc_args
 
         -- Extra Data constraints
@@ -200,13 +214,15 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
         -- 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
-      | main_cls `hasKey` dataClassKey
-      , all (isLiftedTypeKind . typeKind) rep_tc_args
-      = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
-        | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
-      | otherwise
-      = []
+    extra_constraints = [mkThetaOriginFromPreds constrs]
+      where
+        constrs
+          | main_cls `hasKey` dataClassKey
+          , all (isLiftedTypeKind . typeKind) rep_tc_args
+          = [ mk_cls_pred DerivOrigin t_or_k main_cls ty
+            | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
+          | otherwise
+          = []
 
     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]))
@@ -218,6 +234,74 @@ inferConstraints tvs main_cls cls_tys inst_ty rep_tc rep_tc_args mkTheta
 typeToTypeKind :: Kind
 typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
 
+-- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
+-- which gathers its constraints based on the type signatures of the class's
+-- methods instead of the types of the data constructor's field.
+--
+-- See Note [Gathering and simplifying constraints for DeriveAnyClass]
+-- for an explanation of how these constraints are used to determine the
+-- derived instance context.
+inferConstraintsDAC :: Class -> [TyVar] -> [TcType]
+                    -> ([ThetaOrigin] -> [TyVar] -> [TcType] -> TcM a)
+                    -> TcM a
+inferConstraintsDAC cls tvs inst_tys thing =
+  let theta_origins
+        = [ mkThetaOrigin DerivOrigin TypeLevel dm_tvs vanilla_theta' dm_theta'
+          | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls
+          , let vanilla_ty = thdOf3 $ tcSplitMethodTy (varType sel_id)
+                -- See Note [Splitting nested sigma types] in TcTyClsDecls
+                (_,      vanilla_theta, vanilla_tau)
+                  = tcSplitNestedSigmaTys vanilla_ty
+                (dm_tvs, dm_theta,      dm_tau)
+                  = tcSplitNestedSigmaTys dm_ty
+
+                -- The class will start out like:
+                --
+                --   class Foo a where
+                --     bar :: a -> String
+                --     default :: Show a => a -> String
+                --
+                -- If we are anyclass-deriving an instance for, say,
+                -- data Wibble, then we want to collect a (Show Wibble)
+                -- constraint, not a (Show a) constraint! So we must first
+                -- substitute the instantiated types into the default type
+                -- signature (e.g., a |-> Wibble).
+                in_scope  = mkInScopeSet $ tyCoVarsOfTypes
+                                         $ mkTyVarTys dm_tvs ++ inst_tys
+                tv_env    = zipVarEnv (classTyVars cls) inst_tys
+                subst     = mkTvSubst in_scope tv_env
+                dm_theta' = substTheta subst dm_theta
+                dm_tau'   = substTy subst dm_tau
+
+                -- The next obstacle to overcome is the fact that the default
+                -- and non-default type signatures scope over different sets of
+                -- type variables. That is, this imagine that this is the
+                -- class you were anyclass-deriving:
+                --
+                --   class Baz f where
+                --     quux         :: forall a. Eq a => f a -> f a -> Bool
+                --     default quux :: forall b. (Eq b, Show b)
+                --                  => f b -> f b -> Bool
+                --
+                -- We need a way to treat `a` and `b` as the same when
+                -- typechecking a derived Baz instance. So to wrap
+                -- up inferConstraintsDAC, we match up the non-default type
+                -- type signature with the default one, and apply the resulting
+                -- substitution to the non-default type signature.
+                mb_dm_subst = tcMatchTy vanilla_tau dm_tau'
+                -- We can be assured that we'll always get a substitution here
+                -- (i.e., that the type signatures always match up), since we
+                -- checked for this property earlier in checkValidClass.
+                -- See Note [Default method type signatures must align]
+                -- in TcTyClsDecls.
+                dm_subst = fromMaybe
+                  (pprPanic "inferConstraintsDAC" $
+                    vcat [ text "vanilla_tau" <+> ppr vanilla_tau
+                         , text "dm_tau'"     <+> ppr dm_tau' ])
+                  mb_dm_subst
+                vanilla_theta' = substTheta dm_subst vanilla_theta ]
+  in thing theta_origins tvs inst_tys
+
 {-
 Note [Inferring the instance context]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -423,7 +507,8 @@ See also Note [nonDetCmpType nondeterminism]
 -}
 
 
-simplifyInstanceContexts :: [DerivSpec ThetaOrigin] -> TcM [DerivSpec ThetaType]
+simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
+                         -> TcM [DerivSpec ThetaType]
 -- Used only for deriving clauses (InferTheta)
 -- not for standalone deriving
 -- See Note [Simplifying the instance context]
@@ -472,7 +557,7 @@ simplifyInstanceContexts infer_specs
        -- See Note [Deterministic simplifyInstanceContexts]
     canSolution = map (sortBy nonDetCmpType)
     ------------------------------------------------------------------
-    gen_soln :: DerivSpec ThetaOrigin -> TcM ThetaType
+    gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
     gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
                  , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
       = setSrcSpan loc  $
@@ -506,10 +591,10 @@ derivInstCtxt pred
 simplifyDeriv :: PredType -- ^ @C inst_ty@, head of the instance we are
                           -- deriving.  Only used for SkolemInfo.
               -> [TyVar]  -- ^ The tyvars bound by @inst_ty@.
-              -> ThetaOrigin   -- ^ @wanted@ constraints, i.e. @['PredOrigin']@.
+              -> [ThetaOrigin] -- ^ Given and wanted constraints
               -> TcM ThetaType -- ^ Needed constraints (after simplification),
                                -- i.e. @['PredType']@.
-simplifyDeriv pred tvs theta
+simplifyDeriv pred tvs thetas
   = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
                 -- The constraint solving machinery
                 -- expects *TcTyVars* not TyVars.
@@ -519,32 +604,60 @@ simplifyDeriv pred tvs theta
        ; let skol_set  = mkVarSet tvs_skols
              skol_info = DerivSkol pred
              doc = text "deriving" <+> parens (ppr pred)
-             mk_ct (PredOrigin t o t_or_k)
-                 = newWanted o (Just t_or_k) (substTy skol_subst t)
 
-       -- Generate the wanted constraints with the skolemized variables
-       ; (wanted, tclvl) <- pushTcLevelM (mapM mk_ct theta)
+             mk_given_ev :: PredType -> TcM EvVar
+             mk_given_ev given =
+               let given_pred = substTy skol_subst given
+               in newEvVar given_pred
+
+             mk_wanted_ct :: PredOrigin -> TcM CtEvidence
+             mk_wanted_ct (PredOrigin wanted o t_or_k)
+               = newWanted o (Just t_or_k) (substTyUnchecked skol_subst wanted)
+
+             -- Create the implications we need to solve. For stock and newtype
+             -- deriving, these implication constraints will all be of the form
+             --
+             --   forall . () => <wanted_cts>
+             --
+             -- But with DeriveAnyClass, there might be given constraints as
+             -- well.
+             -- See Note [Gathering and simplifying constraints for
+             --           DeriveAnyClass]
+             mk_implics :: ThetaOrigin -> TcM (Bag Implication)
+             mk_implics (ThetaOrigin { to_tvs = local_tvs
+                                     , to_givens = givens
+                                     , to_wanted_origins = wanteds }) = do
+               ((given_evs, wanted_cts), tclvl) <- pushTcLevelM $ do
+                 given_cts  <- mapM mk_given_ev  givens
+                 wanted_cts <- mapM mk_wanted_ct wanteds
+                 pure (given_cts, wanted_cts)
+               (implic, _) <- buildImplicationFor tclvl skol_info local_tvs
+                                given_evs (mkSimpleWC wanted_cts)
+               pure implic
+
+       -- Generate the implication constraints constraints to solve with the
+       -- skolemized variables
+       ; (implics, tclvl) <- pushTcLevelM $ mapM mk_implics thetas
 
        ; traceTc "simplifyDeriv inputs" $
-         vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanted, doc ]
+         vcat [ pprTyVars tvs $$ ppr thetas $$ ppr implics, doc ]
        -- Simplify the constraints
-       ; residual_wanted <- simplifyWantedsTcM wanted
-            -- Result is zonked
+       ; solved_implics <- runTcSDeriveds $ solveWantedsAndDrop
+                                          $ mkImplicWC
+                                          $ unionManyBags implics
 
        -- Split the resulting constraints into bad and good constraints,
        -- building an @unsolved :: WantedConstraints@ representing all
        -- the constraints we can't just shunt to the predicates.
        -- See Note [Exotic derived instance contexts]
-       ; let residual_simple = wc_simple residual_wanted
+       ; let residual_simple = approximateWC True solved_implics
              (bad, good) = partitionBagWith get_good residual_simple
-             unsolved    = residual_wanted { wc_simple = bad }
-
-                         -- See Note [Exotic derived instance contexts]
 
              get_good :: Ct -> Either Ct PredType
              get_good ct | validDerivPred skol_set p
                          , isWantedCt ct
                          = Right p
+                          -- TODO: This is wrong
                           -- NB re 'isWantedCt': residual_wanted may contain
                           -- unsolved CtDerived and we stick them into the
                           -- bad set so that reportUnsolved may decide what
@@ -556,22 +669,26 @@ simplifyDeriv pred tvs theta
        ; traceTc "simplifyDeriv outputs" $
          vcat [ ppr tvs_skols, ppr residual_simple, ppr good, ppr bad ]
 
-       -- If we are deferring type errors, simply ignore any insoluble
-       -- constraints.  They'll come up again when we typecheck the
-       -- generated instance declaration
-       ; defer <- goptM Opt_DeferTypeErrors
-       ; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
-                   -- The buildImplicationFor is just to bind the skolems,
-                   -- in case they are mentioned in error messages
-                   -- See Trac #11347
-       -- Report the (bad) unsolved constraints
-       ; unless defer (reportAllUnsolved (mkImplicWC implic))
-
-
        -- Return the good unsolved constraints (unskolemizing on the way out.)
-       ; let min_theta  = mkMinimalBySCs (bagToList good)
+       ; let min_theta = mkMinimalBySCs (bagToList good)
+             -- An important property of mkMinimalBySCs (used above) is that in
+             -- addition to removing constraints that are made redundant by
+             -- superclass relationships, it also removes _duplicate_
+             -- constraints.
+             -- See Note [Gathering and simplifying constraints for
+             --           DeriveAnyClass]
              subst_skol = zipTvSubst tvs_skols $ mkTyVarTys tvs
                           -- The reverse substitution (sigh)
+
+       ; min_theta_vars <- mapM newEvVar min_theta
+       ; (leftover_implic, _) <- buildImplicationFor tclvl skol_info tvs_skols
+                                   min_theta_vars solved_implics
+       -- This call to simplifyTop is purely for error reporting
+       -- See Note [Error reporting for deriving clauses]
+       -- See also Note [Exotic derived instance contexts], which are caught
+       -- in this line of code.
+       ; _ <- simplifyTop $ mkImplicWC leftover_implic
+
        ; return (substTheta subst_skol min_theta) }
 
 {-
@@ -600,6 +717,106 @@ BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
              the context for the derived instance.
              Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
 
+Note [Gathering and simplifying constraints for DeriveAnyClass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DeriveAnyClass works quite differently from stock and newtype deriving in
+the way it gathers and simplifies constraints to be used in a derived
+instance's context. Stock and newtype deriving gather constraints by looking
+at the data constructors of the data type for which we are deriving an
+instance. But DeriveAnyClass doesn't need to know about a data type's
+definition at all!
+
+To see why, picture this example example of DeriveAnyClass:
+
+  data Maybe a = ... deriving Foo
+
+  class Foo a where
+    bar :: Ix b => a -> b -> String
+    default bar :: (Show a, Ix b) => a -> b -> String
+    bar x _ = show x
+
+    baz :: Eq a => a -> a -> Bool
+    default baz :: (Ord a, Show a) => a -> a -> Bool
+    baz x y = compare x y == EQ
+
+This derives an instance of the form:
+
+  instance ??? => Foo (Maybe a)
+
+Because bar and baz have default signatures, GHC fills them in under the hood:
+
+  instance ??? => Foo (Maybe a) where
+    bar = $gdm_bar
+    baz = $gdm_baz
+
+  $gdm_bar :: Show a => a -> String
+  $gdm_bar = show
+
+  $gdm_baz :: (Ord a, Show a) => a -> a -> Bool
+  $gdm_baz x y = compare x y == EQ
+
+Now it is GHC's job to fill in a suitable ??? (the instance context). It does
+so by simplifying two sets of constraints: the constraints from the default
+type signatures (the wanted constraints), and the constraints from the
+non-default type signatures (the given constraints, which can be used to
+help further simplify the wanted constraints):
+
+  bar: (Givens: [Ix b],         Wanteds: [Show (Maybe a), Ix b])
+  baz: (Givens: [Eq (Maybe a)], Wanteds: [Ord (Maybe a), Show (Maybe a)])
+
+These are just implication constraints. We can combine them into a single
+constraint:
+
+     (forall b. Ix b         => (Show (Maybe a), Ix b))
+  /\
+     (forall  . Eq (Maybe a) => (Ord (Maybe a), Show (Maybe a)))
+
+After simplification, you get:
+
+     (forall b. Ix b         => Show a)
+  /\
+     (forall  . Eq (Maybe a) => (Ord a, Show a))
+
+Now we need to hoist these constraints out of the implications to become our
+candidate for ???. That is done by approximateWC, which will return:
+
+  (Show a, Ord a, Show a)
+
+Now we can use mkMinimalBySCs to remove superclasses and duplicates, giving
+
+  (Show a, Ord a)
+
+And that's what GHC uses for ???.
+
+Note [Error reporting for deriving clauses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A suprisingly tricky aspect of deriving to get right is reporting sensible
+error messages. In particular, if simplifyDeriv reaches a constraint that it
+cannot solve, which might include:
+
+1. Insoluble constraints
+2. "Exotic" constraints (See Note [Exotic derived instance contexts])
+
+Then we report an error immediately in simplifyDeriv.
+
+Another possible choice is to punt and let another part of the typechecker
+(e.g., simplifyInstanceContexts) catch the errors. But this tends to lead
+to worse error messages, so we do it directly in simplifyDeriv.
+
+simplifyDeriv checks for errors in a clever way. If the deriving machinery
+infers the context (Foo a)--that is, if this instance is to be generated:
+
+  instance Foo a => ...
+
+Then we form an implication of the form:
+
+  forall a. Foo a => <residual_wanted_constraints>
+
+And pass it to the simplifier. If the context (Foo a) is enough to discharge
+all the constraints in <residual_wanted_constraints>, then everything is
+hunky-dory. But if <residual_wanted_constraints> contains, say, an insoluble
+constraint, then (Foo a) won't be able to solve it, causing GHC to error.
+
 Note [Exotic derived instance contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In a 'derived' instance declaration, we *infer* the context.  It's a
diff --git a/compiler/typecheck/TcDerivUtils.hs b/compiler/typecheck/TcDerivUtils.hs
index b142b33f06..1e10d147e3 100644
--- a/compiler/typecheck/TcDerivUtils.hs
+++ b/compiler/typecheck/TcDerivUtils.hs
@@ -13,8 +13,8 @@ module TcDerivUtils (
         DerivSpecMechanism(..), isDerivSpecStock,
         isDerivSpecNewtype, isDerivSpecAnyClass,
         DerivContext, DerivStatus(..),
-        PredOrigin(..), ThetaOrigin, mkPredOrigin,
-        mkThetaOrigin, substPredOrigin, substThetaOrigin,
+        PredOrigin(..), ThetaOrigin(..), mkPredOrigin,
+        mkThetaOrigin, mkThetaOriginFromPreds, substPredOrigin,
         checkSideConditions, hasStockDeriving,
         canDeriveAnyClass,
         std_class_via_coercible, non_coercible_class,
@@ -151,24 +151,73 @@ data DerivStatus = CanDerive                 -- Stock class, can derive
 -- | 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
-type ThetaOrigin = [PredOrigin]
+
+-- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') alongside
+-- any corresponding given constraints ('to_givens') and locally quantified
+-- type variables ('to_tvs').
+--
+-- In most cases, 'to_givens' will be empty, as most deriving mechanisms (e.g.,
+-- stock and newtype deriving) do not require given constraints. The exception
+-- is @DeriveAnyClass@, which can involve given constraints. For example,
+-- if you tried to derive an instance for the following class using
+-- @DeriveAnyClass@:
+--
+-- @
+-- class Foo a where
+--   bar :: a -> b -> String
+--   default bar :: (Show a, Ix b) => a -> b -> String
+--   bar = show
+--
+--   baz :: Eq a => a -> a -> Bool
+--   default baz :: Ord a => a -> a -> Bool
+--   baz x y = compare x y == EQ
+-- @
+--
+-- Then it would generate two 'ThetaOrigin's, one for each method:
+--
+-- @
+-- [ ThetaOrigin { to_tvs            = [b]
+--               , to_givens         = []
+--               , to_wanted_origins = [Show a, Ix b] }
+-- , ThetaOrigin { to_tvs            = []
+--               , to_givens         = [Eq a]
+--               , to_wanted_origins = [Ord a] }
+-- ]
+-- @
+data ThetaOrigin
+  = ThetaOrigin { to_tvs            :: [TyVar]
+                , to_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_tvs = tvs
+                   , to_givens = givens
+                   , to_wanted_origins = wanted_origins })
+    = hang (text "ThetaOrigin")
+         2 (vcat [ text "to_tvs            =" <+> ppr tvs
+                 , text "to_givens         =" <+> ppr 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 -> ThetaType -> ThetaOrigin
-mkThetaOrigin origin t_or_k = map (mkPredOrigin origin t_or_k)
+mkThetaOrigin :: CtOrigin -> TypeOrKind -> [TyVar] -> ThetaType -> ThetaType
+              -> ThetaOrigin
+mkThetaOrigin origin t_or_k tvs givens
+  = ThetaOrigin tvs givens . map (mkPredOrigin origin t_or_k)
+
+-- A common case where the ThetaOrigin only contains wanted constraints, with
+-- no givens or locally scoped type variables.
+mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin
+mkThetaOriginFromPreds = ThetaOrigin [] []
 
 substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
 substPredOrigin subst (PredOrigin pred origin t_or_k)
   = PredOrigin (substTy subst pred) origin t_or_k
 
-substThetaOrigin :: HasCallStack => TCvSubst -> ThetaOrigin -> ThetaOrigin
-substThetaOrigin subst = map (substPredOrigin subst)
-
 {-
 ************************************************************************
 *                                                                      *
@@ -270,7 +319,7 @@ checkSideConditions dflags mtheta cls cls_tys rep_tc
                  | otherwise -> DerivableClassError (classArgsErr cls cls_tys)
                    -- e.g. deriving( Eq s )
 
-  | Just err <- canDeriveAnyClass dflags rep_tc cls
+  | NotValid err <- canDeriveAnyClass dflags
   = NonDerivableClass err  -- DeriveAnyClass does not work
 
   | otherwise
@@ -324,27 +373,14 @@ sideConditions mtheta cls
     cond_vanilla = cond_stdOK mtheta True   -- Vanilla data constructors but
                                             --   allow no data cons or polytype arguments
 
-canDeriveAnyClass :: DynFlags -> TyCon -> Class -> Maybe SDoc
--- Nothing: we can (try to) derive it via an empty instance declaration
--- Just s:  we can't, reason s
--- Precondition: the class is not one of the standard ones
-canDeriveAnyClass dflags _tycon clas
+canDeriveAnyClass :: DynFlags -> Validity
+-- IsValid: we can (try to) derive it via an empty instance declaration
+-- NotValid s:  we can't, reason s
+canDeriveAnyClass dflags
   | not (xopt LangExt.DeriveAnyClass dflags)
-  = Just (text "Try enabling DeriveAnyClass")
-  | not (any (target_kind `tcEqKind`) [ liftedTypeKind, typeToTypeKind ])
-  = Just (text "The last argument of class" <+> quotes (ppr clas)
-          <+> text "does not have kind * or (* -> *)")
+  = NotValid (text "Try enabling DeriveAnyClass")
   | otherwise
-  = Nothing   -- OK!
-  where
-    -- We are making an instance  (C t1 .. tn (T s1 .. sm))
-    -- and we can only do so if the kind of C's last argument
-    -- is * or (* -> *).  Because only then can we make a reasonable
-    -- guess at the instance context
-    target_kind = tyVarKind (last (classTyVars clas))
-
-typeToTypeKind :: Kind
-typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
+  = IsValid   -- OK!
 
 type Condition = DynFlags -> TyCon -> Validity
         -- TyCon is the *representation* tycon if the data type is an indexed one
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index a4d5325b4c..61f2c12543 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -11,7 +11,8 @@ module TcSimplify(
        tcCheckSatisfiability,
 
        -- For Rules we need these
-       solveWanteds, runTcSDeriveds
+       solveWanteds, solveWantedsAndDrop,
+       approximateWC, runTcSDeriveds
   ) where
 
 #include "HsVersions.h"
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 44f36a998e..a0ca0b2555 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1817,12 +1817,12 @@ pickCapturedPreds qtvs theta
 type PredWithSCs = (PredType, [PredType])
 
 mkMinimalBySCs :: [PredType] -> [PredType]
--- Remove predicates that can be deduced from others by superclasses
--- Result is a subset of the input
+-- Remove predicates that can be deduced from others by superclasses,
+-- including duplicate predicates. The result is a subset of the input.
 mkMinimalBySCs ptys = go preds_with_scs []
  where
    preds_with_scs :: [PredWithSCs]
-   preds_with_scs = [ (pred, transSuperClasses pred)
+   preds_with_scs = [ (pred, pred : transSuperClasses pred)
                     | pred <- ptys ]
 
    go :: [PredWithSCs]   -- Work list
diff --git a/docs/users_guide/8.2.1-notes.rst b/docs/users_guide/8.2.1-notes.rst
index a01ad1a9d5..45ed5896f5 100644
--- a/docs/users_guide/8.2.1-notes.rst
+++ b/docs/users_guide/8.2.1-notes.rst
@@ -55,6 +55,17 @@ Compiler
   class instance using the :ghc-flag:`-XDerivingStrategies` language extension
   (see :ref:`deriving-strategies`).
 
+- :ghc-flag:`-XDeriveAnyClass` is no longer limited to type classes whose
+  argument is of kind ``*`` or ``* -> *``.
+
+- The means by which :ghc-flag:`-XDeriveAnyClass` infers instance contexts has
+  been completely overhauled. The instance context is now inferred using the
+  type signatures (and default type signatures) of the derived class's methods
+  instead of using the datatype's definition, which often led to
+  overconstrained instances or instances that didn't typecheck (or worse,
+  triggered GHC panics). See the section on
+  :ref:`DeriveAnyClass <derive-any-class>` for more details.
+
 - GHC now allows standalone deriving using :ghc-flag:`-XDeriveAnyClass` on
   any data type, even if its data constructors are not in scope. This is
   consistent with the fact that this code (in the presence of
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 50744f3e11..550bca8949 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -4185,29 +4185,71 @@ Note the following details
   class on a newtype, and :ghc-flag:`-XGeneralizedNewtypeDeriving` is also on,
   :ghc-flag:`-XDeriveAnyClass` takes precedence.
 
-- :ghc-flag:`-XDeriveAnyClass` is allowed only when the last argument of the class
-  has kind ``*`` or ``(* -> *)``.  So this is not allowed: ::
+- The instance context is determined by the type signatures of the derived
+  class's methods. For instance, if the class is: ::
 
-    data T a b = MkT a b deriving( Bifunctor )
+    class Foo a where
+      bar :: a -> String
+      default bar :: Show a => a -> String
+      bar = show
+
+      baz :: a -> a -> Bool
+      default baz :: Ord a => a -> a -> Bool
+      baz x y = compare x y == EQ
+
+  And you attempt to derive it using :ghc-flag:`-XDeriveAnyClass`: ::
+
+    instance Eq   a => Eq   (Option a) where ...
+    instance Ord  a => Ord  (Option a) where ...
+    instance Show a => Show (Option a) where ...
+
+    data Option a = None | Some a deriving Foo
+
+  Then the derived ``Foo`` instance will be: ::
+
+    instance (Show a, Ord a) => Foo (Option a)
+
+  Since the default type signatures for ``bar`` and ``baz`` require ``Show a``
+  and ``Ord a`` constraints, respectively.
+
+  Constraints on the non-default type signatures can play a role in inferring
+  the instance context as well. For example, if you have this class: ::
+
+    class HigherEq f where
+      (==#) :: f a -> f a -> Bool
+      default (==#) :: Eq (f a) => f a -> f a -> Bool
+      x ==# y = (x == y)
+
+  And you tried to derive an instance for it: ::
 
-  because the last argument of ``Bifunctor :: (* -> * -> *) -> Constraint``
-  has the wrong kind.
+    instance Eq a => Eq (Option a) where ...
+    data Option a = None | Some a deriving HigherEq
 
-- The instance context will be generated according to the same rules
-  used when deriving ``Eq`` (if the kind of the type is ``*``), or
-  the rules for ``Functor`` (if the kind of the type is ``(* -> *)``).
-  For example ::
+  Then it will fail with an error to the effect of: ::
 
-    instance C a => C (a,b) where ...
+    No instance for (Eq a)
+        arising from the 'deriving' clause of a data type declaration
 
-    data T a b = MkT a (a,b) deriving( C )
+  That is because we require an ``Eq (Option a)`` instance from the default
+  type signature for ``(==#)``, which in turn requires an ``Eq a`` instance,
+  which we don't have in scope. But if you tweak the definition of
+  ``HigherEq`` slightly: ::
 
-  The ``deriving`` clause will generate ::
+    class HigherEq f where
+      (==#) :: Eq a => f a -> f a -> Bool
+      default (==#) :: Eq (f a) => f a -> f a -> Bool
+      x ==# y = (x == y)
 
-    instance C a => C (T a b) where {}
+  Then it becomes possible to derive a ``HigherEq Option`` instance. Note that
+  the only difference is that now the non-default type signature for ``(==#)``
+  brings in an ``Eq a`` constraint. Constraints from non-default type
+  signatures never appear in the derived instance context itself, but they can
+  be used to discharge obligations that are demanded by the default type
+  signatures. In the example above, the default type signature demanded an
+  ``Eq a`` instance, and the non-default signature was able to satisfy that
+  request, so the derived instance is simply: ::
 
-  The constraints `C a` and `C (a,b)` are generated from the data
-  constructor arguments, but the latter simplifies to `C a`.
+    instance HigherEq Option
 
 - :ghc-flag:`-XDeriveAnyClass` can be used with partially applied classes,
   such as ::
diff --git a/testsuite/tests/deriving/should_compile/T12144_1.hs b/testsuite/tests/deriving/should_compile/T12144_1.hs
new file mode 100644
index 0000000000..f43d84ae6d
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T12144_1.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE KindSignatures #-}
+module T12144_1 where
+
+class C (a :: * -> *)
+data T a = MkT (a -> Int) deriving C
diff --git a/testsuite/tests/deriving/should_compile/T12144_2.hs b/testsuite/tests/deriving/should_compile/T12144_2.hs
new file mode 100644
index 0000000000..dc9f64e90e
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T12144_2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DeriveAnyClass #-}
+module T12144_2 where
+
+class C1 a
+
+instance C1 a => C1 (Foo a)
+
+class C1 a => C2 a where
+  c2 :: a -> String
+  c2 _ = "C2 default"
+
+newtype Foo a = Foo a deriving C2
+
+foo :: C1 a => Foo a -> String
+foo = c2
diff --git a/testsuite/tests/deriving/should_compile/T12423.hs b/testsuite/tests/deriving/should_compile/T12423.hs
new file mode 100644
index 0000000000..f7454497af
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T12423.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DefaultSignatures, DeriveAnyClass #-}
+module T12423 where
+
+class Eq1 f where
+  (==#) :: Eq a => f a -> f a -> Bool
+  default (==#) :: Eq (f a) => f a -> f a -> Bool
+  (==#) = (==)
+
+data Foo a = Foo (Either a a)
+    deriving (Eq, Eq1)
diff --git a/testsuite/tests/deriving/should_compile/T12594.hs b/testsuite/tests/deriving/should_compile/T12594.hs
new file mode 100644
index 0000000000..25d43ca664
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T12594.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+module T12594 where
+
+import GHC.Generics
+
+data Action = Action
+
+class ToField a where
+  toField :: a -> Action
+
+instance ToField Int where
+  -- Not the actual instance, but good enough for testing purposes
+  toField _ = Action
+
+class ToRow a where
+    toRow :: a -> [Action]
+    default toRow :: (Generic a, GToRow (Rep a)) => a -> [Action]
+    toRow = gtoRow . from
+
+class GToRow f where
+    gtoRow :: f p -> [Action]
+
+instance GToRow f => GToRow (M1 c i f) where
+    gtoRow (M1 x) = gtoRow x
+
+instance (GToRow f, GToRow g) => GToRow (f :*: g) where
+    gtoRow (f :*: g) = gtoRow f ++ gtoRow g
+
+instance (ToField a) => GToRow (K1 R a) where
+    gtoRow (K1 a) = [toField a]
+
+instance GToRow U1 where
+    gtoRow _ = []
+
+data Foo = Foo { bar :: Int }
+  deriving (Generic, ToRow)
diff --git a/testsuite/tests/deriving/should_fail/T9968a.hs b/testsuite/tests/deriving/should_compile/T9968a.hs
index ca5b1b082e..ca5b1b082e 100644
--- a/testsuite/tests/deriving/should_fail/T9968a.hs
+++ b/testsuite/tests/deriving/should_compile/T9968a.hs
diff --git a/testsuite/tests/deriving/should_compile/T9968a.stderr b/testsuite/tests/deriving/should_compile/T9968a.stderr
new file mode 100644
index 0000000000..dad865ef4b
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T9968a.stderr
@@ -0,0 +1,5 @@
+
+T9968a.hs:8:13: warning: [-Wmissing-methods (in -Wdefault)]
+    • No explicit implementation for
+        either ‘bimap’ or (‘first’ and ‘second’)
+    • In the instance declaration for ‘Bifunctor Blah’
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 31f8669230..288b3b7fdb 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -61,19 +61,24 @@ test('T10524', normal, compile, [''])
 test('T11148', normal, run_command,
      ['$MAKE -s --no-print-directory T11148'])
 test('T9968', normal, compile, [''])
+test('T9968a', normal, compile, [''])
 test('T11174', normal, compile, [''])
 test('T11416', normal, compile, [''])
 test('T11396', normal, compile, [''])
 test('T11357', normal, compile, [''])
-test('T11509_2', expect_fail, compile, [''])
+test('T11509_2', normal, compile, [''])
 test('T11509_3', normal, compile, [''])
 test('T11732a', normal, compile, [''])
 test('T11732b', normal, compile, [''])
 test('T11732c', normal, compile, [''])
 test('T11833', normal, compile, [''])
+test('T12144_1', normal, compile, [''])
+test('T12144_2', normal, compile, [''])
 test('T12245', normal, compile, [''])
 test('T12399', normal, compile, [''])
+test('T12423', normal, compile, [''])
 test('T12583', normal, compile, [''])
+test('T12594', normal, compile, [''])
 test('T12616', normal, compile, [''])
 test('T12688', normal, compile, [''])
 test('T12814', normal, compile, ['-Wredundant-constraints'])
diff --git a/testsuite/tests/deriving/should_fail/T10598_fail1.stderr b/testsuite/tests/deriving/should_fail/T10598_fail1.stderr
index 0183ec515d..ec4de2f1ad 100644
--- a/testsuite/tests/deriving/should_fail/T10598_fail1.stderr
+++ b/testsuite/tests/deriving/should_fail/T10598_fail1.stderr
@@ -9,9 +9,3 @@ T10598_fail1.hs:10:40: error:
     • Can't make a derived instance of ‘Num B’ with the stock strategy:
         ‘Num’ is not a stock derivable class (Eq, Show, etc.)
     • In the newtype declaration for ‘B’
-
-T10598_fail1.hs:11:41: error:
-    • Can't make a derived instance of
-        ‘Z C’ with the anyclass strategy:
-        The last argument of class ‘Z’ does not have kind * or (* -> *)
-    • In the data declaration for ‘C’
diff --git a/testsuite/tests/deriving/should_fail/T9968a.stderr b/testsuite/tests/deriving/should_fail/T9968a.stderr
deleted file mode 100644
index a72563162e..0000000000
--- a/testsuite/tests/deriving/should_fail/T9968a.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-
-T9968a.hs:8:13: error:
-    • Can't make a derived instance of ‘Bifunctor Blah’:
-        ‘Bifunctor’ is not a stock derivable class (Eq, Show, etc.)
-        The last argument of class ‘Bifunctor’ does not have kind * or (* -> *)
-    • In the data declaration for ‘Blah’
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index b15cda455d..9f3781ccf0 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -54,7 +54,6 @@ test('T9600-1', normal, compile_fail, [''])
 test('T9687', normal, compile_fail, [''])
 
 test('T8984', normal, compile_fail, [''])
-test('T9968a', normal, compile_fail, [''])
 test('T10598_fail1', normal, compile_fail, [''])
 test('T10598_fail2', normal, compile_fail, [''])
 test('T10598_fail3', normal, compile_fail, [''])
diff --git a/testsuite/tests/deriving/should_fail/drvfail004.stderr b/testsuite/tests/deriving/should_fail/drvfail004.stderr
index fe193b929a..1b2d63527b 100644
--- a/testsuite/tests/deriving/should_fail/drvfail004.stderr
+++ b/testsuite/tests/deriving/should_fail/drvfail004.stderr
@@ -1,8 +1,11 @@
 
-drvfail004.hs:8:12:
-    No instance for (Eq (Foo a b))
-      arising from the 'deriving' clause of a data type declaration
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
-    When deriving the instance for (Ord (Foo a b))
+drvfail004.hs:8:12: error:
+    • Could not deduce (Eq (Foo a b))
+        arising from the 'deriving' clause of a data type declaration
+      from the context: (Ord b, Ord a)
+        bound by the deriving clause for ‘Ord (Foo a b)’
+        at drvfail004.hs:8:12-14
+      Possible fix:
+        use a standalone 'deriving instance' declaration,
+          so you can specify the instance context yourself
+    • When deriving the instance for (Ord (Foo a b))
diff --git a/testsuite/tests/deriving/should_fail/drvfail012.stderr b/testsuite/tests/deriving/should_fail/drvfail012.stderr
index 602033fecd..a3becc4197 100644
--- a/testsuite/tests/deriving/should_fail/drvfail012.stderr
+++ b/testsuite/tests/deriving/should_fail/drvfail012.stderr
@@ -1,8 +1,11 @@
 
-drvfail012.hs:5:33:
-    No instance for (Eq (Ego a))
-      arising from the 'deriving' clause of a data type declaration
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
-    When deriving the instance for (Ord (Ego a))
+drvfail012.hs:5:33: error:
+    • Could not deduce (Eq (Ego a))
+        arising from the 'deriving' clause of a data type declaration
+      from the context: Ord a
+        bound by the deriving clause for ‘Ord (Ego a)’
+        at drvfail012.hs:5:33-35
+      Possible fix:
+        use a standalone 'deriving instance' declaration,
+          so you can specify the instance context yourself
+    • When deriving the instance for (Ord (Ego a))
diff --git a/testsuite/tests/typecheck/should_fail/tcfail046.stderr b/testsuite/tests/typecheck/should_fail/tcfail046.stderr
index c144130fe4..967b5a0fe6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail046.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail046.stderr
@@ -1,18 +1,21 @@
 
 tcfail046.hs:10:50: error:
-    No instance for (Eq (Process a))
-      arising from the first field of ‘Do’ (type ‘Process a’)
-      (maybe you haven't applied a function to enough arguments?)
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
-    When deriving the instance for (Eq (Continuation a))
+    • No instance for (Eq (Process a))
+        arising from the first field of ‘Do’ (type ‘Process a’)
+        (maybe you haven't applied a function to enough arguments?)
+      Possible fix:
+        use a standalone 'deriving instance' declaration,
+          so you can specify the instance context yourself
+    • When deriving the instance for (Eq (Continuation a))
 
 tcfail046.hs:22:25: error:
-    No instance for (Eq (Process a))
-      arising from the first field of ‘Create’ (type ‘Process a’)
-      (maybe you haven't applied a function to enough arguments?)
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
-    When deriving the instance for (Eq (Message a))
+    • Could not deduce (Eq (Process a))
+        arising from the first field of ‘Create’ (type ‘Process a’)
+        (maybe you haven't applied a function to enough arguments?)
+      from the context: Eq a
+        bound by the deriving clause for ‘Eq (Message a)’
+        at tcfail046.hs:22:25-26
+      Possible fix:
+        use a standalone 'deriving instance' declaration,
+          so you can specify the instance context yourself
+    • When deriving the instance for (Eq (Message a))
diff --git a/testsuite/tests/typecheck/should_fail/tcfail169.stderr b/testsuite/tests/typecheck/should_fail/tcfail169.stderr
index 75ae3a41a4..bc72c3c423 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail169.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail169.stderr
@@ -1,8 +1,11 @@
 
-tcfail169.hs:7:51:
-    No instance for (Show (Succ a))
-      arising from the second field of ‘Cons’ (type ‘Seq (Succ a)’)
-    Possible fix:
-      use a standalone 'deriving instance' declaration,
-        so you can specify the instance context yourself
-    When deriving the instance for (Show (Seq a))
+tcfail169.hs:7:51: error:
+    • Could not deduce (Show (Succ a))
+        arising from the second field of ‘Cons’ (type ‘Seq (Succ a)’)
+      from the context: Show a
+        bound by the deriving clause for ‘Show (Seq a)’
+        at tcfail169.hs:7:51-54
+      Possible fix:
+        use a standalone 'deriving instance' declaration,
+          so you can specify the instance context yourself
+    • When deriving the instance for (Show (Seq a))