Forall-types should be of a TYPE kind

This is the main ticket for a bunch of related tickets, relating to the kind of (forall a. ty). Specifically

• #22063 (this ticket)
• #8388
• #15979
• #19573

Summary

With or without impredicativity, we usually intend a forall-quantified type to be inhabited by values, i.e. that forall a. {- ... -} :: TYPE r for some r. Apparently this is never checked in GHC and we have roughly:

     Gamma, a |- t :: k
---------------------------
Gamma |- (forall a. t) :: k

This implies that all kinds (even closed) are lifted: forall a. a :: k. Of course in presence of TypeFamilies+UndecidableInstances all kinds are already lifted, but this seems somehow worse.

Furthermore such a type can be used to trigger a core lint error, the wording of which ("Non-*-like kind when *-like expected") suggests that at least on some level it is expected that forall a. ... :: *. Applying a type constructor (other than ->) to a type like forall a. a requires ImpredicativeTypes, but (and this might be an unrelated issue) apparently the type can appear on the left side of an application even without ImpredicativeTypes.

Steps to reproduce

GHCi says:

> :kind forall a. a
forall a. a :: k

The following are accepted by GHC 9.2.3, 8.6.5 and HEAD:

{-# LANGUAGE RankNTypes, DataKinds, KindSignatures #-}
module M where
type F = (forall (f :: * -> *). f) ()
f :: F
f = f

{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, ImpredicativeTypes #-}
module M where
type B = forall (a :: Bool). a
b :: proxy B
b = b

but with -dcore-lint they explode:

*** Core Lint errors : in result of Desugar (before optimization) ***
a.hs:5:1: warning:
    Non-Type-like kind when Type-like expected: * -> *
    when checking the body of forall: f_agw
    In the type of a binder: f
    In the type ‘F’
    Substitution: [TCvSubst
                     In scope: InScope {f_agw}
                     Type env: [agw :-> f_agw]
                     Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)

f :: F
[LclIdX]
f = f
end Rec }

*** End of Offense ***

*** Core Lint errors : in result of Desugar (before optimization) ***
b.hs:5:1: warning:
    Non-Type-like kind when Type-like expected: Bool
    when checking the body of forall: a_auh
    In the type of a binder: b
    In the type ‘forall (proxy :: Bool -> *). proxy B’
    Substitution: [TCvSubst
                     In scope: InScope {a_auh proxy_aui}
                     Type env: [auh :-> a_auh, aui :-> proxy_aui]
                     Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)

b :: forall (proxy :: Bool -> *). proxy B
[LclIdX]
b = \ (@(proxy_awC :: Bool -> *)) -> b @proxy_awC
end Rec }

*** End of Offense ***

GHC 8.4.4 will fail the first program with an impredicativity error, but will still accept it with ImpredicativeTypes enabled, and will still crash with a core lint.

Expected behavior

forall a. e should constrain e :: TYPE r, meaning GHCi should report forall a. a :: * or forall a. a :: TYPE r. Both programs should be rejected with a type error for the above reason. The first program (or programs like it) should raise an "Illegal impredicative type".

Environment

• GHC version used: 8.4.4, 8.6.5, 9.2.3, HEAD

Optional:

• Operating System: GNU/Linux
• System Architecture: x86_64