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