Instantiate field types properly in stock-derived instances

Previously, the `deriving` machinery was very loosey-goosey about how it used
the types of data constructor fields when generating code. It would usually
just consult `dataConOrigArgTys`, which returns the _uninstantiated_ field
types of each data constructor. Usually, you can get away with this, but
issues #20375 and #20387 revealed circumstances where this approach fails.

Instead, when generated code for a stock-derived instance
`C (T arg_1 ... arg_n)`, one must take care to instantiate the field types of
each data constructor with `arg_1 ... arg_n`. The particulars of how this is
accomplished is described in the new
`Note [Instantiating field types in stock deriving]` in
`GHC.Tc.Deriv.Generate`. Some highlights:

* `DerivInstTys` now has a new `dit_dc_inst_arg_env :: DataConEnv [Type]`
  field that caches the instantiated field types of each data constructor.
  Whenever we need to consult the field types somewhere in `GHC.Tc.Deriv.*`
  we avoid using `dataConOrigArgTys` and instead look it up in
  `dit_dc_inst_arg_env`.
* Because `DerivInstTys` now stores the instantiated field types of each
  constructor, some of the details of the `GHC.Tc.Deriv.Generics.mkBindsRep`
  function were able to be simplified. In particular, we no longer need to
  apply a substitution to instantiate the field types in a `Rep(1)` instance,
  as that is already done for us by `DerivInstTys`. We still need a
  substitution to implement the "wrinkle" section of
  `Note [Generating a correctly typed Rep instance]`, but the code is
  nevertheless much simpler than before.
* The `tyConInstArgTys` function has been removed in favor of the new
  `GHC.Core.DataCon.dataConInstUnivs` function, which is really the proper tool
  for the job. `dataConInstUnivs` is much like `tyConInstArgTys` except that it
  takes a data constructor, not a type constructor, as an argument, and it adds
  extra universal type variables from that data constructor at the end of the
  returned list if need be. `dataConInstUnivs` takes care to instantiate the
  kinds of the universal type variables at the end, thereby avoiding a bug in
  `tyConInstArgTys` discovered in
  https://gitlab.haskell.org/ghc/ghc/-/issues/20387#note_377037.

Fixes #20375. Fixes #20387.

