Bring tcTyConScopedTyVars into scope in tcClassDecl2

It is possible that the type variables bound by a class header will map to
something different in the typechecker in the presence of
`StandaloneKindSignatures`. `tcClassDecl2` was not aware of this, however,
leading to #19738. To fix it, in `tcTyClDecls` we map each class `TcTyCon` to
its `tcTyConScopedTyVars` as a `ClassScopedTVEnv`. We then plumb that
`ClassScopedTVEnv` to `tcClassDecl2` where it can be used.

Fixes #19738.

8 files changed, 112 insertions, 30 deletions

diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index a460116c3b..56fe29cb7e 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -976,6 +976,36 @@ where
    * required_tvs the same as tyConTyVars
    * tyConArity = length required_tvs
 
+There are some situations where we need to keep the tcTyConScopedTyVars around
+for later use, even after the TcTyCon has been zonked away:
+
+* When typechecking `deriving` clauses for top-level data declarations, the
+  tcTyConScopedTyVars are brought into scope in through the `di_scoped_tvs`
+  field of GHC.Tc.Deriv.DerivInfo. Example (#16731):
+
+    class C x1 x2
+
+    type T :: a -> Type
+    data T (x :: z) deriving (C z)
+
+  When typechecking `C z`, we want `z` to map to `a`, which is exactly what the
+  tcTyConScopedTyVars for T give us.
+
+* Similarly, when typechecking default definitions for class methods, the
+  tcTyConScopedTyVars ought to be brought into scope. Example (#19738):
+
+    type P :: k -> Type
+    data P a = MkP
+
+    type T :: k -> Constraint
+    class T (a :: j) where
+      f :: P a
+      f = MkP @j @a
+
+  We pass the tcTyConScopedTyVars to GHC.Tc.TyCl.Class.tcClassDecl2, the
+  function responsible for typechecking the default definition of `f`, by way
+  of a ClassScopedTVEnv, which maps each class name to its scoped tyvars.
+
 See also Note [How TcTyCons work] in GHC.Tc.TyCl
 
 Note [Promoted GADT data constructors]
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index fa8817b36a..a899349702 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -170,6 +170,8 @@ data DerivInfo = DerivInfo { di_rep_tc  :: TyCon
                              -- or the *representation* tycon for data families
                            , di_scoped_tvs :: ![(Name,TyVar)]
                              -- ^ Variables that scope over the deriving clause.
+                             -- See @Note [Scoped tyvars in a TcTyCon]@ in
+                             -- "GHC.Core.TyCon".
                            , di_clauses :: [LHsDerivingClause GhcRn]
                            , di_ctxt    :: SDoc -- ^ error context
                            }
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 0511e1e268..fc330061e8 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -75,6 +75,7 @@ import GHC.Tc.Gen.Default
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.Rule
 import GHC.Tc.Gen.Foreign
+import GHC.Tc.TyCl.Class ( ClassScopedTVEnv )
 import GHC.Tc.TyCl.Instance
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
@@ -699,7 +700,7 @@ tcRnHsBootDecls hsc_src decls
 
                 -- Typecheck type/class/instance decls
         ; traceTc "Tc2 (boot)" empty
-        ; (tcg_env, inst_infos, _deriv_binds)
+        ; (tcg_env, inst_infos, _deriv_binds, _class_scoped_tv_env)
              <- tcTyClsInstDecls tycl_decls deriv_decls val_binds
         ; setGblEnv tcg_env     $ do {
 
@@ -1456,7 +1457,8 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
                 -- Source-language instances, including derivings,
                 -- and import the supporting declarations
         traceTc "Tc3" empty ;
-        (tcg_env, inst_infos, XValBindsLR (NValBinds deriv_binds deriv_sigs))
+        (tcg_env, inst_infos, class_scoped_tv_env,
+         XValBindsLR (NValBinds deriv_binds deriv_sigs))
             <- tcTyClsInstDecls tycl_decls deriv_decls val_binds ;
 
         setGblEnv tcg_env       $ do {
@@ -1497,7 +1499,8 @@ tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
                 -- Second pass over class and instance declarations,
                 -- now using the kind-checked decls
         traceTc "Tc6" empty ;
-        inst_binds <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls) inst_infos ;
+        inst_binds <- tcInstDecls2 (tyClGroupTyClDecls tycl_decls)
+                                   inst_infos class_scoped_tv_env ;
 
                 -- Foreign exports
         traceTc "Tc7" empty ;
@@ -1733,13 +1736,14 @@ tcTyClsInstDecls :: [TyClGroup GhcRn]
                          [InstInfo GhcRn],    -- Source-code instance decls to
                                               -- process; contains all dfuns for
                                               -- this module
+                          ClassScopedTVEnv,   -- Class scoped type variables
                           HsValBinds GhcRn)   -- Supporting bindings for derived
                                               -- instances
 
 tcTyClsInstDecls tycl_decls deriv_decls binds
  = tcAddDataFamConPlaceholders (tycl_decls >>= group_instds) $
    tcAddPatSynPlaceholders (getPatSynBinds binds) $
-   do { (tcg_env, inst_info, deriv_info)
+   do { (tcg_env, inst_info, deriv_info, class_scoped_tv_env)
           <- tcTyAndClassDecls tycl_decls ;
       ; setGblEnv tcg_env $ do {
           -- With the @TyClDecl@s and @InstDecl@s checked we're ready to
@@ -1753,7 +1757,8 @@ tcTyClsInstDecls tycl_decls deriv_decls binds
               <- tcInstDeclsDeriv deriv_info deriv_decls
           ; setGblEnv tcg_env' $ do {
                 failIfErrsM
-              ; pure (tcg_env', inst_info' ++ inst_info, val_binds)
+              ; pure ( tcg_env', inst_info' ++ inst_info
+                     , class_scoped_tv_env, val_binds )
       }}}
 
 {- *********************************************************************
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 076c0c0ee0..b2b9f2c106 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -144,31 +144,35 @@ tcTyAndClassDecls :: [TyClGroup GhcRn]      -- Mutually-recursive groups in
                                             -- and their implicit Ids,DataCons
                          , [InstInfo GhcRn] -- Source-code instance decls info
                          , [DerivInfo]      -- Deriving info
+                         , ClassScopedTVEnv -- Class scoped type variables
                          )
 -- Fails if there are any errors
 tcTyAndClassDecls tyclds_s
   -- The code recovers internally, but if anything gave rise to
   -- an error we'd better stop now, to avoid a cascade
   -- Type check each group in dependency order folding the global env
-  = checkNoErrs $ fold_env [] [] tyclds_s
+  = checkNoErrs $ fold_env [] [] emptyNameEnv tyclds_s
   where
     fold_env :: [InstInfo GhcRn]
              -> [DerivInfo]
+             -> ClassScopedTVEnv
              -> [TyClGroup GhcRn]
-             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
-    fold_env inst_info deriv_info []
+             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ClassScopedTVEnv)
+    fold_env inst_info deriv_info class_scoped_tv_env []
       = do { gbl_env <- getGblEnv
-           ; return (gbl_env, inst_info, deriv_info) }
-    fold_env inst_info deriv_info (tyclds:tyclds_s)
-      = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
+           ; return (gbl_env, inst_info, deriv_info, class_scoped_tv_env) }
+    fold_env inst_info deriv_info class_scoped_tv_env (tyclds:tyclds_s)
+      = do { (tcg_env, inst_info', deriv_info', class_scoped_tv_env')
+               <- tcTyClGroup tyclds
            ; setGblEnv tcg_env $
                -- remaining groups are typechecked in the extended global env.
              fold_env (inst_info' ++ inst_info)
                       (deriv_info' ++ deriv_info)
+                      (class_scoped_tv_env' `plusNameEnv` class_scoped_tv_env)
                       tyclds_s }
 
 tcTyClGroup :: TyClGroup GhcRn
-            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
+            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ClassScopedTVEnv)
 -- Typecheck one strongly-connected component of type, class, and instance decls
 -- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
 tcTyClGroup (TyClGroup { group_tyclds = tyclds
@@ -180,7 +184,7 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
            -- Step 1: Typecheck the standalone kind signatures and type/class declarations
        ; traceTc "---- tcTyClGroup ---- {" empty
        ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
-       ; (tyclss, data_deriv_info, kindless) <-
+       ; (tyclss, data_deriv_info, class_scoped_tv_env, kindless) <-
            tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution]
            do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs
               ; tcTyClDecls tyclds kisig_env role_annots }
@@ -216,7 +220,7 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
        ; let deriv_info = datafam_deriv_info ++ data_deriv_info
        ; let gbl_env'' = gbl_env'
                 { tcg_ksigs = tcg_ksigs gbl_env' `unionNameSet` kindless }
-       ; return (gbl_env'', inst_info, deriv_info) }
+       ; return (gbl_env'', inst_info, deriv_info, class_scoped_tv_env) }
 
 -- Gives the kind for every TyCon that has a standalone kind signature
 type KindSigEnv = NameEnv Kind
@@ -225,7 +229,7 @@ tcTyClDecls
   :: [LTyClDecl GhcRn]
   -> KindSigEnv
   -> RoleAnnotEnv
-  -> TcM ([TyCon], [DerivInfo], NameSet)
+  -> TcM ([TyCon], [DerivInfo], ClassScopedTVEnv, NameSet)
 tcTyClDecls tyclds kisig_env role_annots
   = do {    -- Step 1: kind-check this group and returns the final
             -- (possibly-polymorphic) kind of each TyCon and Class
@@ -239,11 +243,12 @@ tcTyClDecls tyclds kisig_env role_annots
             -- NB: We have to be careful here to NOT eagerly unfold
             -- type synonyms, as we have not tested for type synonym
             -- loops yet and could fall into a black hole.
-       ; fixM $ \ ~(rec_tyclss, _, _) -> do
+       ; fixM $ \ ~(rec_tyclss, _, _, _) -> do
            { tcg_env <- getGblEnv
                  -- Forced so we don't retain a reference to the TcGblEnv
            ; let !src  = tcg_src tcg_env
                  roles = inferRoles src role_annots rec_tyclss
+                 class_scoped_tv_env = mk_class_scoped_tv_env tc_tycons
 
                  -- Populate environment with knot-tied ATyCon for TyCons
                  -- NB: if the decls mention any ill-staged data cons
@@ -260,7 +265,7 @@ tcTyClDecls tyclds kisig_env role_annots
 
                  -- Kind and type check declarations for this group
                mapAndUnzipM (tcTyClDecl roles) tyclds
-           ; return (tycons, concat data_deriv_infos, kindless)
+           ; return (tycons, concat data_deriv_infos, class_scoped_tv_env, kindless)
            } }
   where
     ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
@@ -268,6 +273,16 @@ tcTyClDecls tyclds kisig_env role_annots
                                   , ppr (tyConResKind tc)
                                   , ppr (isTcTyCon tc) ])
 
