diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal
index 65ebc84e..af2e0a8c 100644
--- a/haskell/free-foil/free-foil.cabal
+++ b/haskell/free-foil/free-foil.cabal
@@ -40,13 +40,15 @@ library
       Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
       Control.Monad.Free.Foil.Example
-      Control.Monad.Free.Foil.Generic
       Control.Monad.Free.Foil.TH
       Control.Monad.Free.Foil.TH.Convert
       Control.Monad.Free.Foil.TH.MkFreeFoil
       Control.Monad.Free.Foil.TH.PatternSynonyms
       Control.Monad.Free.Foil.TH.Signature
-      Control.Monad.Free.Foil.TH.ZipMatch
+      Data.ZipMatchK
+      Data.ZipMatchK.Bifunctor
+      Data.ZipMatchK.Generic
+      Data.ZipMatchK.Mappings
   other-modules:
       Paths_free_foil
   hs-source-dirs:
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
index f02b6e85..bdb3438c 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
@@ -24,7 +24,7 @@ import qualified Control.Monad.Foil.Internal as Foil
 import qualified Control.Monad.Foil.Relative as Foil
 import           Data.Bifoldable
 import           Data.Bifunctor
-import           Data.Bifunctor.Sum
+import Data.ZipMatchK
 import           Data.Coerce                 (coerce)
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
@@ -165,7 +165,7 @@ refreshScopedAST scope (ScopedAST binder body) =
 -- Compared to 'alphaEquiv', this function may perform some unnecessary
 -- changes of bound variables when the binders are the same on both sides.
 alphaEquivRefreshed
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,21 +178,21 @@ alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST s
 -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
 -- changes of bound variables when both binders in two matching scoped terms coincide.
 alphaEquiv
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
   -> Bool
 alphaEquiv _scope (Var x) (Var y) = x == coerce y
 alphaEquiv scope (Node l) (Node r) =
-  case zipMatch l r of
+  case zipMatch2 l r of
     Nothing -> False
     Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)
 alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
 alphaEquivScoped
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,20 +237,20 @@ alphaEquivScoped scope
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
 unsafeEqAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
 unsafeEqAST (Var x) (Var y) = x == coerce y
 unsafeEqAST (Node t1) (Node t2) =
-  case zipMatch t1 t2 of
+  case zipMatch2 t1 t2 of
     Nothing -> False
     Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
 unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
 unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
@@ -260,20 +260,6 @@ unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
       (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2
   ]
 
--- ** Syntactic matching (unification)
-
--- | Perform one-level matching for the two (non-variable) terms.
-class ZipMatch sig where
-  zipMatch
-    :: sig scope term     -- ^ Left non-variable term.
-    -> sig scope' term'   -- ^ Right non-variable term.
-    -> Maybe (sig (scope, scope') (term, term'))
-
-instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
-  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'
-  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'
-  zipMatch _ _            = Nothing
-
 -- * Converting to and from free foil
 
 -- ** Convert to free foil
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs
index bc3fcbc6..a1ca2633 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs
@@ -2,10 +2,8 @@ module Control.Monad.Free.Foil.TH (
   module Control.Monad.Free.Foil.TH.Signature,
   module Control.Monad.Free.Foil.TH.PatternSynonyms,
   module Control.Monad.Free.Foil.TH.Convert,
-  module Control.Monad.Free.Foil.TH.ZipMatch,
 ) where
 
 import Control.Monad.Free.Foil.TH.Signature
 import Control.Monad.Free.Foil.TH.PatternSynonyms
 import Control.Monad.Free.Foil.TH.Convert
-import Control.Monad.Free.Foil.TH.ZipMatch
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
index 0f35e98d..2ec7c7b1 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
@@ -83,7 +83,7 @@ mkPatternSynonym signatureType scope term = \case
       where
         l = mkName ("l" ++ show i)
 
