{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs #-}

import Control.Applicative

-- | Type-level naturals
data Nat = Z | S Nat

-- | Type family for n-ary functions
type family   Fn (n :: Nat) a b
type instance Fn Z     a b = b
type instance Fn (S n) a b = a -> Fn n a b

-- | Lists exposing their length in their type
data List a (n :: Nat) where
  Nil :: List a Z
  Cons :: a -> List a n -> List a (S n)

-- | General <*> applied to a list of arguments of the right length
class Apply (n :: Nat) where
   foldF :: Applicative f => f (Fn n a b) -> List (f a) n -> f b

instance Apply Z where
   foldF f0 Nil = f0

instance Apply n => Apply (S n) where
   foldF fn (Cons x xs) = foldF (fn <*> x) xs

-- test :: [(Integer,Integer,Integer)]
test :: [(Integer,Integer,Int)]
test = foldF (pure (,,)) (Cons [10,11] (Cons [20,21] (Cons [30,31] Nil)))
-- Result: [(10,20,30),(10,20,31),(10,21,30),(10,21,31)
--         ,(11,20,30),(11,20,31),(11,21,30),(11,21,31)]
{-
prog.hs:30:15:
    Couldn't match type `Integer' with `Int'
    Expected type: [Fn
                      ('S ('S ('S 'Z))) Integer (Integer, Integer, Int)]
      Actual type: [Integer
                    -> Integer -> Integer -> (Integer, Integer, Integer)]
    In the return type of a call of `pure'
    In the first argument of `foldF', namely `(pure (,,))'
    In the expression:
      foldF
        (pure (,,)) (Cons [10, 11] (Cons [20, 21] (Cons [30, 31] Nil)))
-}

main = print test

main2 = print $ zipWith3 (,,) [10,11] ([20,21]::[Integer]) ([30,31]::[Int])