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

[Troels Henriksen]

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
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats
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