From 64566bf990e71d20f695c838fd99ce0c2805e4e6 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Sun, 27 Oct 2024 23:28:13 +0300
Subject: [PATCH 1/2] Factor out Data.ZipMatchK, remove ZipMatch

---
 haskell/free-foil/free-foil.cabal             |  6 +-
 .../free-foil/src/Control/Monad/Free/Foil.hs  | 30 +++------
 .../src/Control/Monad/Free/Foil/TH.hs         |  2 -
 .../Monad/Free/Foil/TH/PatternSynonyms.hs     |  2 +-
 .../Control/Monad/Free/Foil/TH/ZipMatch.hs    | 57 ----------------
 haskell/free-foil/src/Data/ZipMatchK.hs       | 36 ++++++++++
 .../free-foil/src/Data/ZipMatchK/Bifunctor.hs | 30 +++++++++
 .../Free/Foil => Data/ZipMatchK}/Generic.hs   | 66 +++++--------------
 .../free-foil/src/Data/ZipMatchK/Mappings.hs  | 44 +++++++++++++
 .../src/Language/LambdaPi/Impl/FreeFoil.hs    | 23 +++----
 .../src/Language/LambdaPi/Impl/FreeFoilTH.hs  |  5 +-
 .../soas/src/Language/SOAS/Impl/Generated.hs  |  6 +-
 12 files changed, 150 insertions(+), 157 deletions(-)
 delete mode 100644 haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
 create mode 100644 haskell/free-foil/src/Data/ZipMatchK.hs
 create mode 100644 haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
 rename haskell/free-foil/src/{Control/Monad/Free/Foil => Data/ZipMatchK}/Generic.hs (80%)
 create mode 100644 haskell/free-foil/src/Data/ZipMatchK/Mappings.hs

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))]

From 0ace9241d6a4a6e3314e0e2532d3e58d2e148a58 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 28 Oct 2024 00:34:17 +0300
Subject: [PATCH 2/2] Improve documentation and type errors

---
 haskell/free-foil/free-foil.cabal             |  1 +
 .../free-foil/src/Control/Monad/Free/Foil.hs  | 11 +--
 haskell/free-foil/src/Data/ZipMatchK.hs       | 52 ++++++++++++-
 .../free-foil/src/Data/ZipMatchK/Bifunctor.hs |  9 ++-
 .../free-foil/src/Data/ZipMatchK/Functor.hs   | 34 ++++++++
 .../free-foil/src/Data/ZipMatchK/Generic.hs   | 77 +++++++++++++------
 .../free-foil/src/Data/ZipMatchK/Mappings.hs  | 22 +++++-
 7 files changed, 169 insertions(+), 37 deletions(-)
 create mode 100644 haskell/free-foil/src/Data/ZipMatchK/Functor.hs

diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal
index af2e0a8c..41748029 100644
--- a/haskell/free-foil/free-foil.cabal
+++ b/haskell/free-foil/free-foil.cabal
@@ -47,6 +47,7 @@ library
       Control.Monad.Free.Foil.TH.Signature
       Data.ZipMatchK
       Data.ZipMatchK.Bifunctor
+      Data.ZipMatchK.Functor
       Data.ZipMatchK.Generic
       Data.ZipMatchK.Mappings
   other-modules:
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
index bdb3438c..6f768cbd 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
@@ -23,6 +23,7 @@ import           Control.DeepSeq
 import qualified Control.Monad.Foil.Internal as Foil
 import qualified Control.Monad.Foil.Relative as Foil
 import           Data.Bifoldable
+import           Data.Bitraversable
 import           Data.Bifunctor
 import Data.ZipMatchK
 import           Data.Coerce                 (coerce)
@@ -165,7 +166,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, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,7 +179,7 @@ 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, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -192,7 +193,7 @@ alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
 alphaEquivScoped
-  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,7 +238,7 @@ alphaEquivScoped scope
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
 unsafeEqAST
-  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
@@ -250,7 +251,7 @@ unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
 unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
diff --git a/haskell/free-foil/src/Data/ZipMatchK.hs b/haskell/free-foil/src/Data/ZipMatchK.hs
index a1151319..02af010c 100644
--- a/haskell/free-foil/src/Data/ZipMatchK.hs
+++ b/haskell/free-foil/src/Data/ZipMatchK.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE RankNTypes #-}
@@ -7,30 +8,73 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+-- | Kind-polymorphic syntactic (first-order) unification.
 module Data.ZipMatchK (
   module Data.ZipMatchK.Mappings,
   ZipMatchK(..),
   zipMatchK,
-  zipMatch2,
+  -- * Specializations
+  -- ** Unification of plain 'Data.Kind.Type's
   zipMatchViaEq,
   zipMatchViaChooseLeft,
+  -- ** Unification of 'Data.Functor.Functor's
+  zipMatchWith1,
+  zipMatch1,
+  -- ** Unification of 'Data.Bifunctor.Bifunctor's
+  zipMatchWith2,
+  zipMatch2,
 ) where
 
 import           Generics.Kind
