What functional dependencies does this size-safe ZipWith variant require, and why?

Question

I'm trying to define operations on lists that have type-parameterized lengths. I end up having quite a number of constraints on these lists (Map, Fold, what have you) so I'd like to use the new GHC ConstraintKinds to simplify my life a little. However, I can't seem to figure them out.

Consider the following (drastically simplified) example:

-- A list where length is implicit in the type.
-- This allows us to have classes like
-- Combineable a b c  u v w | ... where
--    combine :: (a -> b -> c) -> u -> v -> w
-- which is a version of ZipWith that only works on
-- lists of the same length.
data a :. b = !a :. !b

-- A simple class that works on our length-implicit lists
class Fold v a | v -> a where
  fold  :: (a -> a -> a) -> v -> a
instance Fold (a:.()) a where
  fold  f   (a:._) = a
instance Fold (a':.u) a => Fold (a:.a':.u) a where
  fold  f   (a:.v) = f a (fold f v)

-- A type constraint to simplify the constraints on our functions,
-- which in the real world also contain a bunch of things like
-- Map a a v v, Combineable a (Maybe a) (Maybe a) v w w, etc.
type NList v i = ( Fold (v i) i )

-- A function that uses our type constraint
foo :: (Num a, NList v a) -> v a -> a
foo = fold (+) 1

Looks fairly sane to me. Right? Wrong.

> foo ((1::Int) :. ())

Couldn't match type `Int' with `()'
When using functional dependencies to combine
  Fold (a :. ()) a,
    arising from the dependency `v -> a'
    in the instance declaration in `Data.Vec.Base'
  Fold (Int :. ()) (),
    arising from a use of `foo' at <interactive>:72:1-4
In the expression: foo ((1 :: Int) :. ())
In an equation for `it': it = foo ((1 :: Int) :. ())

To me, this error message roughly translates to "why are you trying to program at the type level?"

Obviously, I don't quite understand the implications of Constraint Kinds, but I'm not sure where I went wrong here. Can anyone spot the error?

Answer 1

I might be misunderstanding what you are after, so excuse me if I'm completely off the mark, but this is what I did to make your code work.

The kind of v in

type NList v i = ( Fold (v i) i )

Seems to conflict with the kind of v in Fold

class Fold v a | v -> a where
    fold  :: (a -> a -> a) -> v -> a

The code works for me if we simply remove the definition of NList and change foo to

foo :: (Num a, Fold v a) => v -> a
foo = fold (+)

(I also added a fixity declaration for :. to get correct associativity and added LANGUAGE pragmas)

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FunctionalDependencies #-}

data a :. b = !a :. !b
infixr 5 :.

Now we can run foo in GHCi

*Main> foo (1:.())
1
*Main> foo (1:.2:.3:.())
6