diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index d50cd70e3ab5aa4fc5c77a5934a56962426a19a4..eb31e4177cdf217395d4d46c4b7e20d41a599da6 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1178,17 +1178,30 @@ tc_hs_type mode (HsOpTy _ _ ty1 (L _ op) ty2) exp_kind
= tc_fun_type mode (HsUnrestrictedArrow noHsUniTok) ty1 ty2 exp_kind
--------- Foralls
-tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
- = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
- tc_lhs_type mode ty exp_kind
+tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+ | HsForAllInvis{} <- tele
+ = tc_hs_forall_ty tele ty exp_kind
+ -- For an invisible forall, we allow the body to have
+ -- an arbitrary kind (hence exp_kind above).
+ -- See Note [Body kind of a HsForAllTy]
+
+ | HsForAllVis{} <- tele
+ = do { ek <- newOpenTypeKind
+ ; r <- tc_hs_forall_ty tele ty ek
+ ; checkExpectedKind t r ek exp_kind }
+ -- For a visible forall, we require that the body is of kind TYPE r.
+ -- See Note [Body kind of a HsForAllTy]
+
+ where
+ tc_hs_forall_ty tele ty ek
+ = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
+ tc_lhs_type mode ty ek
-- Pass on the mode from the type, to any wildcards
-- in kind signatures on the forall'd variables
-- e.g. f :: _ -> Int -> forall (a :: _). blah
- -- Why exp_kind? See Note [Body kind of a HsForAllTy]
- -- Do not kind-generalise here! See Note [Kind generalisation]
-
- ; return (mkForAllTys tv_bndrs ty') }
+ -- Do not kind-generalise here! See Note [Kind generalisation]
+ ; return (mkForAllTys tv_bndrs ty') }
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
@@ -2042,25 +2055,23 @@ examples.
Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The body of a forall is usually a type, but in principle
-there's no reason to prohibit *unlifted* types.
-In fact, GHC can itself construct a function with an
-unboxed tuple inside a for-all (via CPR analysis; see
+The body of a forall is usually a type.
+Because of representation polymorphism, it can be a TYPE r, for any r.
+(In fact, GHC can itself construct a function with an
+unboxed tuple inside a for-all via CPR analysis; see
typecheck/should_compile/tc170).
-Moreover in instance heads we get forall-types with
-kind Constraint.
-
-It's tempting to check that the body kind is (TYPE _). But this is
-wrong. For example:
+A forall can also be used in an instance head, then the body should
+be a constraint.
- class C a b
- newtype N = Mk Foo deriving (C a)
+Right now, we do not have any easy way to enforce that a type is
+either a TYPE something or CONSTRAINT something, so we accept any kind.
+This is unsound (#22063). We could fix this by implementing a TypeLike
+predicate, see #20000.
-We're doing newtype-deriving for C. But notice how `a` isn't in scope in
-the predicate `C a`. So we quantify, yielding `forall a. C a` even though
-`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
-convenient. Bottom line: don't check for (TYPE _) here.
+For a forall with a required argument, we do not allow constraints;
+e.g. forall a -> Eq a is invalid. Therefore, we can enforce that the body
+is a TYPE something in this case (#24176).
Note [Body kind of a HsQualTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
index 30bd04b484df768b57405a1fbd0b2d27774bab43..1624cad997b3ac72017ccf0d4e384aaaae89150c 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail12.stderr
@@ -1,8 +1,8 @@
-T16326_Fail12.hs:6:1: error: [GHC-51580]
- • Illegal visible, dependent quantification in the type of a term:
- forall a -> Show a
- • In the context: forall a -> Show a
- While checking the super-classes of class ‘C’
- In the class declaration for ‘C’
- Suggested fix: Perhaps you intended to use RequiredTypeArguments
+T16326_Fail12.hs:6:8: error: [GHC-83865]
+ • Expected a constraint, but ‘forall a -> Show a’ is a type
+ • In the class declaration for ‘C’
+
+T16326_Fail12.hs:6:20: error: [GHC-83865]
+ • Expected a type, but ‘Show a’ is a constraint
+ • In the class declaration for ‘C’
diff --git a/testsuite/tests/vdq-rta/should_fail/T24176.hs b/testsuite/tests/vdq-rta/should_fail/T24176.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ca5f533e272fb4c1980382d727b12b6f9c843b4a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24176.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
+module T24176 where
+
+f :: (forall a -> Eq a) => a
+f = f
diff --git a/testsuite/tests/vdq-rta/should_fail/T24176.stderr b/testsuite/tests/vdq-rta/should_fail/T24176.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..82732ca8bb665d6bf2b5760d553c0dd46347d192
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24176.stderr
@@ -0,0 +1,8 @@
+
+T24176.hs:4:7: error: [GHC-83865]
+ • Expected a constraint, but ‘forall a -> Eq a’ is a type
+ • In the type signature: f :: (forall a -> Eq a) => a
+
+T24176.hs:4:19: error: [GHC-83865]
+ • Expected a type, but ‘Eq a’ is a constraint
+ • In the type signature: f :: (forall a -> Eq a) => a
diff --git a/testsuite/tests/vdq-rta/should_fail/all.T b/testsuite/tests/vdq-rta/should_fail/all.T
index 1a71961c6811fd23bcb30858e11f65d98f375c2e..917a48be493d0ddb18936f9d50ba6a122d6a6ce4 100644
--- a/testsuite/tests/vdq-rta/should_fail/all.T
+++ b/testsuite/tests/vdq-rta/should_fail/all.T
@@ -14,4 +14,5 @@ test('T22326_fail_patsyn', normal, compile_fail, [''])
test('T22326_fail_match', normal, compile_fail, [''])
test('T23738_fail_wild', normal, compile_fail, [''])
test('T23738_fail_implicit_tv', normal, compile_fail, [''])
-test('T23738_fail_var', normal, compile_fail, [''])
\ No newline at end of file
+test('T23738_fail_var', normal, compile_fail, [''])
+test('T24176', normal, compile_fail, [''])