Using an unconfirmed list syntax in a GADT view signature with DataKinds

Question

I read Giving Haskell a Promotion http://dreixel.net/research/pdf/ghp.pdf

And I came across this syntax (which works if you use {-# LANGUAGE KindSignatures, GADTs, DataKinds, TypeOperators #-}):

data HList :: [*] -> * where
    HNil :: HList '[]
    HCons :: a -> HList as -> HList (a ': as)

Checking the information []using :info [], tells me that the data type of the lists is:

data [] a = [] | a : [a]

Which makes me think that this style should also work, since the type constructor is [] anow carried over to the view constructor:

data HList :: [] * -> * where
    HNil :: HList '[]
    HCons :: a -> HList as -> HList (a ': as)

But this is not the case and gives me this error:

parse error on input `]'