Fix type variable substitution in gen_Newtype_fam_instswip/backports-9.6

Previously, `gen_Newtype_fam_insts` was substituting the type variable binders
of a type family instance using `substTyVars`, which failed to take type
variable dependencies into account. There is similar code in
`GHC.Tc.TyCl.Class.tcATDefault` that _does_ perform this substitution properly,
so this patch:

1. Factors out this code into a top-level `substATBndrs` function, and
2. Uses `substATBndrs` in `gen_Newtype_fam_insts`.

Fixes #23329.

(cherry picked from commit e8b72ff6e4aee1f889a9168df57bb1b00168fd21)

5 files changed, 96 insertions, 9 deletions

diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index d4e4b87db8..0da1868beb 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -45,6 +45,7 @@ module GHC.Tc.Deriv.Generate (
 import GHC.Prelude
 
 import GHC.Tc.Utils.Monad
+import GHC.Tc.TyCl.Class ( substATBndrs )
 import GHC.Hs
 import GHC.Types.FieldLabel
 import GHC.Types.Name.Reader
@@ -2097,8 +2098,8 @@ gen_Newtype_fam_insts loc' cls inst_tvs inst_tys rhs_ty
         newFamInst SynFamilyInst axiom
       where
         fam_tvs     = tyConTyVars fam_tc
-        rep_lhs_tys = substTyVars lhs_subst fam_tvs
-        rep_rhs_tys = substTyVars rhs_subst fam_tvs
+        (_, rep_lhs_tys) = substATBndrs lhs_subst fam_tvs
+        (_, rep_rhs_tys) = substATBndrs rhs_subst fam_tvs
         rep_rhs_ty  = mkTyConApp fam_tc rep_rhs_tys
         rep_tcvs    = tyCoVarsOfTypesList rep_lhs_tys
         (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
index 9da7b05192..e3dceb6db9 100644
--- a/compiler/GHC/Tc/TyCl/Class.hs
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -22,6 +22,7 @@ module GHC.Tc.TyCl.Class
    , instDeclCtxt2
    , instDeclCtxt3
    , tcATDefault
+   , substATBndrs
    )
 where
 
@@ -37,7 +38,7 @@ import GHC.Tc.Utils.Unify
 import GHC.Tc.Utils.Instantiate( tcSuperSkolTyVars )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
-import GHC.Core.Type     ( piResultTys )
+import GHC.Core.Type     ( extendTvSubstWithClone, piResultTys )
 import GHC.Core.Predicate
 import GHC.Core.Multiplicity
 import GHC.Tc.Types.Origin
@@ -55,7 +56,7 @@ import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Types.Name.Set
 import GHC.Types.Var
-import GHC.Types.Var.Env
+import GHC.Types.Var.Env ( lookupVarEnv )
 import GHC.Types.SourceFile (HscSource(..))
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
@@ -497,8 +498,7 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
    --            instance C [x]
    -- Then we want to generate the decl:   type F [x] b = ()
   | Just (rhs_ty, _loc) <- defs
-  = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
-                                            (tyConTyVars fam_tc)
+  = do { let (subst', pat_tys') = substATBndrs inst_subst (tyConTyVars fam_tc)
              rhs'     = substTyUnchecked subst' rhs_ty
              tcv' = tyCoVarsOfTypesList pat_tys'
              (tv', cv') = partition isTyVar tcv'
@@ -521,14 +521,73 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
   | otherwise  -- defs = Nothing
   = do { warnMissingAT (tyConName fam_tc)
        ; return [] }
+
+-- | Apply a substitution to the type variable binders of an associated type
+-- family. This is used to compute default instances for associated type
+-- families (see 'tcATDefault') as well as @newtype@-derived associated type
+-- family instances (see @gen_Newtype_fam_insts@ in "GHC.Tc.Deriv.Generate").
+--
+-- As a concrete example, consider the following class and associated type
+-- family:
+--
+-- @
+--   class C k (a :: k) where
+--     type F k a (b :: k) :: Type
+--     type F j p q = (Proxy @j p, Proxy @j (q :: j))
+-- @
+--
+-- If a user defines this instance:
+--
+-- @
+-- instance C (Type -> Type) Maybe where {}
+-- @
+--
+-- Then in order to typecheck the default @F@ instance, we must apply the
+-- substitution @[k :-> (Type -> Type), a :-> Maybe]@ to @F@'s binders, which
+-- are @[k, a, (b :: k)]@. The result should look like this:
+--
+-- @
+--   type F (Type -> Type) Maybe (b :: Type -> Type) =
+--     (Proxy @(Type -> Type) Maybe, Proxy @(Type -> Type) (b :: Type -> Type))
+-- @
+--
+-- Making this work requires some care. There are two cases:
+--
+-- 1. If we encounter a type variable in the domain of the substitution (e.g.,
+--    @k@ or @a@), then we apply the substitution directly.
+--
+-- 2. Otherwise, we substitute into the type variable's kind (e.g., turn
+--    @b :: k@ to @b :: Type -> Type@). We then return an extended substitution
+--    where the old @b@ (of kind @k@) maps to the new @b@ (of kind @Type -> Type@).
+--
+--    This step is important to do in case there are later occurrences of @b@,
+--    which we must ensure have the correct kind. Otherwise, we might end up
+--    with @Proxy \@(Type -> Type) (b :: k)@ on the right-hand side of the
+--    default instance, which would be completely wrong.
+--
+-- Contrast 'substATBndrs' function with similar substitution functions:
+--
+-- * 'substTyVars' does not substitute into the kinds of each type variable,
+--   nor does it extend the substitution. 'substTyVars' is meant for occurrences
+--   of type variables, whereas 'substATBndr's is meant for binders.
+--
+-- * 'substTyVarBndrs' does substitute into kinds and extends the substitution,
+--   but it does not apply the substitution to the variables themselves. As
+--   such, 'substTyVarBndrs' returns a list of 'TyVar's rather than a list of
+--   'Type's.
+substATBndrs :: Subst -> [TyVar] -> (Subst, [Type])
+substATBndrs = mapAccumL substATBndr
   where
-    subst_tv subst tc_tv
+    substATBndr :: Subst -> TyVar -> (Subst, Type)
+    substATBndr subst tc_tv
+        -- Case (1) in the Haddocks
       | Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
       = (subst, ty)
+        -- Case (2) in the Haddocks
       | otherwise
-      = (extendTvSubst subst tc_tv ty', ty')
+      = (extendTvSubstWithClone subst tc_tv tc_tv', mkTyVarTy tc_tv')
       where
-        ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
+        tc_tv' = updateTyVarKind (substTy subst) tc_tv
 
 warnMissingAT :: Name -> TcM ()
 warnMissingAT name
diff --git a/testsuite/tests/deriving/should_compile/T23329.hs b/testsuite/tests/deriving/should_compile/T23329.hs
new file mode 100644
index 0000000000..7b4cd922f8
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T23329.hs
@@ -0,0 +1,9 @@
+module T23329 where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(Proxy))
+
+import T23329_M
+
+foo :: ()
+foo = myMethod @Type @MyMaybe @() () Proxy Proxy
diff --git a/testsuite/tests/deriving/should_compile/T23329_M.hs b/testsuite/tests/deriving/should_compile/T23329_M.hs
new file mode 100644
index 0000000000..a451a2b828
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T23329_M.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T23329_M where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+
+class MyClass (f :: k -> Type) where
+  type MyTypeFamily f (i :: k) :: Type
+  myMethod :: MyTypeFamily f i -> Proxy f -> Proxy i -> ()
+
+instance MyClass Maybe where
+  type MyTypeFamily Maybe i = ()
+  myMethod = undefined
+
+newtype MyMaybe a = MyMaybe (Maybe a)
+  deriving MyClass
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 922b7126b7..503c705169 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -140,3 +140,4 @@ test('T20501', normal, compile, [''])
 test('T20719', normal, compile, [''])
 test('T20994', normal, compile, [''])
 test('T22167', normal, compile, [''])
+test('T23329', normal, multimod_compile, ['T23329', '-v0'])