diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,82 @@
 # CHANGELOG for `free-foil`
 
+# 0.3.0 — 2026-07-14
+
+This release makes generic deriving the default way to instantiate the library:
+`Sinkable`, `CoSinkable`, `UnifiablePattern` and `ZipMatchK` can now all be
+derived via [`kind-generics`](https://hackage.haskell.org/package/kind-generics),
+so a user-defined pattern normally needs no hand-written instances at all.
+The cost is one breaking change, described first.
+
+## Breaking changes
+
+- The `ZipMatch` class is **removed** in favour of the kind-polymorphic `ZipMatchK`,
+  and the modules are reorganised (see [#30](https://github.com/fizruk/free-foil/pull/30)):
+
+  - `Control.Monad.Free.Foil.Generic` is replaced by `Data.ZipMatchK`
+    (with `Data.ZipMatchK.Bifunctor`, `Data.ZipMatchK.Functor`,
+    `Data.ZipMatchK.Generic` and `Data.ZipMatchK.Mappings`);
+  - `Control.Monad.Free.Foil.TH.ZipMatch` (and its `deriveZipMatch`) is removed,
+    and `Control.Monad.Free.Foil.TH` no longer re-exports it.
+
+  To migrate, delete the `ZipMatch` instances and any `deriveZipMatch` splices,
+  and keep only the `ZipMatchK` ones. Where you had
+
+  ```haskell
+  import Control.Monad.Free.Foil.Generic
+
+  instance ZipMatchK a => ZipMatchK (TermSig a)
+  instance ZipMatchK a => ZipMatch  (TermSig a) where zipMatch = genericZipMatch2
+  ```
+
+  the second instance simply goes away:
+
+  ```haskell
+  import Data.ZipMatchK
+
+  instance ZipMatchK a => ZipMatchK (TermSig a)
+  ```
+
+  `ZipMatchK` is derived generically, so the signature needs a `GenericK` instance
+  (`deriveGenericK ''TermSig` from `kind-generics-th`). Note that `kind-generics-th`
+  is not on Stackage, and is not a dependency of this library: a package using
+  `deriveGenericK` must depend on it itself.
+
+- α-equivalence and refreshing now ask for more of the binder: `alphaEquiv`,
+  `alphaEquivRefreshed`, `refreshAST` and `refreshScopedAST` require
+  `SinkableK binder` (and `ZipMatchK sig` in place of `ZipMatch sig`).
+  For binders and patterns generated by our Template Haskell, or derived generically,
+  this constraint is already satisfied and no change is needed.
+
+## Generic deriving of patterns (see [#31](https://github.com/fizruk/free-foil/pull/31))
+
+- New `SinkableK` class, generalising both `Sinkable` and `CoSinkable`:
+  a type `f n₁ n₂ … nₖ` is treated as a generalised binder with variables and terms
+  in scopes `n₁, n₂, …, nₖ`. Generic (kind-polymorphic) implementations are provided
+  for `sinkabilityProof` and `coSinkabilityProof`, so `Sinkable` and `CoSinkable`
+  instances can be left empty.
+- New `HasNameBinders` class, generalising access to the nested `NameBinder`s of a pattern.
+  This is what makes a *generic* `withPattern` possible, so user-defined patterns
+  no longer need a hand-written traversal.
+- `UnifiablePattern` now has a default implementation via `CoSinkable`,
+  so `instance UnifiablePattern MyPattern` normally suffices.
+- Malformed user-defined patterns are now rejected with a readable type error
+  by a separate generic check (`GValidNameBinders`), instead of failing obscurely
+  deeper in the machinery. Terms (and other types) are allowed in patterns,
+  as long as the binders are threaded correctly.
+
+## New functions (see [#32](https://github.com/fizruk/free-foil/pull/32))
+
+- `unsinkAST` — unsink an `AST` from a larger scope into a smaller one, when possible.
+- `freeVarsOf` and `freeVarsOfScopedAST` — collect the free variables of an `AST`.
+- `nameMapToScope` — recover a `Scope` from a `NameMap`.
+- `NameMap` is now a `Functor`, `Foldable` and `Traversable`.
+
+## Fixes
+
+- `GValidNameBinders` no longer rejects a valid constructor that equates its scopes
+  and carries more than one field (substitution now recurses through sums and products).
+
 # 0.2.0 — 2024-10-27
 
 - Generate [`COMPLETE` pragma](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html#complete-pragmas) in `mkPatternSynonyms` (see [#26](https://github.com/fizruk/free-foil/pull/26))
diff --git a/free-foil.cabal b/free-foil.cabal
--- a/free-foil.cabal
+++ b/free-foil.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.39.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           free-foil
-version:        0.2.0
+version:        0.3.0
 synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads)
 description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme>
 category:       Parsing
@@ -31,6 +31,7 @@
       Control.Monad.Foil
       Control.Monad.Foil.Example
       Control.Monad.Foil.Internal
+      Control.Monad.Foil.Internal.ValidNameBinders
       Control.Monad.Foil.Relative
       Control.Monad.Foil.TH
       Control.Monad.Foil.TH.MkFoilData
@@ -40,27 +41,30 @@
       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.Functor
+      Data.ZipMatchK.Generic
+      Data.ZipMatchK.Mappings
   other-modules:
       Paths_free_foil
   hs-source-dirs:
       src
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-depends:
-      array >=0.5.3.0
+      array >=0.5.3.0 && <0.6
     , base >=4.7 && <5
-    , bifunctors
-    , containers
-    , deepseq
-    , kind-generics >=0.5.0
-    , template-haskell >=2.21.0.0
-    , text >=1.2.3.1
+    , bifunctors >=5.5 && <5.7
+    , containers >=0.6 && <0.9
+    , deepseq >=1.4 && <1.6
+    , kind-generics >=0.5.0 && <0.6
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
   default-language: Haskell2010
 
 test-suite doctests
@@ -71,16 +75,16 @@
       test/doctests
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-depends:
-      array >=0.5.3.0
+      array >=0.5.3.0 && <0.6
     , base >=4.7 && <5
-    , bifunctors
-    , containers
-    , deepseq
+    , bifunctors >=5.5 && <5.7
+    , containers >=0.6 && <0.9
+    , deepseq >=1.4 && <1.6
     , doctest-parallel
     , free-foil
-    , kind-generics >=0.5.0
-    , template-haskell >=2.21.0.0
-    , text >=1.2.3.1
+    , kind-generics >=0.5.0 && <0.6
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
   default-language: Haskell2010
 
 test-suite spec
@@ -92,13 +96,13 @@
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      array >=0.5.3.0
+      array >=0.5.3.0 && <0.6
     , base >=4.7 && <5
-    , bifunctors
-    , containers
-    , deepseq
+    , bifunctors >=5.5 && <5.7
+    , containers >=0.6 && <0.9
+    , deepseq >=1.4 && <1.6
     , free-foil
-    , kind-generics >=0.5.0
-    , template-haskell >=2.21.0.0
-    , text >=1.2.3.1
+    , kind-generics >=0.5.0 && <0.6
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
   default-language: Haskell2010
diff --git a/src/Control/Monad/Foil.hs b/src/Control/Monad/Foil.hs
--- a/src/Control/Monad/Foil.hs
+++ b/src/Control/Monad/Foil.hs
@@ -35,8 +35,10 @@
   unsinkName,
   unsinkNamePattern,
   -- * Safe (co)sinking and renaming
+  SinkableK(..),
   Sinkable(..),
   CoSinkable(..),
+  HasNameBinders(getNameBinders),
   sink,
   extendRenaming,
   extendNameBinderRenaming,
diff --git a/src/Control/Monad/Foil/Internal.hs b/src/Control/Monad/Foil/Internal.hs
--- a/src/Control/Monad/Foil/Internal.hs
+++ b/src/Control/Monad/Foil/Internal.hs
@@ -1,16 +1,25 @@
+{-# OPTIONS_GHC -Wno-missing-methods #-}  -- disabled to avoid overlapping type instances
+{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-inaccessible-code #-}  -- disabled because I think GHC is wrong
+{-# LANGUAGE AllowAmbiguousTypes        #-}
 {-# LANGUAGE BlockArguments             #-}
 {-# LANGUAGE ConstraintKinds            #-}
 {-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE DeriveTraversable          #-}
 {-# LANGUAGE EmptyCase                  #-}
+{-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE InstanceSigs               #-}
 {-# LANGUAGE KindSignatures             #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE QuantifiedConstraints      #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
 {-# LANGUAGE UndecidableInstances       #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
@@ -36,15 +45,20 @@
 -- — the number of bits in an 'Int' (32 or 64).
 module Control.Monad.Foil.Internal where
 
-import           Control.DeepSeq (NFData (..))
-import           Data.Coerce     (coerce)
+import           Control.DeepSeq    (NFData (..))
+import           Data.Bifunctor
+import           Data.Coerce        (coerce)
 import           Data.IntMap
-import qualified Data.IntMap     as IntMap
+import qualified Data.IntMap        as IntMap
 import           Data.IntSet
-import qualified Data.IntSet     as IntSet
-import           Data.Kind       (Type)
+import qualified Data.IntSet        as IntSet
+import           Data.Kind          (Type)
+import qualified Data.Type.Equality as Type
+import           Generics.Kind
 import           Unsafe.Coerce
 
+import Control.Monad.Foil.Internal.ValidNameBinders
+
 -- * Safe types and operations
 
 -- | 'S' is a data kind of scope indices.
@@ -563,7 +577,17 @@
 class CoSinkable pattern => UnifiablePattern pattern where
   -- | Unify two patterns and decide which binders need to be renamed.
   unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
+  default unifyPatterns
+    :: (CoSinkable pattern, Distinct n)
+    => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
+  unifyPatterns l r = coerce (unifyPatterns (nameBinderListOf l) (nameBinderListOf r))
 
+instance UnifiablePattern NameBinderList where
+  unifyPatterns NameBinderListEmpty NameBinderListEmpty = SameNameBinders emptyNameBinders
+  unifyPatterns (NameBinderListCons x xs) (NameBinderListCons y ys) =
+    case (assertDistinct x, assertDistinct y) of
+      (Distinct, Distinct) -> unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)
+
 -- | Unification of values in patterns.
 -- By default, 'Eq' instance is used, but it may be useful to ignore
 -- some data in pattens (such as location annotations).
@@ -599,6 +623,10 @@
     -> e n                  -- ^ Expression with free variables in scope @n@.
     -> e l
 
+  default sinkabilityProof
+    :: (GenericK e, GSinkableK (RepK e)) => (Name n -> Name l) -> e n -> e l
+  sinkabilityProof rename = toK . gsinkabilityProof1 rename . fromK
+
 -- | Sinking a 'Name' is as simple as applying the renaming.
 instance Sinkable Name where
   sinkabilityProof rename = rename
@@ -688,6 +716,14 @@
     -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
     -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
     -> r
+  default coSinkabilityProof
+    :: (GenericK pattern, GSinkableK (RepK pattern))
+    => (Name n -> Name n')
+    -> pattern n l
+    -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)
+    -> r
+  coSinkabilityProof rename p cont = gsinkabilityProof2 rename (fromK @_ @pattern p) $ \rename' p' ->
+    cont rename' (toK @_ @pattern p')
 
   -- | Generalized processing of a pattern.
   --
@@ -707,6 +743,16 @@
     -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
     -> r
+  default withPattern
+    :: (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))
+    => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')
+    -> (forall x z z'. DExt z z' => f x x z z')
+    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')
+    -> Scope o
+    -> pattern n l
+    -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
+    -> r
+  withPattern = gunsafeWithPatternViaHasNameBinders
 
 -- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'.
 newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
@@ -808,7 +854,7 @@
 -- * 'Name' maps
 
 -- | A /total/ map from names in scope @n@ to elements of type @a@.
-newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a }
+newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } deriving (Functor, Foldable, Traversable)
 
 -- | An empty map belongs in the empty scope.
 emptyNameMap :: NameMap VoidS a
@@ -818,6 +864,10 @@
 nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o
 nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m)
 
+-- | Convert a 'NameMap' of expressions into a 'Scope'.
+nameMapToScope :: NameMap n a -> Scope n
+nameMapToScope (NameMap m) = UnsafeScope (IntMap.keysSet m)
+
 -- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder').
 --
 -- Note that the input list is expected to have __at least__ the same number of elements
@@ -907,3 +957,378 @@
 class InjectName (e :: S -> Type) where
   -- | Inject names into expressions.
   injectName :: Name n -> e n
+
+-- * Kind-polymorphic sinkability
+
+data RenamingsK (as :: LoT k) (bs :: LoT k) where
+  RNil :: RenamingsK LoT0 LoT0
+  RCons :: (Name a -> Name b) -> RenamingsK as bs -> RenamingsK (a :&&: as) (b :&&: bs)
+  RSkip :: RenamingsK as bs -> RenamingsK (k :&&: as) (k :&&: bs)
+
+class SinkableK (f :: S -> k) where
+  sinkabilityProofK
+    :: forall as bs r.
+       RenamingsK as bs
+    -> f :@@: as
+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)
+    -> r
+  default sinkabilityProofK :: forall as bs r.
+      (GenericK f, GSinkableK (RepK f))
+    => RenamingsK as bs
+    -> f :@@: as
+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)
+    -> r
+  sinkabilityProofK rename e cont =
+    gsinkabilityProofK rename (fromK @_ @f e) $ \rename' e' ->
+      cont rename' (toK @_ @f e')
+
+sinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f :@@: as -> f :@@: bs
+sinkK _ _ = unsafeCoerce
+
+instance SinkableK Name where
+  sinkabilityProofK renameK@(RCons rename RNil) name cont = cont renameK (rename name)
+instance SinkableK NameBinder where
+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinder name) cont =
+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinder name)
+instance SinkableK NameBinders where
+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinders s) cont =
+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinders s)
+
+instance GenericK NameBinderList where
+  type RepK NameBinderList = ((Var0 :~~: Var1) :=>: U1) :+: Exists S
+    (Field (NameBinder :$: Var1 :@: Var0) :*: Field (NameBinderList :$: Var0 :@: Var2))
+  toK (L1 (SuchThat U1))                   = NameBinderListEmpty
+  toK (R1 (Exists (Field x :*: Field xs))) = NameBinderListCons x xs
+  fromK NameBinderListEmpty       = L1 (SuchThat U1)
+  fromK (NameBinderListCons x xs) = R1 (Exists (Field x :*: Field xs))
+
+instance GenericK V2 where
+  type RepK V2 = V1
+  toK _v1 = error "absurd: Generics.Kind.V1"
+  fromK = absurd2
+
+instance GenericK U2 where
+  type RepK U2 = ((Var0 :~~: Var1) :=>: U1)
+  toK (SuchThat U1) = U2
+  fromK U2 = SuchThat U1
+
+instance SinkableK NameBinderList
+instance SinkableK V2
+instance SinkableK U2
+
+sinkabilityProof1 :: SinkableK f => (Name n -> Name n') -> f n -> f n'
+sinkabilityProof1 rename e = sinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'
+
+gsinkabilityProof1 :: GSinkableK f => (Name n -> Name n') -> f (n :&&: LoT0) -> f (n' :&&: LoT0)
+gsinkabilityProof1 rename e = gsinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'
+
+gsinkabilityProof2
+  :: forall f n n' l r. GSinkableK f
+  => (Name n -> Name n') -> f (n :&&: l :&&: LoT0)
+  -> (forall l'. (Name l -> Name l') -> f (n' :&&: l' :&&: LoT0) -> r)
+  -> r
+gsinkabilityProof2 rename e cont =
+  gsinkabilityProofK (RCons rename (RCons id RNil)) e $ \case
+    RCons (_ :: Name n -> Name n'') (RCons rename' RNil) -> \e' ->
+      case unsafeCoerce (Type.Refl :: n' Type.:~: n') :: n' Type.:~: n'' of
+        Type.Refl -> cont rename' e'
+
+gsinkabilityProofK' :: GSinkableK f => RenamingsK as bs -> f as -> f bs
+gsinkabilityProofK' renameK e = gsinkabilityProofK renameK e $ \_ e' -> unsafeCoerce e'
+
+class GSinkableK p where
+  gsinkabilityProofK
+    :: forall as bs r.
+       RenamingsK as bs
+    -> p as
+    -> (forall cs. RenamingsK as cs -> p cs -> r)
+    -> r
+
+gsinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f as -> f bs
+gsinkK _ _ = unsafeCoerce
+
+instance GSinkableK V1 where
+  gsinkabilityProofK irename _v1 cont =
+    cont irename (error "absurd: Generics.Kind.V1")
+
+instance GSinkableK U1 where
+  gsinkabilityProofK irename U1 cont =
+    cont irename U1
+
+instance GSinkableK f => GSinkableK (M1 i c f) where
+  gsinkabilityProofK irename (M1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (M1 x')
+
+instance (GSinkableK f, GSinkableK g) => GSinkableK (f :+: g) where
+  gsinkabilityProofK irename (L1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (L1 x')
+  gsinkabilityProofK irename (R1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (R1 x')
+
+instance (GSinkableK f, GSinkableK g) => GSinkableK (f :*: g) where
+  gsinkabilityProofK irename (x :*: y) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      gsinkabilityProofK irename' y $ \irename'' y' ->
+        cont irename'' (gsinkK irename' irename'' x' :*: y')
+
+instance GSinkableK f => GSinkableK (Exists S f) where
+  gsinkabilityProofK irename (Exists x) cont =
+    gsinkabilityProofK (RCons id irename) x $ \case
+      RCons _ irename' -> \x' ->
+        cont irename' (Exists x')
+
+instance {-# OVERLAPPABLE #-} GSinkableK f => GSinkableK (Exists k f) where
+  gsinkabilityProofK irename (Exists x) cont =
+    gsinkabilityProofK (RSkip irename) x $ \case
+      RSkip irename' -> \x' ->
+        cont irename' (Exists x')
+
+instance GSinkableK f => GSinkableK ((a :~~: b) :=>: f) where
+  gsinkabilityProofK irename (SuchThat x) cont =
+    gsinkabilityProofK irename x $ \(irename' :: RenamingsK as cs) x' ->
+      -- this is sort of safe...
+      case unsafeCoerce (Type.Refl :: Interpret a cs Type.:~: Interpret a cs) :: Interpret a cs Type.:~: Interpret b cs of
+        Type.Refl -> cont irename' (SuchThat x')
+
+instance GSinkableK (Field (Kon a)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field x)
+
+instance GSinkableK (Field (Var a)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (unsafeCoerce x)) -- FIXME: unsafeCoerce?
+
+instance (SinkableK f, ExtractRenamingK i) => GSinkableK (Field (Kon f :@: Var i)) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (RCons (extractRenamingK @_ @i irename) RNil) x $ \case
+      RCons rename' RNil -> \x' ->
+        cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce?
+
+instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where
+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
+    sinkabilityProofK irename x $ \rename' x' ->
+      cont rename' (Field x')
+
+instance SinkableK (f a b) => GSinkableK (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) where
+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
+    sinkabilityProofK irename x $ \rename' x' ->
+      cont rename' (Field x')
+
+class ExtractRenamingK (i :: TyVar k S) where
+  extractRenamingK :: forall (as :: LoT k) (bs :: LoT k).
+    RenamingsK as bs -> Name (Interpret (Var i) as) -> Name (Interpret (Var i) bs)
+  putBackRenamingK :: forall c (as :: LoT k) (bs :: LoT k).
+       (Name (Interpret (Var i) as) -> Name c)
+    -> RenamingsK as bs
+    -> RenamingsK as (PutBackLoT i c bs)
+
+instance ExtractRenamingK VZ where
+  extractRenamingK (RCons f _fs) = f
+  putBackRenamingK f (RCons _ gs) = RCons f gs
+
+instance ExtractRenamingK x => ExtractRenamingK (VS x) where
+  extractRenamingK (RCons _f fs) = extractRenamingK @_ @x fs
+  putBackRenamingK f (RCons g gs) = RCons g (putBackRenamingK @_ @x f gs)
+
+extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK as bs
+  -> RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (Interpret (Var i) bs :&&: Interpret (Var j) bs :&&: LoT0)
+extractTwoRenamingsK irename =
+  (RCons (extractRenamingK @_ @i irename) (RCons (extractRenamingK @_ @j irename) RNil))
+
+putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) c1 c2 (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (c1 :&&: c2 :&&: LoT0)
+  -> RenamingsK as bs
+  -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs))
+putBackTwoRenamingsK (RCons f1 (RCons f2 RNil)) rename
+  = putBackRenamingK @_ @j f2 (putBackRenamingK @_ @i f1 rename)
+
+instance (SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field (Kon f :@: Var (i :: TyVar k S) :@: Var (j :: TyVar k S))) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (extractTwoRenamingsK @_ @i @j irename) x $ \rename' x' ->
+      case rename' of
+        RCons _ (RCons _ RNil) ->
+          cont (putBackTwoRenamingsK @_ @i @j rename' irename)
+              (Field (unsafeCoerce x'))  -- FIXME: can we do better than unsafeCoerce?
+
+instance (Functor f, GSinkableK (Field x)) => GSinkableK (Field (Kon f :@: x)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (fmap
+      (unField . gsinkabilityProofK' @(Field x) irename . Field)
+      x))
+
+instance (Bifunctor f, GSinkableK (Field x), GSinkableK (Field y)) => GSinkableK (Field (Kon f :@: x :@: y)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (bimap
+      (unField . gsinkabilityProofK' @(Field x) irename . Field)
+      (unField . gsinkabilityProofK' @(Field y) irename . Field)
+      x))
+
+-- * Kind-polymorphic types with binders
+
+-- ** Generic version of 'withPattern'
+
+-- | Generic generalized processing of a pattern via 'GHasNameBinders'.
+--
+-- This can be used as a default implementation of 'withPattern'.
+gunsafeWithPatternViaHasNameBinders
+  :: forall pattern f o n l r.
+      (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))
+  => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')
+  -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern.
+  -> (forall x z z'. DExt z z' => f x x z z')
+  -- ^ Result in case no binders are present. This can be seen as scope-indexed 'mempty'.
+  -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')
+  -- ^ Composition of results for nested binders/patterns. This can be seen as scope-indexed 'mappend'.
+  -> Scope o
+  -- ^ Ambient scope.
+  -> pattern n l
+  -- ^ Pattern to process.
+  -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
+  -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
+  -> r
+gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont =
+  withPattern withBinder id_ comp_ scope (ggetNameBinders pat) $ \result binders ->
+    cont result (gunsafeSetNameBinders (unsafeCoerce pat) binders) -- FIXME: safer version
+
+-- ** Manipulating nested 'NameBinder's
+-- | If @'HasNameBinders' f@, then @f n l@ is expected to act as a binder,
+-- introducing into scope @n@ some local variables, extending it to scope @l@.
+-- This class allows to extract and modify the set of binders.
+class HasNameBinders f where
+  -- | Extract a set of binders from a pattern.
+  getNameBinders :: f n l -> NameBinders n l
+  getNameBinders = UnsafeNameBinders . IntSet.fromList . getNameBindersRaw
+
+  -- | Replace binders in a pattern.
+  --
+  -- This function is unsafe, because it does not check if the new set of binders
+  -- has the same size. It can therefore crash at runtime.
+  --
+  -- You should probably not use this.
+  -- This is only used for 'gunsafeWithPatternViaHasNameBinders', which is then safe to use.
+  unsafeSetNameBinders :: f n l -> NameBinders n l' -> f n l'
+  unsafeSetNameBinders e (UnsafeNameBinders m) = fst (reallyUnsafeSetNameBindersRaw e (IntSet.toList m))
+
+  -- | Extract 'RawName's of all binders occurring in a pattern.
+  getNameBindersRaw :: f n l -> [RawName]
+  default getNameBindersRaw :: forall n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> [RawName]
+  getNameBindersRaw = ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)
+
+  -- | This is a version of 'unsafeSetNameBinders'
+  -- that takes in a list of 'RawName's.
+  --
+  -- It does not check if the given list has enough elements.
+  -- It does not check if the raw names are fresh in the scope @n@.
+  -- It does not check if the raw names given are distinct.
+  --
+  -- You should never use this. This is only used for generic implementation of 'HasNameBinders'.
+  reallyUnsafeSetNameBindersRaw :: f n l -> [RawName] -> (f n l', [RawName])
+  default reallyUnsafeSetNameBindersRaw :: forall n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName])
+  reallyUnsafeSetNameBindersRaw e names =
+    let (e', names') = greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) names
+     in (toK @_ @f @(n :&&: l' :&&: LoT0) e', names')
+
+instance HasNameBinders NameBinder where
+  getNameBindersRaw (UnsafeNameBinder (UnsafeName name)) = [name]
+  reallyUnsafeSetNameBindersRaw _ (name:names) = (UnsafeNameBinder (UnsafeName name), names)
+
+instance HasNameBinders NameBinderList
+
+-- ** Generic
+
+ggetNameBinders :: forall f n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l
+ggetNameBinders = UnsafeNameBinders . IntSet.fromList . ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)
+
+gunsafeSetNameBinders :: forall f n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l'
+gunsafeSetNameBinders e (UnsafeNameBinders m) = toK @_ @f @(n :&&: l' :&&: LoT0) $
+  fst (greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) (IntSet.toList m))
+
+class GHasNameBinders f where
+  ggetNameBindersRaw :: f as -> [RawName]
+  greallyUnsafeSetNameBindersRaw :: f as -> [RawName] -> (f bs, [RawName])
+
+instance GHasNameBinders V1 where
+  ggetNameBindersRaw _ = error "absurd: Generics.Kind.V1"
+  greallyUnsafeSetNameBindersRaw _ _ = error "absurd: Generics.Kind.V1"
+instance GHasNameBinders U1 where
+  ggetNameBindersRaw U1 = []
+  greallyUnsafeSetNameBindersRaw U1 names = (U1, names)
+
+instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :+: g) where
+  ggetNameBindersRaw (L1 x) = ggetNameBindersRaw x
+  ggetNameBindersRaw (R1 x) = ggetNameBindersRaw x
+
+  greallyUnsafeSetNameBindersRaw (L1 x) names = first L1 (greallyUnsafeSetNameBindersRaw x names)
+  greallyUnsafeSetNameBindersRaw (R1 x) names = first R1 (greallyUnsafeSetNameBindersRaw x names)
+
+-- | FIXME: this is, perhaps, the most "unsafe" place for the user
+-- since it does not reject "parallel" binders:
+--
+--    data BadPattern n l = BadPattern (NameBinder n l) (NameBinder n l)
+--
+-- This instance will treat both binders in the same way as "nested":
+--
+--    data GoodPattern n l = forall i. GoodPattern (NameBinder n i) (NameBinder i l)
+--
+-- However, Template Haskell code at the moment will never generate "parallel" binders,
+-- and the very user is unlikely to misuse this instance, since "parallel" binders
+-- require extra effort to support it.
+--
+-- Still, it would be better to detect and reject any "parallel" or otherwise improper binders.
+instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :*: g) where
+  ggetNameBindersRaw (x :*: y) = ggetNameBindersRaw x <> ggetNameBindersRaw y
+  greallyUnsafeSetNameBindersRaw (x :*: y) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+        (y', names'') = greallyUnsafeSetNameBindersRaw y names'
+     in (x' :*: y', names'')
+
+instance GHasNameBinders f => GHasNameBinders (M1 i c f) where
+  ggetNameBindersRaw (M1 x) = ggetNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (M1 x) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+     in (M1 x', names')
+
+instance GHasNameBinders f => GHasNameBinders (Var i :~~: Var j :=>: f) where
+  ggetNameBindersRaw (SuchThat x) = ggetNameBindersRaw x
+
+  greallyUnsafeSetNameBindersRaw :: forall as bs. (Var i :~~: Var j :=>: f) as -> [RawName] -> ((Var i :~~: Var j :=>: f) bs, [RawName])
+  greallyUnsafeSetNameBindersRaw (SuchThat x) names =
+    -- this is sort of safe...
+    case unsafeCoerce (Type.Refl :: Interpret (Var i) bs Type.:~: Interpret (Var i) bs) :: Interpret (Var i) bs Type.:~: Interpret (Var j) bs of
+      Type.Refl ->
+        let (x', names') = greallyUnsafeSetNameBindersRaw x names
+         in (SuchThat x', names')
+
+instance GHasNameBinders f => GHasNameBinders (Exists k f) where
+  ggetNameBindersRaw (Exists x) = ggetNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (Exists x) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+     in (Exists x', names')
+
+instance GHasNameBinders (Field (Kon a)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field x, names)
+
+instance GHasNameBinders (Field (Var x)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names)  -- FIXME: unsafeCoerce?
+
+instance GHasNameBinders (Field (Kon f :@: Var i)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names) -- FIXME: unsafeCoerce?
+
+instance HasNameBinders f => GHasNameBinders (Field (Kon f :@: Var i :@: Var j)) where
+  ggetNameBindersRaw (Field x) = getNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (Field x) names =
+    let (x', names') = reallyUnsafeSetNameBindersRaw x names
+     in (Field (unsafeCoerce x'), names') -- FIXME: safer version?
diff --git a/src/Control/Monad/Foil/Internal/ValidNameBinders.hs b/src/Control/Monad/Foil/Internal/ValidNameBinders.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Foil/Internal/ValidNameBinders.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE StandaloneKindSignatures  #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators  #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE TypeFamilies  #-}
+{-# LANGUAGE PolyKinds  #-}
+{-# LANGUAGE DataKinds  #-}
+module Control.Monad.Foil.Internal.ValidNameBinders where
+
+import Data.Kind (Type, Constraint)
+import GHC.TypeError
+import GHC.TypeLits
+import Generics.Kind
+import qualified GHC.Generics as GHC
+
+type SubstInRepK :: TyVar d k -> Atom d k -> (LoT d -> Type) -> LoT d -> Type
+type family SubstInRepK i atom f where
+  SubstInRepK i atom V1 = V1
+  SubstInRepK i atom U1 = U1
+  SubstInRepK i atom (M1 info c f) = M1 info c (SubstInRepK i atom f)
+  SubstInRepK i atom (Field field) = Field (SubstInAtom i atom field)
+  SubstInRepK i atom (f :+: g) = SubstInRepK i atom f :+: SubstInRepK i atom g
+  SubstInRepK i atom (f :*: g) = SubstInRepK i atom f :*: SubstInRepK i atom g
+  SubstInRepK i atom f =
+    TypeError
+      ('Text "cannot substitute variable"
+      :$$: 'Text "  " :<>: 'ShowType (Var i)
+      :$$: 'Text "with atom"
+      :$$: 'Text "  " :<>: 'ShowType atom
+      :$$: 'Text "in"
+      :$$: 'Text "  " :<>: 'ShowType f)
+
+type SubstInAtom :: TyVar d k -> Atom d k -> Atom d k1 -> Atom d k1
+type family SubstInAtom i atom f where
+  SubstInAtom i atom (Var i) = atom
+  SubstInAtom i atom (Var j) = Var j
+  SubstInAtom i atom (Kon a) = Kon a
+  SubstInAtom i atom (f :@: x) = SubstInAtom i atom f :@: SubstInAtom i atom x
+  -- SubstInAtom i atom atom' = atom'
+  SubstInAtom i atom atom' =
+    TypeError
+      ('Text "cannot substitute variable"
+      :$$: 'Text "  " :<>: 'ShowType (Var i)
+      :$$: 'Text "with atom"
+      :$$: 'Text "  " :<>: 'ShowType atom
+      :$$: 'Text "in an atom"
+      :$$: 'Text "  " :<>: 'ShowType atom')
+
+type ShowKindedScope oo n ll = ShowScope oo n ll :<>: 'Text " : S"
+
+type ShowScope :: Atom d s -> Atom d s -> Atom d s -> ErrorMessage
+type family ShowScope oo n ll where
+  ShowScope oo ll ll = 'Text "innerScope"
+  ShowScope oo oo ll = 'Text "outerScope"
+  ShowScope oo n  ll = ShowScopeN 1 n
+
+type ShowScopeN :: Natural -> Atom d s -> ErrorMessage
+type family ShowScopeN i n where
+  ShowScopeN i (Var VZ) = 'Text "scope" :<>: 'ShowType i
+  ShowScopeN i (Var (VS x)) = ShowScopeN (i + 1) (Var x)
+
+type ShowSaturatedPatternType pattern oo n l ll =
+  'ShowType pattern :<>: 'Text " " :<>: ShowScope oo n ll :<>: 'Text " " :<>: ShowScope oo l ll
+
+type GInnerScopeOfAtom :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> Atom d Type -> Atom d s -> Atom d s -> Atom d s -> Atom d s
+type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where
+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: n :@: l) oo n ll = l
+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: o :@: i) oo n ll =
+    TypeError
+      ('Text "Unexpected Foil scope extension in the binder/pattern"
+      :$$: 'Text "  " :<>: ShowSaturatedPatternType f oo o i ll
+      :$$: 'Text "the binder/pattern tries to extend scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo o ll
+      :$$: 'Text "to scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo i ll
+      :$$: 'Text "but it is expected to extend the current (outer) scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo n ll
+      :$$: ShowLocalizeError msg icon ifield pattern oo ll
+      )
+  GInnerScopeOfAtom msg icon ifield pattern atom oo n ll = n
+
+type SameInnerScope :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom k s -> Atom k s -> Atom k s
+type family SameInnerScope msg icon pattern n l where
+  SameInnerScope msg icon pattern l l = l
+  SameInnerScope msg icon pattern n l =
+    TypeError
+      ('Text "Unexpected extended (inner) Foil scope in the data type"
+      :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l
+      :$$: 'Text "expecting extended (inner) scope to be"
+      :$$: 'Text "  " :<>: ShowKindedScope n l l
+      :$$: 'Text "but the inferred extended (inner) scope is"
+      :$$: 'Text "  " :<>: ShowKindedScope n n l
+      :$$: ShowLocalizeError msg icon 0 pattern n l
+      )
+
+type GValidNameBinders :: (s -> s -> Type) -> (LoT (s -> s -> Type) -> Type) -> Constraint
+type family GValidNameBinders pattern f :: Constraint where
+  GValidNameBinders pattern (f :: LoT (s -> s -> Type) -> Type) =
+    (GInnerScopeOfRepK ('Text "") 0 0 pattern f Var0 Var0 Var1)
+    ~ (Var1 :: Atom (s -> s -> Type) s)
+
+type AtomSucc :: Atom d k1 -> Atom (k -> d) k1
+type family AtomSucc atom where
+  AtomSucc (Var i) = Var (VS i)
+
+type AtomUnSucc :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom d s -> Atom d s -> Atom (k -> d) k1 -> Atom d k1
+type family AtomUnSucc msg icon pattern oo ll atom where
+  AtomUnSucc msg icon pattern oo ll (Var (VS i)) = Var i
+  AtomUnSucc msg icon pattern oo ll (Var VZ) = TypeError
+    ('Text "Intermediate scope escapes existential quantification for data type"
+      :$$: ShowLocalizeError msg icon 0 pattern oo ll
+      )
+
+type family First x y where
+  First (Var x) (Var y) = Var x
+
+type family AndShowFieldNumber ifield msg where
+  AndShowFieldNumber 0 msg = msg
+  AndShowFieldNumber n msg =
+    'Text "when checking field number " :<>: 'ShowType n
+    :$$: msg
+
+type family AndShowConNumber icon msg where
+  AndShowConNumber 0 msg = msg
+  AndShowConNumber n msg =
+    'Text "when checking constructor number " :<>: 'ShowType n
+    :$$: msg
+
+type AndShowDataType pattern n l msg =
+  'Text "when tracking Foil scopes for the data type"
+  :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l
+  :$$: msg
+
+type ShowLocalizeError msg icon ifield pattern o l =
+    AndShowFieldNumber ifield
+      (AndShowConNumber icon
+        (AndShowDataType pattern o l
+          msg))
+
+type family CountCons f where
+  CountCons (f :+: g) = CountCons f + CountCons g
+  CountCons (M1 GHC.C c f) = 1
+
+type family CountFields f where
+  CountFields (f :*: g) = CountFields f + CountFields g
+  CountFields (M1 GHC.S c f) = 1
+
+type GInnerScopeOfRepK :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> (LoT k -> Type) -> Atom k s -> Atom k s -> Atom k s -> Atom k s
+type family GInnerScopeOfRepK msg icon ifield pattern f o n l where
+  GInnerScopeOfRepK msg icon ifield pattern V1 o n l = l
+  GInnerScopeOfRepK msg icon ifield pattern U1 o n l = n
+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.C c f) o n l =
+    GInnerScopeOfRepK msg icon 1 pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.D c f) o n l =
+    GInnerScopeOfRepK msg 1 ifield pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (M1 i c f) o n l =
+    GInnerScopeOfRepK msg icon ifield pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (f :+: g) o n l = First
+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg icon ifield pattern f o n l) l)
+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg (icon + CountCons f) ifield pattern g o n l) l)
+  GInnerScopeOfRepK msg icon ifield pattern (f :*: g) o n l =
+    GInnerScopeOfRepK msg icon (ifield + CountFields f) pattern g o
+      (GInnerScopeOfRepK msg icon ifield pattern f o n l) l
+  GInnerScopeOfRepK msg icon ifield pattern (Var i :~~: Var j :=>: f) o n l =
+    GInnerScopeOfRepK msg icon ifield pattern (SubstInRepK i (Var j) f)
+      (SubstInAtom i (Var j) o) (SubstInAtom i (Var j) n) (SubstInAtom i (Var j) l)
+  GInnerScopeOfRepK msg icon ifield pattern (Exists k f) o n l =
+    AtomUnSucc msg icon pattern o l
+      (GInnerScopeOfRepK msg icon ifield pattern f (AtomSucc o) (AtomSucc n) (AtomSucc l))
+  GInnerScopeOfRepK msg icon ifield pattern (Field atom) o n l = GInnerScopeOfAtom msg icon ifield pattern atom o n l
+  GInnerScopeOfRepK msg icon ifield pattern f o n l =
+    TypeError
+      ('Text "Unsupported structure in a binder/pattern"
+      :$$: 'Text "  " :<>: 'ShowType f
+      :$$: ShowLocalizeError msg icon 0 pattern n l)
+
+type PutBackLoT :: TyVar d s -> s -> LoT k -> LoT k
+type family PutBackLoT i c bs where
+  PutBackLoT VZ c (b :&&: bs) = c :&&: bs
+  PutBackLoT (VS x) c (b :&&: bs) = b :&&: PutBackLoT x c bs
diff --git a/src/Control/Monad/Free/Foil.hs b/src/Control/Monad/Free/Foil.hs
--- a/src/Control/Monad/Free/Foil.hs
+++ b/src/Control/Monad/Free/Foil.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -23,13 +25,18 @@
 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.Bifunctor.Sum
+import Data.ZipMatchK
+import qualified Generics.Kind as Kind
+import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))
 import           Data.Coerce                 (coerce)
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
+import           Data.Maybe                  (mapMaybe)
 import           Data.Monoid                 (All (..))
 import           GHC.Generics                (Generic)
+import           Unsafe.Coerce               (unsafeCoerce)
 
 -- | Scoped term under a (single) name binder.
 data ScopedAST binder sig n where
@@ -50,15 +57,26 @@
 deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
   => NFData (AST binder sig n)
 
-instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) where
-  sinkabilityProof rename = \case
-    Var name -> Var (rename name)
-    Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)
-    where
-      f (ScopedAST binder body) =
-        Foil.extendRenaming rename binder $ \rename' binder' ->
-          ScopedAST binder' (Foil.sinkabilityProof rename' body)
+instance GenericK (ScopedAST binder sig) where
+  type RepK (ScopedAST binder sig) =
+    Exists Foil.S
+      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))
+  toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast
+  fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)
 
