Add accurate skolem info when quantifyingwip/T22379

Ticket #22379 revealed that skolemiseQuantifiedTyVar was
dropping the passed-in skol_info on the floor when it encountered
a SkolemTv.  Bad!  Several TyCons thereby share a single SkolemInfo
on their binders, which lead to bogus error reports.

9 files changed, 139 insertions, 64 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 77aa280af8..a664092221 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -3489,6 +3489,8 @@ bindTyClTyVars tycon_name thing_inside
 bindTyClTyVarsAndZonk :: Name -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
 -- Like bindTyClTyVars, but in addition
 -- zonk the skolem TcTyVars of a PolyTcTyCon to TyVars
+-- We always do this same zonking after a call to bindTyClTyVars, but
+-- here we do it right away because there are no more unifications to come
 bindTyClTyVarsAndZonk tycon_name thing_inside
   = bindTyClTyVars tycon_name $ \ tc_bndrs tc_kind ->
     do { ze          <- mkEmptyZonkEnv NoFlexi
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index ac5e336e65..225e53d83e 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -411,21 +411,27 @@ TcTyCons are used for two distinct purposes
 2.  When checking a type/class declaration (in module GHC.Tc.TyCl), we come
     upon knowledge of the eventual tycon in bits and pieces, and we use
     a TcTyCon to record what we know before we are ready to build the
-    final TyCon.
+    final TyCon.  Here is the plan:
 
-    We first build a MonoTcTyCon, then generalise to a PolyTcTyCon
-    See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType
-    Specifically:
+    Step 1 (inferInitialKinds, inference only, skipped for checking):
+       Make a MonoTcTyCon whose binders are TcTyVars,
+       which may contain free unification variables
 
-      S1) In kcTyClGroup, we use checkInitialKinds to get the
-          utterly-final Kind of all TyCons in the group that
-            (a) have a kind signature or
-            (b) have a CUSK.
-          This produces a PolyTcTyCon, that is, a TcTyCon in which the binders
-          and result kind are full of TyVars (not TcTyVars).  No unification
-          variables here; everything is in its final form.
+    Step 2 (generaliseTcTyCon)
+       Generalise that MonoTcTyCon to make a PolyTcTyCon
+       Its binders are skolem TcTyVars, with accurate SkolemInfo
+
+    Step 3 (tcTyClDecl)
+       Typecheck the type and class decls to produce a final TyCon
+       Its binders are final TyVars, not TcTyVars
+
+    Note that a MonoTcTyCon can contain unification variables,
+    but a PolyTcTyCon does not: only skolem TcTyVars.  See
+    Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType
+
+    More details about /kind inference/:
 
-      S2) In kcTyClGroup, we use inferInitialKinds to look over the
+      S1) In kcTyClGroup, we use inferInitialKinds to look over the
           declaration of any TyCon that lacks a kind signature or
           CUSK, to determine its "shape"; for example, the number of
           parameters, and any kind signatures.
@@ -434,27 +440,30 @@ TcTyCons are used for two distinct purposes
           "mono" because it has not been been generalised, and its binders
           and result kind may have free unification variables.
 
-      S3) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the
+      S2) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the
           body (class methods, data constructors, etc.) of each of
           these MonoTcTyCons, which has the effect of filling in the
           metavariables in the tycon's initial kind.
 
-      S4) Still in kcTyClGroup, we use generaliseTyClDecl to generalize
-          each MonoTcTyCon to get a PolyTcTyCon, with final TyVars in it,
+      S3) Still in kcTyClGroup, we use generaliseTyClDecl to generalize
+          each MonoTcTyCon to get a PolyTcTyCon, with skolem TcTyVars in it,
           and a final, fixed kind.
 
-      S5) Finally, back in TcTyClDecls, we extend the environment with
+      S4) Finally, back in TcTyClDecls, we extend the environment with
           the PolyTcTyCons, and typecheck each declaration (regardless
           of kind signatures etc) to get final TyCon.
 
-    These TcTyCons are stored in the local environment in GHC.Tc.TyCl,
-    until the real full TyCons can be created during desugaring. A
-    desugared program should never have a TcTyCon.
+    More details about /kind checking/
 
-3.  A MonoTcTyCon can contain unification variables, but a PolyTcTyCon
-    does not: only skolem TcTyVars.
+      S5) In kcTyClGroup, we use checkInitialKinds to get the
+          utterly-final Kind of all TyCons in the group that
+            (a) have a separate kind signature or
+            (b) have a CUSK.
+          This produces a PolyTcTyCon, that is, a TcTyCon in which the binders
+          and result kind are full of TyVars (not TcTyVars).  No unification
+          variables here; everything is in its final form.
 
-4.  tyConScopedTyVars.  A challenging piece in all of this is that we
+3.  tyConScopedTyVars.  A challenging piece in all of this is that we
     end up taking three separate passes over every declaration:
       - one in inferInitialKind (this pass look only at the head, not the body)
       - one in kcTyClDecls (to kind-check the body)
@@ -2425,15 +2434,15 @@ tcClassDecl1 :: RolesInfo -> Name -> Maybe (LHsContext GhcRn)
              -> TcM Class
 tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
   = fixM $ \ clas -> -- We need the knot because 'clas' is passed into tcClassATs
-    bindTyClTyVars class_name $ \ binders res_kind ->
+    bindTyClTyVars class_name $ \ tc_bndrs res_kind ->
     do { checkClassKindSig res_kind
-       ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
+       ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tc_bndrs)
        ; let tycon_name = class_name        -- We use the same name
              roles = roles_info tycon_name  -- for TyCon and Class
 
        ; (ctxt, fds, sig_stuff, at_stuff)
-            <- pushLevelAndSolveEqualities skol_info binders $
-               -- The (binderVars binders) is needed bring into scope the
+            <- pushLevelAndSolveEqualities skol_info tc_bndrs $
+               -- The (binderVars tc_bndrs) is needed bring into scope the
                -- skolems bound by the class decl header (#17841)
                do { ctxt <- tcHsContext hs_ctxt
                   ; fds  <- mapM (addLocMA tc_fundep) fundeps
@@ -2458,9 +2467,10 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
        -- any unfilled coercion variables unless there is such an error
        -- The zonk also squeeze out the TcTyCons, and converts
        -- Skolems to tyvars.
-       ; ze        <- mkEmptyZonkEnv NoFlexi
-       ; ctxt      <- zonkTcTypesToTypesX ze ctxt
-       ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
+       ; ze          <- mkEmptyZonkEnv NoFlexi
+       ; (ze, bndrs) <- zonkTyVarBindersX ze tc_bndrs  -- From TcTyVars to TyVars
+       ; ctxt        <- zonkTcTypesToTypesX ze ctxt
+       ; sig_stuff   <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
          -- ToDo: do we need to zonk at_stuff?
 
        -- TODO: Allow us to distinguish between abstract class,
@@ -2482,8 +2492,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
                   | otherwise
                   = Just (ctxt, at_stuff, sig_stuff, mindef)
 
-       ; clas <- buildClass class_name binders roles fds body
-       ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
+       ; clas <- buildClass class_name bndrs roles fds body
+       ; traceTc "tcClassDecl" (ppr fundeps $$ ppr bndrs $$
                                 ppr fds)
        ; return clas }
   where
@@ -2712,7 +2722,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
                               , fdResultSig = L _ sig
                               , fdInjectivityAnn = inj })
   | DataFamily <- fam_info
-  = bindTyClTyVarsAndZonk tc_name $ \ binders res_kind -> do
+  = bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> do
   { traceTc "tcFamDecl1 data family:" (ppr tc_name)
   ; checkFamFlag tc_name
 
@@ -2729,8 +2739,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   -- See also Note [Datatype return kinds]
   ; checkDataKindSig DataFamilySort res_kind
   ; tc_rep_name <- newTyConRepName tc_name
-  ; let inj   = Injective $ replicate (length binders) True
-        tycon = mkFamilyTyCon tc_name binders
+  ; let inj   = Injective $ replicate (length tc_bndrs) True
+        tycon = mkFamilyTyCon tc_name tc_bndrs
                               res_kind
                               (resultVariableName sig)
                               (DataFamilyTyCon tc_rep_name)
@@ -2738,12 +2748,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   ; return tycon }
 
   | OpenTypeFamily <- fam_info
-  = bindTyClTyVarsAndZonk tc_name $ \ binders res_kind -> do
+  = bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> do
   { traceTc "tcFamDecl1 open type family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; inj' <- tcInjectivity binders inj
+  ; inj' <- tcInjectivity tc_bndrs inj
   ; checkResultSigFlag tc_name sig  -- check after injectivity for better errors
-  ; let tycon = mkFamilyTyCon tc_name binders res_kind
+  ; let tycon = mkFamilyTyCon tc_name tc_bndrs res_kind
                                (resultVariableName sig) OpenSynFamilyTyCon
                                parent inj'
   ; return tycon }
