diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,38 @@
 # CHANGELOG for `free-foil`
 
+# 0.6.0 — 2026-10-26
+
+This release lets `mkFreeFoil` generate most instances of a signature, and adds folds that traverse terms without rebuilding them. Several breaking changes come with it, described first.
+
+Breaking changes:
+
+- Scope indices have the nominal role, so `coerce` can no longer change a scope (see [#113](https://github.com/fizruk/free-foil/pull/113), [#112](https://github.com/fizruk/free-foil/issues/112)). This applies to `Name`, `NameBinder`, `Scope`, `NameSet`, `NameBinders`, `NameMap`, the first index of `Substitution`, and the types of `Control.Monad.Foil.Blocks`.
+  - To migrate, compare names of different scopes by `nameId`, and move a term to an extended scope with `sink`.
+- `mkFreeFoil` generates the `Bifunctor`, `Bifoldable`, `Bitraversable`, `ZipMatchK`, `ZipMatchFoldK` and `NFData` instances of every signature, and `NFData` of every binding type (see [#116](https://github.com/fizruk/free-foil/pull/116), [#118](https://github.com/fizruk/free-foil/pull/118), [#119](https://github.com/fizruk/free-foil/pull/119)).
+  - To migrate, delete these instances (or the splices deriving them), or leave them out with `mkFreeFoilWith`.
+  - Instances for the payload types (identifiers, positions) must now be declared before the `mkFreeFoil` splice.
+- `deriveCoSinkable` takes the scope-safe pattern type, like the other `derive*` functions (see [#122](https://github.com/fizruk/free-foil/pull/122)). The old function, which takes the raw identifier and pattern types, is renamed to `mkCoSinkableFoilPattern`.
+- `nameBinderListOf` is a method of `CoSinkable` (see [#110](https://github.com/fizruk/free-foil/pull/110)). A module that imports `CoSinkable(..)` and defines its own `nameBinderListOf` must hide one of them.
+- `deriveZipMatchK` needs a `ZipMatchFoldK` instance for every container type applied to a zipped parameter (see [#119](https://github.com/fizruk/free-foil/pull/119)). The library provides them for lists, `Maybe`, `Either`, pairs, `NonEmpty`, `Sum` and `Product`. Derive others with `deriveZipMatchK1`.
+
+New:
+
+- `ZipMatchFoldK` matches two values one level deep, like `ZipMatchK`, but folds the paired components into a monoid instead of rebuilding the value (see [#119](https://github.com/fizruk/free-foil/pull/119)). `deriveZipMatchK` derives it together with `ZipMatchK`.
+- `zipMatchAllK` and `zipMatchAnyK` (with `1` and `2` variants) check a relation on all or on any of the paired components (see [#121](https://github.com/fizruk/free-foil/pull/121)).
+- `foldAST` folds a term bottom-up, and `hoistAST` changes its signature by a natural transformation (see [#115](https://github.com/fizruk/free-foil/pull/115)).
+- `deriveCoSinkable` derives `CoSinkable` for a scope-safe pattern type (see [#122](https://github.com/fizruk/free-foil/pull/122)).
+- `mkFreeFoilWith` takes `FreeFoilOptions` to choose which instances to generate (see [#116](https://github.com/fizruk/free-foil/pull/116), [#118](https://github.com/fizruk/free-foil/pull/118)).
+- `zipMatchKInstance` builds a `ZipMatchK` instance from constructor fields, for Template Haskell code (see [#116](https://github.com/fizruk/free-foil/pull/116)).
+- `gnameBinderListOf` lists the binders of a pattern generically (see [#110](https://github.com/fizruk/free-foil/pull/110)).
+
+Performance:
+
+- `nameBinderListOf` no longer traverses the pattern for the library's instances and the generated ones (see [#110](https://github.com/fizruk/free-foil/pull/110), [#123](https://github.com/fizruk/free-foil/pull/123)).
+- `withRefreshedPattern` is `INLINE`, so that it specialises at a known pattern type (see [#120](https://github.com/fizruk/free-foil/pull/120)).
+- `rnf` of `AST` specialises at a known signature, and is about four times faster there (see [#114](https://github.com/fizruk/free-foil/pull/114)).
+- The generated signature instances are marked `INLINE`, since GHC does not inline the derived methods of a large signature (see [#116](https://github.com/fizruk/free-foil/pull/116)).
+- The `ZipMatchK` instances for `Sum` and `Product` are written out instead of generic, and no longer require `Bitraversable` (or `Traversable`) of the components (see [#109](https://github.com/fizruk/free-foil/pull/109)).
+
 # 0.5.0 — 2026-10-07
 
 A release about *binders*. The law tests added after 0.4.0 ([#100](https://github.com/fizruk/free-foil/pull/100)) found bugs in how binders are sunk, ordered, paired and transported, and this release fixes them. The fixes change α-equivalence for patterns of several binders, so the release is major. It also generates single-binder pattern types as newtypes and removes the functions deprecated in 0.3.3 and 0.4.0.
diff --git a/bench/binders/Config.hs b/bench/binders/Config.hs
new file mode 100644
--- /dev/null
+++ b/bench/binders/Config.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- | A raw syntax for 'mkFreeFoil' whose patterns are variables and pairs, in
+-- its own module because Template Haskell may not splice a value defined in
+-- the same module. It follows @PatternsConfig@ of the test suite.
+module Config where
+
+import           Control.Monad.Free.Foil.TH.MkFreeFoil
+
+newtype BVarIdent = BVarIdent String
+
+data BPattern
+  = BPatternVar BVarIdent
+  | BPatternPair BPattern BPattern
+
+newtype BScopedTerm = BScopedTerm BTerm
+
+data BTerm
+  = BVar BVarIdent
+  | BFun BPattern BScopedTerm
+
+intToBVarIdent :: Int -> BVarIdent
+intToBVarIdent i = BVarIdent ("x" <> show i)
+
+bVar :: BVarIdent -> BTerm
+bVar = BVar
+
+bTermToScope :: BTerm -> BScopedTerm
+bTermToScope = BScopedTerm
+
+bScopeToTerm :: BScopedTerm -> BTerm
+bScopeToTerm (BScopedTerm t) = t
+
+bConfig :: FreeFoilConfig
+bConfig = FreeFoilConfig
+  { rawQuantifiedNames = []
+  , freeFoilTermConfigs =
+      [ FreeFoilTermConfig
+          { rawIdentName = ''BVarIdent
+          , rawTermName = ''BTerm
+          , rawBindingName = ''BPattern
+          , rawScopeName = ''BScopedTerm
+          , rawVarConName = 'BVar
+          , rawSubTermNames = []
+          , rawSubScopeNames = []
+          , intToRawIdentName = 'intToBVarIdent
+          , rawVarIdentToTermName = 'bVar
+          , rawTermToScopeName = 'bTermToScope
+          , rawScopeToTermName = 'bScopeToTerm
+          } ]
+  , freeFoilNameModifier = ("FF" ++)
+  , freeFoilScopeNameModifier = ("FFScoped" ++)
+  , freeFoilConNameModifier = ("FF" ++)
+  , freeFoilConvertFromName = ("from" ++)
+  , freeFoilConvertToName = ("to" ++)
+  , signatureNameModifier = (++ "Sig")
+  }
diff --git a/bench/binders/Generated.hs b/bench/binders/Generated.hs
new file mode 100644
--- /dev/null
+++ b/bench/binders/Generated.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE KindSignatures    #-}
+{-# LANGUAGE PatternSynonyms   #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE TypeFamilies      #-}
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+-- | The syntax that 'mkFreeFoil' generates from "Config", whose pattern type
+-- 'FFBPattern' has the 'Control.Monad.Foil.CoSinkable' instance it generates.
+module Generated where
+
+import           Control.Monad.Free.Foil.TH.MkFreeFoil (mkFreeFoil)
+
+import           Config
+
+mkFreeFoil bConfig
+
diff --git a/bench/binders/Main.hs b/bench/binders/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/binders/Main.hs
@@ -0,0 +1,269 @@
+{-# LANGUAGE BangPatterns        #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE DeriveTraversable   #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+-- The raw types below only serve Template Haskell.
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+-- | What it costs to list the binders of a pattern with
+-- 'Foil.nameBinderListOf', and the operations that go through it:
+-- 'Foil.addSubstPattern', 'Foil.unsinkNameSet' (in 'supportOf') and the
+-- default 'Foil.unifyPatterns' (in 'alphaEquiv').
+--
+-- The pattern types cover each way to get a 'Foil.CoSinkable' instance: the
+-- library's own instances (with 'Telescope'), 'mkCoSinkableFoilPattern',
+-- 'mkFreeFoil', instances written by hand and the generic default.
+--
+-- Each pattern type is measured twice. At a known type, a call can be
+-- specialised. Through 'SomePattern', the 'Foil.CoSinkable' dictionary is
+-- passed at run time, as it is in code that is polymorphic in the pattern
+-- type, such as a generic typechecker.
+module Main (main) where
+
+import           Data.Bifunctor.TH
+import           Test.Tasty.Bench
+
+import qualified Control.Monad.Foil            as Foil
+import qualified Control.Monad.Foil.Example    as Example
+import           Control.Monad.Foil.Telescope  (Telescope (..))
+import           Control.Monad.Foil.TH         (mkCoSinkableFoilPattern, mkFoilPattern)
+import           Control.Monad.Free.Foil
+import           Data.ZipMatchK.TH       (deriveZipMatchK)
+import           Generics.Kind.TH        (deriveGenericK)
+
+import           Generated               (FFBPattern (..))
+
+-- | A pattern of two binders, with every instance taken from its generic
+-- default, as a client that derives 'GenericK' gets it.
+data PairPattern (n :: Foil.S) (l :: Foil.S) where
+  PairPattern :: Foil.NameBinder n i -> Foil.NameBinder i l -> PairPattern n l
+
+deriveGenericK ''PairPattern
+instance Foil.SinkableK PairPattern
+instance Foil.HasNameBinders PairPattern
+instance Foil.CoSinkable PairPattern
+instance Foil.UnifiablePattern PairPattern
+
+-- | 'PairPattern' with 'Foil.gnameBinderListOf' for 'Foil.nameBinderListOf'.
+data GPairPattern (n :: Foil.S) (l :: Foil.S) where
+  GPairPattern :: Foil.NameBinder n i -> Foil.NameBinder i l -> GPairPattern n l
+
+deriveGenericK ''GPairPattern
+instance Foil.SinkableK GPairPattern
+instance Foil.HasNameBinders GPairPattern
+instance Foil.CoSinkable GPairPattern where
+  nameBinderListOf = Foil.gnameBinderListOf
+
+-- | A pattern of variables and pairs with the instance that
+-- 'mkCoSinkableFoilPattern' generates, as in a language generated from a BNFC grammar.
+newtype RawIdent = RawIdent String
+data RawPattern = RawPatternVar RawIdent | RawPatternPair RawPattern RawPattern
+
+mkFoilPattern ''RawIdent ''RawPattern
+mkCoSinkableFoilPattern ''RawIdent ''RawPattern
+
+-- | A pattern of two binders with 'Foil.withPattern' written by hand and no
+-- other method.
+data HandPair (n :: Foil.S) (l :: Foil.S) where
+  HandPair :: Foil.NameBinder n i -> Foil.NameBinder i l -> HandPair n l
+
+instance Foil.CoSinkable HandPair where
+  coSinkabilityProof rename (HandPair x y) cont =
+    Foil.coSinkabilityProof rename x $ \rename' x' ->
+      Foil.coSinkabilityProof rename' y $ \rename'' y' ->
+        cont rename'' (HandPair x' y')
+
+  withPattern withBinder _unit comp scope (HandPair x y) cont =
+    withBinder scope x $ \fx x' ->
+      let scope' = Foil.extendScope x' scope
+       in withBinder scope' y $ \fy y' ->
+            cont (comp fx fy) (HandPair x' y') (Foil.extendScope y' scope')
+
+-- | A copy of the pattern of "Language.LambdaPi.Impl.Foil" and its instance:
+-- wildcards, variables and pairs, with a recursive 'Foil.withPattern' and
+-- 'Foil.nameBinderListOf' written by hand.
+data LPPattern (n :: Foil.S) (l :: Foil.S) where
+  LPWildcard :: LPPattern n n
+  LPVar      :: Foil.NameBinder n l -> LPPattern n l
+  LPPair     :: LPPattern n i -> LPPattern i l -> LPPattern n l
+
+instance Foil.CoSinkable LPPattern where
+  coSinkabilityProof rename pattern cont =
+    case pattern of
+      LPWildcard -> cont rename LPWildcard
+      LPVar x ->
+        Foil.coSinkabilityProof rename x $ \rename' x' ->
+          cont rename' (LPVar x')
+      LPPair l r ->
+        Foil.coSinkabilityProof rename l $ \rename' l' ->
+          Foil.coSinkabilityProof rename' r $ \rename'' r' ->
+            cont rename'' (LPPair l' r')
+
+  withPattern withNameBinder id' combine scope pattern cont =
+    case pattern of
+      LPWildcard -> cont id' LPWildcard scope
+      LPVar x    -> withNameBinder scope x $ \f x' ->
+        cont f (LPVar x') (Foil.extendScope x' scope)
+      LPPair l r -> Foil.withPattern withNameBinder id' combine scope l $ \fl l' scope' ->
+        Foil.withPattern withNameBinder id' combine scope' r $ \fr r' scope'' ->
+          cont (combine fl fr) (LPPair l' r') scope''
+
+  nameBinderListOf pattern = go pattern Foil.NameBinderListEmpty
+    where
+      go :: LPPattern x y -> Foil.NameBinderList y z -> Foil.NameBinderList x z
+      go LPWildcard   rest = rest
+      go (LPVar x)    rest = Foil.NameBinderListCons x rest
+      go (LPPair l r) rest = go l $! go r rest
+
+-- | A telescope of @k@ steps @(x1 : \\y. y) (x2 : x1) ... (xk : x(k-1))@,
+-- with the terms of "Control.Monad.Foil.Example" for payloads.
+withTelescope
+  :: forall r. Int
+  -> (forall l. Telescope () Example.Expr Foil.VoidS l -> r)
+  -> r
+withTelescope k cont =
+  Foil.withFresh Foil.emptyScope $ \y ->
+    Foil.withFresh Foil.emptyScope $ \x ->
+      go (k - 1) (Foil.extendScope x Foil.emptyScope) (Foil.nameOf x) $ \rest ->
+        cont (TelescopeCons () (Example.LamE y (Example.VarE (Foil.nameOf y))) x rest)
+  where
+    go :: Foil.Distinct n
+       => Int -> Foil.Scope n -> Foil.Name n
+       -> (forall l. Telescope () Example.Expr n l -> r) -> r
+    go 0 _ _ cont' = cont' TelescopeEmpty
+    go j scope prev cont' = Foil.withFresh scope $ \b ->
+      go (j - 1) (Foil.extendScope b scope) (Foil.nameOf b) $ \rest ->
+        cont' (TelescopeCons () (Example.VarE (Foil.sink prev)) b rest)
+
+data LamSig scope term
+  = App term term
+  | Lam scope
+  deriving (Functor, Foldable, Traversable)
+
+deriveBifunctor ''LamSig
+deriveBifoldable ''LamSig
+deriveBitraversable ''LamSig
+deriveZipMatchK ''LamSig
+
+-- | A pattern whose 'Foil.CoSinkable' dictionary travels with it.
+data SomePattern where
+  SomePattern :: Foil.CoSinkable pattern => pattern Foil.VoidS l -> SomePattern
+
+-- | The length of a list of binders, which forces its spine.
+size :: Foil.NameBinderList n l -> Int
+size = go 0
+  where
+    go :: Int -> Foil.NameBinderList n l -> Int
+    go !acc Foil.NameBinderListEmpty         = acc
+    go !acc (Foil.NameBinderListCons _ rest) = go (acc + 1) rest
+
+-- | 'Foil.nameBinderListOf' through a dictionary. Not inlined, so that the
+-- dictionary stays unknown at the call.
+{-# NOINLINE listedSome #-}
+listedSome :: SomePattern -> Int
+listedSome (SomePattern pattern) = size (Foil.nameBinderListOf pattern)
+
+-- | 'Foil.addSubstPattern' through a dictionary.
+{-# NOINLINE substSome #-}
+substSome :: [AST PairPattern LamSig Foil.VoidS] -> SomePattern -> Bool
+substSome args (SomePattern pattern) =
+  Foil.nullSubst (Foil.addSubstPattern Foil.identitySubst pattern args)
+
+-- | A chain of λ-abstractions, each binding a pair of names, with a variable
+-- bound by the outermost one at the bottom.
+pairChain :: Int -> AST PairPattern LamSig Foil.VoidS
+pairChain depth =
+  withPair Foil.emptyScope $ \pattern x scope ->
+    Node (Lam (ScopedAST pattern (go scope x (depth - 1))))
+  where
+    go :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Int -> AST PairPattern LamSig n
+    go _scope x 0 = Var x
+    go scope x d = withPair scope $ \pattern _ scope' ->
+      Node (Lam (ScopedAST pattern (go scope' (Foil.sink x) (d - 1))))
+
+    withPair
+      :: Foil.Distinct n
+      => Foil.Scope n
+      -> (forall l. Foil.DExt n l => PairPattern n l -> Foil.Name l -> Foil.Scope l -> r)
+      -> r
+    withPair scope cont =
+      Foil.withFresh scope $ \b1 ->
+        let scope1 = Foil.extendScope b1 scope
+         in Foil.withFresh scope1 $ \b2 ->
+              cont (PairPattern b1 b2) (Foil.sink (Foil.nameOf b1)) (Foil.extendScope b2 scope1)
+
+main :: IO ()
+main =
+  Foil.withFresh Foil.emptyScope $ \b1 ->
+  Foil.withFresh (Foil.extendScope b1 Foil.emptyScope) $ \b2 ->
+  Foil.withFreshNameBinderList [(), (), (), ()] Foil.emptyScope Foil.emptyNameMap $ \_ list4 _ ->
+  withTelescope 4 $ \tele4 ->
+    let pair = PairPattern b1 b2
+        var = FoilRawPatternVar b1
+        thPair = FoilRawPatternPair (FoilRawPatternVar b1) (FoilRawPatternVar b2)
+        ffPair = FFBPatternPair (FFBPatternVar b1) (FFBPatternVar b2)
+        handPair = HandPair b1 b2
+        lpPair = LPPair (LPVar b1) (LPVar b2)
+        gpair = GPairPattern b1 b2
+        args = [Node (App t t), t]
+        t = pairChain 1
+        chain = pairChain 1000
+     in defaultMain
+          [ bgroup "nameBinderListOf"
+              [ bgroup "NameBinder"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) b1
+                  , bench "a dictionary" $ whnf listedSome (SomePattern b1)
+                  ]
+              , bgroup "TH pattern of 1"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) var
+                  , bench "a dictionary" $ whnf listedSome (SomePattern var)
+                  ]
+              , bgroup "NameBinderList of 4"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) list4
+                  , bench "a dictionary" $ whnf listedSome (SomePattern list4)
+                  ]
+              , bgroup "mkCoSinkableFoilPattern pair of 2"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) thPair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern thPair)
+                  ]
+              , bgroup "mkFreeFoil pair of 2"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) ffPair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern ffPair)
+                  ]
+              , bgroup "hand-written pair of 2"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) handPair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern handPair)
+                  ]
+              , bgroup "lambda-pi pattern, pair of 2"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) lpPair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern lpPair)
+                  ]
+              , bgroup "Telescope of 4"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) tele4
+                  , bench "a dictionary" $ whnf listedSome (SomePattern tele4)
+                  ]
+              , bgroup "generic pattern of 2"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) pair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern pair)
+                  ]
+              , bgroup "generic pattern of 2 with gnameBinderListOf"
+                  [ bench "known type"   $ whnf (size . Foil.nameBinderListOf) gpair
+                  , bench "a dictionary" $ whnf listedSome (SomePattern gpair)
+                  ]
+              ]
+          , bgroup "addSubstPattern, generic pattern of 2"
+              [ bench "known type"   $
+                  whnf (\p -> Foil.nullSubst (Foil.addSubstPattern Foil.identitySubst p args)) pair
+              , bench "a dictionary" $ whnf (substSome args) (SomePattern pair)
+              ]
+          , bgroup "1000 nested generic patterns of 2"
+              [ bench "alphaEquiv" $ whnf (alphaEquiv Foil.emptyScope chain) chain
+              , bench "supportOf"  $ whnf (Foil.nameSetSize . supportOf) chain
+              ]
+          ]
diff --git a/bench/nfdata/Main.hs b/bench/nfdata/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/nfdata/Main.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric  #-}
+{-# LANGUAGE GADTs          #-}
+
+-- | What it costs to force a term with 'rnf'.
+--
+-- Benchmarks force their results with 'rnf' (for example, through 'nf' of
+-- tasty-bench), so the 'NFData' instance of 'AST' adds to every measurement
+-- of a function that returns a term. The signature here takes the generic
+-- 'NFData' instance, as user code usually does.
+--
+-- The workload is 100 random closed λ-terms of 4 to 32 nodes (about 1,850
+-- nodes in total), comparable in size to the 100 normal forms of the
+-- @random15@ corpus of [lambda-n-ways](https://github.com/sweirich/lambda-n-ways)
+-- (Weirich's benchmark suite), and one random term of 20,000 nodes.
+module Main (main) where
+
+import           Control.DeepSeq   (NFData, force, rnf)
+import           Control.Exception (evaluate)
+import           Data.Bits         (shiftR)
+import           Data.Word         (Word64)
+import           GHC.Generics      (Generic)
+import           Test.Tasty.Bench
+
+import qualified Control.Monad.Foil      as Foil
+import           Control.Monad.Free.Foil
+
+data LamSig scope term
+  = App term term
+  | Lam scope
+  deriving (Generic, NFData)
+
+type Term = AST Foil.NameBinder LamSig
+
+-- | A λ-term with de Bruijn indices, generated first and then converted.
+data Raw = RVar Int | RApp Raw Raw | RLam Raw
+
+-- | The linear congruential generator of Knuth's MMIX.
+next :: Word64 -> Word64
+next g = g * 6364136223846793005 + 1442695040888963407
+
+-- | A number below @k@, from the high bits of the state.
+pick :: Word64 -> Int -> Int
+pick g k = fromIntegral ((g `shiftR` 33) `mod` fromIntegral k)
+
+-- | @'gen' d s g@ is a random term of @s@ nodes under @d@ binders.
+gen :: Int -> Int -> Word64 -> (Raw, Word64)
+gen d s g0
+  | s <= 1 && d > 0 = (RVar (pick g d), g)
+  | d == 0 || s == 2 || pick g 100 < 50 =
+      let (body, g') = gen (d + 1) (s - 1) g in (RLam body, g')
+  | otherwise =
+      let k = 1 + pick (next g) (s - 2)
+          (fun, g1) = gen d k (next (next g))
+          (arg, g2) = gen d (s - 1 - k) g1
+       in (RApp fun arg, g2)
+  where
+    g = next g0
+
+toTerm :: Foil.Distinct n => Foil.Scope n -> [Foil.Name n] -> Raw -> Term n
+toTerm _ names (RVar i) = Var (names !! i)
+toTerm scope names (RApp fun arg) = Node (App (toTerm scope names fun) (toTerm scope names arg))
+toTerm scope names (RLam body) = Foil.withFresh scope $ \binder ->
+  let scope' = Foil.extendScope binder scope
+   in Node (Lam (ScopedAST binder (toTerm scope' (Foil.nameOf binder : map Foil.sink names) body)))
+
+closed :: Raw -> Term Foil.VoidS
+closed = toTerm Foil.emptyScope []
+
+-- | 100 terms of 4 to 32 nodes.
+corpus :: [Raw]
+corpus = go (100 :: Int) 42
+  where
+    go 0 _ = []
+    go k g =
+      let (t, g') = gen 0 (4 + pick g 29) (next g)
+       in t : go (k - 1) g'
+
+main :: IO ()
+main = do
+  terms <- evaluate (force (map closed corpus))
+  big <- evaluate (force (closed (fst (gen 0 20000 7))))
+  defaultMain
+    [ bench "rnf, 100 small terms" $ nf (foldr (\t r -> rnf t `seq` r) ()) terms
+    , bench "rnf, one term of 20000 nodes" $ nf rnf big
+    ]
diff --git a/bench/zipmatchk/Main.hs b/bench/zipmatchk/Main.hs
--- a/bench/zipmatchk/Main.hs
+++ b/bench/zipmatchk/Main.hs
@@ -26,14 +26,21 @@
 -- across the whole signature — as a real language's terms are — should cost the
 -- generic instance more the larger the signature is. The derived instance
 -- compiles to a single @case@, and should not care.
+--
+-- The last group measures the instances for 'Sum' and 'Product' of two
+-- signatures (the data types à la carte of Swierstra), each with a derived
+-- instance.
 module Main (main) where
 
+import           Data.Bifunctor.Product  (Product (..))
+import           Data.Bifunctor.Sum      (Sum (..))
 import           Data.Bifunctor.TH
 import           Test.Tasty.Bench
 
 import qualified Control.Monad.Foil      as Foil
 import           Control.Monad.Free.Foil
 import           Data.ZipMatchK
+import           Data.ZipMatchK.Bifunctor ()
 import           Data.ZipMatchK.TH       (deriveZipMatchK)
 import           Generics.Kind.TH        (deriveGenericK)
 
@@ -81,6 +88,35 @@
 deriveBitraversable ''Sig44H
 deriveZipMatchK ''Sig44H
 
+-- * Two signatures to combine
+
+-- | Application alone.
+data AppOnly scope term = AppOnly term term
+  deriving (Functor, Foldable, Traversable)
+
+-- | λ-abstraction alone.
+newtype LamOnly scope term = LamOnly scope
+  deriving (Functor, Foldable, Traversable)
+
+-- | A tag with no children, to pair with every node of a signature.
+data Tag scope term = Tag
+  deriving (Functor, Foldable, Traversable)
+
+deriveBifunctor ''AppOnly
+deriveBifoldable ''AppOnly
+deriveBitraversable ''AppOnly
+deriveZipMatchK ''AppOnly
+
+deriveBifunctor ''LamOnly
+deriveBifoldable ''LamOnly
+deriveBitraversable ''LamOnly
+deriveZipMatchK ''LamOnly
+
+deriveBifunctor ''Tag
+deriveBifoldable ''Tag
+deriveBitraversable ''Tag
+deriveZipMatchK ''Tag
+
 -- * A large closed term
 
 -- | A closed term of the given depth: an application tree with a λ every other
@@ -123,6 +159,10 @@
           [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t44) t44
           , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u44) u44
           ]
+      , bgroup "two signatures"
+          [ bench "Sum"     $ whnf (alphaEquiv Foil.emptyScope s) s
+          , bench "Product" $ whnf (alphaEquiv Foil.emptyScope p) p
+          ]
       ]
   ]
   where
@@ -132,3 +172,5 @@
     u10 = mkTerm appSig10H lamSig10H depth
     t44 = mkTerm appSig44G lamSig44G depth
     u44 = mkTerm appSig44H lamSig44H depth
+    s = mkTerm (\_ l r -> L2 (AppOnly l r)) (R2 . LamOnly) depth
+    p = mkTerm (\d l r -> Pair (appSig2H d l r) Tag) (\scope -> Pair (lamSig2H scope) Tag) depth
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.39.1.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:           free-foil
-version:        0.5.0
+version:        0.6.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
@@ -106,9 +106,11 @@
       Control.Monad.Foil.BlocksSpec
       Control.Monad.Foil.ExampleLawsSpec
       Control.Monad.Foil.LawsSpec
+      Control.Monad.Foil.NameBinderListOfSpec
       Control.Monad.Foil.NameMapSpec
       Control.Monad.Foil.NameRangeSpec
       Control.Monad.Foil.PatternTransportSpec
+      Control.Monad.Foil.RolesSpec
       Control.Monad.Foil.SinkableSpec
       Control.Monad.Foil.TelescopeLawsSpec
       Control.Monad.Foil.UnifiablePatternSpec
@@ -116,7 +118,9 @@
       Control.Monad.Free.Foil.AlphaEquivSpec
       Control.Monad.Free.Foil.AnnotatedSpec
       Control.Monad.Free.Foil.ExampleSyntax
+      Control.Monad.Free.Foil.HoistSpec
       Control.Monad.Free.Foil.LawsSpec
+      Control.Monad.Free.Foil.NFDataSpec
       Control.Monad.Free.Foil.SupportSpec
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config
@@ -125,6 +129,7 @@
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax
       Control.Monad.Free.Foil.TH.PatternTypesSpec
+      Data.ZipMatchK.SumProductSpec
       Data.ZipMatchK.THSpec
       SpecHook
       Control.Monad.Foil.Laws
@@ -149,6 +154,7 @@
     , hspec-discover
     , kind-generics >=0.5.0 && <0.6
     , kind-generics-th
+    , should-not-typecheck >=2.1.0 && <2.2
     , template-haskell >=2.21.0.0 && <2.24
     , text >=1.2.3.1 && <2.2
   default-language: Haskell2010
@@ -160,6 +166,55 @@
       Paths_free_foil
   hs-source-dirs:
       bench/alphaequiv
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts
+  build-depends:
+      array >=0.5.3.0 && <0.6
+    , base >=4.19 && <5
+    , bifunctors >=5.5 && <5.7
+    , binary ==0.8.*
+    , bytestring >=0.11 && <0.13
+    , containers >=0.6.8 && <0.9
+    , deepseq >=1.4 && <1.6
+    , free-foil
+    , kind-generics >=0.5.0 && <0.6
+    , tasty-bench
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
+  default-language: Haskell2010
+
+benchmark binders
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Config
+      Generated
+      Paths_free_foil
+  hs-source-dirs:
+      bench/binders
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts
+  build-depends:
+      array >=0.5.3.0 && <0.6
+    , base >=4.19 && <5
+    , bifunctors >=5.5 && <5.7
+    , binary ==0.8.*
+    , bytestring >=0.11 && <0.13
+    , containers >=0.6.8 && <0.9
+    , deepseq >=1.4 && <1.6
+    , free-foil
+    , kind-generics >=0.5.0 && <0.6
+    , kind-generics-th
+    , tasty-bench
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
+  default-language: Haskell2010
+
+benchmark nfdata
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Paths_free_foil
+  hs-source-dirs:
+      bench/nfdata
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -O2 -rtsopts
   build-depends:
       array >=0.5.3.0 && <0.6
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
@@ -116,7 +116,7 @@
   withFreshNameBinderListIn,
   NameBinderList(..),
   nameBindersList,
-  nameBinderListOf,
+  gnameBinderListOf,
   fromNameBindersList,
   snocNameBinderList,
   concatNameBinderLists,
diff --git a/src/Control/Monad/Foil/Blocks.hs b/src/Control/Monad/Foil/Blocks.hs
--- a/src/Control/Monad/Foil/Blocks.hs
+++ b/src/Control/Monad/Foil/Blocks.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE RoleAnnotations     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
@@ -77,6 +78,7 @@
 --
 -- @since 0.4.0
 data ExtWithin (n :: S) (l :: S) = UnsafeExtWithin [NameRange]
+type role ExtWithin nominal nominal
 
 -- | The reservations an 'ExtWithin' is evidence about: sorted, disjoint,
 -- adjacent ranges coalesced, empty ones dropped.
@@ -345,6 +347,7 @@
 --
 -- @since 0.4.0
 data ScopeUnion (n :: S) (m :: S) (k :: S) = UnsafeScopeUnion
+type role ScopeUnion nominal nominal nominal
 
 -- | Test that a scope is precisely the union of two others, and produce the
 -- witness if so. \(O(n+m)\).
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
@@ -16,6 +16,7 @@
 {-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE QuantifiedConstraints      #-}
 {-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE RoleAnnotations            #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeFamilies               #-}
@@ -85,12 +86,17 @@
 -- @since 0.0.1
 newtype Scope (n :: S) = UnsafeScope RawScope
   deriving newtype NFData
+-- Scope indices are nominal here and in the other types below, so that
+-- 'Data.Coerce.coerce' cannot change them unless the @Unsafe@ constructors
+-- are in scope.
+type role Scope nominal
 
 -- | A name in a safe scope, indexed by a type-level scope index @n@.
 --
 -- @since 0.0.1
 newtype Name (n :: S) = UnsafeName RawName
   deriving newtype (NFData, Eq, Ord, Show)
+type role Name nominal
 
 -- | Convert 'Name' into an identifier.
 -- This may be useful for printing and debugging.
@@ -105,6 +111,7 @@
 newtype NameBinder (n :: S) (l :: S) =
   UnsafeNameBinder (Name l)
     deriving newtype (NFData, Eq, Ord, Show)
+type role NameBinder nominal nominal
 
 -- | An empty scope (without any names).
 --
@@ -209,7 +216,7 @@
 -- @since 0.1.0
 compNamesOf :: NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''
 compNamesOf (NamesOf xs) (NamesOf ys) =
-  NamesOf (coerce xs ++ ys)
+  NamesOf (unsafeCoerce xs ++ ys)
 
 -- ** Refreshing binders
 
@@ -367,7 +374,7 @@
 -- variable.
 --
 -- @since 0.0.1
-{-# INLINABLE withRefreshedPattern #-}
+{-# INLINE withRefreshedPattern #-}
 withRefreshedPattern
   :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
   => Scope o      -- ^ Ambient scope.
@@ -593,6 +600,7 @@
 -- @since 0.4.0
 newtype NameSet (n :: S) = UnsafeNameSet RawScope
   deriving newtype (NFData, Eq, Semigroup, Monoid)
+type role NameSet nominal
 
 -- | An empty set of names.
 --
@@ -660,6 +668,7 @@
 -- | The names a pattern binds.
 --
 -- @since 0.4.0
+{-# INLINABLE nameSetOfPattern #-}
 nameSetOfPattern :: CoSinkable binder => binder n l -> NameSet l
 nameSetOfPattern binder = UnsafeNameSet bound
   where
@@ -686,6 +695,7 @@
 -- an occurrence of the outer name.
 --
 -- @since 0.4.0
+{-# INLINABLE unsinkNameSet #-}
 unsinkNameSet :: CoSinkable binder => binder n l -> NameSet l -> NameSet n
 unsinkNameSet binder (UnsafeNameSet names) = UnsafeNameSet (names IntSet.\\ bound)
   where
@@ -940,6 +950,7 @@
 --
 -- @since 0.1.0
 newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet
+type role NameBinders nominal nominal
 
 -- | /Unsafely/ merge sets of binders (via set union).
 --
@@ -1088,6 +1099,8 @@
     withPattern withBinder unit comp scope (nameBindersList binders) $ \f binders' scope' ->
       cont f (fromNameBindersList binders') scope'
 
+  nameBinderListOf = nameBindersList
+
 instance CoSinkable NameBinderList where
   coSinkabilityProof rename NameBinderListEmpty cont = cont rename NameBinderListEmpty
   coSinkabilityProof rename (NameBinderListCons binder binders) cont =
@@ -1095,14 +1108,36 @@
       coSinkabilityProof rename' binders $ \rename'' binders' ->
         cont rename'' (NameBinderListCons binder' binders')
 
-  withPattern withBinder unit comp scope binders cont = case binders of
-    NameBinderListEmpty -> cont unit NameBinderListEmpty scope
-    NameBinderListCons x xs ->
-      withBinder scope x $ \f x' ->
-        let scope' = extendScope x' scope
-        in withPattern withBinder unit comp scope' xs $ \f' xs' scope'' ->
-            cont (comp f f') (NameBinderListCons x' xs') scope''
+  withPattern
+    :: forall o f n l r. Distinct o
+    => (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
+    -> NameBinderList n l
+    -> (forall o'. DExt o o' => f n l o o' -> NameBinderList o o' -> Scope o' -> r)
+    -> r
+  withPattern withBinder unit comp = go
+    where
+      -- The loop takes the three functions from its context, so that a call
+      -- with known functions specialises it when 'withPattern' inlines.
+      go
+        :: forall p i. Distinct p
+        => Scope p
+        -> NameBinderList i l
+        -> (forall p'. DExt p p' => f i l p p' -> NameBinderList p p' -> Scope p' -> r)
+        -> r
+      go scope binders cont = case binders of
+        NameBinderListEmpty -> cont unit NameBinderListEmpty scope
+        NameBinderListCons x xs ->
+          withBinder scope x $ \f x' ->
+            let scope' = extendScope x' scope
+            in go scope' xs $ \f' xs' scope'' ->
+                cont (comp f f') (NameBinderListCons x' xs') scope''
+  {-# INLINE withPattern #-}
 
+  nameBinderListOf = id
+
 -- ** Pattern combinators
 
 -- | An empty pattern type specifies zero possibilities for patterns.
@@ -1121,6 +1156,7 @@
 instance CoSinkable V2 where
   coSinkabilityProof _ v2 _ = absurd2 v2
   withPattern _ _ _ _ v2 _ = absurd2 v2
+  nameBinderListOf = absurd2
 instance UnifiablePattern V2 where
   unifyPatterns = absurd2
 
@@ -1133,6 +1169,7 @@
 instance CoSinkable U2 where
   coSinkabilityProof rename U2 cont = cont rename U2
   withPattern _withBinder unit _combine scope U2 cont = cont unit U2 scope
+  nameBinderListOf U2 = NameBinderListEmpty
 instance UnifiablePattern U2 where
   unifyPatterns U2 U2 = SameNameBinders emptyNameBinders
 
@@ -1269,6 +1306,7 @@
 -- an instance that checks the shape of two patterns first.
 --
 -- @since 0.5.0
+{-# INLINABLE unsafeUnifyPatternBinders #-}
 unsafeUnifyPatternBinders
   :: (CoSinkable pattern, Distinct n)
   => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
@@ -1670,7 +1708,30 @@
     -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> Scope o' -> r)
     -> r
   withPattern = gunsafeWithPatternViaHasNameBinders
+  -- Inlining the generic traversal lets a caller with known functions, such
+  -- as the default 'nameBinderListOf', specialise it.
+  {-# INLINE withPattern #-}
 
+  -- | Collect name binders of a generalized pattern into a name binder list,
+  -- in the order 'withPattern' visits them.
+  --
+  -- The default collects them with 'withPattern'
+  -- ('nameBinderListOfViaWithPattern'). It is cheap when the instance's
+  -- 'withPattern' inlines into it, as the generic default does and as a
+  -- non-recursive one marked @INLINE@ does. Otherwise it costs a traversal
+  -- that allocates several closures per binder, and an instance should list
+  -- its binders directly, as the instances that @mkCoSinkableFoilPattern@ and
+  -- @mkFreeFoil@ generate do. An instance with the generic 'withPattern' can
+  -- take 'gnameBinderListOf'.
+  --
+  -- This is a method of 'CoSinkable' since 0.6.0. Up to 0.5.0, it was a
+  -- function outside the class, of the same type.
+  --
+  -- @since 0.2.0
+  nameBinderListOf :: pattern n l -> NameBinderList n l
+  nameBinderListOf = nameBinderListOfViaWithPattern
+  {-# INLINE nameBinderListOf #-}
+
 -- ** Transporting a pattern's payloads
 
 -- | The renaming that carries a pattern's payloads into the ambient scope of
@@ -1796,17 +1857,20 @@
 compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) =
   WithNameBinderList (f . g)
 
--- | Collect name binders of a generalized pattern into a name binder list,
--- which can be more easily traversed.
+-- | Collect the binders of a pattern with 'withPattern'. This is the default
+-- of 'nameBinderListOf'.
 --
--- @since 0.2.0
-nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l
-nameBinderListOf pat = withPattern
+-- @since 0.6.0
+{-# INLINE nameBinderListOfViaWithPattern #-}
+nameBinderListOfViaWithPattern :: (CoSinkable binder) => binder n l -> NameBinderList n l
+nameBinderListOfViaWithPattern pat = withPattern
   (\_scope' binder k ->
     unsafeAssertFresh binder $ \binder' ->
       k (WithNameBinderList (NameBinderListCons binder)) binder')
   idWithNameBinderList
-  compWithNameBinderList
+  -- Unlike 'compWithNameBinderList', this builds the rest of the list first,
+  -- so that no binder leaves a thunk behind.
+  (\(WithNameBinderList f) (WithNameBinderList g) -> WithNameBinderList (\rest -> f $! g rest))
   emptyScope
   pat
   (\(WithNameBinderList f) _ _ -> f NameBinderListEmpty)
@@ -1815,6 +1879,8 @@
   coSinkabilityProof _rename (UnsafeNameBinder name) cont =
     cont unsafeCoerce (UnsafeNameBinder name)
 
+  nameBinderListOf binder = NameBinderListCons binder NameBinderListEmpty
+
   withPattern withBinder _ _ scope binder cont =
     withBinder scope binder $ \f binder' ->
       cont f binder' (extendScope binder' scope)
@@ -1827,6 +1893,7 @@
 -- @since 0.0.1
 newtype Substitution (e :: S -> Type) (i :: S) (o :: S) =
   UnsafeSubstitution (IntMap (e o))
+type role Substitution representational nominal nominal
 
 -- | Apply substitution to a given name.
 --
@@ -1874,6 +1941,7 @@
 -- order the pattern binds them.
 --
 -- @since 0.2.0
+{-# INLINABLE addSubstPattern #-}
 addSubstPattern
   :: CoSinkable binder
   => Substitution e i o
@@ -1923,6 +1991,7 @@
 --
 -- @since 0.0.1
 newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a } deriving (Functor, Foldable, Traversable)
+type role NameMap nominal representational
 
 -- | An empty map belongs in the empty scope.
 --
@@ -1959,6 +2028,7 @@
 -- as there are binders in the input pattern (generalized binder).
 --
 -- @since 0.2.0
+{-# INLINABLE addNameBinders #-}
 addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a
 addNameBinders pat = addNameBinderList (nameBinderListOf pat)
 
@@ -2541,6 +2611,7 @@
   -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> Scope o' -> r)
   -- ^ Continuation, accepting the result for the entire pattern, a (possibly refreshed) pattern, and the scope extended by that pattern.
   -> r
+{-# INLINE gunsafeWithPatternViaHasNameBinders #-}
 gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont =
   withPattern withBinder id_ comp_ scope (unsafeNameBinderListFromRaw raw) $ \result binders scope' ->
     cont result (gunsafeSetNameBinderList (unsafeCoerce pat) binders) scope' -- FIXME: safer version
@@ -2548,6 +2619,22 @@
     -- The binders in the order of the pattern. 'NameBinders' is a set, so
     -- going through it would put them back in ascending order of names.
     raw = ggetNameBindersRaw (fromK @_ @pattern @(n :&&: l :&&: LoT0) pat)
+
+-- | 'nameBinderListOf' through the generic representation, without a
+-- traversal by 'withPattern'. It lists the binders in the order of the
+-- generic 'withPattern' ('gunsafeWithPatternViaHasNameBinders'), so an
+-- instance that takes the generic default of 'withPattern' can use it:
+--
+-- > instance CoSinkable MyPattern where
+-- >   nameBinderListOf = gnameBinderListOf
+--
+-- @since 0.6.0
+gnameBinderListOf
+  :: forall pattern n l. (GenericK pattern, GHasNameBinders (RepK pattern))
+  => pattern n l -> NameBinderList n l
+gnameBinderListOf pat =
+  unsafeNameBinderListFromRaw (ggetNameBindersRaw (fromK @_ @pattern @(n :&&: l :&&: LoT0) pat))
+{-# INLINE gnameBinderListOf #-}
 
 -- | The binders of a pattern, in the order of the pattern, from their raw names.
 --
diff --git a/src/Control/Monad/Foil/TH/MkInstancesFoil.hs b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
--- a/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
+++ b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
@@ -3,7 +3,11 @@
 {-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 {-# OPTIONS_GHC -fno-warn-type-defaults #-}
-module Control.Monad.Foil.TH.MkInstancesFoil where
+module Control.Monad.Foil.TH.MkInstancesFoil (
+  mkInstancesFoil,
+  mkCoSinkableFoilPattern,
+  deriveCoSinkable,
+) where
 
 import           Language.Haskell.TH
 
@@ -23,7 +27,7 @@
   TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
   TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
 
-  coSinkablePatternD <- deriveCoSinkable nameT patternT
+  coSinkablePatternD <- mkCoSinkableFoilPattern nameT patternT
 
   return $
     [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))
@@ -79,20 +83,26 @@
           where
             xi = mkName ("x" ++ show i)
 
--- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.
+-- | Generate the 'Foil.CoSinkable' instance of the pattern type that
+-- 'Control.Monad.Foil.TH.MkFoilData.mkFoilPattern' generates from a raw
+-- pattern type, given the raw types of identifiers and patterns.
+-- 'deriveCoSinkable' takes the scope-safe pattern type itself.
 --
--- @since 0.1.0
-deriveCoSinkable
+-- Up to 0.5.0, this was 'deriveCoSinkable'.
+--
+-- @since 0.6.0
+mkCoSinkableFoilPattern
   :: Name -- ^ Type name for raw variable identifiers.
   -> Name -- ^ Type name for raw patterns.
   -> Q [Dec]
-deriveCoSinkable nameT patternT = do
+mkCoSinkableFoilPattern nameT patternT = do
   TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
 
   return
     [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))
         [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons)
-        , FunD 'Foil.withPattern (map clauseWithPattern patternCons) ]
+        , FunD 'Foil.withPattern (map clauseWithPattern patternCons)
+        , FunD 'Foil.nameBinderListOf (map clauseNameBinderListOf patternCons) ]
     ]
 
   where
@@ -132,6 +142,27 @@
           where
             xi = mkName ("x" ++ show i)
 
+    -- The binders of the binding fields, in order, without going through
+    -- 'Foil.withPattern'.
+    clauseNameBinderListOf :: Con -> Clause
+    clauseNameBinderListOf (NormalC conName params) =
+      Clause [ConP foilConName [] conParamPatterns] (NormalB body) []
+      where
+        foilConName = mkName ("Foil" ++ nameBase conName)
+        conParamPatterns = zipWith mkConParamPattern params [1 :: Int ..]
+        mkConParamPattern (_bang, PeelConT tyName _)
+          | tyName == nameT || tyName == patternT = VarP . xi
+        mkConParamPattern _ = const WildP
+        xi i = mkName ("x" ++ show i)
+        binding =
+          [ AppE (VarE 'Foil.nameBinderListOf) (VarE (xi i))
+          | ((_bang, PeelConT tyName _), i) <- zip params [1 :: Int ..]
+          , tyName == nameT || tyName == patternT ]
+        body = case binding of
+          [] -> ConE 'Foil.NameBinderListEmpty
+          _  -> foldr1 (\l r -> foldl AppE (VarE 'Foil.concatNameBinderLists) [l, r]) binding
+    clauseNameBinderListOf _ = error "Only normal constructors are supported here"
+
     clauseWithPattern :: Con -> Clause
     clauseWithPattern RecC{} = error "Record constructors (RecC) are not supported yet!"
     clauseWithPattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"
@@ -169,3 +200,187 @@
           go (i + 1) scope' rename' (AppE p (VarE xi)) conPatterns
           where
             xi = mkName ("x" ++ show i)
+
+-- | Generate the 'Foil.CoSinkable' instance of a scope-safe pattern type.
+-- 'mkCoSinkableFoilPattern' takes the raw pattern type instead.
+--
+-- > data Pat (n :: S) (l :: S) where
+-- >   PatVar  :: NameBinder n l -> Pat n l
+-- >   PatPair :: NameBinder n i -> NameBinder i l -> Pat n l
+-- >
+-- > deriveCoSinkable ''Pat
+--
+-- A field is a 'Foil.NameBinder', a nested pattern, or a payload that
+-- mentions no scope. A payload indexed by a scope needs a hand-written
+-- instance (see 'Foil.transportPayload').
+--
+-- @since 0.6.0
+deriveCoSinkable :: Name -> Q [Dec]
+deriveCoSinkable patternT = do
+  (tvars, cons) <- reify patternT >>= \case
+    TyConI (DataD _ _ tvs _ cs _)    -> return (tvs, cs)
+    TyConI (NewtypeD _ _ tvs _ c _)  -> return (tvs, [c])
+    _ -> fail ("deriveCoSinkable: " ++ show patternT ++ " is not a data type")
+  let params = map tvarName tvars
+  if length params < 2
+    then fail ("deriveCoSinkable: " ++ show patternT ++ " has fewer than two type parameters")
+    else do
+      fields <- concat <$> mapM (patternConFields patternT) cons
+      coSinkClauses <- mapM patternCoSinkabilityProofClause fields
+      withPatClauses <- mapM patternWithPatternClause fields
+      listClauses <- mapM patternNameBinderListOfClause fields
+      -- A pattern that nests itself has a recursive 'Foil.withPattern', which
+      -- cannot inline.
+      let recursive = or [ h == ConT patternT | (_, sorts) <- fields, PatternNested h <- sorts ]
+          inline = [ PragmaD (InlineP 'Foil.withPattern Inline FunLike AllPhases) | not recursive ]
+      return
+        [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (foldl AppT (ConT patternT) (map VarT (take (length params - 2) params))))
+            ([ FunD 'Foil.coSinkabilityProof coSinkClauses
+             , FunD 'Foil.withPattern withPatClauses
+             , FunD 'Foil.nameBinderListOf listClauses
+             ] ++ inline)
+        ]
+
+-- | How a field of a pattern constructor takes part in its instance.
+data PatternField
+  = PatternBinder        -- ^ A 'Foil.NameBinder'.
+  | PatternNested Type   -- ^ A nested pattern, with its own 'Foil.CoSinkable'; its type's head.
+  | PatternPayload       -- ^ A field that mentions no scope.
+
+-- | The constructors of a pattern type, each with the sorts of its fields.
+-- The scopes of a constructor are the last two arguments of its return type
+-- and its existential variables, such as the intermediate scope of a pair.
+patternConFields :: Name -> Con -> Q [(Name, [PatternField])]
+patternConFields patternT = go []
+  where
+    go bound = \case
+      NormalC conName _ -> fail ("deriveCoSinkable: constructor " ++ show conName
+        ++ " of " ++ show patternT ++ " is not in GADT syntax, so its scopes are unknown")
+      RecC conName _ -> go bound (NormalC conName [])
+      InfixC _ conName _ -> go bound (NormalC conName [])
+      ForallC tvs _ con -> go (bound ++ map tvarName tvs) con
+      RecGadtC conNames types retType -> go bound (GadtC conNames (map removeName types) retType)
+      GadtC conNames types retType -> do
+        let (_, args) = unApplyType retType
+            scopes = [ v | VarT v <- drop (length args - 2) args ] ++ bound
+        sorts <- mapM (fieldSort scopes . snd) types
+        return [ (conName, sorts) | conName <- conNames ]
+
+    fieldSort scopes type_ =
+      let (headT, args) = unApplyType type_
+          mentions = any (`elem` scopes) (namesOfType type_)
+          lastTwoScopes = case reverse args of
+            VarT b : VarT a : _ -> a `elem` scopes && b `elem` scopes
+            _                   -> False
+      in case headT of
+           ConT n | n == ''Foil.NameBinder -> return PatternBinder
+           _ | lastTwoScopes -> return (PatternNested headT)
+             | not mentions  -> return PatternPayload
+             | otherwise -> fail ("deriveCoSinkable: a field of type " ++ pprint type_
+                 ++ " in " ++ show patternT ++ " mentions a scope; write the instance by hand"
+                 ++ " (transportPayload is the sanctioned way to rebuild such a field)")
+
+-- | A type split into its head and arguments, without parentheses and kind
+-- signatures.
+unApplyType :: Type -> (Type, [Type])
+unApplyType = go []
+  where
+    go acc (AppT f x)   = go (x : acc) f
+    go acc (ParensT t)  = go acc t
+    go acc (SigT t _)   = go acc t
+    go acc t            = (t, acc)
+
+-- | The type variables a type mentions.
+namesOfType :: Type -> [Name]
+namesOfType = \case
+  VarT v       -> [v]
+  AppT f x     -> namesOfType f ++ namesOfType x
+  SigT t _     -> namesOfType t
+  ParensT t    -> namesOfType t
+  AppKindT t _ -> namesOfType t
+  _            -> []
+
+isBindingField :: PatternField -> Bool
+isBindingField = \case
+  PatternPayload -> False
+  _              -> True
+
+-- | One 'Foil.coSinkabilityProof' clause: the binding fields are renamed in
+-- turn, each with the renaming the previous one extended.
+patternCoSinkabilityProofClause :: (Name, [PatternField]) -> Q Clause
+patternCoSinkabilityProofClause (conName, sorts) = do
+  rename <- newName (if any isBindingField sorts then "rename" else "_rename")
+  cont <- newName "cont"
+  xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]
+  let go renameCur [] fields = return (VarE cont `AppE` VarE renameCur `AppE` foldl AppE (ConE conName) (fields []))
+      go renameCur ((PatternPayload, x) : rest) fields = go renameCur rest (fields . (VarE x :))
+      go renameCur ((_, x) : rest) fields = do
+        renameNext <- newName "rename'"
+        x' <- newName (nameBase x ++ "'")
+        body <- go renameNext rest (fields . (VarE x' :))
+        return (VarE 'Foil.coSinkabilityProof `AppE` VarE renameCur `AppE` VarE x
+                  `AppE` LamE [VarP renameNext, VarP x'] body)
+  body <- go rename (zip sorts xs) id
+  return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) [])
+
+-- | One 'Foil.withPattern' clause, in the form of
+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil': a binder field goes
+-- through @withBinder@ and extends the scope for the fields to its right, a
+-- nested pattern through its own 'Foil.withPattern', and the results compose
+-- left to right.
+patternWithPatternClause :: (Name, [PatternField]) -> Q Clause
+patternWithPatternClause (conName, sorts) = do
+  let nBinding = length (filter isBindingField sorts)
+      hasNested = any (\case PatternNested _ -> True; _ -> False) sorts
+      usedIf b n = if b then n else '_' : n
+  withBinder <- newName (usedIf (nBinding > 0) "withBinder")
+  unit_ <- newName (usedIf (nBinding == 0 || hasNested) "unit_")
+  comp_ <- newName (usedIf (nBinding >= 2 || hasNested) "comp_")
+  scope <- newName "scope"
+  cont <- newName "cont"
+  xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]
+  let go scopeCur acc [] fields =
+        return (VarE cont `AppE` maybe (VarE unit_) id acc
+                  `AppE` foldl AppE (ConE conName) (fields [])
+                  `AppE` VarE scopeCur)
+      go scopeCur acc ((PatternPayload, x) : rest) fields = go scopeCur acc rest (fields . (VarE x :))
+      go scopeCur acc ((sort_, x) : rest) fields = do
+        x' <- newName (nameBase x ++ "'")
+        f <- newName "f"
+        scopeNext <- newName "scope'"
+        let acc' = case acc of
+              Nothing -> VarE f
+              Just a  -> VarE comp_ `AppE` a `AppE` VarE f
+        body <- go scopeNext (Just acc') rest (fields . (VarE x' :))
+        return $ case sort_ of
+          PatternBinder ->
+            VarE withBinder `AppE` VarE scopeCur `AppE` VarE x
+              `AppE` LamE [VarP f, VarP x']
+                  (LetE [ValD (VarP scopeNext)
+                           (NormalB (VarE 'Foil.extendScope `AppE` VarE x' `AppE` VarE scopeCur)) []]
+                     body)
+          _ ->
+            VarE 'Foil.withPattern `AppE` VarE withBinder `AppE` VarE unit_
+              `AppE` VarE comp_ `AppE` VarE scopeCur `AppE` VarE x
+              `AppE` LamE [VarP f, VarP x', VarP scopeNext] body
+  body <- go scope Nothing (zip sorts xs) id
+  return (Clause
+    [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]
+    (NormalB body) [])
+
+-- | One 'Foil.nameBinderListOf' clause: the binding fields, left to right.
+patternNameBinderListOfClause :: (Name, [PatternField]) -> Q Clause
+patternNameBinderListOfClause (conName, sorts) = do
+  xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts]
+  let pats = [ if isBindingField s then VarP x else WildP | (s, x) <- zip sorts xs ]
+      -- A binder is consed on directly. Only a nested pattern's list is
+      -- concatenated, since 'Foil.concatNameBinderLists' is recursive and
+      -- copies its first argument.
+      list = \case
+        [] -> ConE 'Foil.NameBinderListEmpty
+        [(PatternNested _, x)] -> VarE 'Foil.nameBinderListOf `AppE` VarE x
+        (PatternNested _, x) : rest ->
+          VarE 'Foil.concatNameBinderLists `AppE` (VarE 'Foil.nameBinderListOf `AppE` VarE x) `AppE` list rest
+        (_, x) : rest -> ConE 'Foil.NameBinderListCons `AppE` VarE x `AppE` list rest
+      body = list [ (s, x) | (s, x) <- zip sorts xs, isBindingField s ]
+  return (Clause [ConP conName [] pats] (NormalB body) [])
diff --git a/src/Control/Monad/Foil/Telescope.hs b/src/Control/Monad/Foil/Telescope.hs
--- a/src/Control/Monad/Foil/Telescope.hs
+++ b/src/Control/Monad/Foil/Telescope.hs
@@ -62,6 +62,9 @@
 -- with each payload moved by the transport and the scope reached /before/ its
 -- own binder. Moving a payload may refresh its own binders, which is why the
 -- instance needs @'RelMonad' 'Name' e@.
+--
+-- 'nameBinderListOf' is 'telescopeBinders', which reads the binders off the
+-- telescope rather than rebuilding it with 'withPattern'.
 instance (Sinkable e, RelMonad Name e) => CoSinkable (Telescope label e) where
   coSinkabilityProof rename TelescopeEmpty cont = cont rename TelescopeEmpty
   coSinkabilityProof rename (TelescopeCons label payload binder rest) cont =
@@ -103,6 +106,8 @@
               (TelescopeCons label (transportPayload scope transport payload) binder' rest')
               scope''
 
+  nameBinderListOf = telescopeBinders
+
 -- | Two telescopes unify when their binders line up and their payloads agree.
 --
 -- Labels are ignored, which is what α-equivalence should do with a label: a
@@ -221,15 +226,14 @@
 
 -- | The chain of binders a telescope forms.
 --
--- This is 'nameBinderListOf' at a telescope, written out. The general one
--- goes through 'withPattern' and so rebuilds the telescope only to throw it
--- away, which is worth avoiding on the checking path.
+-- This is 'nameBinderListOf' at a telescope, as a function of its own, which
+-- needs no 'RelMonad' instance for the payloads.
 --
 -- @since 0.4.0
 telescopeBinders :: Telescope label e n l -> NameBinderList n l
 telescopeBinders TelescopeEmpty = NameBinderListEmpty
 telescopeBinders (TelescopeCons _ _ binder rest) =
-  NameBinderListCons binder (telescopeBinders rest)
+  NameBinderListCons binder $! telescopeBinders rest
 
 -- | Close a set of parameters under the parameters their payloads need.
 --
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
@@ -32,7 +32,6 @@
 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.IntMap.Strict          (IntMap)
 import qualified Data.IntMap.Strict          as IntMap
 import           Data.Map                    (Map)
@@ -46,7 +45,9 @@
 data ScopedAST binder sig n where
   ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n
 
+-- INLINABLE, so that it specialises together with the instance for AST.
 instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where
+  {-# INLINABLE rnf #-}
   rnf (ScopedAST binder body) = rnf binder `seq` rnf body
 
 -- | A term, generated by a signature 'Bifunctor' @sig@,
@@ -60,9 +61,20 @@
   Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
 
 deriving instance Generic (AST binder sig n)
-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)
 
+-- | 'rnf' forces the names, the binders, and the nodes through the 'NFData'
+-- instance of the signature. GHC specialises it where the binder and the
+-- signature are known. On the λ-terms of the @nfdata@ benchmark, the
+-- specialised 'rnf' is about four times faster than the general one.
+instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
+  => NFData (AST binder sig n) where
+  -- Without a specialisation, each node is forced through dictionaries built
+  -- from the quantified constraints. The specialised rnf calls itself on the
+  -- subterms and inlines the signature's rnf.
+  {-# INLINABLE rnf #-}
+  rnf (Var name)  = rnf name
+  rnf (Node node) = rnf node
+
 instance GenericK (ScopedAST binder sig) where
   type RepK (ScopedAST binder sig) =
     Exists Foil.S
@@ -167,6 +179,7 @@
 -- | Substitution for a single generalized pattern.
 --
 -- @since 0.2.0
+{-# INLINABLE substitutePattern #-}
 substitutePattern
   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o                           -- ^ Resulting scope.
@@ -180,6 +193,47 @@
   where
     env' = Foil.addSubstPattern env binders args
 
+-- * Transformations between signatures
+
+-- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes
+-- through the first function, a scoped subterm through the second, given its
+-- binder and the fold of its body, and a node through the third, once its
+-- subterms are folded. The scope indices stay as they are, so the carrier
+-- can be another kind of term, as in 'hoistAST', or anything indexed by the
+-- scope, such as @'Const' Int@ for a node count.
+--
+-- To change the binder type as well, map it in the second function:
+--
+-- > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node
+--
+-- @since 0.6.0
+{-# INLINABLE foldAST #-}
+foldAST
+  :: forall binder sig r s n. Bifunctor sig
+  => (forall m. Foil.Name m -> r m)             -- ^ A variable.
+  -> (forall m l. binder m l -> r l -> s m)     -- ^ A scoped subterm, from its binder and the fold of its body.
+  -> (forall m. sig (s m) (r m) -> r m)         -- ^ A node, its subterms folded.
+  -> AST binder sig n
+  -> r n
+foldAST var scoped node = go
+  where
+    go :: forall m. AST binder sig m -> r m
+    go (Var x)  = var x
+    go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t)
+
+-- | Change the signature of a term by a natural transformation of
+-- signatures, keeping the binders, as @hoistFree@ of the free package does
+-- for a free monad. Each node is rebuilt, so this costs a traversal.
+--
+-- @since 0.6.0
+{-# INLINABLE hoistAST #-}
+hoistAST
+  :: Bifunctor sig
+  => (forall a b. sig a b -> sig' a b)
+  -> AST binder sig n
+  -> AST binder sig' n
+hoistAST f = foldAST Var ScopedAST (Node . f)
+
 -- * \(\alpha\)-equivalence
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.
@@ -249,7 +303,7 @@
   -> AST binder sig n
   -> AST binder sig n
   -> Bool
-alphaEquiv _scope (Var x) (Var y) = x == coerce y
+alphaEquiv _scope (Var x) (Var y) = x == y
 alphaEquiv scope (Node l) (Node r) =
   case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of
     Nothing -> False
@@ -483,7 +537,7 @@
   => AST binder sig n
   -> AST binder sig l
   -> Bool
-unsafeEqAST (Var x) (Var y) = x == coerce y
+unsafeEqAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y
 unsafeEqAST (Node t1) (Node t2) =
   case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of
     Nothing -> False
diff --git a/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
--- a/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
+++ b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
@@ -8,20 +8,28 @@
 module Control.Monad.Free.Foil.TH.MkFreeFoil (
   FreeFoilConfig(..),
   FreeFoilTermConfig(..),
+  FreeFoilOptions(..),
+  defaultFreeFoilOptions,
   mkFreeFoil,
+  mkFreeFoilWith,
   mkFreeFoilConversions,
 ) where
 
 import           Language.Haskell.TH
 import           Language.Haskell.TH.Syntax (addModFinalizer)
 
-import           Control.Monad              (forM, forM_, when)
+import           Control.DeepSeq            (NFData (..))
+import           Control.Monad              (forM, forM_, unless, when)
 import qualified Control.Monad.Foil         as Foil
 import           Control.Monad.Foil.TH.Util
 import qualified Control.Monad.Free.Foil    as Foil
+import           Data.Bifoldable            (Bifoldable (..))
 import           Data.Bifunctor
+import           Data.Bitraversable         (Bitraversable (..))
+import           Data.ZipMatchK             (ZipMatchFoldK, ZipMatchK)
+import           Data.ZipMatchK.TH          (zipMatchFoldKInstance, zipMatchKInstance)
 import           Data.Char                  (toUpper)
-import           Data.List                  (find, unzip4, (\\), nub)
+import           Data.List                  (find, intercalate, unzip4, (\\), nub)
 import           Data.Maybe                 (fromMaybe, isJust, catMaybes, listToMaybe, mapMaybe,
                                              maybeToList)
 import Data.Map (Map)
@@ -566,6 +574,35 @@
     [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]
     (NormalB body) [])
 
+-- | One 'Foil.nameBinderListOf' clause for a generated binding constructor:
+--
+-- > nameBinderListOf (Con x1 x2 _) =
+-- >   concatNameBinderLists (nameBinderListOf x1) (nameBinderListOf x2)
+--
+-- The binder and nested-pattern fields are listed left to right, in the order
+-- in which the 'Foil.withPattern' clause of 'mkWithPatternClause' visits them,
+-- and payload fields are skipped. A constructor that binds nothing lists no
+-- binders.
+mkNameBinderListOfClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause
+mkNameBinderListOfClause config (rawConName, rawFieldTypes) = do
+  let conName = toConName config rawConName
+      sorts = map (bindingFieldSortOf config) rawFieldTypes
+  xs <- mapM (\i -> newName ("x" <> show i)) [1 .. length sorts]
+  let fieldPattern sort x
+        | isBindingFieldSort sort = VarP x
+        | otherwise               = WildP
+      -- A binder is consed on directly. Only a nested binding type's list is
+      -- concatenated, since 'Foil.concatNameBinderLists' is recursive and
+      -- copies its first argument.
+      list = \case
+        [] -> ConE 'Foil.NameBinderListEmpty
+        [(FieldPattern, x)] -> VarE 'Foil.nameBinderListOf `AppE` VarE x
+        (FieldPattern, x) : rest ->
+          VarE 'Foil.concatNameBinderLists `AppE` (VarE 'Foil.nameBinderListOf `AppE` VarE x) `AppE` list rest
+        (_, x) : rest -> ConE 'Foil.NameBinderListCons `AppE` VarE x `AppE` list rest
+      body = list [ (sort, x) | (sort, x) <- zip sorts xs, isBindingFieldSort sort ]
+  return (Clause [ConP conName [] (zipWith fieldPattern sorts xs)] (NormalB body) [])
+
 termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
 termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go
   where
@@ -909,6 +946,39 @@
       ForallC _params _ctx con -> go con
       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)
 
+-- | Options of 'mkFreeFoilWith'.
+--
+-- @since 0.6.0
+data FreeFoilOptions = FreeFoilOptions
+  { signatureInstances :: [Name]
+    -- ^ The classes whose instances every generated signature gets.
+    -- 'Bifunctor', 'Bifoldable', 'Bitraversable' and 'NFData' come with
+    -- @INLINE@ pragmas on the methods, and 'ZipMatchK' and 'ZipMatchFoldK' are
+    -- written out as "Data.ZipMatchK.TH" derives them. All six are generated
+    -- by default, since GHC does not inline the derived methods of a
+    -- signature with about ten constructors or more, and every generic
+    -- traversal of the syntax goes through them. Leave out the instances you write or derive
+    -- yourself. With @[]@, none is generated. Any other class name is
+    -- rejected by the splice, and so is 'Bitraversable' without its
+    -- superclasses. The instances of the payload types, such as identifiers
+    -- and positions, must be declared before the splice, since a later
+    -- declaration group is not visible to it.
+  , patternInstances :: [Name]
+    -- ^ The classes whose instances every generated binding type gets:
+    -- 'NFData' by default, written out. A binding type is a GADT whenever a
+    -- constructor binds two names, which rules out the 'GHC.Generics.Generic'
+    -- default. The same rules as for 'signatureInstances' apply.
+  }
+
+-- | The default options. Every instance is generated.
+--
+-- @since 0.6.0
+defaultFreeFoilOptions :: FreeFoilOptions
+defaultFreeFoilOptions = FreeFoilOptions
+  { signatureInstances = [''Bifunctor, ''Bifoldable, ''Bitraversable, ''ZipMatchK, ''ZipMatchFoldK, ''NFData]
+  , patternInstances = [''NFData]
+  }
+
 -- | Generate scope-safe types and pattern synonyms for a given raw set of types:
 --
 --  1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)
@@ -923,11 +993,20 @@
 -- pattern has the runtime representation of the field it wraps. Otherwise the
 -- pattern type is @data@.
 --
+-- Signatures are generated together with instances of 'Bitraversable',
+-- 'ZipMatchK' and 'ZipMatchFoldK'. Use 'mkFreeFoilWith' to control which instances are generated.
+--
 -- @since 0.2.0
 mkFreeFoil :: FreeFoilConfig -> Q [Dec]
-mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence
+mkFreeFoil = mkFreeFoilWith defaultFreeFoilOptions
+
+-- | 'mkFreeFoil' with options.
+--
+-- @since 0.6.0
+mkFreeFoilWith :: FreeFoilOptions -> FreeFoilConfig -> Q [Dec]
+mkFreeFoilWith FreeFoilOptions{..} config@FreeFoilConfig{..} = checkSignatureInstances >> concat <$> sequence
   [ mapM mkQuantifiedType rawQuantifiedNames
-  , mapM mkBindingType freeFoilTermConfigs
+  , concat <$> mapM mkBindingType freeFoilTermConfigs
   , concat <$> mapM mkPatternCoSinkable freeFoilTermConfigs
   , concat <$> mapM mkSignatureTypes freeFoilTermConfigs
   , concat <$> mapM mkPatternSynonyms freeFoilTermConfigs
@@ -963,7 +1042,16 @@
         ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.")
       return (DataD [] name newParams Nothing newCons [])
 
-    mkBindingType FreeFoilTermConfig{..} = do
+    -- The binding type and, unless opted out, its instances.
+    mkBindingType termConfig = do
+      dec <- mkBindingType' termConfig
+      instances <- case dec of
+        DataD _ name params _ cons _    -> mkPatternInstances patternInstances name params cons
+        NewtypeD _ name params _ con _  -> mkPatternInstances patternInstances name params [con]
+        _                               -> return []
+      return (dec : instances)
+
+    mkBindingType' FreeFoilTermConfig{..} = do
       (tvars, cons) <- reifyDataOrNewtype rawBindingName
       let bindingName = toFreeFoilName config rawBindingName
           rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)
@@ -984,7 +1072,9 @@
     -- GenericK default routes every binder operation through a generic
     -- representation traversal, which costs a measurable constant per binder
     -- at runtime (see issue #82); the concrete instance removes it, and a
-    -- client no longer declares (or hand-writes) the instance itself.
+    -- client no longer declares (or hand-writes) the instance itself. The
+    -- instance lists its binders directly in 'Foil.nameBinderListOf', since
+    -- the default would go through the recursive 'Foil.withPattern'.
     mkPatternCoSinkable FreeFoilTermConfig{..} = do
       (tvars, cons) <- reifyDataOrNewtype rawBindingName
       let bindingName = toFreeFoilName config rawBindingName
@@ -1002,10 +1092,12 @@
             _ -> return ()
       coSinkClauses <- mapM (mkCoSinkabilityProofClause config) flatCons
       withPatClauses <- mapM (mkWithPatternClause config) flatCons
+      listClauses <- mapM (mkNameBinderListOfClause config) flatCons
       return
         [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) bindingT)
             [ FunD 'Foil.coSinkabilityProof coSinkClauses
             , FunD 'Foil.withPattern withPatClauses
+            , FunD 'Foil.nameBinderListOf listClauses
             ]
         ]
 
@@ -1014,7 +1106,29 @@
       subsigs <- concat <$> mapM (mkSignatureType termConfig) (rawSubTermNames <> rawSubScopeNames)
       return (sig ++ subsigs)
 
-    mkSignatureType termConfig@FreeFoilTermConfig{..} rawName = do
+    -- The signature with its synonyms and, unless opted out, its instances.
+    mkSignatureType termConfig rawName = do
+      decs <- mkSignatureType' termConfig rawName
+      instances <- concat <$> sequence
+        [ mkSignatureInstances signatureInstances name (map tvarName (take (length params - 2) params)) scope term cons
+        | DataD _ name params _ cons _ <- decs ]
+      return (decs ++ instances)
+
+    checkSignatureInstances = do
+      let unknown = filter (`notElem` supportedSignatureInstances) signatureInstances
+      unless (null unknown) $ fail $ unlines
+        [ "mkFreeFoilWith: cannot generate instances of " <> intercalate ", " (map show unknown)
+        , "  the signature instances it generates are " <> intercalate ", " (map show supportedSignatureInstances)
+        ]
+      let unknownPat = filter (`notElem` supportedPatternInstances) patternInstances
+      unless (null unknownPat) $ fail $ unlines
+        [ "mkFreeFoilWith: cannot generate instances of " <> intercalate ", " (map show unknownPat)
+        , "  the pattern instances it generates are " <> intercalate ", " (map show supportedPatternInstances)
+        ]
+      when (''Bitraversable `elem` signatureInstances && any (`notElem` signatureInstances) [''Bifunctor, ''Bifoldable]) $
+        fail "mkFreeFoilWith: Bitraversable needs Bifunctor and Bifoldable among the signature instances"
+
+    mkSignatureType' termConfig@FreeFoilTermConfig{..} rawName = do
       (tvars, cons) <- reifyDataOrNewtype rawName
       let sigName = toSignatureName config rawName
           tvars' = map (VarT . tvarName) tvars
@@ -1057,6 +1171,211 @@
   TyConI (DataD _ctx _name tvars _kind cons _deriv) -> return (tvars, cons)
   TyConI (NewtypeD _ctx _name tvars _kind con _deriv) -> return (tvars, [con])
   _ -> error ("not a data or newtype: " ++ show name)
+
+-- * Instances of a generated signature
+
+-- | The shape of a field of a signature constructor, as far as its bifunctor
+-- instances care. It is the scoped position, the term position, a type that
+-- mentions neither, or a type constructor applied to one or two trailing
+-- arguments that do, such as a list of terms or a sub-signature applied to
+-- the scope and the term.
+data SigField
+  = SigPayload
+  | SigScope
+  | SigTerm
+  | SigInside [SigField]
+
+sigFieldShape :: Name -> Name -> Name -> Type -> Q SigField
+sigFieldShape conName scope term fieldType = go fieldType
+  where
+    mentions t = sigMentions scope t || sigMentions term t
+    go t = case sigStrip t of
+      VarT v
+        | v == scope -> return SigScope
+        | v == term  -> return SigTerm
+      t' -> do
+        let (_, args) = sigUnApply t'
+            trailing = dropWhile (not . mentions) args
+        case trailing of
+          [] -> return SigPayload
+          _ | length trailing <= 2 -> SigInside <$> mapM go trailing
+            | otherwise -> fail $ unlines
+                [ "mkFreeFoil: cannot generate the bifunctor instances of a signature:"
+                , "  constructor " <> show conName <> " has a field of type " <> pprint fieldType
+                , "  whose scope or term positions sit under a type constructor of arity above two;"
+                , "  leave the bifunctor classes out of signatureInstances (see mkFreeFoilWith)"
+                , "  and derive those instances yourself"
+                ]
+
+isSigPayload :: SigField -> Bool
+isSigPayload SigPayload = True
+isSigPayload _          = False
+
+-- | The function to apply at a field under @bimap f g@, @bifoldMap f g@ and
+-- @bitraverse f g@ respectively.
+sigMapper, sigFolder, sigTraverser :: Exp -> Exp -> SigField -> Exp
+sigMapper f g = \case
+  SigPayload       -> VarE 'id
+  SigScope         -> f
+  SigTerm          -> g
+  SigInside [a]    -> AppE (VarE 'fmap) (sigMapper f g a)
+  SigInside [a, b] -> AppE (AppE (VarE 'bimap) (sigMapper f g a)) (sigMapper f g b)
+  SigInside _      -> error "mkFreeFoil: a field of arity above two"
+sigFolder f g = \case
+  SigPayload       -> AppE (VarE 'const) (VarE 'mempty)
+  SigScope         -> f
+  SigTerm          -> g
+  SigInside [a]    -> AppE (VarE 'foldMap) (sigFolder f g a)
+  SigInside [a, b] -> AppE (AppE (VarE 'bifoldMap) (sigFolder f g a)) (sigFolder f g b)
+  SigInside _      -> error "mkFreeFoil: a field of arity above two"
+sigTraverser f g = \case
+  SigPayload       -> VarE 'pure
+  SigScope         -> f
+  SigTerm          -> g
+  SigInside [a]    -> AppE (VarE 'traverse) (sigTraverser f g a)
+  SigInside [a, b] -> AppE (AppE (VarE 'bitraverse) (sigTraverser f g a)) (sigTraverser f g b)
+  SigInside _      -> error "mkFreeFoil: a field of arity above two"
+
+-- | The constructors of a generated signature with their fields.
+sigConFields :: Con -> [(Name, [Type])]
+sigConFields = \case
+  GadtC names fields _ -> [ (n, map snd fields) | n <- names ]
+  ForallC _ _ con      -> sigConFields con
+  NormalC n fields     -> [(n, map snd fields)]
+  RecC n fields        -> [(n, [ t | (_, _, t) <- fields ])]
+  _                    -> []
+
+-- | The classes 'mkSignatureInstances' knows.
+supportedSignatureInstances :: [Name]
+supportedSignatureInstances = [''Bifunctor, ''Bifoldable, ''Bitraversable, ''ZipMatchK, ''ZipMatchFoldK, ''NFData]
+
+-- | The classes 'mkPatternInstances' knows.
+supportedPatternInstances :: [Name]
+supportedPatternInstances = [''NFData]
+
+-- | An 'NFData' instance written out: one clause per constructor, forcing
+-- every field in turn. The signatures get @INLINE@ on 'rnf', since theirs can
+-- be large and is never self-recursive (the recursive positions are the type
+-- variables); a binding type's is small and may be recursive, so it gets none.
+nfDataInstance :: Bool -> Type -> [Type] -> [(Name, [Type])] -> Q Dec
+nfDataInstance inline headT context fields = do
+  clauses <- forM fields $ \(conName, types) -> do
+    xs <- mapM (const (newName "x")) types
+    let body = case xs of
+          [] -> ConE '()
+          _  -> foldr1 (\a b -> InfixE (Just a) (VarE 'seq) (Just b)) [ AppE (VarE 'rnf) (VarE x) | x <- xs ]
+    return (Clause [ConP conName [] (map VarP xs)] (NormalB body) [])
+  return (InstanceD Nothing context (AppT (ConT ''NFData) headT)
+            ([ PragmaD (InlineP 'rnf Inline FunLike AllPhases) | inline ] ++ [FunD 'rnf clauses]))
+
+-- | The fixed type parameters a field mentions, for an instance context.
+usedParams :: [Name] -> [(Name, [Type])] -> [Name]
+usedParams params fields = [ v | v <- params, any (any (sigMentions v) . snd) fields ]
+
+-- | The requested instances of a generated binding type, out of 'NFData'.
+mkPatternInstances :: [Name] -> Name -> [TyVarBndr BndrVis] -> [Con] -> Q [Dec]
+mkPatternInstances wanted name params cons
+  | ''NFData `elem` wanted, not (null fields) = do
+      dec <- nfDataInstance False headT [ AppT (ConT ''NFData) (VarT v) | v <- usedParams fixed fields ] fields
+      return [dec]
+  | otherwise = return []
+  where
+    fields = concatMap sigConFields cons
+    names = map tvarName params
+    fixed = take (length names - 2) names
+    headT = foldl AppT (ConT name) (map VarT names)
+
+-- | The requested instances of a generated signature, out of 'Bifunctor',
+-- 'Bifoldable' and 'Bitraversable', their methods marked @INLINE@,
+-- 'ZipMatchK' and 'ZipMatchFoldK'. A signature without constructors gets none.
+mkSignatureInstances :: [Name] -> Name -> [Name] -> Name -> Name -> [Con] -> Q [Dec]
+mkSignatureInstances wanted sigName params scope term cons
+  | null fields = return []
+  | otherwise = do
+      bifunctorDecs <-
+        if any want [''Bifunctor, ''Bifoldable, ''Bitraversable]
+          then mkBifunctorInstances
+          else return []
+      zipDecs <-
+        if want ''ZipMatchK
+          then zipMatchKInstance sigName (params ++ [scope, term]) 2 fields
+          else return []
+      zipFoldDecs <-
+        if want ''ZipMatchFoldK
+          then zipMatchFoldKInstance sigName (params ++ [scope, term]) 2 fields
+          else return []
+      nfDecs <-
+        if want ''NFData
+          then (: []) <$> nfDataInstance True (AppT (AppT headT (VarT scope)) (VarT term))
+                 -- Only the positions and parameters some field mentions: a
+                 -- signature without scoped positions gets no constraint on
+                 -- @scope@, which -Wredundant-constraints would otherwise flag.
+                 [ AppT (ConT ''NFData) (VarT v) | v <- usedParams (params ++ [scope, term]) fields ] fields
+          else return []
+      return (bifunctorDecs ++ zipDecs ++ zipFoldDecs ++ nfDecs)
+  where
+    fields = concatMap sigConFields cons
+    want = (`elem` wanted)
+    headT = foldl AppT (ConT sigName) (map VarT params)
+    inline name = PragmaD (InlineP name Inline FunLike AllPhases)
+    instanceOf cls decs = InstanceD Nothing [] (AppT (ConT cls) headT) decs
+
+    mkBifunctorInstances = do
+      shapes <- forM fields $ \(conName, types) ->
+        (,) conName <$> mapM (sigFieldShape conName scope term) types
+      -- Underscored, since a constructor may use neither function.
+      f <- newName "_f"
+      g <- newName "_g"
+      let methodClause (conName, sh) mkBody = do
+            xs <- mapM (const (newName "_x")) sh
+            return (Clause [VarP f, VarP g, ConP conName [] (map VarP xs)] (NormalB (mkBody conName (zip sh xs))) [])
+          at s x = AppE s (VarE x)
+          bimapBody conName shxs = foldl AppE (ConE conName)
+            [ if isSigPayload sh then VarE x else sigMapper (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs ]
+          bifoldBody _ shxs =
+            case [ sigFolder (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs, not (isSigPayload sh) ] of
+              [] -> VarE 'mempty
+              es -> foldr1 (\a b -> InfixE (Just a) (VarE '(<>)) (Just b)) es
+          bitravBody conName shxs =
+            case [ sigTraverser (VarE f) (VarE g) sh `at` x | (sh, x) <- shxs ] of
+              []       -> AppE (VarE 'pure) (ConE conName)
+              (e : es) -> foldl (\acc e' -> InfixE (Just acc) (VarE '(<*>)) (Just e'))
+                                (InfixE (Just (ConE conName)) (VarE '(<$>)) (Just e)) es
+      bimapClauses <- mapM (`methodClause` bimapBody) shapes
+      bifoldClauses <- mapM (`methodClause` bifoldBody) shapes
+      bitravClauses <- mapM (`methodClause` bitravBody) shapes
+      return $ concat
+        [ [ instanceOf ''Bifunctor [inline 'bimap, FunD 'bimap bimapClauses] | want ''Bifunctor ]
+        , [ instanceOf ''Bifoldable [inline 'bifoldMap, FunD 'bifoldMap bifoldClauses] | want ''Bifoldable ]
+        , [ instanceOf ''Bitraversable [inline 'bitraverse, FunD 'bitraverse bitravClauses] | want ''Bitraversable ]
+        ]
+
+sigMentions :: Name -> Type -> Bool
+sigMentions v = go
+  where
+    go = \case
+      VarT u          -> u == v
+      AppT a b        -> go a || go b
+      AppKindT t _    -> go t
+      SigT t _        -> go t
+      ParensT t       -> go t
+      InfixT l _ r    -> go l || go r
+      UInfixT l _ r   -> go l || go r
+      ForallT _ _ t   -> go t
+      _               -> False
+
+sigStrip :: Type -> Type
+sigStrip (ParensT t) = sigStrip t
+sigStrip (SigT t _)  = sigStrip t
+sigStrip t           = t
+
+sigUnApply :: Type -> (Type, [Type])
+sigUnApply = go []
+  where
+    go args (AppT f x)  = go (x : args) f
+    go args (ParensT t) = go args t
+    go args (SigT t _)  = go args t
+    go args t           = (t, args)
 
 -- | Generate conversions to and from scope-safe representation:
 --
diff --git a/src/Data/ZipMatchK.hs b/src/Data/ZipMatchK.hs
--- a/src/Data/ZipMatchK.hs
+++ b/src/Data/ZipMatchK.hs
@@ -13,6 +13,9 @@
   module Data.ZipMatchK.Mappings,
   ZipMatchK(..),
   zipMatchK,
+  ZipMatchFoldK(..),
+  zipMatchAllK,
+  zipMatchAnyK,
   -- * Specializations
   -- ** Unification of plain 'Data.Kind.Type's
   zipMatchViaEq,
@@ -20,11 +23,19 @@
   -- ** Unification of 'Data.Functor.Functor's
   zipMatchWith1,
   zipMatch1,
+  zipMatchFold1,
+  zipMatchAll1,
+  zipMatchAny1,
   -- ** Unification of 'Data.Bifunctor.Bifunctor's
   zipMatchWith2,
   zipMatch2,
+  zipMatchFold2,
+  zipMatchAll2,
+  zipMatchAny2,
 ) where
 
+import           Data.Coerce (coerce)
+import           Data.Monoid (All (..), Any (..))
 import           Generics.Kind
 import Data.Bitraversable
 
@@ -92,3 +103,122 @@
 -- @since 0.3.0
 zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
 zipMatch2 = zipMatchWith2 pairA pairA
+
+-- | 'zipMatchFoldK' specialised to functors.
+--
+-- >>> zipMatchFold1 (\x y -> [x + y]) (Just 1) (Just (2 :: Int))
+-- Just [3]
+-- >>> zipMatchFold1 (\x y -> [x + y]) [1, 2] [10, 20 :: Int]
+-- Just [11,22]
+-- >>> zipMatchFold1 (\x y -> [x + y]) [1, 2] [10 :: Int]
+-- Nothing
+--
+-- @since 0.6.0
+zipMatchFold1
+  :: (ZipMatchFoldK f, Monoid m)
+  => (a -> a' -> m)
+  -> f a -> f a' -> Maybe m
+zipMatchFold1 f = zipMatchFoldK (f :%: F0)
+
+-- | 'zipMatchFoldK' specialised to bifunctors. With 'Data.Monoid.All' it
+-- checks that two nodes have the same constructor and that their components
+-- satisfy a relation, without building anything for the components:
+--
+-- >>> import Data.Monoid (All (..))
+-- >>> let same = zipMatchFold2 (\x y -> All (x == y)) (\x y -> All (x == y))
+-- >>> getAll <$> same (Left 1) (Left (1 :: Int) :: Either Int Int)
+-- Just True
+-- >>> getAll <$> same (Left 1) (Left (2 :: Int) :: Either Int Int)
+-- Just False
+-- >>> getAll <$> same (Left 1) (Right (1 :: Int) :: Either Int Int)
+-- Nothing
+--
+-- @since 0.6.0
+zipMatchFold2
+  :: (ZipMatchFoldK f, Monoid m)
+  => (a -> a' -> m)
+  -> (b -> b' -> m)
+  -> f a b -> f a' b' -> Maybe m
+zipMatchFold2 f g = zipMatchFoldK (f :%: g :%: F0)
+
+-- | Check a relation on all paired components: 'Nothing' when the shapes
+-- differ, as for 'zipMatchFoldK', and otherwise whether every component
+-- satisfies its relation. The components are checked left to right, and the
+-- check stops at the first that fails.
+--
+-- > zipMatchAllK = fmap getAll . zipMatchFoldK (coerce relations)
+--
+-- @since 0.6.0
+zipMatchAllK :: forall f as bs. ZipMatchFoldK f => Folds Bool as bs -> f :@@: as -> f :@@: bs -> Maybe Bool
+zipMatchAllK relations x y = getAll <$> zipMatchFoldK @_ @f @as @bs (coerce relations) x y
+{-# INLINE zipMatchAllK #-}
+
+-- | 'zipMatchAllK' specialised to functors.
+--
+-- >>> zipMatchAll1 (==) (Just 1) (Just (1 :: Int))
+-- Just True
+-- >>> zipMatchAll1 (==) [1, 2] [1, 3 :: Int]
+-- Just False
+-- >>> zipMatchAll1 (==) [1, 2] [1 :: Int]
+-- Nothing
+--
+-- @since 0.6.0
+zipMatchAll1 :: ZipMatchFoldK f => (a -> a' -> Bool) -> f a -> f a' -> Maybe Bool
+zipMatchAll1 f = zipMatchAllK (f :%: F0)
+{-# INLINE zipMatchAll1 #-}
+
+-- | 'zipMatchAllK' specialised to bifunctors.
+--
+-- >>> zipMatchAll2 (==) (==) (Left 1) (Left (1 :: Int) :: Either Int Int)
+-- Just True
+-- >>> zipMatchAll2 (==) (==) (Left 1) (Right (1 :: Int) :: Either Int Int)
+-- Nothing
+--
+-- @since 0.6.0
+zipMatchAll2
+  :: ZipMatchFoldK f
+  => (a -> a' -> Bool)
+  -> (b -> b' -> Bool)
+  -> f a b -> f a' b' -> Maybe Bool
+zipMatchAll2 f g = zipMatchAllK (f :%: g :%: F0)
+{-# INLINE zipMatchAll2 #-}
+
+-- | Check a relation on some paired component: 'Nothing' when the shapes
+-- differ, as for 'zipMatchFoldK', and otherwise whether some component
+-- satisfies its relation. The components are checked left to right, and the
+-- check stops at the first that succeeds.
+--
+-- > zipMatchAnyK = fmap getAny . zipMatchFoldK (coerce relations)
+--
+-- @since 0.6.0
+zipMatchAnyK :: forall f as bs. ZipMatchFoldK f => Folds Bool as bs -> f :@@: as -> f :@@: bs -> Maybe Bool
+zipMatchAnyK relations x y = getAny <$> zipMatchFoldK @_ @f @as @bs (coerce relations) x y
+{-# INLINE zipMatchAnyK #-}
+
+-- | 'zipMatchAnyK' specialised to functors.
+--
+-- >>> zipMatchAny1 (==) [1, 2] [3, 2 :: Int]
+-- Just True
+-- >>> zipMatchAny1 (==) [1, 2] [3, 4 :: Int]
+-- Just False
+-- >>> zipMatchAny1 (==) [] [1 :: Int]
+-- Nothing
+--
+-- @since 0.6.0
+zipMatchAny1 :: ZipMatchFoldK f => (a -> a' -> Bool) -> f a -> f a' -> Maybe Bool
+zipMatchAny1 f = zipMatchAnyK (f :%: F0)
+{-# INLINE zipMatchAny1 #-}
+
+-- | 'zipMatchAnyK' specialised to bifunctors.
+--
+-- >>> zipMatchAny2 (==) (==) (Right 1) (Right (2 :: Int) :: Either Int Int)
+-- Just False
+--
+-- @since 0.6.0
+zipMatchAny2
+  :: ZipMatchFoldK f
+  => (a -> a' -> Bool)
+  -> (b -> b' -> Bool)
+  -> f a b -> f a' b' -> Maybe Bool
+zipMatchAny2 f g = zipMatchAnyK (f :%: g :%: F0)
+{-# INLINE zipMatchAny2 #-}
diff --git a/src/Data/ZipMatchK/Bifunctor.hs b/src/Data/ZipMatchK/Bifunctor.hs
--- a/src/Data/ZipMatchK/Bifunctor.hs
+++ b/src/Data/ZipMatchK/Bifunctor.hs
@@ -8,13 +8,17 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
--- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+{-# LANGUAGE GADTs #-}
+-- | This module provides 'GenericK', 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and 'Product',
 -- to enable the use of 'ZipMatchK' with the data types à la carte approach.
+--
+-- The 'ZipMatchK' and 'ZipMatchFoldK' instances are written out, in the form that
+-- "Data.ZipMatchK.TH" derives, rather than taken from the generic default,
+-- which converts every node to its "Generics.Kind" representation and back.
 module Data.ZipMatchK.Bifunctor where
 
 import Data.Kind (Type)
 import Generics.Kind
-import Data.Bitraversable
 import Data.Bifunctor.Sum
 import Data.Bifunctor.Product
 
@@ -30,6 +34,27 @@
     :*: 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))
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type)) where
+  zipMatchWithK mappings@(_ :^: _ :^: M0) l r = case (l, r) of
+    (L2 x, L2 y) -> L2 <$> zipMatchWithK @_ @f mappings x y
+    (R2 x, R2 y) -> R2 <$> zipMatchWithK @_ @g mappings x y
+    _            -> Nothing
+
 -- | 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))
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type)) where
+  zipMatchWithK mappings@(_ :^: _ :^: M0) (Pair x1 x2) (Pair y1 y2) =
+    Pair <$> zipMatchWithK @_ @f mappings x1 y1 <*> zipMatchWithK @_ @g mappings x2 y2
+
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Sum f (g :: Type -> Type -> Type)) where
+  {-# INLINE zipMatchFoldK #-}
+  zipMatchFoldK folds@(_ :%: _ :%: F0) l r = case (l, r) of
+    (L2 x, L2 y) -> zipMatchFoldK @_ @f folds x y
+    (R2 x, R2 y) -> zipMatchFoldK @_ @g folds x y
+    _            -> Nothing
+
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Product f (g :: Type -> Type -> Type)) where
+  {-# INLINE zipMatchFoldK #-}
+  zipMatchFoldK folds@(_ :%: _ :%: F0) (Pair x1 x2) (Pair y1 y2) =
+    (<>) <$> zipMatchFoldK @_ @f folds x1 y1 <*> zipMatchFoldK @_ @g folds x2 y2
diff --git a/src/Data/ZipMatchK/Functor.hs b/src/Data/ZipMatchK/Functor.hs
--- a/src/Data/ZipMatchK/Functor.hs
+++ b/src/Data/ZipMatchK/Functor.hs
@@ -8,8 +8,13 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
--- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+{-# LANGUAGE GADTs #-}
+-- | This module provides 'GenericK', 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and 'Product',
 -- to enable the use of 'ZipMatchK' with the data types à la carte approach.
+--
+-- The 'ZipMatchK' and 'ZipMatchFoldK' instances are written out, in the form that
+-- "Data.ZipMatchK.TH" derives, rather than taken from the generic default,
+-- which converts every node to its "Generics.Kind" representation and back.
 module Data.ZipMatchK.Functor where
 
 import Data.Kind (Type)
@@ -28,7 +33,28 @@
     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))
+-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type)) where
+  zipMatchWithK mappings@(_ :^: M0) l r = case (l, r) of
+    (InL x, InL y) -> InL <$> zipMatchWithK @_ @f mappings x y
+    (InR x, InR y) -> InR <$> zipMatchWithK @_ @g mappings x y
+    _              -> Nothing
+
+-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type)) where
+  zipMatchWithK mappings@(_ :^: M0) (Pair x1 x2) (Pair y1 y2) =
+    Pair <$> zipMatchWithK @_ @f mappings x1 y1 <*> zipMatchWithK @_ @g mappings x2 y2
+
+-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.
+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Sum f (g :: Type -> Type)) where
+  {-# INLINE zipMatchFoldK #-}
+  zipMatchFoldK folds@(_ :%: F0) l r = case (l, r) of
+    (InL x, InL y) -> zipMatchFoldK @_ @f folds x y
+    (InR x, InR y) -> zipMatchFoldK @_ @g folds x y
+    _              -> Nothing
+
+-- | Note: instance is limited to 'Type'-kinded functors @f@ and @g@.
+instance (ZipMatchFoldK f, ZipMatchFoldK g) => ZipMatchFoldK (Product f (g :: Type -> Type)) where
+  {-# INLINE zipMatchFoldK #-}
+  zipMatchFoldK folds@(_ :%: F0) (Pair x1 x2) (Pair y1 y2) =
+    (<>) <$> zipMatchFoldK @_ @f folds x1 y1 <*> zipMatchFoldK @_ @g folds x2 y2
diff --git a/src/Data/ZipMatchK/Generic.hs b/src/Data/ZipMatchK/Generic.hs
--- a/src/Data/ZipMatchK/Generic.hs
+++ b/src/Data/ZipMatchK/Generic.hs
@@ -20,6 +20,7 @@
 
 import           Data.Kind              (Constraint, Type)
 import           Data.List.NonEmpty
+import           Data.Monoid            (Ap (..))
 import           Generics.Kind
 import           Generics.Kind.Examples ()
 import           GHC.TypeError
@@ -56,6 +57,43 @@
     => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
   zipMatchWithK = genericZipMatchWithK @f @as @bs @cs
 
+-- | Kind-polymorphic syntactic matching of two values that folds the paired
+-- components into a monoid instead of rebuilding the value.
+--
+-- 'zipMatchFoldK' answers 'Nothing' exactly when 'zipMatchWithK' with
+-- functions that always succeed would: when the constructors differ, or a
+-- component compared by its own 'ZipMatchK' differs. Otherwise it combines
+-- the folding functions applied to the paired components, left to right with
+-- '<>'. Nothing else is built, neither the matched value nor a pair per
+-- component, so a check of all components (with 'Data.Monoid.All', say)
+-- allocates nothing for the components and stops at the first one that
+-- fails.
+--
+-- The default implementation is generic, via 'Generics.Kind.RepK', with the
+-- costs described at 'ZipMatchK'. 'Data.ZipMatchK.TH.deriveZipMatchK' derives
+-- a written-out instance together with the one of 'ZipMatchK'.
+--
+-- @since 0.6.0
+class ZipMatchFoldK (f :: k) where
+  -- | Perform one level of equality testing and fold the paired components.
+  --
+  -- @since 0.6.0
+  zipMatchFoldK :: forall as bs m. Monoid m => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m
+  default zipMatchFoldK :: forall as bs m.
+    (GenericK f, GZipMatchFold (RepK f), Monoid m)
+    => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m
+  zipMatchFoldK = genericZipMatchFoldK @f @as @bs @m
+
+-- | Generic implementation of 'zipMatchFoldK'.
+--
+-- @since 0.6.0
+genericZipMatchFoldK :: forall f as bs m.
+    (GenericK f, GZipMatchFold (RepK f), Monoid m)
+    => Folds m as bs -> f :@@: as -> f :@@: bs -> Maybe m
+genericZipMatchFoldK folds x y = gzipMatchFold folds
+  (fromK @_ @f @as x)
+  (fromK @_ @f @bs y)
+
 -- | Generic implementation of 'Data.ZipMatch.zipMatchK'.
 --
 -- @since 0.2.0
@@ -89,6 +127,14 @@
 instance ZipMatchK a => ZipMatchK (Either a)
 instance ZipMatchK NonEmpty
 
+instance ZipMatchFoldK (,)
+instance ZipMatchK a => ZipMatchFoldK ((,) a)
+instance ZipMatchFoldK []
+instance ZipMatchFoldK Maybe
+instance ZipMatchFoldK Either
+instance ZipMatchK a => ZipMatchFoldK (Either a)
+instance ZipMatchFoldK NonEmpty
+
 -- | What 'gzipMatchWith' requires when the components are paired up.
 --
 -- @since 0.2.0
@@ -235,3 +281,120 @@
   :$$: '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
+
+-- | Folding matches on the "Generics.Kind" representation of a type, which is
+-- what the default 'ZipMatchFoldK' instance goes through.
+--
+-- @since 0.6.0
+class GZipMatchFold (f :: LoT k -> Type) where
+  -- | Match two representations and fold their components with the given
+  -- functions.
+  --
+  -- @since 0.6.0
+  gzipMatchFold :: Monoid m => Folds m as bs -> f as -> f bs -> Maybe m
+
+instance GZipMatchFold V1 where
+  gzipMatchFold _ _ _ = error "impossible: Generics.Kind.V1 value!"
+
+instance GZipMatchFold U1 where
+  gzipMatchFold _ U1 U1 = Just mempty
+
+instance GZipMatchFold f => GZipMatchFold (M1 i c f) where
+  gzipMatchFold g (M1 x) (M1 y) = gzipMatchFold g x y
+
+instance (GZipMatchFold f, GZipMatchFold g) => GZipMatchFold (f :+: g) where
+  gzipMatchFold g (L1 x) (L1 y) = gzipMatchFold g x y
+  gzipMatchFold g (R1 x) (R1 y) = gzipMatchFold g x y
+  gzipMatchFold _ _ _           = Nothing
+
+instance (GZipMatchFold f, GZipMatchFold g) => GZipMatchFold (f :*: g) where
+  gzipMatchFold g (x :*: y) (x' :*: y') =
+    liftA2 (<>) (gzipMatchFold g x x') (gzipMatchFold g y y')
+
+instance ZipMatchFieldsFold t => GZipMatchFold (Field t) where
+  gzipMatchFold = zipMatchFieldsFold
+
+instance GZipMatchFold f => GZipMatchFold (c :=>: f) where
+  gzipMatchFold g (SuchThat x) (SuchThat y) = gzipMatchFold g x y
+
+instance TypeError ('Text "Existentials are not supported")
+         => GZipMatchFold (Exists k f) where
+  gzipMatchFold = undefined
+
+-- | Folding matches of a single field of a constructor, by the shape of its
+-- type. A field of a type that has no zipped parameter is compared by its
+-- 'ZipMatchK' and contributes 'mempty'. A field of a type applied to zipped
+-- parameters is folded by that type's 'ZipMatchFoldK'.
+--
+-- @since 0.6.0
+class ZipMatchFieldsFold (t :: Atom d Type) where
+  -- | Match two fields and fold their contents.
+  --
+  -- @since 0.6.0
+  zipMatchFieldsFold :: Monoid m => Folds m as bs -> Field t as -> Field t bs -> Maybe m
+
+instance ApplyMappings v => ZipMatchFieldsFold (Var v) where
+  zipMatchFieldsFold g (Field x) (Field y) = Just (applyFolds @_ @v g x y)
+
+instance ZipMatchK k => ZipMatchFieldsFold (Kon k) where
+  zipMatchFieldsFold _ (Field l) (Field r) = mempty <$ zipMatchWithK @_ @k M0 l r
+
+-- The components of a nested field can fail to match (two lists of different
+-- lengths, say), so they are folded in @'Ap' 'Maybe' m@.
+instance {-# OVERLAPPING #-} (ZipMatchFieldsFold t, ZipMatchFoldK k) => ZipMatchFieldsFold (Kon k :@: t) where
+  zipMatchFieldsFold :: forall as bs m. Monoid m =>
+    Folds m as bs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe m
+  zipMatchFieldsFold g (Field l) (Field r) =
+    getAp =<< zipMatchFoldK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0)
+      ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t as) (Field rr :: Field t bs))) :%: F0) l r
+
+instance {-# OVERLAPPING #-} (ZipMatchFieldsFold t1, ZipMatchFieldsFold t2, ZipMatchFoldK k) => ZipMatchFieldsFold ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where
+  zipMatchFieldsFold :: forall as bs m. Monoid m =>
+    Folds m as bs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe m
+  zipMatchFieldsFold g (Field l) (Field r) =
+    getAp =<< zipMatchFoldK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0)
+      ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t1 as) (Field rr :: Field t1 bs)))
+        :%: ((\ll rr -> Ap (zipMatchFieldsFold g (Field ll :: Field t2 as) (Field rr :: Field t2 bs)))
+        :%: F0)) 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))
+  => ZipMatchFieldsFold (Kon (k :: kk -> Type) :@: t) where
+  zipMatchFieldsFold = 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))
+  => ZipMatchFieldsFold ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where
+  zipMatchFieldsFold = undefined
+
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "Atom :@: is not supported by ZipMatchFieldsFold is a general form:"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (f :@: t)
+  :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))
+  => ZipMatchFieldsFold ((f :: Atom d (k1 -> Type)) :@: t) where
+  zipMatchFieldsFold = undefined
+
+instance TypeError
+  ('Text "Atom ForAll is not supported by ZipMatchFieldsFold"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (ForAll a)) => ZipMatchFieldsFold (ForAll a) where
+  zipMatchFieldsFold = undefined
+instance TypeError
+  ('Text "Atom :=>>: is not supported by ZipMatchFieldsFold"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (c :=>>: a)) => ZipMatchFieldsFold (c :=>>: a) where
+  zipMatchFieldsFold = undefined
+instance TypeError
+  ('Text "Atom Eval is not supported by ZipMatchFieldsFold"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (Eval a)) => ZipMatchFieldsFold (Eval a) where
+  zipMatchFieldsFold = undefined
diff --git a/src/Data/ZipMatchK/Mappings.hs b/src/Data/ZipMatchK/Mappings.hs
--- a/src/Data/ZipMatchK/Mappings.hs
+++ b/src/Data/ZipMatchK/Mappings.hs
@@ -35,6 +35,20 @@
         -> Mappings as bs cs      -- ^ Zipping for other type parameters.
         -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
 
+infixr 5 :%:
+type Folds :: Type -> LoT k -> LoT k -> Type
+-- | A collection of folding functions for 'Data.ZipMatchK.zipMatchFoldK',
+-- one per type parameter, each combining two components into a monoid.
+--
+-- @since 0.6.0
+data Folds m (as :: LoT k) (bs :: LoT k) where
+  -- | An empty collection (when there are no (more) type parameters).
+  F0 :: Folds m LoT0 LoT0
+  -- | A non-empty collection (when there is at least one type parameter).
+  (:%:) :: (a -> b -> m)          -- ^ Folding for the first type parameter.
+        -> Folds m as bs          -- ^ Folding for other type parameters.
+        -> Folds m (a :&&: as) (b :&&: bs)
+
 -- | Type parameter lists that can be paired up componentwise.
 --
 -- @since 0.2.0
@@ -63,11 +77,22 @@
     -> Interpret (Var v) bs   -- ^ Second collection of values (one per type parameter).
     -> Maybe (Interpret (Var v) cs)
 
+  -- | Apply a collection of folding functions to collections of values.
+  --
+  -- @since 0.6.0
+  applyFolds :: forall m (as :: LoT d) (bs :: LoT d).
+       Folds m as bs          -- ^ A collection of folding 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).
+    -> m
+
 instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
   applyMappings (f :^: _) x y = f x y
+  applyFolds (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
+  applyFolds (_ :%: fs) x y = applyFolds @_ @v fs x y
 
 -- | Pair two values in a context.
 --
diff --git a/src/Data/ZipMatchK/TH.hs b/src/Data/ZipMatchK/TH.hs
--- a/src/Data/ZipMatchK/TH.hs
+++ b/src/Data/ZipMatchK/TH.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE LambdaCase      #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ViewPatterns    #-}
--- | Template Haskell derivation of 'ZipMatchK' instances.
+-- | Template Haskell derivation of 'ZipMatchK' and 'ZipMatchFoldK' instances.
 --
 -- The generic instance (the one obtained by writing @instance ZipMatchK TermSig@
 -- with no body) converts a node into its "Generics.Kind" representation on
@@ -35,6 +35,8 @@
   deriveZipMatchK1,
   deriveZipMatchK2,
   deriveZipMatchKWith,
+  zipMatchKInstance,
+  zipMatchFoldKInstance,
 ) where
 
 import           Data.List             (foldl')
@@ -42,10 +44,12 @@
 import           Language.Haskell.TH
 
 import           Control.Monad.Foil.TH.Util (removeName, tvarName)
-import           Data.ZipMatchK.Generic    (ZipMatchK (..))
-import           Data.ZipMatchK.Mappings   (Mappings (..))
+import           Data.Monoid               (Ap (..))
+import           Data.ZipMatchK.Generic    (ZipMatchFoldK (..), ZipMatchK (..))
+import           Data.ZipMatchK.Mappings   (Folds (..), Mappings (..))
 
--- | Derive a 'ZipMatchK' instance, zipping /all/ type parameters.
+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances, zipping /all/ type
+-- parameters.
 --
 -- For a signature bifunctor
 --
@@ -59,6 +63,12 @@
 -- >     (AppSig l1 l2, AppSig r1 r2) -> AppSig <$> g l1 r1 <*> g l2 r2
 -- >     (LamSig l1, LamSig r1)       -> LamSig <$> f l1 r1
 -- >     _                            -> Nothing
+-- >
+-- > instance ZipMatchFoldK TermSig where
+-- >   zipMatchFoldK (f :%: g :%: F0) x y = case (x, y) of
+-- >     (AppSig l1 l2, AppSig r1 r2) -> Just (g l1 r1 <> g l2 r2)
+-- >     (LamSig l1, LamSig r1)       -> Just (f l1 r1)
+-- >     _                            -> Nothing
 --
 -- Use 'deriveZipMatchK2' when the type has extra parameters that should stay
 -- fixed (an annotation, say), as a signature generated by
@@ -68,15 +78,16 @@
 deriveZipMatchK :: Name -> Q [Dec]
 deriveZipMatchK = deriveZipMatchKWith Nothing
 
--- | Derive a 'ZipMatchK' instance for a functor, zipping the last type parameter
--- and fixing the rest.
+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances for a functor, zipping
+-- the last type parameter and fixing the rest.
 --
 -- @since 0.3.2
 deriveZipMatchK1 :: Name -> Q [Dec]
 deriveZipMatchK1 = deriveZipMatchKWith (Just 1)
 
--- | Derive a 'ZipMatchK' instance for a signature bifunctor, zipping the last two
--- type parameters (the scoped terms and the terms) and fixing the rest.
+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances for a signature
+-- bifunctor, zipping the last two type parameters (the scoped terms and the
+-- terms) and fixing the rest.
 --
 -- For a signature with an extra parameter (a source position, for instance)
 --
@@ -95,8 +106,8 @@
 deriveZipMatchK2 :: Name -> Q [Dec]
 deriveZipMatchK2 = deriveZipMatchKWith (Just 2)
 
--- | Derive a 'ZipMatchK' instance, zipping the last @n@ type parameters and
--- fixing the rest. 'Nothing' zips all of them.
+-- | Derive the 'ZipMatchK' and 'ZipMatchFoldK' instances, zipping the last @n@
+-- type parameters and fixing the rest. 'Nothing' zips all of them.
 --
 -- Every fixed parameter that occurs in a field gets a 'ZipMatchK' constraint in
 -- the instance context.
@@ -113,32 +124,184 @@
     then fail (show typeName ++ " has " ++ show (length params)
                 ++ " type parameter(s), cannot zip the last " ++ show n)
     else do
-      let (fixed, zipped) = splitAt (length params - n) params
-          zippedSet = Set.fromList zipped
+      let zippedSet = Set.fromList (drop (length params - n) params)
+      fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons
+      (++) <$> zipMatchKInstance typeName params n fieldsOf
+           <*> zipMatchFoldKInstance typeName params n fieldsOf
 
-      -- One zipping function per zipped parameter, in order.
-      mappingVars <- mapM (const (newName "_f")) zipped
-      let mappings = zip zipped (map VarE mappingVars)
-          mappingsPat = foldr (\v p -> InfixP (VarP v) '(:^:) p) (ConP 'M0 [] []) mappingVars
+-- | The 'ZipMatchK' instance of a data type, given its name, its type
+-- parameters in order, how many of the last ones are zipped, and the fields
+-- of each constructor in terms of those parameters. This is what
+-- 'deriveZipMatchKWith' generates after reifying the type. It is for code
+-- that declares the type in the same splice, such as
+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil', which cannot reify it.
+--
+-- @since 0.6.0
+zipMatchKInstance :: Name -> [Name] -> Int -> [(Name, [Type])] -> Q [Dec]
+zipMatchKInstance typeName params n fieldsOf = do
+  let (fixed, zipped) = splitAt (length params - n) params
+      zippedSet = Set.fromList zipped
 
-      fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons
-      clauses <- mapM (conClause zippedSet mappings) fieldsOf
-      let fallthrough
-            | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]
-            | otherwise           = []
+  -- One zipping function per zipped parameter, in order.
+  mappingVars <- mapM (const (newName "_f")) zipped
+  let mappings = zip zipped (map VarE mappingVars)
+      mappingsPat = foldr (\v p -> InfixP (VarP v) '(:^:) p) (ConP 'M0 [] []) mappingVars
 
-      x <- newName "x"
-      y <- newName "y"
-      let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)
-          impl = FunD 'zipMatchWithK
-            [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []]
+  clauses <- mapM (conClause zippedSet mappings) fieldsOf
+  let fallthrough
+        | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]
+        | otherwise           = []
 
-          headType = foldl' AppT (ConT typeName) (map VarT fixed)
-          usedVars = foldMap (foldMap freeVarsOfType . snd) fieldsOf
-          context = [ AppT (ConT ''ZipMatchK) (VarT v)
-                    | v <- fixed, v `Set.member` usedVars ]
+  x <- newName "x"
+  y <- newName "y"
+  let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)
+      impl = FunD 'zipMatchWithK
+        [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []]
 
-      return [InstanceD Nothing context (AppT (ConT ''ZipMatchK) headType) [impl]]
+      headType = foldl' AppT (ConT typeName) (map VarT fixed)
+      usedVars = foldMap (foldMap freeVarsOfType . snd) fieldsOf
+      context = [ AppT (ConT ''ZipMatchK) (VarT v)
+                | v <- fixed, v `Set.member` usedVars ]
+
+  return [InstanceD Nothing context (AppT (ConT ''ZipMatchK) headType) [impl]]
+
+-- | The 'ZipMatchFoldK' instance of a data type, from the same arguments as
+-- 'zipMatchKInstance'. A field of a zipped parameter contributes the result of
+-- its folding function, a field of a type applied to zipped parameters is
+-- folded by that type's 'ZipMatchFoldK', and any other field is compared by
+-- its 'ZipMatchK' and contributes nothing. The contributions are combined with
+-- '<>', nested to the right, so that a lazy monoid such as 'Data.Monoid.All'
+-- stops at the first field that fails. The method is @INLINE@, so that at a
+-- call site with a known monoid and known folding functions the match
+-- compiles to a @case@ on the two values with the functions applied in place.
+--
+-- @since 0.6.0
+zipMatchFoldKInstance :: Name -> [Name] -> Int -> [(Name, [Type])] -> Q [Dec]
+zipMatchFoldKInstance typeName params n fieldsOf = do
+  let (fixed, zipped) = splitAt (length params - n) params
+      zippedSet = Set.fromList zipped
+
+  -- One folding function per zipped parameter, in order.
+  foldVars <- mapM (const (newName "_f")) zipped
+  let folds = zip zipped (map VarE foldVars)
+      foldsPat = foldr (\v p -> InfixP (VarP v) '(:%:) p) (ConP 'F0 [] []) foldVars
+
+  clauses <- mapM (foldConClause zippedSet folds) fieldsOf
+  let fallthrough
+        | length fieldsOf > 1 = [Match WildP (NormalB (ConE 'Nothing)) []]
+        | otherwise           = []
+
+  x <- newName "x"
+  y <- newName "y"
+  let body = CaseE (TupE [Just (VarE x), Just (VarE y)]) (clauses ++ fallthrough)
+      impl = FunD 'zipMatchFoldK
+        [Clause [foldsPat, VarP x, VarP y] (NormalB body) []]
+
+      headType = foldl' AppT (ConT typeName) (map VarT fixed)
+      types = concatMap snd fieldsOf
+      needsZipMatchK = foldMap (zipMatchKVars zippedSet) types
+      needsZipMatchFoldK = foldMap (zipMatchFoldKVars zippedSet) types
+      context = [ AppT (ConT ''ZipMatchK) (VarT v) | v <- fixed, v `Set.member` needsZipMatchK ]
+             ++ [ AppT (ConT ''ZipMatchFoldK) (VarT v) | v <- fixed, v `Set.member` needsZipMatchFoldK ]
+
+  return [InstanceD Nothing context (AppT (ConT ''ZipMatchFoldK) headType)
+            [PragmaD (InlineP 'zipMatchFoldK Inline FunLike AllPhases), impl]]
+
+-- | How a field takes part in a folding match.
+data FieldFolder
+  = Total Exp    -- ^ @l -> r -> m@: a zipped parameter.
+  | Partial Exp  -- ^ @l -> r -> Maybe m@: a type applied to zipped parameters.
+  | Check Exp    -- ^ @l -> r -> Maybe c@: a type without zipped parameters.
+
+-- | Compile a field type into a 'FieldFolder', as 'fieldZipper' does for
+-- 'zipMatchWithK'. The components of a nested type can fail to match, so when
+-- one of them does, all of them are folded in @'Ap' 'Maybe' m@.
+fieldFolder :: Set.Set Name -> [(Name, Exp)] -> Type -> Q FieldFolder
+fieldFolder zipped folds type_ = case stripType type_ of
+  VarT v | Just f <- lookup v folds -> return (Total f)
+  t | not (mentionsZipped zipped t) -> return (Check (AppE (VarE 'zipMatchWithK) (ConE 'M0)))
+    | otherwise -> do
+        let (_headType, args) = unApply t
+            zippedArgs = dropWhile (not . mentionsZipped zipped) args
+        argFolders <- mapM (fieldFolder zipped folds) zippedArgs
+        let list = foldr (\e m -> InfixE (Just e) (ConE '(:%:)) (Just m)) (ConE 'F0)
+            total = [ e | Total e <- argFolders ]
+        if length total == length argFolders
+          then return (Partial (AppE (VarE 'zipMatchFoldK) (list total)))
+          else do
+            wrapped <- mapM inAp argFolders
+            l <- newName "l"
+            r <- newName "r"
+            let call = AppE (AppE (AppE (VarE 'zipMatchFoldK) (list wrapped)) (VarE l)) (VarE r)
+            return (Partial (LamE [VarP l, VarP r]
+                      (InfixE (Just (VarE 'getAp)) (VarE '(=<<)) (Just call))))
+  where
+    -- A folding function into @'Ap' 'Maybe' m@.
+    inAp folder = do
+      a <- newName "a"
+      b <- newName "b"
+      let applied e = AppE (AppE e (VarE a)) (VarE b)
+          ap e = LamE [VarP a, VarP b] (AppE (ConE 'Ap) e)
+      return $ case folder of
+        Total e   -> ap (AppE (ConE 'Just) (applied e))
+        Partial e -> ap (applied e)
+        Check e   -> ap (InfixE (Just (VarE 'mempty)) (VarE '(<$)) (Just (applied e)))
+
+-- | One @case@ alternative of 'zipMatchFoldK', matching a constructor with
+-- itself: the fields that can fail are matched first, then the contributions
+-- are combined.
+foldConClause :: Set.Set Name -> [(Name, Exp)] -> (Name, [Type]) -> Q Match
+foldConClause zipped folds (conName, types) = do
+  lvars <- mapM (const (newName "l")) types
+  rvars <- mapM (const (newName "r")) types
+  folders <- mapM (fieldFolder zipped folds) types
+  steps <- sequence
+    [ case folder of
+        Total f   -> return (Nothing, Just (AppE (AppE f (VarE l)) (VarE r)))
+        Partial f -> do
+          m <- newName "m"
+          return (Just (AppE (AppE f (VarE l)) (VarE r), VarP m), Just (VarE m))
+        Check f   ->
+          return (Just (AppE (AppE f (VarE l)) (VarE r), WildP), Nothing)
+    | (folder, (l, r)) <- zip folders (zip lvars rvars) ]
+  let contributions = [ e | (_, Just e) <- steps ]
+      combined = case contributions of
+        [] -> VarE 'mempty
+        _  -> foldr1 (\a b -> InfixE (Just a) (VarE '(<>)) (Just b)) contributions
+      matchJust (scrutinee, pat) rest =
+        CaseE scrutinee
+          [ Match (ConP 'Nothing [] []) (NormalB (ConE 'Nothing)) []
+          , Match (ConP 'Just [] [pat]) (NormalB rest) [] ]
+      body = foldr matchJust (AppE (ConE 'Just) combined) [ c | (Just c, _) <- steps ]
+  return (Match
+            (TupP [ ConP conName [] (map VarP lvars)
+                  , ConP conName [] (map VarP rvars) ])
+            (NormalB body) [])
+
+-- | The fixed type parameters whose 'ZipMatchK' instance folding a field of
+-- this type needs: those of a type without zipped parameters, and the fixed
+-- arguments of a type applied to zipped ones.
+zipMatchKVars :: Set.Set Name -> Type -> Set.Set Name
+zipMatchKVars zipped type_ = case stripType type_ of
+  VarT v | v `Set.member` zipped -> Set.empty
+  t | not (mentionsZipped zipped t) -> freeVarsOfType t
+    | otherwise ->
+        let (_headType, args) = unApply t
+            (fixedArgs, zippedArgs) = break (mentionsZipped zipped) args
+        in foldMap freeVarsOfType fixedArgs <> foldMap (zipMatchKVars zipped) zippedArgs
+
+-- | The fixed type parameters whose 'ZipMatchFoldK' instance folding a field of
+-- this type needs: a parameter applied to zipped ones.
+zipMatchFoldKVars :: Set.Set Name -> Type -> Set.Set Name
+zipMatchFoldKVars zipped type_ = case stripType type_ of
+  t | not (mentionsZipped zipped t) -> Set.empty
+    | otherwise ->
+        let (headType, args) = unApply t
+            zippedArgs = dropWhile (not . mentionsZipped zipped) args
+            here = case stripType headType of
+              VarT v | null (takeWhile (not . mentionsZipped zipped) args) -> Set.singleton v
+              _ -> Set.empty
+        in here <> foldMap (zipMatchFoldKVars zipped) zippedArgs
 
 -- | The type parameters and constructors of a @data@ or @newtype@ declaration.
 reifyDataType :: Name -> Q ([TyVarBndr BndrVis], [Con])
diff --git a/test/Control/Monad/Foil/NameBinderListOfSpec.hs b/test/Control/Monad/Foil/NameBinderListOfSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/Foil/NameBinderListOfSpec.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeFamilies        #-}
+-- The raw types below only serve Template Haskell.
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+-- | The laws of 'Foil.CoSinkable', with the agreement of
+-- 'Foil.nameBinderListOf' and 'Foil.withPattern', for the ways to get an
+-- instance that no other suite covers: 'mkCoSinkableFoilPattern',
+-- 'deriveCoSinkable' and the generic defaults of this package. The
+-- pattern types consist of wildcards, variables and pairs, so that the
+-- binders of a pattern come from fields at different depths. One more pattern
+-- type binds two names in one constructor, next to a payload.
+module Control.Monad.Foil.NameBinderListOfSpec (spec) where
+
+import           Test.Hspec
+import           Test.QuickCheck
+
+import qualified Control.Monad.Foil      as Foil
+-- 'mkCoSinkableFoilPattern' binds a variable named @rename@.
+import           Control.Monad.Foil.Laws hiding (rename)
+import           Control.Monad.Foil.TH   (deriveCoSinkable, mkCoSinkableFoilPattern, mkFoilPattern)
+import           Generics.Kind.TH        (deriveGenericK)
+
+-- | A raw pattern, from which 'mkFoilPattern' and 'mkCoSinkableFoilPattern' generate
+-- 'FoilRawPattern' and its instance, which lists its binders directly.
+newtype RawIdent = RawIdent String
+data RawPattern
+  = RawPatternWild
+  | RawPatternVar RawIdent
+  | RawPatternPair RawPattern RawPattern
+
+mkFoilPattern ''RawIdent ''RawPattern
+mkCoSinkableFoilPattern ''RawIdent ''RawPattern
+
+-- | A scope-safe pattern whose instance 'deriveCoSinkable' generates.
+data DerivedPattern (n :: Foil.S) (l :: Foil.S) where
+  DerivedPatternWild :: DerivedPattern n n
+  DerivedPatternVar  :: Foil.NameBinder n l -> DerivedPattern n l
+  DerivedPatternPair :: DerivedPattern n i -> DerivedPattern i l -> DerivedPattern n l
+
+deriveCoSinkable ''DerivedPattern
+
+-- | A scope-safe pattern that binds two names in one constructor, next to a
+-- payload, as a pattern for a pair or a recursor might.
+data TwoPattern (n :: Foil.S) (l :: Foil.S) where
+  TwoPatternVar  :: Foil.NameBinder n l -> TwoPattern n l
+  TwoPatternPair :: Int -> Foil.NameBinder n i -> Foil.NameBinder i l -> TwoPattern n l
+
+deriveCoSinkable ''TwoPattern
+
+-- | A pattern whose instances are the generic defaults.
+data GenericPattern (n :: Foil.S) (l :: Foil.S) where
+  GenericPatternWild :: GenericPattern n n
+  GenericPatternVar  :: Foil.NameBinder n l -> GenericPattern n l
+  GenericPatternPair :: GenericPattern n i -> GenericPattern i l -> GenericPattern n l
+
+deriveGenericK ''GenericPattern
+instance Foil.SinkableK GenericPattern
+instance Foil.HasNameBinders GenericPattern
+instance Foil.CoSinkable GenericPattern
+
+spec :: Spec
+spec = do
+  describe "a pattern from mkCoSinkableFoilPattern" $
+    coSinkableSpec rawPatternNames genRawPattern extensionByCoercion
+  describe "a pattern from deriveCoSinkable" $
+    coSinkableSpec derivedPatternNames genDerivedPattern extensionByCoercion
+  describe "a pattern with two binders and a payload, from deriveCoSinkable" $
+    coSinkableSpec twoPatternNames genTwoPattern extensionByCoercion
+  describe "a pattern with the generic defaults" $ do
+    coSinkableSpec genericPatternNames genGenericPattern extensionByCoercion
+    it "gnameBinderListOf lists the binders in the order of withPattern" $
+      forAllShow (genPatternCase genGenericPattern Inclusions) (showPatternCase genericPatternNames) $
+        \(PatternCase _ p) ->
+          nameBinderListNames (Foil.gnameBinderListOf p) === patternRawNames p
+
+-- | The shape of a pattern: where the wildcards, variables and pairs are. This
+-- follows the generators of "Control.Monad.Free.Foil.TH.PatternTypesSpec".
+data Shape = Wildcard | Variable | Pair Shape Shape
+
+-- | A shape of nesting depth at most @d@.
+genShape :: Int -> Gen Shape
+genShape d = frequency $
+  [ (1, pure Wildcard), (3, pure Variable) ] ++
+  [ (2, Pair <$> genShape (d - 1) <*> genShape (d - 1)) | d > 0 ]
+
+-- | A pattern of a random shape, built with the given constructors.
+genShaped
+  :: forall p. Foil.CoSinkable p
+  => (forall n. p n n)
+  -> (forall n l. Foil.NameBinder n l -> p n l)
+  -> (forall n i l. p n i -> p i l -> p n l)
+  -> GenPattern p
+genShaped wild var pair ctx = withCtx ctx $ \scope -> do
+  shape <- genShape 2
+  go shape scope
+  where
+    go :: Foil.Distinct m => Shape -> Foil.Scope m -> Gen (PatIn p m)
+    go shape scope = case shape of
+      Wildcard -> pure (PatIn wild)
+      Variable -> withHintedBinder scope (pure . PatIn . var)
+      Pair left right -> do
+        PatIn l <- go left scope
+        PatIn r <- go right (Foil.extendScopePattern l scope)
+        pure (PatIn (pair l r))
+
+rawPatternNames :: PatternNames FoilRawPattern
+rawPatternNames = \case
+  FoilRawPatternWild     -> []
+  FoilRawPatternVar b    -> [Foil.nameId (Foil.nameOf b)]
+  FoilRawPatternPair l r -> rawPatternNames l ++ rawPatternNames r
+
+genRawPattern :: GenPattern FoilRawPattern
+genRawPattern = genShaped FoilRawPatternWild FoilRawPatternVar FoilRawPatternPair
+
+genericPatternNames :: PatternNames GenericPattern
+genericPatternNames = \case
+  GenericPatternWild     -> []
+  GenericPatternVar b    -> [Foil.nameId (Foil.nameOf b)]
+  GenericPatternPair l r -> genericPatternNames l ++ genericPatternNames r
+
+genGenericPattern :: GenPattern GenericPattern
+genGenericPattern = genShaped GenericPatternWild GenericPatternVar GenericPatternPair
+
+derivedPatternNames :: PatternNames DerivedPattern
+derivedPatternNames = \case
+  DerivedPatternWild     -> []
+  DerivedPatternVar b    -> [Foil.nameId (Foil.nameOf b)]
+  DerivedPatternPair l r -> derivedPatternNames l ++ derivedPatternNames r
+
+genDerivedPattern :: GenPattern DerivedPattern
+genDerivedPattern = genShaped DerivedPatternWild DerivedPatternVar DerivedPatternPair
+
+twoPatternNames :: PatternNames TwoPattern
+twoPatternNames = \case
+  TwoPatternVar b      -> [Foil.nameId (Foil.nameOf b)]
+  TwoPatternPair _ x y -> [Foil.nameId (Foil.nameOf x), Foil.nameId (Foil.nameOf y)]
+
+genTwoPattern :: GenPattern TwoPattern
+genTwoPattern ctx = withCtx ctx $ \scope -> oneof
+  [ withHintedBinder scope (pure . PatIn . TwoPatternVar)
+  , withHintedBinder scope $ \x ->
+      withHintedBinder (Foil.extendScope x scope) $ \y -> do
+        k <- arbitrary
+        pure (PatIn (TwoPatternPair k x y))
+  ]
diff --git a/test/Control/Monad/Foil/RolesSpec.hs b/test/Control/Monad/Foil/RolesSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/Foil/RolesSpec.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}
+
+-- | The scope indices of the foil's types are nominal, so 'coerce' cannot
+-- change them, while 'sink' and coercions that keep the scope still work.
+--
+-- The rejected coercions are checked with 'shouldNotTypecheck' from the
+-- @should-not-typecheck@ package, which needs this module to be compiled
+-- with @-fdefer-type-errors@. The module imports only the public modules,
+-- where the @Unsafe@ constructors are not in scope: with them, 'coerce'
+-- would still unwrap the newtypes and succeed.
+module Control.Monad.Foil.RolesSpec (spec) where
+
+import           Data.Coerce               (coerce)
+import           Data.Foldable             (toList)
+import           Data.Monoid               (Sum (..))
+import           Test.Hspec
+import           Test.ShouldNotTypecheck   (shouldNotTypecheck)
+
+import           Control.Monad.Foil
+import           Control.Monad.Foil.Blocks
+
+-- * Coercions that change a scope index (none of these typecheck)
+
+-- | A name moves to an unrelated scope.
+anyName :: Name n -> Name l
+anyName = coerce
+
+-- | A name of the inner scope escapes its binder.
+escapeName :: NameBinder n l -> Name l -> Name n
+escapeName _ = coerce
+
+binderOuter :: NameBinder n l -> NameBinder n' l
+binderOuter = coerce
+
+binderInner :: NameBinder n l -> NameBinder n l'
+binderInner = coerce
+
+anyScope :: Scope n -> Scope l
+anyScope = coerce
+
+anyNameSet :: NameSet n -> NameSet l
+anyNameSet = coerce
+
+substDomain :: Substitution e i o -> Substitution e i' o
+substDomain = coerce
+
+nameBindersOuter :: NameBinders n l -> NameBinders n' l
+nameBindersOuter = coerce
+
+nameBindersInner :: NameBinders n l -> NameBinders n l'
+nameBindersInner = coerce
+
+anyNameMap :: NameMap n a -> NameMap l a
+anyNameMap = coerce
+
+extWithinOuter :: ExtWithin n l -> ExtWithin n' l
+extWithinOuter = coerce
+
+extWithinInner :: ExtWithin n l -> ExtWithin n l'
+extWithinInner = coerce
+
+blockOuter :: Block c l -> Block c' l
+blockOuter = coerce
+
+blockInner :: Block c l -> Block c l'
+blockInner = coerce
+
+scopeUnionLeft :: ScopeUnion n m k -> ScopeUnion n' m k
+scopeUnionLeft = coerce
+
+scopeUnionRight :: ScopeUnion n m k -> ScopeUnion n m' k
+scopeUnionRight = coerce
+
+scopeUnionWhole :: ScopeUnion n m k -> ScopeUnion n m k'
+scopeUnionWhole = coerce
+
+-- | The value does not typecheck. Weak head normal form is enough to raise
+-- the deferred type error of a 'coerce', and not every type here has an
+-- 'Control.DeepSeq.NFData' instance, so the value is forced with 'seq'.
+rejected :: a -> Expectation
+rejected x = shouldNotTypecheck (x `seq` ())
+
+-- * Coercions that keep the scope (these typecheck)
+
+-- | A user newtype over names, as a generated single-binder pattern is.
+newtype Var n = Var (Name n)
+
+toVar :: Name n -> Var n
+toVar = coerce
+
+valuesAsSum :: NameMap n Int -> NameMap n (Sum Int)
+valuesAsSum = coerce
+
+-- | 'sink', with the target scope pinned by a binder the caller holds.
+sunkVia :: (Sinkable e, DExt n l) => NameBinder n l -> e n -> e l
+sunkVia _ = sink
+
+sunk1Via :: (Functor f, Sinkable e, DExt n l) => NameBinder n l -> f (e n) -> f (e l)
+sunk1Via _ = sink1
+
+spec :: Spec
+spec = do
+  describe "coerce cannot change a scope index" $ do
+    it "of a Name" $
+      withFresh emptyScope $ \x -> rejected (nameId (anyName (nameOf x)))
+    it "of a Name bound by a NameBinder (escaping the binder)" $
+      withFresh emptyScope $ \x -> rejected (nameId (escapeName x (nameOf x)))
+    it "of a NameBinder (the outer scope)" $
+      withFresh emptyScope $ \x -> rejected (nameId (nameOf (binderOuter x)))
+    it "of a NameBinder (the inner scope)" $
+      withFresh emptyScope $ \x -> rejected (nameId (nameOf (binderInner x)))
+    it "of a Scope" $
+      rejected (anyScope emptyScope)
+    it "of a NameSet" $
+      withFresh emptyScope $ \x -> rejected (anyNameSet (nameSetSingleton (nameOf x)))
+    it "of a Substitution (the domain)" $
+      rejected (substDomain (voidSubst :: Substitution Name VoidS VoidS))
+    it "of NameBinders (the outer scope)" $
+      rejected (nameBindersOuter (emptyNameBinders :: NameBinders VoidS VoidS))
+    it "of NameBinders (the inner scope)" $
+      rejected (nameBindersInner (emptyNameBinders :: NameBinders VoidS VoidS))
+    it "of a NameMap" $
+      rejected (anyNameMap (emptyNameMap :: NameMap VoidS Char))
+    it "of ExtWithin (the outer scope)" $
+      rejected (extWithinOuter (extWithinRefl (NameRange 0 9) :: ExtWithin VoidS VoidS))
+    it "of ExtWithin (the inner scope)" $
+      rejected (extWithinInner (extWithinRefl (NameRange 0 9) :: ExtWithin VoidS VoidS))
+    it "of a Block (the outer scope)" $
+      rejected (blockOuter (beginBlock (NameRange 0 9) :: Block VoidS VoidS))
+    it "of a Block (the inner scope)" $
+      rejected (blockInner (beginBlock (NameRange 0 9) :: Block VoidS VoidS))
+    it "of a ScopeUnion (each of the three scopes)" $
+      case checkScopeUnion emptyScope emptyScope emptyScope of
+        Nothing -> expectationFailure "the empty scope is the union of two empty scopes"
+        Just u -> do
+          rejected (scopeUnionLeft u)
+          rejected (scopeUnionRight u)
+          rejected (scopeUnionWhole u)
+
+  describe "scope changes that remain possible" $ do
+    it "sink moves a name to an extended scope" $
+      withFresh emptyScope $ \x ->
+        withFresh (extendScope x emptyScope) $ \y ->
+          nameId (sunkVia y (nameOf x)) `shouldBe` nameId (nameOf x)
+    it "sink1 moves a list of names to an extended scope" $
+      withFresh emptyScope $ \x ->
+        withFresh (extendScope x emptyScope) $ \y ->
+          map nameId (sunk1Via y [nameOf x]) `shouldBe` [nameId (nameOf x)]
+    it "coerce wraps a name in a user newtype, keeping its scope" $
+      withFresh emptyScope $ \x ->
+        case toVar (nameOf x) of
+          Var x' -> nameId x' `shouldBe` nameId (nameOf x)
+    it "coerce changes the values of a NameMap, keeping its scope" $
+      withFresh emptyScope $ \x ->
+        map getSum (toList (valuesAsSum (addNameBinder x 1 emptyNameMap))) `shouldBe` [1]
diff --git a/test/Control/Monad/Free/Foil/HoistSpec.hs b/test/Control/Monad/Free/Foil/HoistSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/Free/Foil/HoistSpec.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+-- | 'foldAST' and 'hoistAST' on the untyped λ-calculus of
+-- "Control.Monad.Free.Foil.Example". The identity transformations are
+-- identities, a round trip through a sum of signatures is one, and a fold
+-- into a node count counts.
+module Control.Monad.Free.Foil.HoistSpec (spec) where
+
+import           Data.Bifunctor.Sum              (Sum (..))
+import           Test.Hspec
+
+import           Control.Monad.Foil              (NameBinder, S (..))
+import           Control.Monad.Free.Foil
+import           Control.Monad.Free.Foil.Example
+
+-- | The terms under test: Church numerals and their applications.
+terms :: [(String, Expr VoidS)]
+terms =
+  [ ("church " ++ show n, churchN n) | n <- [0 .. 6 :: Int] ] ++
+  [ ("church 2 applied to church 3", AppE (churchN 2) (churchN 3))
+  , ("church 3 normalised", nf' (AppE (churchN 2) (churchN 3)))
+  ]
+
+-- | A node count, indexed by the scope so that it can be the carrier of
+-- 'foldAST'.
+newtype Count (n :: S) = Count { getCount :: Int }
+
+-- | The number of variables and nodes of a term, through 'foldAST'.
+sizeOf :: Expr n -> Int
+sizeOf = getCount . foldAST (const (Count 1)) (\_ body -> Count (getCount body)) node
+  where
+    node :: ExprF (Count m) (Count m) -> Count m
+    node = \case
+      AppF f x -> Count (1 + getCount f + getCount x)
+      LamF b   -> Count (1 + getCount b)
+
+spec :: Spec
+spec = do
+  describe "hoistAST" $ do
+    it "is the identity on the identity transformation" $
+      mapM_ (\(name, t) -> (name, show (hoistAST id t)) `shouldBe` (name, show t)) terms
+    it "round-trips through a sum of signatures" $
+      let there = hoistAST L2 :: Expr n -> AST NameBinder (Sum ExprF ExprF) n
+          back  = hoistAST (\case L2 x -> x; R2 x -> x)
+      in mapM_ (\(name, t) -> (name, show (back (there t))) `shouldBe` (name, show t)) terms
+  describe "foldAST" $ do
+    it "rebuilds a term with the constructors" $
+      mapM_ (\(name, t) -> (name, show (foldAST Var ScopedAST Node t)) `shouldBe` (name, show t)) terms
+    it "counts the nodes of a Church numeral" $
+      mapM_ (\n -> (n, sizeOf (churchN n)) `shouldBe` (n, 2 * n + 3)) [0 .. 6 :: Int]
diff --git a/test/Control/Monad/Free/Foil/NFDataSpec.hs b/test/Control/Monad/Free/Foil/NFDataSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/Free/Foil/NFDataSpec.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric  #-}
+-- | 'rnf' of a term forces every field of every node, also the fields that
+-- hold no subterms, which a traversal of the signature as a 'Bifoldable'
+-- would skip.
+module Control.Monad.Free.Foil.NFDataSpec (spec) where
+
+import           Control.DeepSeq   (NFData, rnf)
+import           Control.Exception (evaluate)
+import           GHC.Generics      (Generic)
+import           Test.Hspec
+
+import qualified Control.Monad.Foil      as Foil
+import           Control.Monad.Free.Foil
+
+-- | λ-terms with integer literals.
+data LitSig scope term
+  = AppSig term term
+  | LamSig scope
+  | LitSig Int
+  deriving (Generic, NFData)
+
+type Term = AST Foil.NameBinder LitSig
+
+-- | @λx. x lit@.
+applyToLit :: Int -> Term Foil.VoidS
+applyToLit n = Foil.withFresh Foil.emptyScope $ \binder ->
+  Node (LamSig (ScopedAST binder (Node (AppSig (Var (Foil.nameOf binder)) (Node (LitSig n))))))
+
+spec :: Spec
+spec = describe "rnf of AST" $ do
+  it "forces a term" $
+    evaluate (rnf (applyToLit 1)) `shouldReturn` ()
+  it "forces a field of the signature under a binder" $
+    evaluate (rnf (applyToLit (error "the literal"))) `shouldThrow` errorCall "the literal"
diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs
--- a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs
+++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs
@@ -12,6 +12,12 @@
 
 import qualified Control.Monad.Foil                               as Foil
 import qualified Data.Map                                         as Map
+import           Control.DeepSeq                                  (rnf)
+import           Data.Bifoldable                                  (bifoldMap)
+import           Data.Bifunctor                                   (bimap)
+import           Data.Bitraversable                               (bitraverse)
+import           Data.Monoid                                      (Sum (..))
+import           Data.ZipMatchK                                   (Mappings (..), ZipMatchK (..))
 import           Test.Hspec
 
 import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config
@@ -34,6 +40,19 @@
 
 spec :: Spec
 spec = do
+  describe "the generated instances of the signature" $ do
+    it "map the term and the scoped positions apart" $
+      bimap (+ 1) (* 2) (LetSig (10 :: Int) (3 :: Int)) `shouldBe` LetSig 20 4
+    it "fold over both positions" $
+      getSum (bifoldMap (const (Sum 1)) (const (Sum 10)) (LetSig () ())) `shouldBe` (11 :: Int)
+    it "traverse both positions" $
+      bitraverse Just Just (AppSig 'a' 'b' :: TermSig () Char) `shouldBe` Just (AppSig 'a' 'b')
+    it "force a term and its patterns" $
+      rnf (toTerm Foil.emptyScope Map.empty (Let (PatternVar x) identity (ScopedTerm (Var x)))) `shouldBe` ()
+    it "match equal constructors and reject different ones" $ do
+      zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22)
+      zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing
+
   describe "a pattern adjacent to its scope (Fun)" $
     it "round-trips, and the body still refers to the binder" $
       case roundtrip (Fun (PatternVar x) (ScopedTerm (Var x))) of
@@ -71,3 +90,6 @@
   where
     isFun Fun{} = True
     isFun _     = False
+
+zipAdd :: Int -> Int -> Maybe Int
+zipAdd a b = Just (a + b)
diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs
--- a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs
+++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/PatternsSyntax.hs
@@ -21,8 +21,6 @@
 import           Control.Monad.Free.Foil.Binary                          ()
 import           Control.Monad.Free.Foil.Binary.TH                       (deriveBinaryPattern)
 import           Control.Monad.Free.Foil.TH.MkFreeFoil
-import           Data.Bifunctor.TH
-import           Data.ZipMatchK
 import           Generics.Kind.TH                                         (deriveGenericK)
 
 import           Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsConfig
@@ -46,19 +44,5 @@
 instance Foil.HasNameBinders FFNPattern
 instance Foil.UnifiablePattern FFNPattern
 deriveBinaryPattern ''FFNPattern
-
-deriveBifunctor ''MTermSig
-deriveBifoldable ''MTermSig
-deriveBitraversable ''MTermSig
-deriveGenericK ''MTermSig
-instance ZipMatchK MTermSig
-
-deriveBifunctor ''ATermSig
-deriveBifoldable ''ATermSig
-deriveBitraversable ''ATermSig
-
-deriveBifunctor ''NTermSig
-deriveBifoldable ''NTermSig
-deriveBitraversable ''NTermSig
 
 mkFreeFoilConversions conversionsConfig
diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs
--- a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs
+++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE DeriveGeneric     #-}
 {-# LANGUAGE DeriveTraversable #-}
@@ -29,7 +31,6 @@
 import           Control.Monad.Free.Foil.Binary          ()
 import           Control.Monad.Free.Foil.Binary.TH       (deriveBinaryPattern)
 import           Control.Monad.Free.Foil.TH.MkFreeFoil
-import           Data.Bifunctor.TH
 import           Data.ZipMatchK
 import           Generics.Kind.TH                                (deriveGenericK)
 
@@ -44,12 +45,10 @@
 instance Foil.UnifiablePattern FFPattern
 deriveBinaryPattern ''FFPattern
 
-deriveBifunctor ''TermSig
-deriveBifoldable ''TermSig
-deriveBitraversable ''TermSig
-
-deriveGenericK ''TermSig
 instance ZipMatchK VarIdent where zipMatchWithK = zipMatchViaEq
-instance ZipMatchK TermSig
 
 mkFreeFoilConversions config
+
+-- For the tests of the generated instances.
+deriving instance (Eq scope, Eq term) => Eq (TermSig scope term)
+deriving instance (Show scope, Show term) => Show (TermSig scope term)
diff --git a/test/Data/ZipMatchK/SumProductSpec.hs b/test/Data/ZipMatchK/SumProductSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/ZipMatchK/SumProductSpec.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE TypeFamilies      #-}
+{-# LANGUAGE TypeOperators     #-}
+
+-- | The written-out 'ZipMatchK' and 'ZipMatchFoldK' instances for 'Sum' and
+-- 'Product' must agree with the generic ones, which 'genericZipMatchWithK' and
+-- 'genericZipMatchFoldK' still compute from the 'Generics.Kind.GenericK'
+-- instances. As in "Data.ZipMatchK.THSpec", the test
+-- compares the two on every pair of a set of sample values.
+module Data.ZipMatchK.SumProductSpec (spec) where
+
+import qualified Data.Bifunctor.Product   as Bi
+import qualified Data.Bifunctor.Sum       as Bi
+import qualified Data.Functor.Product     as F
+import qualified Data.Functor.Sum         as F
+import           Generics.Kind            (LoT (..))
+import           Test.Hspec
+
+import           Data.ZipMatchK
+import           Data.ZipMatchK.Bifunctor ()
+import           Data.ZipMatchK.Functor   ()
+import           Data.ZipMatchK.Generic   (genericZipMatchFoldK, genericZipMatchWithK)
+import           Data.ZipMatchK.TH
+
+-- | A signature bifunctor.
+data LamSig scope term = App term term | Lam scope
+  deriving (Functor, Foldable, Traversable, Eq, Show)
+
+deriveZipMatchK ''LamSig
+
+-- | A functor.
+newtype Boxed term = Boxed [term]
+  deriving (Functor, Foldable, Traversable, Eq, Show)
+
+deriveZipMatchK1 ''Boxed
+
+-- | Zip two values by equality, so that the result has the same type as the
+-- inputs and can be compared with '=='.
+zipEq :: Eq a => a -> a -> Maybe a
+zipEq x y
+  | x == y    = Just x
+  | otherwise = Nothing
+
+lamSamples :: [LamSig String String]
+lamSamples = [App "x" "y", App "x" "x", Lam "s", Lam "t"]
+
+boxedSamples :: [Boxed String]
+boxedSamples = [Boxed [], Boxed ["x"], Boxed ["x", "y"]]
+
+spec :: Spec
+spec = do
+  describe "Data.Bifunctor.Sum" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @(Bi.Sum LamSig LamSig) mappings2 x y
+            `shouldBe` genericZipMatchWithK @(Bi.Sum LamSig LamSig) mappings2 x y
+        | let samples = map Bi.L2 lamSamples ++ map Bi.R2 lamSamples
+        , x <- samples, y <- samples ]
+
+  describe "Data.Bifunctor.Product" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @(Bi.Product LamSig LamSig) mappings2 x y
+            `shouldBe` genericZipMatchWithK @(Bi.Product LamSig LamSig) mappings2 x y
+        | let samples = [Bi.Pair a b | a <- lamSamples, b <- lamSamples]
+        , x <- samples, y <- samples ]
+
+  describe "Data.Functor.Sum" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @(F.Sum Boxed Boxed) (zipEq :^: M0) x y
+            `shouldBe` genericZipMatchWithK @(F.Sum Boxed Boxed) (zipEq :^: M0) x y
+        | let samples = map F.InL boxedSamples ++ map F.InR boxedSamples
+        , x <- samples, y <- samples ]
+
+  describe "Data.Functor.Product" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @(F.Product Boxed Boxed) (zipEq :^: M0) x y
+            `shouldBe` genericZipMatchWithK @(F.Product Boxed Boxed) (zipEq :^: M0) x y
+        | let samples = [F.Pair a b | a <- boxedSamples, b <- boxedSamples]
+        , x <- samples, y <- samples ]
+
+  describe "Data.Bifunctor.Sum, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @(Bi.Sum LamSig LamSig) folds2 x y
+            `shouldBe` genericZipMatchFoldK @(Bi.Sum LamSig LamSig) folds2 x y
+        | let samples = map Bi.L2 lamSamples ++ map Bi.R2 lamSamples
+        , x <- samples, y <- samples ]
+
+  describe "Data.Bifunctor.Product, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @(Bi.Product LamSig LamSig) folds2 x y
+            `shouldBe` genericZipMatchFoldK @(Bi.Product LamSig LamSig) folds2 x y
+        | let samples = [Bi.Pair a b | a <- lamSamples, b <- lamSamples]
+        , x <- samples, y <- samples ]
+
+  describe "Data.Functor.Sum, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @(F.Sum Boxed Boxed) (collect "t" :%: F0) x y
+            `shouldBe` genericZipMatchFoldK @(F.Sum Boxed Boxed) (collect "t" :%: F0) x y
+        | let samples = map F.InL boxedSamples ++ map F.InR boxedSamples
+        , x <- samples, y <- samples ]
+
+  describe "Data.Functor.Product, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @(F.Product Boxed Boxed) (collect "t" :%: F0) x y
+            `shouldBe` genericZipMatchFoldK @(F.Product Boxed Boxed) (collect "t" :%: F0) x y
+        | let samples = [F.Pair a b | a <- boxedSamples, b <- boxedSamples]
+        , x <- samples, y <- samples ]
+  where
+    mappings2 :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
+    mappings2 = zipEq :^: zipEq :^: M0
+
+    folds2 :: Folds [String] (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
+    folds2 = collect "s" :%: collect "t" :%: F0
+
+    -- The two components, tagged with the position they come from.
+    collect :: String -> String -> String -> [String]
+    collect tag x y = [tag ++ ":" ++ x ++ "/" ++ y]
diff --git a/test/Data/ZipMatchK/THSpec.hs b/test/Data/ZipMatchK/THSpec.hs
--- a/test/Data/ZipMatchK/THSpec.hs
+++ b/test/Data/ZipMatchK/THSpec.hs
@@ -11,12 +11,15 @@
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE UndecidableInstances  #-}
 
--- | The derived 'ZipMatchK' instance must agree with the generic one.
+-- | The derived 'ZipMatchK' and 'ZipMatchFoldK' instances must agree with the
+-- generic ones.
 --
 -- Both are available for the same type: 'deriveZipMatchK' provides the
--- instance, and 'genericZipMatchWithK' computes the generic answer without
--- needing one. So the test compares the two, on every pair of a set of sample
--- values, over the field shapes a signature actually uses.
+-- instances, and 'genericZipMatchWithK' and 'genericZipMatchFoldK' compute the
+-- generic answers without needing them. So the test compares the two, on every
+-- pair of a set of sample values, over the field shapes a signature actually
+-- uses. The folds collect the components they meet, so the comparison also
+-- checks the order in which they are combined.
 module Data.ZipMatchK.THSpec (spec) where
 
 import           Data.List.NonEmpty      (NonEmpty (..))
@@ -26,7 +29,8 @@
 import           Test.Hspec
 
 import           Data.ZipMatchK
-import           Data.ZipMatchK.Generic  (genericZipMatchWithK)
+import           Data.Maybe              (isJust)
+import           Data.ZipMatchK.Generic  (genericZipMatchFoldK, genericZipMatchWithK)
 import           Data.ZipMatchK.TH
 
 -- | An annotation, standing for the extra parameter a generated signature has.
@@ -127,6 +131,43 @@
         [ zipMatchWithK @_ @Boxed (zipEq :^: M0) x y
             `shouldBe` genericZipMatchWithK @Boxed (zipEq :^: M0) x y
         | x <- boxedSamples, y <- boxedSamples ]
+
+  describe "deriveZipMatchK2, ZipMatchFoldK" $ do
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @(RichSig Ann) folds x y
+            `shouldBe` genericZipMatchFoldK @(RichSig Ann) folds x y
+        | x <- richSamples, y <- richSamples ]
+    it "fails exactly where zipMatchWithK fails" $
+      sequence_
+        [ isJust (zipMatchFoldK @_ @(RichSig Ann) folds x y)
+            `shouldBe` isJust (zipMatchWithK @_ @(RichSig Ann) keep x y)
+        | x <- richSamples, y <- richSamples ]
+
+  describe "deriveZipMatchK, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @LamSig folds x y
+            `shouldBe` genericZipMatchFoldK @LamSig folds x y
+        | x <- lamSamples, y <- lamSamples ]
+
+  describe "deriveZipMatchK1, ZipMatchFoldK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchFoldK @_ @Boxed (collect "t" :%: F0) x y
+            `shouldBe` genericZipMatchFoldK @Boxed (collect "t" :%: F0) x y
+        | x <- boxedSamples, y <- boxedSamples ]
   where
     mappings :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
     mappings = zipEq :^: zipEq :^: M0
+
+    -- Functions that always succeed, so that only the shapes can fail.
+    keep :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
+    keep = (\x _ -> Just x) :^: (\x _ -> Just x) :^: M0
+
+    folds :: Folds [String] (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
+    folds = collect "s" :%: collect "t" :%: F0
+
+    -- The two components, tagged with the position they come from.
+    collect :: String -> String -> String -> [String]
+    collect tag x y = [tag ++ ":" ++ x ++ "/" ++ y]
diff --git a/test/laws/Control/Monad/Foil/Laws.hs b/test/laws/Control/Monad/Foil/Laws.hs
--- a/test/laws/Control/Monad/Foil/Laws.hs
+++ b/test/laws/Control/Monad/Foil/Laws.hs
@@ -75,6 +75,7 @@
   -- * Laws of 'CoSinkable'
   PatternCase (..),
   genPatternCase,
+  showPatternCase,
   CoSinkableLaws (..),
   coSinkableLaws,
   CoSinkLaw (..),
@@ -242,10 +243,21 @@
   NameBinderListCons b rest -> nameId (nameOf b) : nameBinderListNames rest
 
 -- | The raw names a pattern binds, in the order in which 'withPattern'
--- visits them (through 'nameBinderListOf').
+-- visits them.
 patternRawNames :: CoSinkable p => p n l -> [Int]
-patternRawNames = nameBinderListNames . nameBinderListOf
+patternRawNames pat = withPattern
+  (\scope binder k -> withFresh scope $ \binder' ->
+      k (RawNames (nameId (nameOf binder) :)) binder')
+  (RawNames id)
+  (\(RawNames f) (RawNames g) -> RawNames (f . g))
+  emptyScope
+  pat
+  (\(RawNames f) _ _ -> f [])
 
+-- | A difference list of raw names, indexed like the results of
+-- 'withPattern'.
+newtype RawNames (n :: S) (l :: S) (o :: S) (o' :: S) = RawNames ([Int] -> [Int])
+
 -- | Show the names a pattern binds, in the library's order.
 showPattern :: CoSinkable p => p n l -> String
 showPattern = showPatternWith patternRawNames
@@ -526,7 +538,7 @@
 -- order of 'withPattern'.
 data CoSinkLaw
   = CoSinkIdentity | CoSinkComposition | CoSinkExtension | CoSinkBinders
-  | WithPatternOrder
+  | WithPatternOrder | NameBinderListOfOrder
   deriving (Eq, Show, Enum, Bounded)
 
 -- | 'withPattern' visits the binders of a pattern in the order of its
@@ -537,8 +549,16 @@
   counterexample "the order of the pattern is on the left, the order of withPattern on the right" $
     binders p === patternRawNames p
 
+-- | 'nameBinderListOf' lists the binders of a pattern in the order in which
+-- 'withPattern' visits them, as its default does.
+nameBinderListOfLaw :: CoSinkable p => p n l -> Property
+nameBinderListOfLaw p =
+  counterexample "nameBinderListOf on the left, the order of withPattern on the right" $
+    nameBinderListNames (nameBinderListOf p) === patternRawNames p
+
 -- | All laws of 'coSinkabilityProof' for a pattern type, along each class
--- of renamings, and the law of the traversal order of 'withPattern'.
+-- of renamings, the law of the traversal order of 'withPattern', and the
+-- agreement of 'nameBinderListOf' with it.
 coSinkableSpec
   :: CoSinkable p
   => PatternNames p -> GenPattern p -> (RenamingClass -> CoSinkLaw -> Verdict) -> Spec
@@ -546,6 +566,9 @@
   law (verdict Inclusions WithPatternOrder) "withPattern visits binders in the order of the pattern" $
     forAllShow (genPatternCase genPat Inclusions) (showPatternCase binders) $
       \(PatternCase _ p) -> withPatternOrderLaw binders p
+  law (verdict Inclusions NameBinderListOfOrder) "nameBinderListOf lists the binders in the order of withPattern" $
+    forAllShow (genPatternCase genPat Inclusions) (showPatternCase binders) $
+      \(PatternCase _ p) -> nameBinderListOfLaw p
   forM_ allRenamingClasses $ \cls -> describe ("along " <> show cls) $
     forM_ [CoSinkIdentity, CoSinkComposition, CoSinkExtension, CoSinkBinders] $ \name ->
       law (verdict cls name) (show name) $
@@ -557,6 +580,7 @@
     lawOf CoSinkExtension   = coSinkExtension laws
     lawOf CoSinkBinders     = coSinkBinders laws
     lawOf WithPatternOrder  = \(PatternCase _ p) -> withPatternOrderLaw binders p
+    lawOf NameBinderListOfOrder = \(PatternCase _ p) -> nameBinderListOfLaw p
 
 -- * Laws of 'UnifiablePattern'