# [Haskell-cafe] Strange things with type literals of kind Nat

Troels Henriksen athas at sigkill.dk
Tue Oct 2 20:54:39 CEST 2012

```Consider the following definition of lists with a statically determined
minimum length.

data Nat' = Z | S Nat'

data NList (n::Nat') a where
Rest :: [a] -> NList Z a
(:>) :: a -> NList n a -> NList (S n) a

uncons :: NList (S n) a -> (a, NList n a)
uncons (x :> xs) = (x, xs)

This works fine.  Now consider an implementation using the new type
literals in GHC:

data NList (n::Nat) a where
Rest :: NList 0 [a]
(:>) :: a -> NList n a -> NList (n+1) a

uncons :: NList (n+1) a -> NList n a
uncons (x :> l) = l

This gives a type error:

/home/athas/code/nonempty_lists.hs:41:19:
Could not deduce (n1 ~ n)
from the context ((n + 1) ~ (n1 + 1))
bound by a pattern with constructor
:> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,
in an equation for `uncons'
at /home/athas/code/nonempty_lists.hs:41:9-14
`n1' is a rigid type variable bound by
a pattern with constructor
:> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,
in an equation for `uncons'
at /home/athas/code/nonempty_lists.hs:41:9
`n' is a rigid type variable bound by
the type signature for uncons :: NList (n + 1) a -> NList n a
at /home/athas/code/nonempty_lists.hs:40:11
Expected type: NList n a
Actual type: NList n1 a
In the expression: l
In an equation for `uncons': uncons (x :> l) = l

I don't understand why GHC cannot infer that the two types are the same.
My guess is that 'n+1' is not "structural" to GHC in the same way that
'S n' is.  The page