Following along with RAE at https://www.youtube.com/watch?v=iGSKqcebhfs

ZipWith.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module ZipWith where

import Data.Kind (Type)
import Prelude hiding (zipWith)

-- S/Z instead of Succ/Zero
data Nat = Z | S Nat

type family CountArgs (f :: Type) :: Nat where
  CountArgs (a -> r) = 'S (CountArgs r)
  CountArgs r = 'Z

type family ListsFrom (f :: Type) :: Type where
  ListsFrom (a -> r) = [a] -> ListsFrom r
  ListsFrom r = [r]

-- I didn't use LFC. Once we added (n :: Nat) to ListFromWitness, it seemed easier
-- to explicitly pass it through ListsFromClass and CountArgs

data ListsFromWitness (f ::Type) (n :: Nat) where
  ListsFromFun :: (ListsFromClass r n, CountArgs r ~ n) => ListsFromWitness (a -> r) ('S n)
  ListsFromNil :: ListsFrom r ~ [r] => ListsFromWitness r 'Z

class ListsFromClass (f :: Type) (n :: Nat) where
  witness :: ListsFromWitness f n

instance (ListsFromClass r n, CountArgs r ~ n) => ListsFromClass (a -> r) ('S n) where
  witness = ListsFromFun

instance ListsFrom r ~ [r] => ListsFromClass r 'Z where
  witness = ListsFromNil

zipWith :: (CountArgs f ~ n, ListsFromClass f n) => f -> ListsFrom f
zipWith = zipping . repeat

zipping
  :: forall f n . (CountArgs f ~ n, ListsFromClass f n) => [f] -> ListsFrom f
zipping fs = case witness @f @n of
  ListsFromNil -> fs
  ListsFromFun -> \xs -> zipping $ apply fs xs

apply :: forall a b . [a -> b] -> [a] -> [b]
apply (f : fs) (x : xs) = f x : apply fs xs
apply _        _        = []

sums :: [Int]
sums = zipWith (+) [1 :: Int ..] [20 .. 100]