hlist.hs

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}
data HList xs where
    HNil :: HList []
    (:::) :: a -> HList as -> HList (a : as)

-- error:
/home/matt/hlist.hs:4:38: error:
    • Expected kind ‘* -> *’, but ‘a : as’ has kind ‘[*]’
    • In the first argument of ‘HList’, namely ‘(a : as)’
      In the type ‘HList (a : as)’
      In the definition of data constructor ‘:::’
  |
4 |     (:::) :: a -> HList as -> HList (a : as)
  |                                      ^^^^^^

/home/matt/hlist.hs:4:42: error:
    • Expecting one more argument to ‘as’
      Expected kind ‘[*]’, but ‘as’ has kind ‘* -> *’
    • In the second argument of ‘(:)’, namely ‘as’
      In the first argument of ‘HList’, namely ‘(a : as)’
      In the type ‘HList (a : as)’
  |
4 |     (:::) :: a -> HList as -> HList (a : as)
  |                                          ^^

---------------------------------------------------

hlist2.hs

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}
data HList xs where
    (:::) :: a -> HList as -> HList (a : as)
    HNil :: HList []
    
-- error:
/home/matt/hlist.hs:4:19: error:
    • Expecting one more argument to ‘[]’
      Expected kind ‘[*]’, but ‘[]’ has kind ‘* -> *’
    • In the first argument of ‘HList’, namely ‘[]’
      In the type ‘HList []’
      In the definition of data constructor ‘HNil’
  |
4 |     HNil :: HList []
  |                   ^^

kindsig.hs

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeOperators #-}
data HList (xs :: [*]) where
    (:::) :: a -> HList as -> HList (a : as)
    HNil :: HList []

-- error:
    • Expecting one more argument to ‘[]’
      Expected kind ‘[*]’, but ‘[]’ has kind ‘* -> *’
    • In the first argument of ‘HList’, namely ‘[]’
      In the type ‘HList []’
      In the definition of data constructor ‘HNil’
  |
4 |     HNil :: HList []
  |                   ^^

-- i actually expected this one to work! huh.