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.