{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, TypeOperators
, ScopedTypeVariables, FlexibleContexts #-}

-- n-ary zipWith

data Nil
data a ::: b

infixr :::

data Tuple ts where
  Nil   :: Tuple Nil
  (:::) :: t -> Tuple ts -> Tuple (t ::: ts)

type family Fun ts r :: *
type instance Fun Nil r = r
type instance Fun (t ::: ts) r = t -> Fun ts r

type family Lists ts :: *
type instance Lists Nil = Nil
type instance Lists (t ::: ts) = [t] ::: Lists ts

class Tup ts where
  uncurryT :: Fun ts r -> Tuple ts -> r
  curryT   :: (Tuple ts -> r) -> Fun ts r
  zipT :: Tuple (Lists ts) -> [Tuple ts]

instance Tup Nil where
  uncurryT r Nil = r
  curryT f = f Nil
  zipT Nil = repeat Nil

instance Tup ts => Tup (t ::: ts) where
  uncurryT f (v ::: vs) = uncurryT (f v) vs
  curryT f = \v -> curryT (\t -> f (v ::: t))
  zipT (l ::: ls) = zipWith (:::) l (zipT ls)

zipWithT :: forall ts r. (Tup ts, Tup (Lists ts)) => 
            ts -> Fun ts r -> Fun (Lists ts) [r]
zipWithT witness f = cT (\t -> map (uT f) (zipT t))
 where
 cT :: (Tuple (Lists ts) -> [r]) -> Fun (Lists ts) [r]
 cT = curryT
 uT :: Fun ts r -> Tuple ts -> r
 uT = uncurryT

zwp :: [Int] -> [Int] -> [Int] -> [Int]
zwp = zipWithT (undefined :: Int ::: Int ::: Int ::: Nil) (\x y z -> x + y + z)