# 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

## 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