Skip to content

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]
Edited by Roel van Dijk
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information