+import Data.Bitraversable
 
 import Data.ZipMatchK.Generic
 import Data.ZipMatchK.Mappings
 
+-- | Perform one level of equality testing for two values and pair up components using @(,)@:
+--
+-- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)
 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)
-
+-- | Unify values via 'Eq'.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
 zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
 zipMatchViaEq _ x y
   | x == y = Just x
   | otherwise = Nothing
 
+-- | Always successfully unify any two values of type @a@ by preferring the left value.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
 zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
 zipMatchViaChooseLeft _ x _ = Just x
+
+-- | 'zipMatchWithK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatchWith1
+  :: (Traversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> f a -> f a' -> Maybe (f a'')
+zipMatchWith1 f = zipMatchWithK (f :^: M0)
+
+-- | 'zipMatchK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))
+zipMatch1 = zipMatchWith1 pairA
+-- | 'zipMatchWithK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatchWith2
+  :: (Bitraversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> (b -> b' -> Maybe b'')
+  -> f a b -> f a' b' -> Maybe (f a'' b'')
+zipMatchWith2 f g = zipMatchWithK (f :^: g :^: M0)
+
+-- | 'zipMatchK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
+zipMatch2 = zipMatchWith2 pairA pairA
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
index 5d752440..9092065e 100644
--- a/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
+++ b/haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs
@@ -8,10 +8,13 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.
 module Data.ZipMatchK.Bifunctor where
 
 import Data.Kind (Type)
 import Generics.Kind
+import Data.Bitraversable
 import Data.Bifunctor.Sum
 import Data.Bifunctor.Product
 
@@ -26,5 +29,7 @@ instance GenericK (Product f g) where
     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)
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type))
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Bitraversable f, Bitraversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type))
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Functor.hs b/haskell/free-foil/src/Data/ZipMatchK/Functor.hs
new file mode 100644
index 00000000..09594af5
--- /dev/null
+++ b/haskell/free-foil/src/Data/ZipMatchK/Functor.hs
@@ -0,0 +1,34 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.
+module Data.ZipMatchK.Functor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Functor.Sum
+import Data.Functor.Product
+
+import Data.ZipMatchK
+
+instance GenericK (Sum f g) where
+  type RepK (Sum f g) =
+    Field (Kon f :@: Var0)
+    :+: Field (Kon g :@: Var0)
+instance GenericK (Product f g) where
+  type RepK (Product f g) =
+    Field (Kon f :@: Var0)
+    :*: Field (Kon g :@: Var0)
+
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type))
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (Traversable f, Traversable g, ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type))
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Generic.hs b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs
index a8da90ab..b040cc83 100644
--- a/haskell/free-foil/src/Data/ZipMatchK/Generic.hs
+++ b/haskell/free-foil/src/Data/ZipMatchK/Generic.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -Wno-missing-methods #-}
+{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-}
 {-# LANGUAGE AllowAmbiguousTypes      #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
@@ -19,23 +19,36 @@
 module Data.ZipMatchK.Generic where
 
 import           Data.Kind              (Constraint, Type)
+import           Data.List.NonEmpty
 import           Generics.Kind
 import           Generics.Kind.Examples ()
 import           GHC.TypeError
 import           Data.ZipMatchK.Mappings
 
+-- | Kind-polymorphic syntactic (first-order) unification of two values.
+--
+-- Note: @f@ is expected to be a traversable n-functor,
+-- but at the moment we lack a @TraversableK@ constraint.
 class ZipMatchK (f :: k) where
+  -- | Perform one level of equality testing:
+  --
+  -- * when @k = 'Type'@, values are compared directly (e.g. via 'Eq');
+  -- * when @k = 'Type' -> 'Type'@, we compare term constructors;
+  --   if term constructors are unequal, we return 'Nothing';
+  --   otherwise, we pair up all components with a given function.
   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
 
+-- | Generic implementation of 'Data.ZipMatch.zipMatchK'.
 genericZipMatchK :: forall f as bs.
     (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)
     => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))
 genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings
 
+-- | Generic implementation of 'zipMatchWithK'.
 genericZipMatchWithK :: forall f 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)
@@ -43,17 +56,20 @@ genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings
   (fromK @_ @f @as x)
   (fromK @_ @f @bs y)
 
