haskell - 在具有 DataKinds 的 GADT 的种类签名中使用非加糖列表语法

Question

我正在阅读给 Haskell 一个推广http://dreixel.net/research/pdf/ghp.pdf

我遇到了这种语法（如果你使用它就有效{-# LANGUAGE KindSignatures, GADTs, DataKinds, TypeOperators #-}）：

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

检查[]using的信息:info []，告诉我列表的数据类型是：

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

这让我觉得，这种风格也应该起作用，因为[] a类型构造函数现在被提升为一种类型的构造函数：

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

但它没有，并给了我这个错误：

parse error on input `]'