compiler/GHC/Core/Type.hs

@@ -50,7 +50,7 @@ module GHC.Core.Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInfForAllTy, mkInfForAllTys,
-        splitForAllTyCoVars,
+        splitForAllTyCoVars, splitForAllTyVars,
         splitForAllReqTyBinders, splitForAllInvisTyBinders,
         splitForAllForAllTyBinders,
         splitForAllTyCoVar_maybe, splitForAllTyCoVar,

compiler/GHC/Tc/Gen/Bind.hs

@@ -49,7 +49,7 @@ import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
 import GHC.Tc.Utils.TcType
-import GHC.Tc.Validity (checkValidType)
+import GHC.Tc.Validity (checkValidType, checkEscapingKind)
 
 import GHC.Core.Predicate
 import GHC.Core.Reduction ( Reduction(..) )
@@ -906,7 +906,8 @@ mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mo
                                           , ppr inferred_poly_ty])
        ; unless insoluble $
          addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
-         checkValidType (InfSigCtxt poly_name) inferred_poly_ty
+         do { checkEscapingKind inferred_poly_ty
+            ; checkValidType (InfSigCtxt poly_name) inferred_poly_ty }
          -- See Note [Validity of inferred types]
          -- If we found an insoluble error in the function definition, don't
          -- do this check; otherwise (#14000) we may report an ambiguity

compiler/GHC/Tc/TyCl.hs

@@ -4408,10 +4408,7 @@ checkValidDataCon dflags existential_ok tc con
           --  e.g. reject this:   MkT :: T (forall a. a->a)
           -- Reason: it's really the argument of an equality constraint
         ; checkValidMonoType orig_res_ty
-
-        -- Check for an escaping result kind
-        -- See Note [Check for escaping result kind]
-        ; checkEscapingKind con
+        ; checkEscapingKind (dataConWrapperType con)
 
         -- For /data/ types check that each argument has a fixed runtime rep
         -- If we are dealing with a /newtype/, we allow representation
@@ -4576,47 +4573,6 @@ checkNewDataCon con
     ok_mult OneTy = True
     ok_mult _     = False
 
-
--- | Reject nullary data constructors where a type variable
--- would escape through the result kind
--- See Note [Check for escaping result kind]
-checkEscapingKind :: DataCon -> TcM ()
-checkEscapingKind data_con
-  | null eq_spec, null theta, null arg_tys
-  , let tau_kind = typeKind res_ty
-  , Nothing <- occCheckExpand (univ_tvs ++ ex_tvs) tau_kind
-    -- Ensure that none of the tvs occur in the kind of the forall
-    -- /after/ expanding type synonyms.
-    -- See Note [Phantom type variables in kinds] in GHC.Core.Type
-  = failWithTc $ TcRnForAllEscapeError (dataConWrapperType data_con) tau_kind
-  | otherwise
-  = return ()
-  where
-    (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
-      = dataConFullSig data_con
-
-{- Note [Check for escaping result kind]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:
-  type T :: TYPE (BoxedRep l)
-  data T = MkT
-This is not OK: we get
-  MkT :: forall l. T @l :: TYPE (BoxedRep l)
-which is ill-kinded.
-
-For ordinary type signatures f :: blah, we make this check as part of kind-checking
-the type signature; see Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.
-But for data constructors we check the type piecemeal, and there is no very
-convenient place to do it.  For example, note that it only applies for /nullary/
-constructors.  If we had
-  data T = MkT Int
-then the type of MkT would be MkT :: forall l. Int -> T @l, which is fine.
-
-So we make the check in checkValidDataCon.
-
-Historical note: we used to do the check in checkValidType (#20929 discusses).
--}
-
 -------------------------------
 checkValidClass :: Class -> TcM ()
 checkValidClass cls

compiler/GHC/Tc/Validity.hs

@@ -12,7 +12,7 @@ module GHC.Tc.Validity (
   Rank(..), UserTypeCtxt(..), checkValidType, checkValidMonoType,
   checkValidTheta,
   checkValidInstance, checkValidInstHead, validDerivPred,
-  checkTySynRhs,
+  checkTySynRhs, checkEscapingKind,
   checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
   arityErr,
@@ -466,6 +466,53 @@ checkTySynRhs ctxt ty
   where
     actual_kind = typeKind ty
 
+{- Note [Check for escaping result kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+  type T :: TYPE (BoxedRep l)
+  data T = MkT
+This is not OK: we get
+  MkT :: forall l. T @l :: TYPE (BoxedRep l)
+which is ill-kinded.
+
+For ordinary /user-written type signatures f :: blah, we make this
+check as part of kind-checking the type signature in tcHsSigType; see
+Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.
+
+But in two other places we need to check for an escaping result kind:
+
+* For data constructors we check the type piecemeal, and there is no
+  very convenient place to do it.  For example, note that it only
+  applies for /nullary/ constructors.  If we had
+    data T = MkT Int
+  then the type of MkT would be MkT :: forall l. Int -> T @l, which is fine.
+
+  So we make the check in checkValidDataCon.
+
+* When inferring the type of a function, there is no user-written type
+  that we are checking.  Forgetting this led to #22743.  Now we call
+  checkEscapingKind in GHC.Tc.Gen.Bind.mkInferredPolyId
+
+Historical note: we used to do the escaping-kind check in
+checkValidType (#20929 discusses), but that is now redundant.
+-}
+
+checkEscapingKind :: Type -> TcM ()
+-- Give a sigma-type (forall a1 .. an. ty), where (ty :: ki),
+-- check that `ki` does not mention any of the binders a1..an.
+-- Otherwise the type is ill-kinded
+-- See Note [Check for escaping result kind]
+checkEscapingKind poly_ty
+  | (tvs, tau) <- splitForAllTyVars poly_ty
+  , let tau_kind = typeKind tau
+  , Nothing <- occCheckExpand tvs tau_kind
+    -- Ensure that none of the tvs occur in the kind of the forall
+    -- /after/ expanding type synonyms.
+    -- See Note [Phantom type variables in kinds] in GHC.Core.Type
+  = failWithTc $ TcRnForAllEscapeError poly_ty tau_kind
+  | otherwise
+  = return ()
+
 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
 funArgResRank other_rank               = (other_rank, other_rank)
@@ -762,6 +809,9 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env
         ; check_type (ve{ve_tidy_env = env'}) tau
                 -- Allow foralls to right of arrow
 
+        -- Note: skolem-escape in types (e.g. forall r (a::r). a) is handled
+        --       by tcHsSigType and the constraint solver, so no need to
+        --       check it here; c.f. #20929
         }
   where
     (tvbs, phi)   = tcSplitForAllTyVarBinders ty

gmp-tarballs @ 7bb13b55

-Subproject commit 6bbea995472b6f4db172c3cd50aa3f515ddd221c
+Subproject commit 7bb13b556d81e60556db6b5ef8757f55a3925527

parsec @ 1f542120

-Subproject commit 0e23b3246fd7f6d125129316dcbedd609e6d2dca
+Subproject commit 1f542120d9adc5e22f8791a6d595210e93c6c389

testsuite/tests/polykinds/T22743.hs

+{-# LANGUAGE DataKinds #-}
+module M where
+
+import GHC.Exts
+import Data.Kind
+
+f :: forall f (g :: Type) (a :: TYPE (f g)). Int -> a
+f = f
+
+x = f 0

testsuite/tests/polykinds/T22743.stderr

+
+T22743.hs:10:1: error: [GHC-31147]
+    • Quantified type's kind mentions quantified type variable
+        type: ‘forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a’
+      where the body of the forall has this kind: ‘TYPE (f g)’
+    • When checking the inferred type
+        x :: forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a

testsuite/tests/polykinds/all.T

@@ -241,3 +241,4 @@ test('T19739c', normal, compile, [''])
 test('T19739d', normal, compile, [''])
 test('T22379a', normal, compile, [''])
 test('T22379b', normal, compile, [''])
+test('T22743', normal, compile_fail, [''])