-genericZipMatch2
-   :: forall sig scope scope' term term'.
-   (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0))
-   => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
-genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)
+instance GenericK (,) where
+  type RepK (,) = Field Var0 :*: Field Var1
+instance GenericK ((,) a) where
+  type RepK ((,) a) = Field (Kon a) :*: Field Var0
+instance GenericK NonEmpty where
+  type RepK NonEmpty = Field Var0 :*: Field ([] :$: Var0)
 
--- instance ZipMatchK (,)     -- missing GenericK instance upstream
+instance ZipMatchK (,)
+instance ZipMatchK a => ZipMatchK ((,) a)
 instance ZipMatchK []
 instance ZipMatchK Maybe
 instance ZipMatchK Either
 instance ZipMatchK a => ZipMatchK (Either a)
+instance ZipMatchK NonEmpty
 
 type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)
 class GZipMatch (f :: LoT k -> Type) where
@@ -110,7 +126,7 @@ instance ZipMatchK k => ZipMatchFields (Kon k) where
   type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()
   zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r
 
-instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where
+instance {-# OVERLAPPING #-} (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 =>
@@ -130,6 +146,24 @@ instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k)
         :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))
         :^: M0)) l r
 
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "The type constructor is kind-polymorphic:"
+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type)
+  :$$: 'Text "Possible fix:"
+  :$$: 'Text "  add an explicit kind signature"
+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type))
+  => ZipMatchFields (Kon (k :: kk -> Type) :@: t) where
+  zipMatchFieldsWith = undefined
+
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "The type constructor is kind-polymorphic:"
+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type)
+  :$$: 'Text "Possible fix:"
+  :$$: 'Text "  add an explicit kind signature"
+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type))
+  => ZipMatchFields ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where
+  zipMatchFieldsWith = undefined
+
 instance {-# OVERLAPPABLE #-} TypeError
   ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"
   :$$: 'Text "  when attempting to use a generic instance for"
@@ -139,24 +173,21 @@ instance {-# OVERLAPPABLE #-} TypeError
   -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")
   zipMatchFieldsWith = undefined
 
-instance TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") => ZipMatchFields (ForAll a) where
+instance TypeError
+  ('Text "Atom ForAll is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (ForAll a)) => ZipMatchFields (ForAll a) where
   type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-instance TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") => ZipMatchFields (c :=>>: a) where
+instance TypeError
+  ('Text "Atom :=>>: is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (c :=>>: a)) => ZipMatchFields (c :=>>: a) where
   type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-instance TypeError ('Text "Atom Eval is not supported by ZipMatchFields") => ZipMatchFields (Eval a) where
+instance TypeError
+  ('Text "Atom Eval is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where
   type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-
--- instance ZipMatchFields (ForAll f) where
---   type ReqsZipMatchFields (ForAll f) as bs = ???
---   zipMatchFields = ???
-
--- instance ZipMatchFields (c :=>>: f) where
---   type ReqsZipMatchFields (c :=>>: f) as bs = ???
---   zipMatchFields = ???
-
--- instance ZipMatchFields (Eval f) where
---   type ReqsZipMatchFields (Eval f) as bs = ???
---   zipMatchFields = ???
diff --git a/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs
index 9cdef001..e18836a4 100644
--- a/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs
+++ b/haskell/free-foil/src/Data/ZipMatchK/Mappings.hs
@@ -14,31 +14,47 @@ module Data.ZipMatchK.Mappings where
 import           Data.Kind              (Type)
 import           Generics.Kind
 
+-- | Zip to lists of types into a single list of pair types.
 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)
 
+infixr 5 :^:
 type Mappings :: LoT k -> LoT k -> LoT k -> Type
+-- | A collection of zipping functions for 'Data.ZipMatchK.zipMatchWithK'.
 data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
+  -- | An empty collection (when there no (more) type parameters).
   M0 :: Mappings LoT0 LoT0 LoT0
-  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
+  -- | A non-empty collection (when there is at least one type parameter).
+  (:^:) :: (a -> b -> Maybe c)    -- ^ Zipping for the first type parameter.
+        -> Mappings as bs cs      -- ^ Zipping for other type parameters.
+        -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
 
 class PairMappings (as :: LoT k) (bs :: LoT k) where
+  -- | A collection of pairing functions @(\\x y -> Just (x, y))@ for 'Data.ZipMatchK.zipMatchK'.
   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
+  pairMappings = pairA :^: pairMappings
 
 class ApplyMappings (v :: TyVar d Type) where
+  -- | Apply a collection of zipping functions to collections of values.
   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)
+       Mappings as bs cs      -- ^ A collection of zipping functions.
+    -> Interpret (Var v) as   -- ^ First collection of values (one per type parameter).
+    -> Interpret (Var v) bs   -- ^ Second collection of values (one per type parameter).
+    -> 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
+
+-- | Pair two values in a context.
+pairA :: Applicative f => a -> b -> f (a, b)
+pairA x y = pure (x, y)