(yes, confusng, but true)

On Tue, Oct 2, 2012 at 2:54 PM, Troels Henriksen <athas@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
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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe