[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
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
More information about the Haskell-Cafe
mailing list