+    -- Map each class TcTyCon to their tcTyConScopedTyVars. This is ultimately
+    -- meant to be passed to GHC.Tc.TyCl.Class.tcClassDecl2, which consults
+    -- it when bringing type variables into scope over class method defaults.
+    -- See @Note [Scoped tyvars in a TcTyCon]@ in "GHC.Core.TyCon".
+    mk_class_scoped_tv_env :: [TcTyCon] -> ClassScopedTVEnv
+    mk_class_scoped_tv_env tc_tycons =
+      mkNameEnv [ (tyConName tc_tycon, tcTyConScopedTyVars tc_tycon)
+                | tc_tycon <- tc_tycons, tyConFlavour tc_tycon == ClassFlavour
+                ]
+
 zipRecTyClss :: [TcTyCon]
              -> [TyCon]           -- Knot-tied
              -> [(Name,TyThing)]
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
index a55a774069..1c1f6608cd 100644
--- a/compiler/GHC/Tc/TyCl/Class.hs
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -13,6 +13,7 @@
 module GHC.Tc.TyCl.Class
    ( tcClassSigs
    , tcClassDecl2
+   , ClassScopedTVEnv
    , findMethodBind
    , instantiateMethod
    , tcClassMinimalDef
@@ -39,7 +40,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     ( piResultTys, substTyVar )
 import GHC.Core.Predicate
 import GHC.Core.Multiplicity
 import GHC.Tc.Types.Origin
@@ -187,10 +188,16 @@ tcClassSigs clas sigs def_methods
 ************************************************************************
 -}
 
-tcClassDecl2 :: LTyClDecl GhcRn          -- The class declaration
+-- | Maps class names to the type variables that scope over their bodies.
+-- See @Note [Scoped tyvars in a TcTyCon]@ in "GHC.Core.TyCon".
+type ClassScopedTVEnv = NameEnv [(Name, TyVar)]
+
+tcClassDecl2 :: ClassScopedTVEnv         -- Class scoped type variables
+             -> LTyClDecl GhcRn          -- The class declaration
              -> TcM (LHsBinds GhcTc)
 
-tcClassDecl2 (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
+tcClassDecl2 class_scoped_tv_env
+             (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
                                 tcdMeths = default_binds}))
   = recoverM (return emptyLHsBinds) $
     setSrcSpan (getLocA class_name) $
@@ -205,20 +212,31 @@ tcClassDecl2 (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
         -- And since ds is big, it doesn't get inlined, so we don't get good
         -- default methods.  Better to make separate AbsBinds for each
         ; let (tyvars, _, _, op_items) = classBigSig clas
-              prag_fn     = mkPragEnv sigs default_binds
-              sig_fn      = mkHsSigFun sigs
-              clas_tyvars = snd (tcSuperSkolTyVars tyvars)
-              pred        = mkClassPred clas (mkTyVarTys clas_tyvars)
+              prag_fn = mkPragEnv sigs default_binds
+              sig_fn  = mkHsSigFun sigs
+              (skol_subst, clas_tyvars) = tcSuperSkolTyVars tyvars
+              pred = mkClassPred clas (mkTyVarTys clas_tyvars)
+              scoped_tyvars =
+                case lookupNameEnv class_scoped_tv_env (unLoc class_name) of
+                  Just tvs -> tvs
+                  Nothing  -> pprPanic "tcClassDecl2: Class name not in tcg_class_scoped_tvs_env"
+                                       (ppr class_name)
+              -- The substitution returned by tcSuperSkolTyVars maps each type
+              -- variable to a TyVarTy, so it is safe to call getTyVar below.
+              scoped_clas_tyvars =
+                mapSnd ( getTyVar ("tcClassDecl2: Super-skolem substitution maps "
+                                   ++ "type variable to non-type variable")
+                       . substTyVar skol_subst ) scoped_tyvars
         ; this_dict <- newEvVar pred
 
         ; let tc_item = tcDefMeth clas clas_tyvars this_dict
                                   default_binds sig_fn prag_fn
-        ; dm_binds <- tcExtendTyVarEnv clas_tyvars $
+        ; dm_binds <- tcExtendNameTyVarEnv scoped_clas_tyvars $
                       mapM tc_item op_items
 
         ; return (unionManyBags dm_binds) }
 
