2 Oct 2012 20:54

## Strange things with type literals of kind Nat

```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'
```

3 Oct 2012 06:22

### Re: Strange things with type literals of kind Nat

Hello Troels,

there is no solver included with ghc 7.6, if you wish to experiment with equational reasoning with the type level nats, you'll have to look into the ghc type-lits branch which includes a solver.

(yes, confusng, but true)

On Tue, Oct 2, 2012 at 2:54 PM, Troels Henriksen wrote:
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
mentions that "type level numbers of kind Nat have no structure", which
seems to support my suspicion.  What's the complete story, though?

--
\  Troels
/\ Henriksen

_______________________________________________
```_______________________________________________