return type of GADT evaluator

I'm a bit at a loss as to why the last pattern in prodV in the following doesn't work:

 {-# LANGUAGE GADTs #-}

data V a where
  V0 :: Float -> V Float
  Vn :: [Float] -> V [Float]

prodV :: (Num a) => V a -> V a -> a
prodV (V0 x) (V0 y) =  x * y
-- prodV (Vn x) (Vn y) = zipWith (*) x y -- this one works
prodV (Vn xs) (Vn ys) = [ sum $ zipWith (*) xs ys ]
prodV (V0 n) (Vn ys) = map (* n) ys

GHCi 7.8.3 complains:

Couldn't match type ‘Float’ with ‘[Float]’ 
Inaccessible code in
  a pattern with constructor
    Vn :: [Float] -> V [Float],
  in an equation for ‘prodV’
In the pattern: Vn ys`

Any pointers? thanks in advance

Solution

The signature

prodV :: (Num a) => V a -> V a -> a

mandates that both arguments have the same type parameter, but if you match on V0 and Vn the arguments would have to have the types V Float and V [Float] in which the type parameter does not match.

I'm not quite sure what you want the semantics to be but I'm guessing that you want to define the GADT as something like

data V n where
  V0 :: n -> V n
  Vn :: [n] -> V n

and your function as either

prodV :: (Num a) => V a -> V a -> V a
prodV (V0 x) (V0 y) =  V0 $ x * y
prodV (Vn xs) (Vn ys) = Vn $ zipWith (*) xs ys
prodV (V0 n) (Vn ys) = Vn $ map (* n) ys

or possibly

prodV' :: (Num a) => V a -> V a -> a
prodV' (V0 x) (V0 y) =  x * y
prodV' (Vn xs) (Vn ys) = sum $ zipWith (*) xs ys
prodV' (V0 n) (Vn ys) = sum $ map (* n) ys

Can you describe what you would like the function prodV to actually do? The types in your original code don't really make sense to me as they are.