[Haskell-cafe] Smart Constructor Puzzle

[Ronald Guida]

I'm playing around with smart constructors, and I have encountered a
weird puzzle.

My goal is to do vector arithmetic.  I'm using smart constructors so
that I can store a vector as a list and use the type system to
staticly enforce the length of a vector.

So my first step is to define Peano numbers at the type level.

 > data PZero   = PZero   deriving (Show)
 > data PSucc a = PSucc a deriving (Show)
 >
 > type P1 = PSucc PZero
 > type P2 = PSucc P1
 > type P3 = PSucc P2
 > -- etc

Next, I define a vector type and tag it with a Peano number.

 > data Vec s t = Vec [t] deriving (Eq, Ord, Show, Read)

Now I can define a few smart constructors.

 > vec0 :: Vec PZero t
 > vec0 = Vec []
 >
 > vec1 :: t -> Vec P1 t
 > vec1 x = Vec [x]
 >
 > vec2 :: t -> t -> Vec P2 t
 > vec2 x y = Vec [x, y]
 >
 > vec3 :: t -> t -> t -> Vec P3 t
 > vec3 x y z = Vec [x, y, z]

Now here's the puzzle.  I want to create a function "vecLength" that
accepts a vector and returns its length.  The catch is that I want to
calculate the length based on the /type/ of the vector, without
looking at the number of elements in the list.

So I started by defining a class that allows me to convert a Peano
number to an integer.  I couldn't figure out how to define a function
that converts the type directly to an integer, so I am using a
two-step process.  Given a Peano type /t/, I would use the expression
"pToInt (pGetValue :: t)".

 > class Peano t where
 >     pGetValue :: t
 >     pToInt :: t -> Int
 >
 > instance Peano PZero where
 >     pGetValue = PZero
 >     pToInt _ = 0
 >
 > instance (Peano t) => Peano (PSucc t) where
 >     pGetValue = PSucc pGetValue
 >     pToInt (PSucc a) = 1 + pToInt a

Finally, I tried to define vecLength, but I am getting an error.
 
 > vecLength :: (Peano s) => Vec s t -> Int
 > vecLength _ = pToInt (pGetValue :: s)

< Could not deduce (Peano s1) from the context ()
<   arising from a use of `pGetValue'
< Possible fix:
<   add (Peano s1) to the context of the polymorphic type `forall s. s'
< In the first argument of `pToInt', namely `(pGetValue :: s)'
< In the expression: pToInt (pGetValue :: s)
< In the definition of `vecLength':
<     vecLength _ = pToInt (pGetValue :: s)

Any suggestions?
-- Ron