@@ -2754,10 +2764,10 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
     do { traceTc "tcFamDecl1 Closed type family:" (ppr tc_name)
          -- the variables in the header scope only over the injectivity
          -- declaration but this is not involved here
-       ; (inj', binders, res_kind)
-            <- bindTyClTyVarsAndZonk tc_name $ \ binders res_kind ->
-               do { inj' <- tcInjectivity binders inj
-                  ; return (inj', binders, res_kind) }
+       ; (inj', tc_bndrs, res_kind)
+            <- bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind ->
+               do { inj' <- tcInjectivity tc_bndrs inj
+                  ; return (inj', tc_bndrs, res_kind) }
 
        ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
        ; checkResultSigFlag tc_name sig
@@ -2766,14 +2776,14 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
          -- but eqns might be empty in the Just case as well
        ; case mb_eqns of
            Nothing   ->
-               return $ mkFamilyTyCon tc_name binders res_kind
+               return $ mkFamilyTyCon tc_name tc_bndrs res_kind
                                       (resultVariableName sig)
                                       AbstractClosedSynFamilyTyCon parent
                                       inj'
            Just eqns -> do {
 
          -- Process the equations, creating CoAxBranches
-       ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind
+       ; let tc_fam_tc = mkTcTyCon tc_name tc_bndrs res_kind
                                    noTcTyConScopedTyVars
                                    False {- this doesn't matter here -}
                                    ClosedTypeFamilyFlavour
@@ -2792,7 +2802,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
               | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
               | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
 
-             fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
+             fam_tc = mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig)
                       (ClosedSynFamilyTyCon mb_co_ax) parent inj'
 
          -- We check for instance validity later, when doing validity
@@ -2853,10 +2863,10 @@ tcInjectivity tcbs (Just (L loc (InjectivityAnn _ _ lInjNames)))
 tcTySynRhs :: RolesInfo -> Name
            -> LHsType GhcRn -> TcM TyCon
 tcTySynRhs roles_info tc_name hs_ty
-  = bindTyClTyVars tc_name $ \ binders res_kind ->
+  = bindTyClTyVars tc_name $ \ tc_bndrs res_kind ->
     do { env <- getLclEnv
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
-       ; rhs_ty <- pushLevelAndSolveEqualities skol_info binders $
+       ; rhs_ty <- pushLevelAndSolveEqualities skol_info tc_bndrs $
                    tcCheckLHsType hs_ty (TheKind res_kind)
 
          -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
@@ -2870,11 +2880,11 @@ tcTySynRhs roles_info tc_name hs_ty
                                                  , ppr rhs_ty ] ) }
        ; doNotQuantifyTyVars dvs mk_doc
 
-       ; ze            <- mkEmptyZonkEnv NoFlexi
-       ; (ze, binders) <- zonkTyVarBindersX ze binders
-       ; rhs_ty        <- zonkTcTypeToTypeX ze rhs_ty
+       ; ze          <- mkEmptyZonkEnv NoFlexi
+       ; (ze, bndrs) <- zonkTyVarBindersX ze tc_bndrs
+       ; rhs_ty      <- zonkTcTypeToTypeX ze rhs_ty
        ; let roles = roles_info tc_name
-       ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) }
+       ; return (buildSynTyCon tc_name bndrs res_kind roles rhs_ty) }
   where
     skol_info = TyConSkol TypeSynonymFlavour tc_name
 
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 1cb4820745..68b8285af8 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1735,12 +1735,6 @@ quantifyTyVars skol_info ns_strat dvs
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
 
--- Omit: no TyVars now
---      | not (isTcTyVar tkv)
---      = return (Just tkv)  -- For associated types in a class with a standalone
---                           -- kind signature, we have the class variables in
---                           -- scope, and they are TyVars not TcTyVars
-
       | otherwise
       = Just <$> skolemiseQuantifiedTyVar skol_info tkv
 
@@ -1785,13 +1779,19 @@ skolemiseQuantifiedTyVar :: SkolemInfo -> TcTyVar -> TcM TcTyVar
 
 skolemiseQuantifiedTyVar skol_info tv
   = case tcTyVarDetails tv of
-      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
-                        ; return (setTyVarKind tv kind) }
-        -- It might be a skolem type variable,
-        -- for example from a user type signature
-
       MetaTv {} -> skolemiseUnboundMetaTyVar skol_info tv
 
+      SkolemTv _ lvl _  -- It might be a skolem type variable,
+                        -- for example from a user type signature
+        -- But it might also be a shared meta-variable across several
+        -- type declarations, each with its own skol_info. The first
+        -- will skolemise it, but the other uses must update its
+        -- skolem info (#22379)
+        -> do { kind <- zonkTcType (tyVarKind tv)
+              ; let details = SkolemTv skol_info lvl False
+                    name = tyVarName tv
+              ; return (mkTcTyVar name kind details) }
+
       _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
 -- | Default a type variable using the given defaulting strategy.
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 6592912d05..eae089c203 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -428,7 +428,7 @@ Invariants:
   - Flag tcTyConIsPoly = True; this is used only to short-cut zonking
 
   - tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars,
-    with fixed kinds: no unification variables here
+    with fixed kinds, and accurate skolem info: no unification variables here
 
     tyConBinders includes the Inferred binders if any
 
diff --git a/testsuite/tests/deriving/should_fail/T21871.stderr b/testsuite/tests/deriving/should_fail/T21871.stderr
index 3ec33ef61b..4cb5bff9a1 100644
--- a/testsuite/tests/deriving/should_fail/T21871.stderr
+++ b/testsuite/tests/deriving/should_fail/T21871.stderr
@@ -3,7 +3,7 @@ T21871.hs:13:36: error: [GHC-25897]
     • Couldn't match kind ‘k’ with ‘*’
       Expected kind ‘* -> *’, but ‘m’ has kind ‘k -> *’
       ‘k’ is a rigid type variable bound by
-        the newtype declaration for ‘FooT’
+        a `deriving' clause
         at T21871.hs:(10,1)-(13,36)
     • In the second argument of ‘ReaderT’, namely ‘m’
       In the newtype declaration for ‘FooT’
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index ced646a276..35bc2a43b9 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -3,7 +3,7 @@ T15870.hs:32:34: error: [GHC-25897]
     • Couldn't match kind ‘k’ with ‘*’
       Expected kind ‘Optic @{k} a’, but ‘g2’ has kind ‘Optic @{*} b’
       ‘k’ is a rigid type variable bound by
-        the instance declaration
+        a family instance declaration
         at T15870.hs:(27,1)-(32,35)
     • In the second argument of ‘Get’, namely ‘g2’
       In the type ‘Get a g2’
diff --git a/testsuite/tests/polykinds/T22379a.hs b/testsuite/tests/polykinds/T22379a.hs
new file mode 100644
index 0000000000..d4caa01048
--- /dev/null
+++ b/testsuite/tests/polykinds/T22379a.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy (Proxy)
+
+data Delayed (env :: Type) (c :: Type)
+data Handler (a :: Type)
+data Router (a :: Type)
+
+-- class decl, then type decl
+
+class HasServer api where
+  type ServerT api (m :: Type -> Type) :: Type
+
+  route ::
+       Proxy api
+    -> Delayed env (Server api)
+    -> Router env
+
+  hoistServerWithContext
+      :: Proxy api
+      -> (forall x. m x -> n x)
+      -> ServerT api m
+      -> ServerT api n
+
+type Server aqi = ServerT aqi Handler
+
diff --git a/testsuite/tests/polykinds/T22379b.hs b/testsuite/tests/polykinds/T22379b.hs
new file mode 100644
index 0000000000..78cd004090
--- /dev/null
+++ b/testsuite/tests/polykinds/T22379b.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy (Proxy)
+
+data Delayed (env :: Type) (c :: Type)
+data Handler (a :: Type)
+data Router (a :: Type)
+
+-- type decl, then class decl
+
+type Server aqi = ServerT aqi Handler
+
+class HasServer api where
+  type ServerT api (m :: Type -> Type) :: Type
+
+  route ::
+       Proxy api
+    -> Delayed env (Server api)
+    -> Router env
+
+  hoistServerWithContext
+      :: Proxy api
+      -> (forall x. m x -> n x)
+      -> ServerT api m
+      -> ServerT api n
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index fbe65d4b1c..721e41cebd 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -239,3 +239,5 @@ test('T19739a', normal, compile, [''])
 test('T19739b', normal, compile, [''])
 test('T19739c', normal, compile, [''])
 test('T19739d', normal, compile, [''])
+test('T22379a', normal, compile, [''])
+test('T22379b', normal, compile, [''])