-tcClassDecl2 d = pprPanic "tcClassDecl2" (ppr d)
+tcClassDecl2 _ d = pprPanic "tcClassDecl2" (ppr d)
 
 tcDefMeth :: Class -> [TyVar] -> EvVar -> LHsBinds GhcRn
           -> HsSigFun -> TcPragEnv -> ClassOpItem
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index b9a4e17bf7..5a824b0e48 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -27,7 +27,7 @@ import GHC.Hs
 import GHC.Tc.Gen.Bind
 import GHC.Tc.TyCl
 import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv )
-import GHC.Tc.TyCl.Class ( tcClassDecl2, tcATDefault,
+import GHC.Tc.TyCl.Class ( tcClassDecl2, ClassScopedTVEnv, tcATDefault,
                            HsSigFun, mkHsSigFun, badMethodErr,
                            findMethodBind, instantiateMethod )
 import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
@@ -1143,17 +1143,17 @@ takes a slightly different approach.
 *                                                                      *
 ********************************************************************* -}
 
-tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn]
+tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn] -> ClassScopedTVEnv
              -> TcM (LHsBinds GhcTc)
 -- (a) From each class declaration,
 --      generate any default-method bindings
 -- (b) From each instance decl
 --      generate the dfun binding
 
-tcInstDecls2 tycl_decls inst_decls
+tcInstDecls2 tycl_decls inst_decls class_scoped_tv_env
   = do  { -- (a) Default methods from class decls
           let class_decls = filter (isClassDecl . unLoc) tycl_decls
-        ; dm_binds_s <- mapM tcClassDecl2 class_decls
+        ; dm_binds_s <- mapM (tcClassDecl2 class_scoped_tv_env) class_decls
         ; let dm_binds = unionManyBags dm_binds_s
 
           -- (b) instance declarations
diff --git a/testsuite/tests/typecheck/should_compile/T19738.hs b/testsuite/tests/typecheck/should_compile/T19738.hs
new file mode 100644
index 0000000000..4c704b6d5e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19738.hs
@@ -0,0 +1,11 @@
+module T19738 where
+
+import Data.Kind
+
+type P :: k -> Type
+data P a = MkP
+
+type T :: k -> Constraint
+class T (a :: j) where
+  f :: P a
+  f = MkP @j @a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9b3753848f..9d0225a6c2 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -783,4 +783,5 @@ test('T18467', normal, compile, [''])
 test('T19315', normal, compile, [''])
 
 test('T19535', normal, compile, [''])
+test('T19738', normal, compile, [''])
 test('T19742', normal, compile, [''])