+instance GenericK (AST binder sig) where
+  type RepK (AST binder sig) =
+    Field (Foil.Name :$: Var0)
+    :+: Field (sig
+                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)
+                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))
+
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)
+
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)
+
 instance Foil.InjectName (AST binder sig) where
   injectName = Var
 
@@ -66,7 +84,7 @@
 
 -- | Substitution for free (scoped monads).
 substitute
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
   -> Foil.Substitution (AST binder sig) i o
   -> AST binder sig i
@@ -91,7 +109,7 @@
 --
 -- In general, 'substitute' is more efficient since it does not always refresh binders.
 substituteRefreshed
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
   -> Foil.Substitution (AST binder sig) i o
   -> AST binder sig i
@@ -108,7 +126,8 @@
         in ScopedAST binder' body'
 
 -- | @'AST' sig@ is a monad relative to 'Foil.Name'.
-instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST binder sig) where
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)
+  => Foil.RelMonad Foil.Name (AST binder sig) where
   rreturn = Var
   rbind scope term subst =
     case term of
@@ -124,7 +143,7 @@
 
 -- | Substitution for a single generalized pattern.
 substitutePattern
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o                           -- ^ Resulting scope.
   -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.
   -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.
@@ -140,7 +159,7 @@
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.
 refreshAST
