Kind mismatch with singleton [Nat]
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits ( Nat )
data Foo (n :: [Nat]) = Foo
x :: Foo ('(:) 42 '[])
x = Foo
y :: Foo (42 ': '[])
y = Foo
z :: Foo [42]
z = Foo
Expected kind ‘*’, but ‘42’ has kind ‘Nat’
In the type signature for ‘z’: z :: Foo [42]
I would expected z to be identical to both x and y. The error occurs in both GHCi and GHC.
Some more tests:
a_works = Foo '[]
a_fails = Foo []
z_works = Foo '[42]