-    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))
+    mkPatternName conName = mkName (dropEnd (length ("Sig" :: String)) (nameBase conName))
     dropEnd k = reverse . drop k . reverse
 
     collapse = \case
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
deleted file mode 100644
index 72fdbbd8..00000000
--- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE ViewPatterns    #-}
-module Control.Monad.Free.Foil.TH.ZipMatch where
-
-import           Language.Haskell.TH
-
-import           Control.Monad.Foil.TH.Util
-import           Control.Monad.Free.Foil
-
--- | Generate 'ZipMatch' instance for a given bifunctor.
-deriveZipMatch
-  :: Name -- ^ Type name for the signature bifunctor.
-  -> Q [Dec]
-deriveZipMatch signatureT = do
-  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT
-
-  case reverse signatureTVars of
-    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do
-      let signatureType = PeelConT signatureT (map (VarT . tvarName) params)
-      clauses <- concat <$> mapM (toClause scope term) signatureCons
-      let defaultClause = Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []
-      let instType = AppT (ConT ''ZipMatch) signatureType
-
-      return
-        [ InstanceD Nothing [] instType
-          [ FunD 'zipMatch (clauses ++ [defaultClause]) ]
-        ]
-    _ -> fail "cannot generate pattern synonyms"
-
-  where
-    toClause :: Name -> Name -> Con -> Q [Clause]
-    toClause scope term = go
-      where
-        go = \case
-          NormalC conName types -> mkClause conName types
-          RecC conName types -> go (NormalC conName (map removeName types))
-          InfixC l conName r -> go (NormalC conName [l, r])
-          ForallC _ _ con -> go con
-          GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames
-          RecGadtC conNames types retType -> go (GadtC conNames (map removeName types) retType)
-
-        mkClause :: Name -> [BangType] -> Q [Clause]
-        mkClause conName types = return
-          [Clause [ConP conName [] lpats, ConP conName [] rpats]
-            (NormalB (AppE (ConE 'Just) (foldl AppE (ConE conName) args))) []]
-          where
-            (lpats, rpats, args) = unzip3
-              [ case type_ of
-                  VarT typeName
-                    | typeName `elem` [scope, term] -> (VarP l, VarP r, TupE [Just (VarE l), Just (VarE r)])
-                  _ -> (VarP l, WildP, VarE l)
-              | (i, (_bang, type_)) <- zip [0..] types
-              , let l = mkName ("l" ++ show i)
-              , let r = mkName ("r" ++ show i)
-              ]
diff --git a/haskell/free-foil/src/Data/ZipMatchK.hs b/haskell/free-foil/src/Data/ZipMatchK.hs
new file mode 100644
index 00000000..a1151319
--- /dev/null
+++ b/haskell/free-foil/src/Data/ZipMatchK.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.ZipMatchK (
+  module Data.ZipMatchK.Mappings,
+  ZipMatchK(..),
+  zipMatchK,
+  zipMatch2,
+  zipMatchViaEq,
+  zipMatchViaChooseLeft,
+) where
+
+import           Generics.Kind
+
+import Data.ZipMatchK.Generic
+import Data.ZipMatchK.Mappings
+
+zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
+zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings
+
+zipMatch2 :: forall f a b a' b'. (ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
+zipMatch2 = zipMatchK @f @(a :&&: b :&&: LoT0) @(a' :&&: b' :&&: LoT0)
+
+zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaEq _ x y
+  | x == y = Just x
+  | otherwise = Nothing
+
+zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaChooseLeft _ x _ = Just x
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
new file mode 100644
index 00000000..5d752440
--- /dev/null
+++ b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.ZipMatchK.Bifunctor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Bifunctor.Sum
+import Data.Bifunctor.Product
+
+import Data.ZipMatchK
+
+instance GenericK (Sum f g) where
+  type RepK (Sum f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :+: Field ((Kon g :@: Var0) :@: Var1)
+instance GenericK (Product f g) where
+  type RepK (Product f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :*: Field ((Kon g :@: Var0) :@: Var1)
+
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum (f :: Type -> Type -> Type) g)
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product (f :: Type -> Type -> Type) g)
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs
similarity index 80%
rename from haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs
rename to haskell/free-foil/src/Data/ZipMatchK/Generic.hs
index 16ae815e..a8da90ab 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs
+++ b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs
@@ -16,41 +16,20 @@
 {-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE UndecidableInstances     #-}
-module Control.Monad.Free.Foil.Generic where
+module Data.ZipMatchK.Generic where
 
 import           Data.Kind              (Constraint, Type)
 import           Generics.Kind
 import           Generics.Kind.Examples ()
 import           GHC.TypeError
+import           Data.ZipMatchK.Mappings
 
-type ZipLoT :: LoT k -> LoT k -> LoT k
-type family ZipLoT as bs where
-  ZipLoT LoT0 LoT0 = LoT0
-  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)
-
-type Mappings :: LoT k -> LoT k -> LoT k -> Type
-data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
-  M0 :: Mappings LoT0 LoT0 LoT0
-  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
-
-class PairMappings (as :: LoT k) (bs :: LoT k) where
-  pairMappings :: Mappings as bs (ZipLoT as bs)
-
-instance PairMappings LoT0 LoT0 where
-  pairMappings = M0
-
-instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where
-  pairMappings = (\x y -> Just (x, y)) :^: pairMappings
-
-class ApplyMappings (v :: TyVar d Type) where
-  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
-    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)
-
-instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
-  applyMappings (f :^: _) x y = f x y
-
-instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where
-  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y
+class ZipMatchK (f :: k) where
+  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
+  default zipMatchWithK :: forall as bs cs.
+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
+  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs
 
 genericZipMatchK :: forall f as bs.
     (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)
@@ -70,24 +49,6 @@ genericZipMatch2
    => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
 genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)
 
-zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
-zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings
-
-class ZipMatchK (f :: k) where
-  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
-  default zipMatchWithK :: forall as bs cs.
-    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
-    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
-  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs
-
-zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
-zipMatchViaEq _ x y
-  | x == y = Just x
-  | otherwise = Nothing
-
-zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
-zipMatchViaChooseLeft _ x _ = Just x
-
 -- instance ZipMatchK (,)     -- missing GenericK instance upstream
 instance ZipMatchK []
 instance ZipMatchK Maybe
@@ -153,12 +114,12 @@ instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where
   type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
 
   zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>
-    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon k :@: t) cs)
+    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon (k :: Type -> Type) :@: t) cs)
   zipMatchFieldsWith g (Field l) (Field r) =
     Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)
       ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r
 
-instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: t1) :@: t2) where
+instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where
   type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)
 
   zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>
@@ -169,7 +130,12 @@ instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields (
         :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))
         :^: M0)) l r
 
-instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: t) where
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (f :@: t)
+  :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))
+  => ZipMatchFields ((f :: Atom d (k1 -> Type)) :@: t) where
   -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")
   zipMatchFieldsWith = undefined
 
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs
new file mode 100644
index 00000000..9cdef001
--- /dev/null
+++ b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+module Data.ZipMatchK.Mappings where
+
+import           Data.Kind              (Type)
+import           Generics.Kind
+
+type ZipLoT :: LoT k -> LoT k -> LoT k
+type family ZipLoT as bs where
+  ZipLoT LoT0 LoT0 = LoT0
+  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)
+
+type Mappings :: LoT k -> LoT k -> LoT k -> Type
+data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
+  M0 :: Mappings LoT0 LoT0 LoT0
+  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
+
+class PairMappings (as :: LoT k) (bs :: LoT k) where
+  pairMappings :: Mappings as bs (ZipLoT as bs)
+
+instance PairMappings LoT0 LoT0 where
+  pairMappings = M0
+
+instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where
+  pairMappings = (\x y -> Just (x, y)) :^: pairMappings
+
+class ApplyMappings (v :: TyVar d Type) where
+  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
+    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)
+
+instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
+  applyMappings (f :^: _) x y = f x y
+
+instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where
+  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
index 9d58a2f1..2e73910a 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE KindSignatures    #-}
+{-# LANGUAGE TypeFamilies      #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs             #-}
@@ -35,13 +37,16 @@ import           Data.Bifunctor.Sum
 import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
+import           Data.ZipMatchK
 import           Data.String                     (IsString (..))
+import           Generics.Kind.TH                (deriveGenericK)
 import qualified Language.LambdaPi.Syntax.Abs    as Raw
 import qualified Language.LambdaPi.Syntax.Layout as Raw
 import qualified Language.LambdaPi.Syntax.Lex    as Raw
 import qualified Language.LambdaPi.Syntax.Par    as Raw
 import qualified Language.LambdaPi.Syntax.Print  as Raw
 import           System.Exit                     (exitFailure)
+import Data.ZipMatchK.Bifunctor ()
 
 -- $setup
 -- >>> import qualified Control.Monad.Foil as Foil
@@ -59,13 +64,8 @@ data LambdaPiF scope term
 deriveBifunctor ''LambdaPiF
 deriveBifoldable ''LambdaPiF
 deriveBitraversable ''LambdaPiF
-
-instance ZipMatch LambdaPiF where
-  zipMatch (AppF l r) (AppF l' r') = Just (AppF (l, l') (r, r'))
-  zipMatch (LamF t) (LamF t')      = Just (LamF (t, t'))
-  zipMatch (PiF l r) (PiF l' r')   = Just (PiF (l, l') (r, r'))
-  zipMatch UniverseF UniverseF     = Just UniverseF
-  zipMatch _ _                     = Nothing
+deriveGenericK ''LambdaPiF
+instance ZipMatchK LambdaPiF
 
 -- | The signature 'Bifunctor' for pairs.
 data PairF scope term