-  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -149,7 +168,7 @@
   Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)
 
 -- | Similar to `refreshAST`, but for scoped terms.
-refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -165,7 +184,7 @@
 -- 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)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,21 +197,21 @@
 -- 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)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK 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)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,20 +256,20 @@
 -- 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)
+  :: (Bitraversable 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)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
@@ -260,20 +279,6 @@
       (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
@@ -389,3 +394,23 @@
   ScopedAST binder body ->
     ( makePattern binder
     , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))
+
+-- ** Unsinking AST
+
+-- | Unsink an AST from a larger scope to a smaller scope.
+unsinkAST :: (Foil.Distinct l, Foil.CoSinkable binder, Bifoldable sig) => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n)
+unsinkAST scope term
+  | all (`Foil.member` scope) (freeVarsOf term) = Just (unsafeCoerce term)
+  | otherwise = Nothing
+
+-- | Get the free variables of an AST.
+freeVarsOf :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => AST binder sig n -> [Foil.Name n]
+freeVarsOf = \case
+  Var name -> [name]
+  Node node -> bifoldMap freeVarsOfScopedAST freeVarsOf node
+
+-- | Get the free variables of a scoped AST.
+freeVarsOfScopedAST :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => ScopedAST binder sig n -> [Foil.Name n]
+freeVarsOfScopedAST (ScopedAST binder body) =
+  case Foil.assertDistinct binder of
+    Foil.Distinct -> mapMaybe (Foil.unsinkNamePattern binder) (freeVarsOf body)
diff --git a/src/Control/Monad/Free/Foil/Generic.hs b/src/Control/Monad/Free/Foil/Generic.hs
deleted file mode 100644
--- a/src/Control/Monad/Free/Foil/Generic.hs
+++ /dev/null
@@ -1,196 +0,0 @@
-{-# OPTIONS_GHC -Wno-missing-methods #-}
-{-# LANGUAGE AllowAmbiguousTypes      #-}
-{-# LANGUAGE ConstraintKinds          #-}
-{-# LANGUAGE DataKinds                #-}
-{-# LANGUAGE DefaultSignatures        #-}
-{-# LANGUAGE FlexibleContexts         #-}
-{-# LANGUAGE FlexibleInstances        #-}
-{-# LANGUAGE GADTs                    #-}
-{-# LANGUAGE InstanceSigs             #-}
-{-# LANGUAGE MultiParamTypeClasses    #-}
-{-# LANGUAGE PolyKinds                #-}
-{-# LANGUAGE RankNTypes               #-}
-{-# LANGUAGE ScopedTypeVariables      #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeApplications         #-}
-{-# LANGUAGE TypeFamilies             #-}
-{-# LANGUAGE TypeOperators            #-}
-{-# LANGUAGE UndecidableInstances     #-}
-module Control.Monad.Free.Foil.Generic where
-
-import           Data.Kind              (Constraint, Type)
-import           Generics.Kind
-import           Generics.Kind.Examples ()
-import           GHC.TypeError
-
-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
-
-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
-
-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)
-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)
-
-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
-instance ZipMatchK Either
-instance ZipMatchK a => ZipMatchK (Either a)
-
-type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)
-class GZipMatch (f :: LoT k -> Type) where
-  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint
-  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
-
-instance GZipMatch V1 where
-  type ReqsZipMatchWith V1 as bs cs = ()
-  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd
-
-instance GZipMatch U1 where
-  type ReqsZipMatchWith U1 as bs cs = ()
-  gzipMatchWith _ U1 U1 = Just U1
-
-instance GZipMatch f => GZipMatch (M1 i c f) where
-  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs
-  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y
-
-instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where
-  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
-  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y
-  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y
-  gzipMatchWith _ _ _           = Nothing
-
-instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where
-  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
-  gzipMatchWith g (x :*: y) (x' :*: y') =
-    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')
-
-instance ZipMatchFields t => GZipMatch (Field t) where
-  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
-  gzipMatchWith f x y = zipMatchFieldsWith f x y
-
-instance GZipMatch f => GZipMatch (c :=>: f) where
-  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)
-  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))
-  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y
-
-instance TypeError ('Text "Existentials are not supported")
-         => GZipMatch (Exists k f) where
-  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")
-  gzipMatchWith = undefined
-
-class ZipMatchFields (t :: Atom d Type) where
-  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint
-  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
-
-instance ApplyMappings v => ZipMatchFields (Var v) where
-  -- this is always true, but GHC is not smart enough to know that, I think
-  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))
-  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y
-
-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
-  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)
-  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
-  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 =>
-    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)
-  zipMatchFieldsWith g (Field l) (Field r) =
-    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)
-      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))
-        :^: ((\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
-  -- 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
-  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
-  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
-  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/src/Control/Monad/Free/Foil/TH.hs b/src/Control/Monad/Free/Foil/TH.hs
--- a/src/Control/Monad/Free/Foil/TH.hs
+++ b/src/Control/Monad/Free/Foil/TH.hs
@@ -2,10 +2,8 @@
   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/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
--- a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
+++ b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
@@ -83,7 +83,7 @@
       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/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
deleted file mode 100644
--- a/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/src/Data/ZipMatchK.hs b/src/Data/ZipMatchK.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ZipMatchK.hs
@@ -0,0 +1,80 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | Kind-polymorphic syntactic (first-order) unification.
+module Data.ZipMatchK (
+  module Data.ZipMatchK.Mappings,
+  ZipMatchK(..),
+  zipMatchK,
+  -- * 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
+
+-- | 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/src/Data/ZipMatchK/Bifunctor.hs b/src/Data/ZipMatchK/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ZipMatchK/Bifunctor.hs
@@ -0,0 +1,35 @@
+{-# 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.Bifunctor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Bitraversable
+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)
+
+-- | 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/src/Data/ZipMatchK/Functor.hs b/src/Data/ZipMatchK/Functor.hs
new file mode 100644
--- /dev/null
+++ b/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/src/Data/ZipMatchK/Generic.hs b/src/Data/ZipMatchK/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ZipMatchK/Generic.hs
@@ -0,0 +1,193 @@
+{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes      #-}
+{-# LANGUAGE ConstraintKinds          #-}
+{-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE DefaultSignatures        #-}
+{-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE InstanceSigs             #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
+{-# LANGUAGE PolyKinds                #-}
+{-# LANGUAGE RankNTypes               #-}
+{-# LANGUAGE ScopedTypeVariables      #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances     #-}
+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)
+genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings
+  (fromK @_ @f @as x)
+  (fromK @_ @f @bs y)
+
+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 (,)
+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
+  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint
+  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
+
+instance GZipMatch V1 where
+  type ReqsZipMatchWith V1 as bs cs = ()
+  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd
+
+instance GZipMatch U1 where
+  type ReqsZipMatchWith U1 as bs cs = ()
+  gzipMatchWith _ U1 U1 = Just U1
+
+instance GZipMatch f => GZipMatch (M1 i c f) where
+  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs
+  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y
+
+instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where
+  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
+  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y
+  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y
+  gzipMatchWith _ _ _           = Nothing
+
+instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where
+  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
+  gzipMatchWith g (x :*: y) (x' :*: y') =
+    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')
+
+instance ZipMatchFields t => GZipMatch (Field t) where
+  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
+  gzipMatchWith f x y = zipMatchFieldsWith f x y
+
+instance GZipMatch f => GZipMatch (c :=>: f) where
+  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)
+  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))
+  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y
+
+instance TypeError ('Text "Existentials are not supported")
+         => GZipMatch (Exists k f) where
+  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")
+  gzipMatchWith = undefined
+
+class ZipMatchFields (t :: Atom d Type) where
+  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint
+  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
+
+instance ApplyMappings v => ZipMatchFields (Var v) where
+  -- this is always true, but GHC is not smart enough to know that, I think
+  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))
+  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y
+
+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 {-# 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 =>
+    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 {-# 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 =>
+    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)
+  zipMatchFieldsWith g (Field l) (Field r) =
+    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)
+      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))
+        :^: ((\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"
+  :$$: '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
+
+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"
+  :$$: '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"
+  :$$: '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
diff --git a/src/Data/ZipMatchK/Mappings.hs b/src/Data/ZipMatchK/Mappings.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ZipMatchK/Mappings.hs
@@ -0,0 +1,60 @@
+{-# 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
+
+-- | 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 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 = 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      -- ^ 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)