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

Carter Schonwald carter.schonwald at gmail.com
Wed Oct 3 06:22:27 CEST 2012

```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 <athas at sigkill.dk> 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
>
> _______________________________________________