14 files changed, 599 insertions, 266 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index dc14f2dcc3..e95e68441f 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -41,6 +41,7 @@ module GHC.Core.DataCon (
         dataConOtherTheta,
         dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
         dataConInstOrigArgTys, dataConRepArgTys,
+        dataConInstUnivs,
         dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
         dataConSrcBangs,
         dataConSourceArity, dataConRepArity,
@@ -71,6 +72,7 @@ import GHC.Core.Type as Type
 import GHC.Core.Coercion
 import GHC.Core.Unify
 import GHC.Core.TyCon
+import GHC.Core.TyCo.Subst
 import GHC.Core.Multiplicity
 import {-# SOURCE #-} GHC.Types.TyThing
 import GHC.Types.FieldLabel
@@ -80,6 +82,7 @@ import GHC.Types.Name
 import GHC.Builtin.Names
 import GHC.Core.Predicate
 import GHC.Types.Var
+import GHC.Types.Var.Env
 import GHC.Types.Basic
 import GHC.Data.FastString
 import GHC.Unit.Types
@@ -1489,6 +1492,59 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
     tyvars = univ_tvs ++ ex_tvs
     subst  = zipTCvSubst tyvars inst_tys
 
+-- | Given a data constructor @dc@ with /n/ universally quantified type
+-- variables @a_{1}@, @a_{2}@, ..., @a_{n}@, and given a list of argument
+-- types @dc_args@ of length /m/ where /m/ <= /n/, then:
+--
+-- @
+-- dataConInstUnivs dc dc_args
+-- @
+--
+-- Will return:
+--
+-- @
+-- [dc_arg_{1}, dc_arg_{2}, ..., dc_arg_{m}, a_{m+1}, ..., a_{n}]
+-- @
+--
+-- That is, return the list of universal type variables with
+-- @a_{1}@, @a_{2}@, ..., @a_{m}@ instantiated with
+-- @dc_arg_{1}@, @dc_arg_{2}@, ..., @dc_arg_{m}@. It is possible for @m@ to
+-- be less than @n@, in which case the remaining @n - m@ elements will simply
+-- be universal type variables (with their kinds possibly instantiated).
+--
+-- Examples:
+--
+-- * Given the data constructor @D :: forall a b. Foo a b@ and
+--   @dc_args@ @[Int, Bool]@, then @dataConInstUnivs D dc_args@ will return
+--   @[Int, Bool]@.
+--
+-- * Given the data constructor @D :: forall a b. Foo a b@ and
+--   @dc_args@ @[Int]@, then @@dataConInstUnivs D dc_args@ will return
+--   @[Int, b]@.
+--
+-- * Given the data constructor @E :: forall k (a :: k). Bar k a@ and
+--   @dc_args@ @[Type]@, then @@dataConInstUnivs D dc_args@ will return
+--   @[Type, (a :: Type)]@.
+--
+-- This is primarily used in @GHC.Tc.Deriv.*@ in service of instantiating data
+-- constructors' field types.
+-- See @Note [Instantiating field types in stock deriving]@ for a notable
+-- example of this.
+dataConInstUnivs :: DataCon -> [Type] -> [Type]
+dataConInstUnivs dc dc_args = chkAppend dc_args $ map mkTyVarTy dc_args_suffix
+  where
+    (dc_univs_prefix, dc_univs_suffix)
+                        = -- Assert that m <= n
+                          assertPpr (dc_args `leLength` dataConUnivTyVars dc)
+                                    (text "dataConInstUnivs"
+                                      <+> ppr dc_args
+                                      <+> ppr (dataConUnivTyVars dc)) $
+                          splitAt (length dc_args) $ dataConUnivTyVars dc
+    (_, dc_args_suffix) = substTyVarBndrs prefix_subst dc_univs_suffix
+    prefix_subst        = mkTvSubst prefix_in_scope prefix_env
+    prefix_in_scope     = mkInScopeSet $ tyCoVarsOfTypes dc_args
+    prefix_env          = zipTyEnv dc_univs_prefix dc_args
+
 -- | Returns the argument types of the wrapper, excluding all dictionary arguments
 -- and without substituting for any type variables
 dataConOrigArgTys :: DataCon -> [Scaled Type]
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 708239c0ba..bf95f5c58f 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -5,6 +5,7 @@
 -}
 
 
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE TypeFamilies #-}
 
@@ -1241,11 +1242,13 @@ mk_deriv_inst_tys_maybe fam_envs cls_tys inst_ty =
       -- Find the instance of a data family
       -- Note [Looking up family instances for deriving]
       let (rep_tc, rep_tc_args, _co) = tcLookupDataFamInst fam_envs tc tc_args
-      in DerivInstTys { dit_cls_tys     = cls_tys
-                      , dit_tc          = tc
-                      , dit_tc_args     = tc_args
-                      , dit_rep_tc      = rep_tc
-                      , dit_rep_tc_args = rep_tc_args }
+          dc_inst_arg_env = buildDataConInstArgEnv rep_tc rep_tc_args
+      in DerivInstTys { dit_cls_tys         = cls_tys
+                      , dit_tc              = tc
+                      , dit_tc_args         = tc_args
+                      , dit_rep_tc          = rep_tc
+                      , dit_rep_tc_args     = rep_tc_args
+                      , dit_dc_inst_arg_env = dc_inst_arg_env }
 
 {-
 Note [Looking up family instances for deriving]
@@ -1327,7 +1330,7 @@ mk_eqn_from_mechanism mechanism
        dfun_name <- lift $ newDFunName cls inst_tys loc
        case deriv_ctxt of
         InferContext wildcard ->
-          do { (inferred_constraints, tvs', inst_tys')
+          do { (inferred_constraints, tvs', inst_tys', mechanism')
                  <- inferConstraints mechanism
              ; return $ InferTheta $ DS
                    { ds_loc = loc
@@ -1336,7 +1339,7 @@ mk_eqn_from_mechanism mechanism
                    , ds_theta = inferred_constraints
                    , ds_overlap = overlap_mode
                    , ds_standalone_wildcard = wildcard
-                   , ds_mechanism = mechanism } }
+                   , ds_mechanism = mechanism' } }
 
         SupplyContext theta ->
             return $ GivenTheta $ DS
@@ -1351,12 +1354,10 @@ mk_eqn_from_mechanism mechanism
 mk_eqn_stock :: DerivInstTys -- Information about the arguments to the class
              -> DerivM EarlyDerivSpec
 mk_eqn_stock dit
-  = do DerivEnv { denv_cls  = cls
-                , denv_ctxt = deriv_ctxt } <- ask
-       dflags <- getDynFlags
+  = do dflags <- getDynFlags
        let isDeriveAnyClassEnabled =
              deriveAnyClassEnabled (xopt LangExt.DeriveAnyClass dflags)
-       case checkOriginativeSideConditions dflags deriv_ctxt cls dit of
+       checkOriginativeSideConditions dit >>= \case
          CanDeriveStock gen_fn -> mk_eqn_from_mechanism $
                                   DerivSpecStock { dsm_stock_dit    = dit
                                                  , dsm_stock_gen_fn = gen_fn }
@@ -1430,8 +1431,6 @@ mk_eqn_no_strategy = do
     mk_eqn_originative :: DerivInstTys -> DerivM EarlyDerivSpec
     mk_eqn_originative dit@(DerivInstTys { dit_tc     = tc
                                          , dit_rep_tc = rep_tc }) = do
-      DerivEnv { denv_cls  = cls
-               , denv_ctxt = deriv_ctxt } <- ask
       dflags <- getDynFlags
       let isDeriveAnyClassEnabled =
             deriveAnyClassEnabled (xopt LangExt.DeriveAnyClass dflags)
@@ -1443,7 +1442,7 @@ mk_eqn_no_strategy = do
             | otherwise
             = DerivErrNotStockDeriveable isDeriveAnyClassEnabled
 
-      case checkOriginativeSideConditions dflags deriv_ctxt cls dit of
+      checkOriginativeSideConditions dit >>= \case
         NonDerivableClass     -> derivingThingFailWith NoGeneralizedNewtypeDeriving dac_error
         StockClassError why   -> derivingThingFailWith NoGeneralizedNewtypeDeriving why
         CanDeriveStock gen_fn -> mk_eqn_from_mechanism $
@@ -1474,8 +1473,7 @@ mkNewTypeEqn newtype_strat dit@(DerivInstTys { dit_cls_tys     = cls_tys
                                              , dit_rep_tc      = rep_tycon
                                              , dit_rep_tc_args = rep_tc_args })
 -- Want: instance (...) => cls (cls_tys ++ [tycon tc_args]) where ...
-  = do DerivEnv { denv_cls   = cls
-                , denv_ctxt  = deriv_ctxt } <- ask
+  = do DerivEnv{denv_cls = cls} <- ask
        dflags <- getDynFlags
 
        let newtype_deriving  = xopt LangExt.GeneralizedNewtypeDeriving dflags
@@ -1567,7 +1565,7 @@ mkNewTypeEqn newtype_strat dit@(DerivInstTys { dit_cls_tys     = cls_tys
              && ((newtype_deriving && not deriveAnyClass)
                   || std_class_via_coercible cls)
          then mk_eqn_newtype dit rep_inst_ty
-         else case checkOriginativeSideConditions dflags deriv_ctxt cls dit of
+         else checkOriginativeSideConditions dit >>= \case
                StockClassError why
                  -- There's a particular corner case where
                  --
diff --git a/compiler/GHC/Tc/Deriv/Functor.hs b/compiler/GHC/Tc/Deriv/Functor.hs
index 204c8ce88d..1f781398ca 100644
--- a/compiler/GHC/Tc/Deriv/Functor.hs
+++ b/compiler/GHC/Tc/Deriv/Functor.hs
@@ -163,8 +163,8 @@ gen_Functor_binds loc (DerivInstTys{dit_rep_tc = tycon})
                                coerce_Expr]
     fmap_match_ctxt = mkPrefixFunRhs fmap_name
 
-gen_Functor_binds loc (DerivInstTys{ dit_rep_tc = tycon
-                                   , dit_rep_tc_args = tycon_args })
+gen_Functor_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                       , dit_rep_tc_args = tycon_args })
   = (listToBag [fmap_bind, replace_bind], emptyBag)
   where
     data_cons = getPossibleDataCons tycon tycon_args
@@ -177,7 +177,7 @@ gen_Functor_binds loc (DerivInstTys{ dit_rep_tc = tycon
     fmap_eqn con = flip evalState bs_RDRs $
                      match_for_con fmap_match_ctxt [f_Pat] con parts
       where
-        parts = foldDataConArgs ft_fmap con
+        parts = foldDataConArgs ft_fmap con dit
 
     fmap_eqns = map fmap_eqn data_cons
 
@@ -216,7 +216,7 @@ gen_Functor_binds loc (DerivInstTys{ dit_rep_tc = tycon
     replace_eqn con = flip evalState bs_RDRs $
         match_for_con replace_match_ctxt [z_Pat] con parts
       where
-        parts = foldDataConArgs ft_replace con
+        parts = foldDataConArgs ft_replace con dit
 
     replace_eqns = map replace_eqn data_cons
 
@@ -553,10 +553,10 @@ deepSubtypesContaining tv
             , ft_forall = \v xs -> filterOut ((v `elemVarSet`) . tyCoVarsOfType) xs })
 
 
-foldDataConArgs :: FFoldType a -> DataCon -> [a]
+foldDataConArgs :: FFoldType a -> DataCon -> DerivInstTys -> [a]
 -- Fold over the arguments of the datacon
-foldDataConArgs ft con
-  = map foldArg (map scaledThing $ dataConOrigArgTys con)
+foldDataConArgs ft con dit
+  = map foldArg (derivDataConInstArgTys con dit)
   where
     foldArg
       = case getTyVar_maybe (last (tyConAppArgs (dataConOrigResTy con))) of
@@ -798,8 +798,8 @@ gen_Foldable_binds loc (DerivInstTys{dit_rep_tc = tycon})
                                   mempty_Expr]
     foldMap_match_ctxt = mkPrefixFunRhs foldMap_name
 
-gen_Foldable_binds loc (DerivInstTys{ dit_rep_tc = tycon
-                                    , dit_rep_tc_args = tycon_args })
+gen_Foldable_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                        , dit_rep_tc_args = tycon_args })
   | null data_cons  -- There's no real point producing anything but
                     -- foldMap for a type with no constructors.
   = (unitBag foldMap_bind, emptyBag)
@@ -816,7 +816,7 @@ gen_Foldable_binds loc (DerivInstTys{ dit_rep_tc = tycon
     foldr_eqn con
       = evalState (match_foldr z_Expr [f_Pat,z_Pat] con =<< parts) bs_RDRs
       where
-        parts = sequence $ foldDataConArgs ft_foldr con
+        parts = sequence $ foldDataConArgs ft_foldr con dit
     foldr_match_ctxt = mkPrefixFunRhs foldr_name
 
     foldMap_name = L (noAnnSrcSpan loc) foldMap_RDR
@@ -830,7 +830,7 @@ gen_Foldable_binds loc (DerivInstTys{ dit_rep_tc = tycon
     foldMap_eqn con
       = evalState (match_foldMap [f_Pat] con =<< parts) bs_RDRs
       where
-        parts = sequence $ foldDataConArgs ft_foldMap con
+        parts = sequence $ foldDataConArgs ft_foldMap con dit
     foldMap_match_ctxt = mkPrefixFunRhs foldMap_name
 
     -- Given a list of NullM results, produce Nothing if any of
@@ -849,7 +849,7 @@ gen_Foldable_binds loc (DerivInstTys{ dit_rep_tc = tycon
     null_eqns = map null_eqn data_cons
     null_eqn con
       = flip evalState bs_RDRs $ do
-          parts <- sequence $ foldDataConArgs ft_null con
+          parts <- sequence $ foldDataConArgs ft_null con dit
           case convert parts of
             Nothing -> return $
               mkMatch null_match_ctxt [nlParPat (nlWildConPat con)]
@@ -1033,8 +1033,8 @@ gen_Traversable_binds loc (DerivInstTys{dit_rep_tc = tycon})
                        (nlHsApps pure_RDR [nlHsApp coerce_Expr z_Expr])]
     traverse_match_ctxt = mkPrefixFunRhs traverse_name
 
-gen_Traversable_binds loc (DerivInstTys{ dit_rep_tc = tycon
-                                       , dit_rep_tc_args = tycon_args })
+gen_Traversable_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                           , dit_rep_tc_args = tycon_args })
   = (unitBag traverse_bind, emptyBag)
   where
     data_cons = getPossibleDataCons tycon tycon_args
@@ -1048,7 +1048,7 @@ gen_Traversable_binds loc (DerivInstTys{ dit_rep_tc = tycon
     traverse_eqn con
       = evalState (match_for_con [f_Pat] con =<< parts) bs_RDRs
       where
-        parts = sequence $ foldDataConArgs ft_trav con
+        parts = sequence $ foldDataConArgs ft_trav con dit
     traverse_match_ctxt = mkPrefixFunRhs traverse_name
 
     -- Yields 'Just' an expression if we're folding over a type that mentions
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 79843eb77f..e3856765ec 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -36,8 +36,9 @@ module GHC.Tc.Deriv.Generate (
         ordOpTbl, boxConTbl, litConTbl,
         mkRdrFunBind, mkRdrFunBindEC, mkRdrFunBindSE, error_Expr,
 
-        getPossibleDataCons, tyConInstArgTys,
-        DerivInstTys(..)
+        getPossibleDataCons,
+        DerivInstTys(..), buildDataConInstArgEnv,
+        derivDataConInstArgTys, substDerivInstTys
     ) where
 
 import GHC.Prelude
@@ -68,11 +69,12 @@ import GHC.Core.Coercion.Axiom ( coAxiomSingleBranch )
 import GHC.Builtin.Types.Prim
 import GHC.Builtin.Types
 import GHC.Core.Type
-import GHC.Core.Multiplicity
 import GHC.Core.Class
+import GHC.Types.Unique.FM ( lookupUFM )
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
 import GHC.Utils.Misc
+import GHC.Types.Unique.FM ( listToUFM )
 import GHC.Types.Var
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
@@ -214,8 +216,8 @@ produced don't get through the typechecker.
 -}
 
 gen_Eq_binds :: SrcSpan -> DerivInstTys -> TcM (LHsBinds GhcPs, BagDerivStuff)
-gen_Eq_binds loc (DerivInstTys{ dit_rep_tc = tycon
-                              , dit_rep_tc_args = tycon_args }) = do
+gen_Eq_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                  , dit_rep_tc_args = tycon_args }) = do
     return (method_binds, emptyBag)
   where
     all_cons = getPossibleDataCons tycon tycon_args
@@ -260,9 +262,9 @@ gen_Eq_binds loc (DerivInstTys{ dit_rep_tc = tycon
             con_arity   = length tys_needed
             as_needed   = take con_arity as_RDRs
             bs_needed   = take con_arity bs_RDRs
-            tys_needed  = dataConOrigArgTys data_con
+            tys_needed  = derivDataConInstArgTys data_con dit
         in
-        ([con1_pat, con2_pat], nested_eq_expr (map scaledThing tys_needed) as_needed bs_needed)
+        ([con1_pat, con2_pat], nested_eq_expr tys_needed as_needed bs_needed)
       where
         nested_eq_expr []  [] [] = true_Expr
         nested_eq_expr tys as bs
@@ -391,8 +393,8 @@ gtResult OrdGT      = true_Expr
 
 ------------
 gen_Ord_binds :: SrcSpan -> DerivInstTys -> TcM (LHsBinds GhcPs, BagDerivStuff)
-gen_Ord_binds loc (DerivInstTys{ dit_rep_tc = tycon
-                               , dit_rep_tc_args = tycon_args }) = do
+gen_Ord_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                   , dit_rep_tc_args = tycon_args }) = do
     return $ if null tycon_data_cons -- No data-cons => invoke bale-out case
       then ( unitBag $ mkFunBindEC 2 loc compare_RDR (const eqTag_Expr) []
            , emptyBag)
@@ -510,7 +512,7 @@ gen_Ord_binds loc (DerivInstTys{ dit_rep_tc = tycon
     -- Returns a case alternative  Ki b1 b2 ... bv -> compare (a1,a2,...) with (b1,b2,...)
     mkInnerEqAlt op data_con
       = mkHsCaseAlt (nlConVarPat data_con_RDR bs_needed) $
-        mkCompareFields op (map scaledThing $ dataConOrigArgTys data_con)
+        mkCompareFields op (derivDataConInstArgTys data_con dit)
       where
         data_con_RDR = getRdrName data_con
         bs_needed    = take (dataConSourceArity data_con) bs_RDRs
@@ -1021,7 +1023,7 @@ we want to be able to parse (Left 3) just fine.
 gen_Read_binds :: (Name -> Fixity) -> SrcSpan -> DerivInstTys
                -> (LHsBinds GhcPs, BagDerivStuff)
 
-gen_Read_binds get_fixity loc (DerivInstTys{dit_rep_tc = tycon})
+gen_Read_binds get_fixity loc dit@(DerivInstTys{dit_rep_tc = tycon})
   = (listToBag [read_prec, default_readlist, default_readlistprec], emptyBag)
   where
     -----------------------------------------------------------------------
@@ -1110,7 +1112,7 @@ gen_Read_binds get_fixity loc (DerivInstTys{dit_rep_tc = tycon})
         is_infix     = dataConIsInfix data_con
         is_record    = labels `lengthExceeds` 0
         as_needed    = take con_arity as_RDRs
-        read_args    = zipWithEqual "gen_Read_binds" read_arg as_needed (map scaledThing $ dataConOrigArgTys data_con)
+        read_args    = zipWithEqual "gen_Read_binds" read_arg as_needed (derivDataConInstArgTys data_con dit)
         (read_a1:read_a2:_) = read_args
 
         prefix_prec = appPrecedence
@@ -1205,8 +1207,8 @@ Example
 gen_Show_binds :: (Name -> Fixity) -> SrcSpan -> DerivInstTys
                -> (LHsBinds GhcPs, BagDerivStuff)
 
-gen_Show_binds get_fixity loc (DerivInstTys{ dit_rep_tc = tycon
-                                           , dit_rep_tc_args = tycon_args })
+gen_Show_binds get_fixity loc dit@(DerivInstTys{ dit_rep_tc = tycon
+                                               , dit_rep_tc_args = tycon_args })
   = (unitBag shows_prec, emptyBag)
   where
     data_cons = getPossibleDataCons tycon tycon_args
@@ -1226,7 +1228,7 @@ gen_Show_binds get_fixity loc (DerivInstTys{ dit_rep_tc = tycon
              data_con_RDR  = getRdrName data_con
              con_arity     = dataConSourceArity data_con
              bs_needed     = take con_arity bs_RDRs
-             arg_tys       = dataConOrigArgTys data_con         -- Correspond 1-1 with bs_needed
+             arg_tys       = derivDataConInstArgTys data_con dit -- Correspond 1-1 with bs_needed
              con_pat       = nlConVarPat data_con_RDR bs_needed
              nullary_con   = con_arity == 0
              labels        = map flLabel $ dataConFieldLabels data_con
@@ -1254,7 +1256,7 @@ gen_Show_binds get_fixity loc (DerivInstTys{ dit_rep_tc = tycon
                  where
                    nm       = wrapOpParens (unpackFS l)
 
-             show_args               = zipWithEqual "gen_Show_binds" show_arg bs_needed (map scaledThing arg_tys)
+             show_args               = zipWithEqual "gen_Show_binds" show_arg bs_needed arg_tys
              (show_arg1:show_arg2:_) = show_args
              show_prefix_args        = intersperse (nlHsVar showSpace_RDR) show_args
 
@@ -2646,36 +2648,31 @@ newAuxBinderRdrName loc parent occ_fun = do
 getPossibleDataCons :: TyCon -> [Type] -> [DataCon]
 getPossibleDataCons tycon tycon_args = filter isPossible $ tyConDataCons tycon
   where
-    isPossible = not . dataConCannotMatch (tyConInstArgTys tycon tycon_args)
+    isPossible dc = not $ dataConCannotMatch (dataConInstUnivs dc tycon_args) dc
 
--- | Given a type constructor @tycon@ of arity /n/ and a list of argument types
--- @tycon_args@ of length /m/,
+-- | Information about the arguments to the class in a stock- or
+-- newtype-derived instance. For a @deriving@-generated instance declaration
+-- such as this one:
 --
 -- @
--- tyConInstArgTys tycon tycon_args
+-- instance Ctx => Cls cls_ty_1 ... cls_ty_m (TC tc_arg_1 ... tc_arg_n) where ...
 -- @
 --
--- returns
---
--- @
--- [tycon_arg_{1}, tycon_arg_{2}, ..., tycon_arg_{m}, extra_arg_{m+1}, ..., extra_arg_{n}]
--- @
+-- * 'dit_cls_tys' corresponds to @cls_ty_1 ... cls_ty_m@.
 --
--- where @extra_args@ are distinct type variables.
+-- * 'dit_tc' corresponds to @TC@.
 --
--- Examples:
+-- * 'dit_tc_args' corresponds to @tc_arg_1 ... tc_arg_n@.
 --
--- * Given @tycon: Foo a b@ and @tycon_args: [Int, Bool]@, return @[Int, Bool]@.
+-- See @Note [DerivEnv and DerivSpecMechanism]@ in "GHC.Tc.Deriv.Utils" for a
+-- more in-depth explanation, including the relationship between
+-- 'dit_tc'/'dit_rep_tc' and 'dit_tc_args'/'dit_rep_tc_args'.
 --
--- * Given @tycon: Foo a b@ and @tycon_args: [Int]@, return @[Int, b]@.
-tyConInstArgTys :: TyCon -> [Type] -> [Type]
-tyConInstArgTys tycon tycon_args = chkAppend tycon_args $ map mkTyVarTy tycon_args_suffix
-  where
-    tycon_args_suffix = drop (length tycon_args) $ tyConTyVars tycon
-
--- | Information about the arguments to the class in a stock- or
--- newtype-derived instance.
--- See @Note [DerivEnv and DerivSpecMechanism]@.
+-- A 'DerivInstTys' value can be seen as a more structured representation of
+-- the 'denv_inst_tys' in a 'DerivEnv', as the 'denv_inst_tys' is equal to
+-- @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'.
 data DerivInstTys = DerivInstTys
   { dit_cls_tys     :: [Type]
     -- ^ Other arguments to the class except the last
@@ -2690,17 +2687,68 @@ data DerivInstTys = DerivInstTys
   , dit_rep_tc_args :: [Type]
     -- ^ The representation types for 'dit_tc_args'
     --   (for data family instances). Otherwise the same as 'dit_tc_args'.
+  , dit_dc_inst_arg_env :: DataConEnv [Type]
+    -- ^ The cached results of instantiating each data constructor's field
+    --   types using @'dataConInstUnivs' data_con 'dit_rep_tc_args'@.
+    --   See @Note [Instantiating field types in stock deriving]@.
+    --
+    --   This field is only used for stock-derived instances and goes unused
+    --   for newtype-derived instances. It is put here mainly for the sake of
+    --   convenience.
   }
 
 instance Outputable DerivInstTys where
   ppr (DerivInstTys { dit_cls_tys = cls_tys, dit_tc = tc, dit_tc_args = tc_args
-                    , dit_rep_tc = rep_tc, dit_rep_tc_args = rep_tc_args })
+                    , dit_rep_tc = rep_tc, dit_rep_tc_args = rep_tc_args
+                    , dit_dc_inst_arg_env = dc_inst_arg_env })
     = hang (text "DerivInstTys")
-         2 (vcat [ text "dit_cls_tys"     <+> ppr cls_tys
-                 , text "dit_tc"          <+> ppr tc
-                 , text "dit_tc_args"     <+> ppr tc_args
-                 , text "dit_rep_tc"      <+> ppr rep_tc
-                 , text "dit_rep_tc_args" <+> ppr rep_tc_args ])
+         2 (vcat [ text "dit_cls_tys"         <+> ppr cls_tys
+                 , text "dit_tc"              <+> ppr tc
+                 , text "dit_tc_args"         <+> ppr tc_args
+                 , text "dit_rep_tc"          <+> ppr rep_tc
+                 , text "dit_rep_tc_args"     <+> ppr rep_tc_args
+                 , text "dit_dc_inst_arg_env" <+> ppr dc_inst_arg_env ])
+
+-- | Look up a data constructor's instantiated field types in a 'DerivInstTys'.
+-- See @Note [Instantiating field types in stock deriving]@.
+derivDataConInstArgTys :: DataCon -> DerivInstTys -> [Type]
+derivDataConInstArgTys dc dit =
+  case lookupUFM (dit_dc_inst_arg_env dit) dc of
+    Just inst_arg_tys -> inst_arg_tys
+    Nothing           -> pprPanic "derivDataConInstArgTys" (ppr dc)
+
+-- | @'buildDataConInstArgEnv' tycon arg_tys@ constructs a cache that maps
+-- each of @tycon@'s data constructors to their field types, with are to be
+-- instantiated with @arg_tys@.
+-- See @Note [Instantiating field types in stock deriving]@.
+buildDataConInstArgEnv :: TyCon -> [Type] -> DataConEnv [Type]
+buildDataConInstArgEnv rep_tc rep_tc_args =
+  listToUFM [ (dc, inst_arg_tys)
+            | dc <- tyConDataCons rep_tc
+            , let (_, _, inst_arg_tys) =
+                    dataConInstSig dc $ dataConInstUnivs dc rep_tc_args
+            ]
+
+-- | Apply a substitution to all of the 'Type's contained in a 'DerivInstTys'.
+-- See @Note [Instantiating field types in stock deriving]@ for why we need to
+-- substitute into a 'DerivInstTys' in the first place.
+substDerivInstTys :: TCvSubst -> DerivInstTys -> DerivInstTys
+substDerivInstTys subst
+  dit@(DerivInstTys { dit_cls_tys = cls_tys, dit_tc_args = tc_args
+                    , dit_rep_tc = rep_tc, dit_rep_tc_args = rep_tc_args })
+
+  | isEmptyTCvSubst subst
+  = dit
+  | otherwise
+  = 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'
+       }
+  where
+    cls_tys'     = substTys subst cls_tys
+    tc_args'     = substTys subst tc_args
+    rep_tc_args' = substTys subst rep_tc_args
 
 {-
 Note [Auxiliary binders]
@@ -2971,4 +3019,82 @@ Classes that do not currently filter constructors may do so in the future, if
 there is a valid use-case and we have requirements for how they should work.
 
 See #16341 and the T16341.hs test case.
+
+Note [Instantiating field types in stock deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Figuring out what the types of data constructor fields are in `deriving` can
+be surprisingly tricky. Here are some examples (adapted from #20375) to set
+the scene:
+
+  data Ta = MkTa Int#
+  data Tb (x :: TYPE IntRep) = MkTb x
+
+  deriving instance Eq Ta        -- 1.
+  deriving instance Eq (Tb a)    -- 2.
+  deriving instance Eq (Tb Int#) -- 3.
+
+Example (1) is accepted, as `deriving Eq` has a special case for fields of type
+Int#. Example (2) is rejected, however, as the special case for Int# does not
+extend to all types of kind (TYPE IntRep).
+
+Example (3) ought to typecheck. If you instantiate the field of type `x` in
+MkTb to be Int#, then `deriving Eq` is capable of handling that. We must be
+careful, however. If we naïvely use, say, `dataConOrigArgTys` to retrieve the
+field types, then we would get `b`, which `deriving Eq` would reject. In
+order to handle `deriving Eq` (and, more generally, any stock deriving
+strategy) correctly, we /must/ instantiate the field types as needed.
+Not doing so led to #20375 and #20387.
+
+In fact, we end up needing to instantiate the field types in quite a few
+places:
+
+* When performing validity checks for stock deriving strategies (e.g., in
+  GHC.Tc.Deriv.Utils.cond_stdOK)
+
+* When inferring the instance context in
+  GHC.Tc.Deriv.Infer.inferConstraintStock
+
+* When generating code for stock-derived instances in
+  GHC.Tc.Deriv.{Functor,Generate,Generics}
+
+Repeatedly performing these instantiations in multiple places would be
+wasteful, so we build a cache of data constructor field instantiations in
+the `dit_dc_inst_arg_env` field of DerivInstTys. Specifically:
+
+1. When beginning to generate code for a stock-derived instance
+   `T arg_1 ... arg_n`, the `dit_dc_inst_arg_env` field is created by taking
+   each data constructor `dc`, instantiating its field types with
+   `dataConInstUnivs dc [arg_1, ..., arg_n]`, and mapping `dc` to the
+   instantiated field types in the cache. The `buildDataConInstArgEnv` function
+   is responsible for orchestrating this.
+
+2. When a part of the code in GHC.Tc.Deriv.* needs to look up the field
+   types, we deliberately avoid using `dataConOrigArgTys`. Instead, we use
+   `derivDataConInstArgTys`, which looks up a DataCon's instantiated field
+   types in the cache.
+
+StandaloneDeriving is one way for the field types to become instantiated.
+Another way is by deriving Functor and related classes, as chronicled in
+Note [Inferring the instance context] in GHC.Tc.Deriv.Infer. Here is one such
+example:
+
+  newtype Compose (f :: k -> Type) (g :: j -> k) (a :: j) = Compose (f (g a))
+    deriving Generic1
+
+This ultimately generates the following instance:
+
+  instance forall (f :: Type -> Type) (g :: j -> Type).
+    Functor f => Generic1 (Compose f g) where ...
+
+Note that because of the inferred `Functor f` constraint, `k` was instantiated
+to be `Type`. GHC's deriving machinery doesn't realize this until it performs
+constraint inference (in GHC.Tc.Deriv.Infer.inferConstraintsStock), however,
+which is *after* the initial DerivInstTys has been created. As a result, the
+`dit_dc_inst_arg_env` field might need to be updated after constraint inference,
+as the inferred constraints might instantiate the field types further.
+
+This is accomplished by way of `substDerivInstTys`, which substitutes all of
+the fields in a `DerivInstTys`, including the `dit_dc_inst_arg_env`.
+It is important to do this in inferConstraintsStock, as the
+deriving/should_compile/T20387 test case will not compile otherwise.
 -}
diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs
index db7bf0fc8b..a6969170c9 100644
--- a/compiler/GHC/Tc/Deriv/Generics.hs
+++ b/compiler/GHC/Tc/Deriv/Generics.hs
@@ -31,7 +31,6 @@ import GHC.Tc.Errors.Types
 import GHC.Core.DataCon
 import GHC.Core.TyCon
 import GHC.Core.FamInstEnv ( FamInst, FamFlavor(..), mkSingleCoAxiom )
-import GHC.Core.Multiplicity
 import GHC.Tc.Instance.Family
 import GHC.Unit.Module ( moduleName, moduleNameFS
                         , moduleUnit, unitFS, getModule )
@@ -156,7 +155,7 @@ canDoGenerics :: DerivInstTys -> Validity' [DeriveGenericsErrReason]
 --
 -- It returns IsValid if deriving is possible. It returns (NotValid reason)
 -- if not.
-canDoGenerics (DerivInstTys{dit_rep_tc = tc})
+canDoGenerics dit@(DerivInstTys{dit_rep_tc = tc})
   = mergeErrors (
           -- Check (b) from Note [Requirements for deriving Generic and Rep].
               (if (not (null (tyConStupidTheta tc)))
@@ -178,7 +177,7 @@ canDoGenerics (DerivInstTys{dit_rep_tc = tc})
         -- it relies on instantiating *polymorphic* sum and product types
         -- at the argument types of the constructors
     bad_con :: DataCon -> Validity' DeriveGenericsErrReason
-    bad_con dc = if any bad_arg_type (map scaledThing $ dataConOrigArgTys dc)
+    bad_con dc = if any bad_arg_type (derivDataConInstArgTys dc dit)
                   then NotValid $ DerivErrGenericsMustNotHaveExoticArgs dc
                   else if not (isVanillaDataCon dc)
                           then NotValid $ DerivErrGenericsMustBeVanillaDataCon dc
@@ -258,7 +257,7 @@ canDoGenerics1 dit@(DerivInstTys{dit_rep_tc = rep_tc}) =
     data_cons = tyConDataCons rep_tc
     check_con con = case check_vanilla con of
       j@(NotValid {}) -> [j]
-      IsValid -> _ccdg1_errors `map` foldDataConArgs (ft_check con) con
+      IsValid -> _ccdg1_errors `map` foldDataConArgs (ft_check con) con dit
 
     check_vanilla :: DataCon -> Validity' DeriveGenericsErrReason
     check_vanilla con | isVanillaDataCon con = IsValid
@@ -331,7 +330,7 @@ gk2gkDC Gen1_{} d = Gen1_DC $ last $ dataConUnivTyVars d
 
 -- Bindings for the Generic instance
 mkBindsRep :: DynFlags -> GenericKind -> DerivInstTys -> (LHsBinds GhcPs, [LSig GhcPs])
-mkBindsRep dflags gk (DerivInstTys{dit_rep_tc = tycon}) = (binds, sigs)
+mkBindsRep dflags gk dit@(DerivInstTys{dit_rep_tc = tycon}) = (binds, sigs)
       where
         binds = unitBag (mkRdrFunBind (L loc' from01_RDR) [from_eqn])
               `unionBags`
@@ -378,7 +377,7 @@ mkBindsRep dflags gk (DerivInstTys{dit_rep_tc = tycon}) = (binds, sigs)
 
         -- Recurse over the sum first
         from_alts, to_alts :: [Alt]
-        (from_alts, to_alts) = mkSum gk_ (1 :: US) datacons
+        (from_alts, to_alts) = mkSum gk_ (1 :: US) dit datacons
           where gk_ = case gk of
                   Gen0 -> Gen0_
                   Gen1 -> assert (tyvars `lengthAtLeast` 1) $
@@ -406,8 +405,6 @@ tc_mkRepFamInsts gk inst_tys dit@(DerivInstTys{dit_rep_tc = tycon}) =
          Gen0 -> tcLookupTyCon repTyConName
          Gen1 -> tcLookupTyCon rep1TyConName
 
-     ; fam_envs <- tcGetFamInstEnvs
-
      ; let -- If the derived instance is
            --   instance Generic (Foo x)
            -- then:
@@ -422,19 +419,10 @@ tc_mkRepFamInsts gk inst_tys dit@(DerivInstTys{dit_rep_tc = tycon}) =
              (Gen1, [arg_k, inst_t]) -> (arg_k,          inst_t)
              _ -> pprPanic "tc_mkRepFamInsts" (ppr inst_tys)
 
-     ; let mbFamInst         = tyConFamInst_maybe tycon
-           -- If we're examining a data family instance, we grab the parent
-           -- TyCon (ptc) and use it to determine the type arguments
-           -- (inst_args) for the data family *instance*'s type variables.
-           ptc               = maybe tycon fst mbFamInst
-           (_, inst_args, _) = tcLookupDataFamInst fam_envs ptc $ snd
-                                 $ tcSplitTyConApp inst_ty
-
-     ; let -- `tyvars` = [a,b]
-           (tyvars, gk_) = case gk of
-             Gen0 -> (all_tyvars, Gen0_)
+           gk_ = case gk of
+             Gen0 -> Gen0_
              Gen1 -> assert (not $ null all_tyvars)
-                     (init all_tyvars, Gen1_ $ last all_tyvars)
+                     Gen1_ $ last all_tyvars
              where all_tyvars = tyConTyVars tycon
 
        -- `repTy` = D1 ... (C1 ... (S1 ... (Rec0 a))) :: * -> *
@@ -447,19 +435,14 @@ tc_mkRepFamInsts gk inst_tys dit@(DerivInstTys{dit_rep_tc = tycon}) =
            rep_occ = case gk of Gen0 -> mkGenR tc_occ; Gen1 -> mkGen1R tc_occ
      ; rep_name <- newGlobalBinder mod rep_occ loc
 
-       -- We make sure to substitute the tyvars with their user-supplied
-       -- type arguments before generating the Rep/Rep1 instance, since some
-       -- of the tyvars might have been instantiated when deriving.
-       -- See Note [Generating a correctly typed Rep instance].
-     ; let (env_tyvars, env_inst_args)
-             = case gk_ of
-                 Gen0_ -> (tyvars, inst_args)
-                 Gen1_ last_tv
-                          -- See the "wrinkle" in
-                          -- Note [Generating a correctly typed Rep instance]
-                       -> ( last_tv : tyvars
-                          , anyTypeOfKind (tyVarKind last_tv) : inst_args )
-           env        = zipTyEnv env_tyvars env_inst_args
+       -- If deriving Generic1, make sure to substitute the last type variable
+       -- with Any in the generated Rep1 instance. This avoids issues like what
+       -- is documented in the "wrinkle" section of
+       -- Note [Generating a correctly typed Rep instance].
+     ; let env = case gk_ of
+                   Gen0_ -> emptyTvSubstEnv
+                   Gen1_ last_tv
+                     -> zipTyEnv [last_tv] [anyTypeOfKind (tyVarKind last_tv)]
            in_scope   = mkInScopeSet (tyCoVarsOfTypes inst_tys)
            subst      = mkTvSubst in_scope env
            repTy'     = substTyUnchecked  subst repTy
@@ -550,7 +533,7 @@ tc_mkRepTy ::  -- Gen0_ or Gen1_, for Rep or Rep1
             -> Kind
                -- Generated representation0 type
             -> TcM Type
-tc_mkRepTy gk_ (DerivInstTys{dit_rep_tc = tycon}) k =
+tc_mkRepTy gk_ dit@(DerivInstTys{dit_rep_tc = tycon}) k =
   do
     d1      <- tcLookupTyCon d1TyConName
     c1      <- tcLookupTyCon c1TyConName
@@ -600,8 +583,7 @@ tc_mkRepTy gk_ (DerivInstTys{dit_rep_tc = tycon}) k =
         mkD    a   = mkTyConApp d1 [ k, metaDataTy, sumP (tyConDataCons a) ]
         mkC      a = mkTyConApp c1 [ k
                                    , metaConsTy a
-                                   , prod (map scaledThing . dataConInstOrigArgTys a
-                                            . mkTyVarTys . tyConTyVars $ tycon)
+                                   , prod (derivDataConInstArgTys a dit)
                                           (dataConSrcBangs    a)
                                           (dataConImplBangs   a)
                                           (dataConFieldLabels a)]
@@ -732,41 +714,43 @@ mkBoxTy uAddr uChar uDouble uFloat uInt uWord rec0 k ty
 --------------------------------------------------------------------------------
 
 mkSum :: GenericKind_ -- Generic or Generic1?
-      -> US          -- Base for generating unique names
-      -> [DataCon]   -- The data constructors
-      -> ([Alt],     -- Alternatives for the T->Trep "from" function
-          [Alt])     -- Alternatives for the Trep->T "to" function
+      -> US           -- Base for generating unique names
+      -> DerivInstTys -- Information about the last type argument to Generic(1)
+      -> [DataCon]    -- The data constructors
+      -> ([Alt],      -- Alternatives for the T->Trep "from" function
+          [Alt])      -- Alternatives for the Trep->T "to" function
 
 -- Datatype without any constructors
-mkSum _ _ [] = ([from_alt], [to_alt])
+mkSum _ _ _ [] = ([from_alt], [to_alt])
   where
     from_alt = (x_Pat, nlHsCase x_Expr [])
     to_alt   = (x_Pat, nlHsCase x_Expr [])
                -- These M1s are meta-information for the datatype
 
 -- Datatype with at least one constructor
-mkSum gk_ us datacons =
+mkSum gk_ us dit datacons =
   -- switch the payload of gk_ to be datacon-centric instead of tycon-centric
- unzip [ mk1Sum (gk2gkDC gk_ d) us i (length datacons) d
+ unzip [ mk1Sum (gk2gkDC gk_ d) us i (length datacons) dit d
            | (d,i) <- zip datacons [1..] ]
 
 -- Build the sum for a particular constructor
 mk1Sum :: GenericKind_DC -- Generic or Generic1?
-       -> US        -- Base for generating unique names
-       -> Int       -- The index of this constructor
-       -> Int       -- Total number of constructors
-       -> DataCon   -- The data constructor
-       -> (Alt,     -- Alternative for the T->Trep "from" function
-           Alt)     -- Alternative for the Trep->T "to" function
-mk1Sum gk_ us i n datacon = (from_alt, to_alt)
+       -> US             -- Base for generating unique names
+       -> Int            -- The index of this constructor
+       -> Int            -- Total number of constructors
+       -> DerivInstTys   -- Information about the last type argument to Generic(1)
+       -> DataCon        -- The data constructor
+       -> (Alt,          -- Alternative for the T->Trep "from" function
+           Alt)          -- Alternative for the Trep->T "to" function
+mk1Sum gk_ us i n dit datacon = (from_alt, to_alt)
   where
     gk = forgetArgVar gk_
 
     -- Existentials already excluded
-    argTys = dataConOrigArgTys datacon
+    argTys = derivDataConInstArgTys datacon dit
     n_args = dataConSourceArity datacon
 
-    datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) (map scaledThing argTys)
+    datacon_varTys = zip (map mkGenericLocal [us .. us+n_args-1]) argTys
     datacon_vars = map fst datacon_varTys
 
     datacon_rdr  = getRdrName datacon
@@ -924,59 +908,55 @@ details on why URec is implemented the way it is.
 Note [Generating a correctly typed Rep instance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 tc_mkRepTy derives the RHS of the Rep(1) type family instance when deriving
-Generic(1). That is, it derives the ellipsis in the following:
-
-    instance Generic Foo where
-      type Rep Foo = ...
+Generic(1). For example, given the following data declaration:
 
-However, tc_mkRepTy only has knowledge of the *TyCon* of the type for which
-a Generic(1) instance is being derived, not the fully instantiated type. As a
-result, tc_mkRepTy builds the most generalized Rep(1) instance possible using
-the type variables it learns from the TyCon (i.e., it uses tyConTyVars). This
-can cause problems when the instance has instantiated type variables
-(see #11732). As an example:
+    data Foo a = MkFoo a
+      deriving stock Generic
 
-    data T a = MkT a
-    deriving instance Generic (T Int)
-    ==>
-    instance Generic (T Int) where
-      type Rep (T Int) = (... (Rec0 a)) -- wrong!
+tc_mkRepTy would generate the `Rec0 a` portion of this instance:
 
--XStandaloneDeriving is one way for the type variables to become instantiated.
-Another way is when Generic1 is being derived for a datatype with a visible
-kind binder, e.g.,
+    instance Generic (Foo a) where
+      type Rep (Foo a) = Rec0 a
+      ...
 
-   data P k (a :: k) = MkP k deriving Generic1
-   ==>
-   instance Generic1 (P *) where
-     type Rep1 (P *) = (... (Rec0 k)) -- wrong!
+(The full `Rep` instance is more complicated than this, but we have simplified
+it for presentation purposes.)
 
-See Note [Unify kinds in deriving] in GHC.Tc.Deriv.
+`tc_mkRepTy` figures out the field types to use in the RHS by inspecting a
+DerivInstTys, which contains the instantiated field types for each data
+constructor. (See Note [Instantiating field types in stock deriving] for a
+description of how this works.) As a result, `tc_mkRepTy` "just works" even
+when dealing with StandaloneDeriving, such as in this example:
 
-In any such scenario, we must prevent a discrepancy between the LHS and RHS of
-a Rep(1) instance. To do so, we create a type variable substitution that maps
-the tyConTyVars of the TyCon to their counterparts in the fully instantiated
-type. (For example, using T above as example, you'd map a :-> Int.) We then
-apply the substitution to the RHS before generating the instance.
+    deriving stock instance Generic (Foo Int)
+      ===>
+    instance Generic (Foo Int) where
+      type Rep (Foo Int) = Rec0 Int -- The `a` has been instantiated here
 
-A wrinkle in all of this: when forming the type variable substitution for
-Generic1 instances, we map the last type variable of the tycon to Any. Why?
-It's because of wily data types like this one (#15012):
+A wrinkle in all of this: what happens when deriving a Generic1 instance where
+the last type variable appears in a type synonym that discards it? That is,
+what should happen in this example (taken from #15012)?
 
-   data T a = MkT (FakeOut a)
-   type FakeOut a = Int
+    type FakeOut a = Int
+    data T a = MkT (FakeOut a)
+      deriving Generic1
 
-If we ignore a, then we'll produce the following Rep1 instance:
+MkT is a particularly wily data constructor. Although the last type variable
+`a` technically appears in `FakeOut a`, it's just a smokescreen, as `FakeOut a`
+simply expands to `Int`. As a result, `MkT` doesn't really *use* the last type
+variable. Therefore, T's `Rep` instance would use Rec0 to represent MkT's
+field. But we must be careful not to produce code like this:
 
    instance Generic1 T where
-     type Rep1 T = ... (Rec0 (FakeOut a))
+     type Rep1 T = Rec0 (FakeOut a)
      ...
 
-Oh no! Now we have `a` on the RHS, but it's completely unbound. Instead, we
-ensure that `a` is mapped to Any:
+Oh no! Now we have `a` on the RHS, but it's completely unbound. This can cause
+issues like what was observed in #15012. To avoid this, we ensure that `a` is
+instantiated to Any:
 
    instance Generic1 T where
-     type Rep1 T = ... (Rec0 (FakeOut Any))
+     type Rep1 T = Rec0 (FakeOut Any)
      ...
 
 And now all is good.
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index 2466931219..f5f9e9d9ba 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -59,7 +59,7 @@ import Data.Maybe
 ----------------------
 
 inferConstraints :: DerivSpecMechanism
-                 -> DerivM ([ThetaOrigin], [TyVar], [TcType])
+                 -> DerivM ([ThetaOrigin], [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
@@ -80,11 +80,13 @@ inferConstraints mechanism
                   , denv_cls      = main_cls
                   , denv_inst_tys = inst_tys } <- ask
        ; wildcard <- isStandaloneWildcardDeriv
-       ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType])
+       ; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism)
              infer_constraints =
                case mechanism of
                  DerivSpecStock{dsm_stock_dit = dit}
-                   -> inferConstraintsStock dit
+                   -> do (thetas, tvs, inst_tys, dit') <- inferConstraintsStock dit
+                         pure ( thetas, tvs, inst_tys
+                              , mechanism{dsm_stock_dit = dit'} )
                  DerivSpecAnyClass
                    -> infer_constraints_simple inferConstraintsAnyclass
                  DerivSpecNewtype { dsm_newtype_dit =
@@ -104,10 +106,10 @@ inferConstraints mechanism
              -- Note [Inferring the instance context].
              infer_constraints_simple
                :: DerivM [ThetaOrigin]
-               -> DerivM ([ThetaOrigin], [TyVar], [TcType])
+               -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivSpecMechanism)
              infer_constraints_simple infer_thetas = do
                thetas <- infer_thetas
-               pure (thetas, tvs, inst_tys)
+               pure (thetas, tvs, inst_tys, mechanism)
 
              -- Constraints arising from superclasses
              -- See Note [Superclasses of derived instance]
@@ -120,13 +122,14 @@ inferConstraints mechanism
              cls_subst = assert (equalLength cls_tvs inst_tys) $
                          zipTvSubst cls_tvs inst_tys
 
-       ; (inferred_constraints, tvs', inst_tys') <- infer_constraints
+       ; (inferred_constraints, tvs', inst_tys', mechanism')
+           <- infer_constraints
        ; lift $ traceTc "inferConstraints" $ vcat
               [ ppr main_cls <+> ppr inst_tys'
               , ppr inferred_constraints
               ]
        ; return ( sc_constraints ++ inferred_constraints
-                , tvs', inst_tys' ) }
+                , tvs', inst_tys', mechanism' ) }
 
 -- | Like 'inferConstraints', but used only in the case of the @stock@ deriving
 -- strategy. The constraints are inferred by inspecting the fields of each data
@@ -152,12 +155,12 @@ inferConstraints mechanism
 -- 'TyVar's/'TcType's, /not/ @[k]@/@[k, f, g]@.
 -- See Note [Inferring the instance context].
 inferConstraintsStock :: DerivInstTys
-                      -> DerivM ([ThetaOrigin], [TyVar], [TcType])
-inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
-                                    , dit_tc          = tc
-                                    , dit_tc_args     = tc_args
-                                    , dit_rep_tc      = rep_tc
-                                    , dit_rep_tc_args = rep_tc_args })
+                      -> DerivM ([ThetaOrigin], [TyVar], [TcType], DerivInstTys)
+inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
+                                        , dit_tc          = tc
+                                        , dit_tc_args     = tc_args
+                                        , dit_rep_tc      = rep_tc
+                                        , dit_rep_tc_args = rep_tc_args })
   = do DerivEnv { denv_tvs      = tvs
                 , denv_cls      = main_cls
                 , denv_inst_tys = inst_tys } <- ask
@@ -176,7 +179,7 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
              :: (CtOrigin -> TypeOrKind
                           -> Type
                           -> [([PredOrigin], Maybe TCvSubst)])
-             -> ([ThetaOrigin], [TyVar], [TcType])
+             -> ([ThetaOrigin], [TyVar], [TcType], DerivInstTys)
            con_arg_constraints get_arg_constraints
              = let -- Constraints from the fields of each data constructor.
                    (predss, mbSubsts) = unzip
@@ -184,13 +187,13 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
                      | data_con <- tyConDataCons rep_tc
                      , (arg_n, arg_t_or_k, arg_ty)
                          <- zip3 [1..] t_or_ks $
-                            dataConInstOrigArgTys data_con all_rep_tc_args
+                            derivDataConInstArgTys data_con dit
                        -- No constraints for unlifted types
                        -- See Note [Deriving and unboxed types]
-                     , not (isUnliftedType (irrelevantMult arg_ty))
+                     , not (isUnliftedType arg_ty)
                      , let orig = DerivOriginDC data_con arg_n wildcard
                      , preds_and_mbSubst
-                         <- get_arg_constraints orig arg_t_or_k (irrelevantMult arg_ty)
+                         <- get_arg_constraints orig arg_t_or_k arg_ty
                      ]
                    -- Stupid constraints from DatatypeContexts. Note that we
                    -- must gather these constraints from the data constructors,
@@ -199,7 +202,7 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
                    -- See Note [The stupid context] in GHC.Core.DataCon.
                    stupid_theta =
                      [ substTyWith (dataConUnivTyVars data_con)
-                                   all_rep_tc_args
+                                   (dataConInstUnivs data_con rep_tc_args)
                                    stupid_pred
                      | data_con <- tyConDataCons rep_tc
                      , stupid_pred <- dataConStupidTheta data_con
@@ -220,9 +223,10 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
                                          substTheta subst' stupid_theta
                    preds'       = map (substPredOrigin subst') preds
                    inst_tys'    = substTys subst' inst_tys
+                   dit'         = substDerivInstTys subst' dit
                    tvs'         = tyCoVarsOfTypesWellScoped inst_tys'
                in ( [stupid_theta_origin, mkThetaOriginFromPreds preds']
-                  , tvs', inst_tys' )
+                  , tvs', inst_tys', dit' )
 
            is_generic  = main_cls `hasKey` genClassKey
            is_generic1 = main_cls `hasKey` gen1ClassKey
@@ -270,14 +274,6 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
 
            rep_tc_tvs      = tyConTyVars rep_tc
            last_tv         = last rep_tc_tvs
-           -- 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 = tyConInstArgTys rep_tc rep_tc_args
 
            -- Extra Data constraints
            -- The Data class (only) requires that for
@@ -310,7 +306,7 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
 
        if    -- Generic constraints are easy
           |  is_generic
-           -> return ([], tvs, inst_tys)
+           -> return ([], tvs, inst_tys, dit)
 
              -- Generic1 needs Functor
              -- See Note [Getting base classes]
@@ -324,19 +320,14 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys     = cls_tys
 
              -- The others are a bit more complicated
           |  otherwise
-           -> -- See the comment with all_rep_tc_args for an explanation of
-              -- this assertion
-              assertPpr (equalLength rep_tc_tvs all_rep_tc_args)
-                        ( ppr main_cls <+> ppr rep_tc
-                          $$ ppr rep_tc_tvs $$ ppr all_rep_tc_args) $
-                do { let (arg_constraints, tvs', inst_tys')
-                           = con_arg_constraints get_std_constrained_tys
-                   ; lift $ traceTc "inferConstraintsStock" $ vcat
-                          [ ppr main_cls <+> ppr inst_tys'
-                          , ppr arg_constraints
-                          ]
-                   ; return ( extra_constraints ++ arg_constraints
-                            , tvs', inst_tys') }
+           -> do { let (arg_constraints, tvs', inst_tys', dit')
+                         = con_arg_constraints get_std_constrained_tys
+                 ; lift $ traceTc "inferConstraintsStock" $ vcat
+                        [ ppr main_cls <+> ppr inst_tys'
+                        , ppr arg_constraints
+                        ]
+                 ; return ( extra_constraints ++ arg_constraints
+                          , tvs', inst_tys', dit' ) }
 
 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
 -- which gathers its constraints based on the type signatures of the class's
diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs
index a65dcca956..1737ae2e50 100644
--- a/compiler/GHC/Tc/Deriv/Utils.hs
+++ b/compiler/GHC/Tc/Deriv/Utils.hs
@@ -4,6 +4,7 @@
 
 -}
 
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- | Error-checking and other utilities for @deriving@ clauses or declarations.
@@ -50,7 +51,6 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcType
 import GHC.Builtin.Names.TH (liftClassKey)
 import GHC.Core.TyCon
-import GHC.Core.Multiplicity
 import GHC.Core.Type
 import GHC.Utils.Misc
 import GHC.Types.Var.Set
@@ -303,12 +303,15 @@ Each deriving strategy imposes restrictions on arg_1 through arg_n as follows:
 
   This extra structure is witnessed by the DerivInstTys data type, which stores
   arg_1 through arg_(n-1) (dit_cls_tys), the algebraic type constructor
-  (dit_tc), and its arguments (dit_tc_args). If dit_tc is an ordinary data type
-  constructor, then dit_rep_tc/dit_rep_tc_args are the same as
-  dit_tc/dit_tc_args. If dit_tc is a data family type constructor, then
-  dit_rep_tc is the representation type constructor for the data family
-  instance, and dit_rep_tc_args are the arguments to the representation type
-  constructor in the corresponding instance.
+  (dit_tc), and its arguments (dit_tc_args). A DerivInstTys value can be seen
+  as a more structured representation of the denv_inst_tys field of DerivEnv.
+
+  If dit_tc is an ordinary data type constructor, then
+  dit_rep_tc/dit_rep_tc_args are the same as dit_tc/dit_tc_args. If dit_tc is a
+  data family type constructor, then dit_rep_tc is the representation type
+  constructor for the data family instance, and dit_rep_tc_args are the
+  arguments to the representation type constructor in the corresponding
+  instance.
 
 * newtype (DerivSpecNewtype):
 
@@ -648,32 +651,34 @@ getDataConFixityFun tc
 -- the data constructors - but we need to be careful to fall back to the
 -- family tycon (with indexes) in error messages.
 
-checkOriginativeSideConditions
-  :: DynFlags -> DerivContext -> Class -> DerivInstTys
-  -> OriginativeDerivStatus
-checkOriginativeSideConditions dflags deriv_ctxt cls
-                               dit@(DerivInstTys{dit_cls_tys = cls_tys})
-    -- First, check if stock deriving is possible...
-  | Just cond <- stockSideConditions deriv_ctxt cls
-  = case cond dflags dit of
-        NotValid err -> StockClassError err  -- Class-specific error
-        IsValid  | null (filterOutInvisibleTypes (classTyCon cls) cls_tys)
-                   -- All stock derivable classes are unary in the sense that
-                   -- there should be not types in cls_tys (i.e., no type args
-                   -- other than last). Note that cls_types can contain
-                   -- invisible types as well (e.g., for Generic1, which is
-                   -- poly-kinded), so make sure those are not counted.
-                 , Just gen_fn <- hasStockDeriving cls
-                   -> CanDeriveStock gen_fn
-                 | otherwise -> StockClassError (classArgsErr cls cls_tys)
-                   -- e.g. deriving( Eq s )
-
-    -- ...if not, try falling back on DeriveAnyClass.
-  | xopt LangExt.DeriveAnyClass dflags
-  = CanDeriveAnyClass   -- DeriveAnyClass should work
-
-  | otherwise
-  = NonDerivableClass -- Neither anyclass nor stock work
+checkOriginativeSideConditions :: DerivInstTys -> DerivM OriginativeDerivStatus
+checkOriginativeSideConditions dit@(DerivInstTys{dit_cls_tys = cls_tys}) =
+  do DerivEnv { denv_cls  = cls
+              , denv_ctxt = deriv_ctxt } <- ask
+     dflags <- getDynFlags
+
+     if    -- First, check if stock deriving is possible...
+        |  Just cond <- stockSideConditions deriv_ctxt cls
+        -> case cond dflags dit of
+             NotValid err -> pure $ StockClassError err  -- Class-specific error
+             IsValid  |  null (filterOutInvisibleTypes (classTyCon cls) cls_tys)
+                         -- All stock derivable classes are unary in the sense that
+                         -- there should be not types in cls_tys (i.e., no type args
+                         -- other than last). Note that cls_types can contain
+                         -- invisible types as well (e.g., for Generic1, which is
+                         -- poly-kinded), so make sure those are not counted.
+                      ,  Just gen_fn <- hasStockDeriving cls
+                      -> pure $ CanDeriveStock gen_fn
+                      |  otherwise
+                      -> pure $ StockClassError $ classArgsErr cls cls_tys
+                        -- e.g. deriving( Eq s )
+
+           -- ...if not, try falling back on DeriveAnyClass.
+        |  xopt LangExt.DeriveAnyClass dflags
+        -> pure CanDeriveAnyClass   -- DeriveAnyClass should work
+
+        |  otherwise
+        -> pure NonDerivableClass -- Neither anyclass nor stock work
 
 
 classArgsErr :: Class -> [Type] -> DeriveInstanceErrReason
@@ -810,7 +815,7 @@ cond_stdOK deriv_ctxt permissive dflags
       = bad DerivErrBadConHasExistentials
       | not (null theta) -- 4.
       = bad DerivErrBadConHasConstraints
-      | not (permissive || all isTauTy (map scaledThing $ dataConOrigArgTys con)) -- 5.
+      | not (permissive || all isTauTy (derivDataConInstArgTys con dit)) -- 5.
       = bad DerivErrBadConHasHigherRankType
       | otherwise
       = IsValid
@@ -851,13 +856,13 @@ cond_args :: Class -> Condition
 -- by generating specialised code.  For others (eg 'Data') we don't.
 -- For even others (eg 'Lift'), unlifted types aren't even a special
 -- consideration!
-cond_args cls _ (DerivInstTys{dit_rep_tc = rep_tc})
+cond_args cls _ dit@(DerivInstTys{dit_rep_tc = rep_tc})
   = case bad_args of
       []     -> IsValid
       (ty:_) -> NotValid $ DerivErrDunnoHowToDeriveForType ty
   where
     bad_args = [ arg_ty | con <- tyConDataCons rep_tc
-                        , Scaled _ arg_ty <- dataConOrigArgTys con
+                        , arg_ty <- derivDataConInstArgTys con dit
                         , isLiftedType_maybe arg_ty /= Just True
                         , not (ok_ty arg_ty) ]
 
@@ -893,7 +898,7 @@ cond_functorOK :: Bool -> Bool -> Condition
 --            (d) optionally: don't use function types
 --            (e) no "stupid context" on data type
 cond_functorOK allowFunctions allowExQuantifiedLastTyVar _
-               (DerivInstTys{dit_rep_tc = rep_tc})
+               dit@(DerivInstTys{dit_rep_tc = rep_tc})
   | null tc_tvs
   = NotValid $ DerivErrMustHaveSomeParameters rep_tc
 
@@ -913,7 +918,7 @@ cond_functorOK allowFunctions allowExQuantifiedLastTyVar _
       -- See Note [Check that the type variable is truly universal]
 
     data_cons = tyConDataCons rep_tc
-    check_con con = allValid (check_universal con : foldDataConArgs (ft_check con) con)
+    check_con con = allValid (check_universal con : foldDataConArgs (ft_check con) con dit)
 
     check_universal :: DataCon -> Validity' DeriveInstanceErrReason
     check_universal con
diff --git a/testsuite/tests/deriving/should_compile/T20375.hs b/testsuite/tests/deriving/should_compile/T20375.hs
new file mode 100644
index 0000000000..33a54a7c7c
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T20375.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+module T20375 where
+
+import Data.Data (Data)
+import Data.Ix (Ix)
+import GHC.Exts (Int#, RuntimeRep(..), TYPE)
+import GHC.Generics (Generic, Generic1)
+
+-- Test special-casing for unlifted types (e.g., Int#)
+data D1 (a :: TYPE IntRep) b = MkD1 a b
+deriving stock instance Eq (D1 Int# Int)
+deriving stock instance Ord (D1 Int# Int)
+deriving stock instance Generic (D1 Int# Int)
+deriving stock instance Generic1 (D1 Int#)
+deriving stock instance Show (D1 Int# Int)
+
+-- Test special-casing for tuples
+data D2 p a = MkD2 (p a Int)
+deriving stock instance Foldable (D2 (,))
+deriving stock instance Functor (D2 (,))
+deriving stock instance Traversable (D2 (,))
+
+-- Ensure that validity checks don't get tripped up by a runtime-polymorphic
+-- type that is instantiated to something runtime-monomorphic.
+newtype D3 (a :: TYPE r) = MkD3 a
+deriving stock instance Bounded (D3 Int)
+deriving stock instance Data (D3 Int)
+deriving stock instance Eq (D3 Int)
+deriving stock instance Foldable D3
+deriving stock instance Functor D3
+deriving stock instance Generic (D3 Int)
+deriving stock instance Generic1 D3
+deriving stock instance Ix (D3 Int)
+deriving stock instance Ord (D3 Int)
+deriving stock instance Read (D3 Int)
+deriving stock instance Show (D3 Int)
+deriving stock instance Traversable D3
diff --git a/testsuite/tests/deriving/should_compile/T20387.hs b/testsuite/tests/deriving/should_compile/T20387.hs
new file mode 100644
index 0000000000..e056b0d29d
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T20387.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+module T20387 where
+
+import Data.Kind (Type)
+import GHC.Exts (TYPE)
+import GHC.Generics (Generic1)
+
+newtype D (a :: TYPE r) = MkD a
+  deriving Generic1
+
+type T :: forall j k -> (k -> Type) -> (j -> k) -> j -> Type
+data T j k f g a = MkT j k (f (g a))
+  deriving Generic1
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index eb558b11cf..e2680a8f9d 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -132,4 +132,6 @@ test('T18914', normal, compile, [''])
 # They are printed in tcDeriv beginning with "rnd" line
 # and are indented with spaces.
 test('T20496', multiline_grep_errmsg(r"rnd\n( .*\n)*"), compile, ['-ddump-tc-trace'])
+test('T20375', normal, compile, [''])
+test('T20387', normal, compile, [''])
 test('T20501', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr
index b3efbc1b41..81c6da1b69 100644
--- a/testsuite/tests/typecheck/should_fail/T15883b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr
@@ -1,7 +1,18 @@
 
 T15883b.hs:14:1: error:
-    • Can't make a derived instance of
-        ‘Eq (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
-        Don't know how to derive ‘Eq’ for type ‘forall (a :: TYPE rep). a’
-    • In the stand-alone deriving instance for
-        ‘Eq (Foo (BoxedRep Lifted))’
+    • Ambiguous type variable ‘a0’ arising from a use of ‘==’
+      prevents the constraint ‘(Eq a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Eq SpecConstrAnnotation -- Defined in ‘GHC.Exts’
+        instance Eq Ordering -- Defined in ‘GHC.Classes’
+        instance Eq (Foo ('BoxedRep 'Lifted)) -- Defined at T15883b.hs:14:1
+        ...plus 24 others
+        ...plus four instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: a1 == b1
+      In an equation for ‘==’: (==) (MkFoo a1) (MkFoo b1) = ((a1 == b1))
+      When typechecking the code for ‘==’
+        in a derived instance for ‘Eq (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Eq (Foo ('BoxedRep 'Lifted))’
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr
index 2aa1049fa5..4ef9e5ef52 100644
--- a/testsuite/tests/typecheck/should_fail/T15883c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr
@@ -1,7 +1,43 @@
 
 T15883c.hs:14:1: error:
-    • Can't make a derived instance of
-        ‘Ord (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
-        Don't know how to derive ‘Ord’ for type ‘forall (a :: TYPE rep). a’
-    • In the stand-alone deriving instance for
-        ‘Ord (Foo (BoxedRep Lifted))’
+    • No instance for (Eq (Foo ('BoxedRep 'Lifted)))
+        arising from the superclasses of an instance declaration
+    • In the instance declaration for ‘Ord (Foo ('BoxedRep 'Lifted))’
+
+T15883c.hs:14:1: error:
+    • Ambiguous type variable ‘a0’ arising from a use of ‘compare’
+      prevents the constraint ‘(Ord a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Ord Ordering -- Defined in ‘GHC.Classes’
+        instance Ord (Foo ('BoxedRep 'Lifted))
+          -- Defined at T15883c.hs:14:1
+        instance Ord Integer -- Defined in ‘GHC.Num.Integer’
+        ...plus 23 others
+        ...plus two instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: a1 `compare` b1
+      In a case alternative: MkFoo b1 -> (a1 `compare` b1)
+      In the expression: case b of MkFoo b1 -> (a1 `compare` b1)
+      When typechecking the code for ‘compare’
+        in a derived instance for ‘Ord (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+
+T15883c.hs:14:1: error:
+    • Ambiguous type variable ‘a1’ arising from a use of ‘<’
+      prevents the constraint ‘(Ord a1)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a1’ should be.
+      These potential instances exist:
+        instance Ord Ordering -- Defined in ‘GHC.Classes’
+        instance Ord (Foo ('BoxedRep 'Lifted))
+          -- Defined at T15883c.hs:14:1
+        instance Ord Integer -- Defined in ‘GHC.Num.Integer’
+        ...plus 23 others
+        ...plus two instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: a1 < b1
+      In a case alternative: MkFoo b1 -> (a1 < b1)
+      In the expression: case b of MkFoo b1 -> (a1 < b1)
+      When typechecking the code for ‘<’
+        in a derived instance for ‘Ord (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr
index 96a294bc9e..67ce3eff57 100644
--- a/testsuite/tests/typecheck/should_fail/T15883d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr
@@ -1,8 +1,21 @@
 
 T15883d.hs:14:1: error:
-    • Can't make a derived instance of
-        ‘Show (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
-        Don't know how to derive ‘Show’
-          for type ‘forall (a :: TYPE rep). a’
-    • In the stand-alone deriving instance for
-        ‘Show (Foo (BoxedRep Lifted))’
+    • Ambiguous type variable ‘a0’ arising from a use of ‘showsPrec’
+      prevents the constraint ‘(Show a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Show Ordering -- Defined in ‘GHC.Show’
+        instance Show (Foo ('BoxedRep 'Lifted))
+          -- Defined at T15883d.hs:14:1
+        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+        ...plus 28 others
+        ...plus 9 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the second argument of ‘(.)’, namely ‘(showsPrec 11 b1)’
+      In the second argument of ‘showParen’, namely
+        ‘((.) (showString "MkFoo ") (showsPrec 11 b1))’
+      In the expression:
+        showParen (a >= 11) ((.) (showString "MkFoo ") (showsPrec 11 b1))
+      When typechecking the code for ‘showsPrec’
+        in a derived instance for ‘Show (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr
index c7006fb790..72483274e9 100644
--- a/testsuite/tests/typecheck/should_fail/T15883e.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr
@@ -1,8 +1,70 @@
 
 T15883e.hs:16:1: error:
-    • Can't make a derived instance of
-        ‘Data (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
-        Don't know how to derive ‘Data’
-          for type ‘forall (a :: TYPE rep). a’
-    • In the stand-alone deriving instance for
-        ‘Data (Foo (BoxedRep Lifted))’
+    • Ambiguous type variable ‘d0’ arising from a use of ‘k’
+      prevents the constraint ‘(Data d0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘d0’ should be.
+      These potential instances exist:
+        instance (Data a, Data b) => Data (Either a b)
+          -- Defined in ‘Data.Data’
+        instance Data a => Data (Down a) -- Defined in ‘Data.Data’
+        instance Data SpecConstrAnnotation -- Defined in ‘GHC.Exts’
+        ...plus 20 others
+        ...plus 48 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: z (\ a1 -> MkFoo a1) `k` a1
+      In an equation for ‘Data.Data.gfoldl’:
+          Data.Data.gfoldl k z (MkFoo a1) = (z (\ a1 -> MkFoo a1) `k` a1)
+      When typechecking the code for ‘Data.Data.gfoldl’
+        in a derived instance for ‘Data (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Data (Foo ('BoxedRep 'Lifted))’
+
+T15883e.hs:16:1: error:
+    • Couldn't match expected type ‘a’ with actual type ‘d0’
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        a type expected by the context:
+          forall a. a
+        at T15883e.hs:16:1-52
+    • In the first argument of ‘MkFoo’, namely ‘a1’
+      In the expression: MkFoo a1
+      In the first argument of ‘z’, namely ‘(\ a1 -> MkFoo a1)’
+      When typechecking the code for ‘Data.Data.gfoldl’
+        in a derived instance for ‘Data (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+    • Relevant bindings include a1 :: d0 (bound at T15883e.hs:16:1)
+
+T15883e.hs:16:1: error:
+    • Ambiguous type variable ‘b0’ arising from a use of ‘k’
+      prevents the constraint ‘(Data b0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘b0’ should be.
+      These potential instances exist:
+        instance (Data a, Data b) => Data (Either a b)
+          -- Defined in ‘Data.Data’
+        instance Data a => Data (Down a) -- Defined in ‘Data.Data’
+        instance Data SpecConstrAnnotation -- Defined in ‘GHC.Exts’
+        ...plus 20 others
+        ...plus 48 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the expression: k (z (\ a1 -> MkFoo a1))
+      In an equation for ‘Data.Data.gunfold’:
+          Data.Data.gunfold k z _ = k (z (\ a1 -> MkFoo a1))
+      When typechecking the code for ‘Data.Data.gunfold’
+        in a derived instance for ‘Data (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+      In the instance declaration for ‘Data (Foo ('BoxedRep 'Lifted))’
+
+T15883e.hs:16:1: error:
+    • Couldn't match expected type ‘a’ with actual type ‘b0’
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        a type expected by the context:
+          forall a. a
+        at T15883e.hs:16:1-52
+    • In the first argument of ‘MkFoo’, namely ‘a1’
+      In the expression: MkFoo a1
+      In the first argument of ‘z’, namely ‘(\ a1 -> MkFoo a1)’
+      When typechecking the code for ‘Data.Data.gunfold’
+        in a derived instance for ‘Data (Foo ('BoxedRep 'Lifted))’:
+        To see the code I am typechecking, use -ddump-deriv
+    • Relevant bindings include a1 :: b0 (bound at T15883e.hs:16:1)