@@ -77,13 +77,8 @@ data PairF scope term
 deriveBifunctor ''PairF
 deriveBifoldable ''PairF
 deriveBitraversable ''PairF
-
-instance ZipMatch PairF where
-  zipMatch (PairF l r) (PairF l' r')       = Just (PairF (l, l') (r, r'))
-  zipMatch (FirstF t) (FirstF t')          = Just (FirstF (t, t'))
-  zipMatch (SecondF t) (SecondF t')        = Just (SecondF (t, t'))
-  zipMatch (ProductF l r) (ProductF l' r') = Just (ProductF (l, l') (r, r'))
-  zipMatch _ _                             = Nothing
+deriveGenericK ''PairF
+instance ZipMatchK PairF
 
 -- | Sum of signature bifunctors.
 type (:+:) = Sum
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
index 01040b19..948db1f5 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -38,12 +38,12 @@ module Language.LambdaPi.Impl.FreeFoilTH where
 import qualified Control.Monad.Foil              as Foil
 import           Control.Monad.Foil.TH
 import           Control.Monad.Free.Foil
-import           Control.Monad.Free.Foil.Generic
 import           Control.Monad.Free.Foil.TH
 import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
 import           Data.String                     (IsString (..))
+import           Data.ZipMatchK
 import           Generics.Kind.TH                (deriveGenericK)
 import qualified GHC.Generics                    as GHC
 import qualified Language.LambdaPi.Syntax.Abs    as Raw
@@ -102,9 +102,6 @@ instance ZipMatchK Raw.BNFC'Position where zipMatchWithK = zipMatchViaChooseLeft
 -- | Generic 'ZipMatchK' instance.
 instance ZipMatchK a => ZipMatchK (Term'Sig a)
 
-instance ZipMatchK a => ZipMatch (Term'Sig a) where
-  zipMatch = genericZipMatch2
-
 -- * User-defined code
 
 -- | Generic annotated scope-safe \(\lambda\Pi\)-terms with patterns.
diff --git a/haskell/soas/src/Language/SOAS/Impl/Generated.hs b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
index bdd0fb57..6385487c 100644
--- a/haskell/soas/src/Language/SOAS/Impl/Generated.hs
+++ b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
@@ -20,12 +20,11 @@ import qualified Data.Map as Map
 import Data.String (IsString(..))
 import qualified Control.Monad.Foil as Foil
 import           Control.Monad.Free.Foil.TH.MkFreeFoil
-import           Control.Monad.Free.Foil
 import qualified Language.SOAS.Syntax.Abs    as Raw
 import qualified Language.SOAS.Syntax.Lex    as Raw
 import qualified Language.SOAS.Syntax.Par    as Raw
 import qualified Language.SOAS.Syntax.Print  as Raw
-import Control.Monad.Free.Foil.Generic
+import Data.ZipMatchK
 import Generics.Kind.TH (deriveGenericK)
 import Language.SOAS.FreeFoilConfig (soasConfig)
 
@@ -105,9 +104,6 @@ instance ZipMatchK a => ZipMatchK (Term'Sig a)
 instance ZipMatchK a => ZipMatchK (OpArg'Sig a)
 instance ZipMatchK a => ZipMatchK (Type'Sig a)
 
-instance ZipMatchK a => ZipMatch (Term'Sig a) where zipMatch = genericZipMatch2
-instance ZipMatchK a => ZipMatch (Type'Sig a) where zipMatch = genericZipMatch2
-
 -- |
 -- >>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS
 -- ?m [App (Lam (x0 . x0), Lam (x0 . x0))]