Promoted empty list fails to kind-check with arity 0
Data constructors that are promoted to the kind level can be partially applied, just like any other type constructor. For instance, this kind-checks:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
type N :: forall a. Maybe a
type N = ('Nothing :: forall a. Maybe a)
Note that I've given 'Nothing
an explicit forall a. Maybe a
kind signature to ensure that N
has arity 0. That is, N
does not require any arguments in order to partially apply it.
While most promoted data constructors (e.g., 'Nothing
) can be partially applied this way, there is a strange exception to this rule: the promoted empty list. If you try to write this:
type L :: forall a. [a]
type L = ('[] :: forall a. [a])
Then it will fail to kind-check:
$ ghc-9.6.2 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:12:11: error: [GHC-83865]
• Expected kind ‘forall a. [a]’, but ‘'[]’ has kind ‘[k0]’
• In the type ‘('[] :: forall a. [a])’
In the type declaration for ‘L’
|
12 | type L = ('[] :: forall a. [a])
| ^^^
I think this should kind-check, as '[]
is a promoted data constructor just like 'Nothing
is. My suspicion is that GHC is special-casing '[]
applications somewhere in the typechecker, and the special code path is likely mishandling things in some way.