diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,31 @@
 # CHANGELOG for `free-foil`
 
+# 0.3.2 — 2026-07-15
+
+An additive release: the annotation layer, the `ZipMatchK` derivers, and a set of performance improvements. Upgrading from 0.3.1 needs no work.
+
+New:
+
+- `Control.Monad.Free.Foil.Annotated`, a layer that annotates every node with an `ann term` built from the node's own term ([#42](https://github.com/fizruk/free-foil/pull/42), [#46](https://github.com/fizruk/free-foil/pull/46)). `Bifoldable` skips the annotation, so `alphaEquiv` is annotation-blind; `freeVarsOfAnnotated` sees the variables inside annotations that `freeVarsOf` skips. `AnnSig`'s `ZipMatchK` is derived rather than generic, since on an annotated signature it sits on a typechecker's hottest path. An annotation-blind instance must return `Just` lazily, and the module documents why a strict one is wrong.
+
+- `Data.ZipMatchK.TH`, Template Haskell derivers for `ZipMatchK` ([#43](https://github.com/fizruk/free-foil/pull/43)). `deriveZipMatchK` zips every type parameter, `deriveZipMatchK2` the last two (for a signature with an annotation parameter), with `deriveZipMatchK1` and `deriveZipMatchKWith` for the rest. The generic instance rebuilds a `Generics.Kind` view of every node on every comparison, at a cost that grows with the number of constructors. The derived instance is flat, and on a 44-constructor signature runs `alphaEquiv` 1.8 times faster for 2.3 times less allocation. It replaces the deriver 0.3.0 dropped along with the old `ZipMatch` class.
+
+- `sinkContainer` sinks a whole container of sinkables (an `IntMap` or `Map` of terms) in O(1) by coercion, instead of `fmap sink` over the spine ([#44](https://github.com/fizruk/free-foil/pull/44)). A `Scope` is not sinkable and a `NameMap` must stay total, both noted with the function.
+
+- `zipmatchk` and `normalize` benchmarks ([#43](https://github.com/fizruk/free-foil/pull/43), [#45](https://github.com/fizruk/free-foil/pull/45)): `alphaEquiv` across signature sizes, and full β-normalisation of untyped λ-terms. CI builds them and does not run them.
+
+Performance:
+
+- `alphaEquiv` and `unsafeEqAST` no longer copy the node into a tuple before folding over it. They recurse inside the zipping functions, allocating nothing and short-circuiting on the first mismatch ([#44](https://github.com/fizruk/free-foil/pull/44)). On the benchmark, 294 µs to 217 µs and 3.1 MB to 2.8 MB with a derived instance. Behaviour is unchanged.
+
+- `substitute`, `alphaEquiv`, `refreshAST` and friends are now `INLINABLE`, so a call site can specialise them for its own signature instead of passing dictionaries ([#44](https://github.com/fizruk/free-foil/pull/44)).
+
+Changed:
+
+- `soas` and `Language.LambdaPi.Impl.FreeFoilTH` derive their `ZipMatchK` instances. `Language.LambdaPi.Impl.FreeFoil` writes them out by hand, so the two implementations show both ways.
+
+- The `base` lower bound is now `>= 4.19` (GHC 9.8). The package has required GHC 9.8 all along through `template-haskell >= 2.21`, so this only makes the bound honest, and lets Hackage's documentation builder pick a compatible GHC ([#15](https://github.com/fizruk/free-foil/issues/15)).
+
 # 0.3.1 — 2026-07-14
 
 A bug fix and a set of additions, all of them prompted by the projects built on free-foil. Nothing is removed or changed, so upgrading from 0.3.0 needs no work.
diff --git a/bench/normalize/Main.hs b/bench/normalize/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/normalize/Main.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE GADTs            #-}
+{-# LANGUAGE LambdaCase       #-}
+{-# LANGUAGE PatternSynonyms  #-}
+{-# LANGUAGE TypeFamilies     #-}
+
+-- | Normalisation benchmark: full β-normalisation of untyped λ-terms over the
+-- free foil, which is where the library's 'substitute' is put under pressure.
+--
+-- The workload is Church-numeral exponentiation. A Church numeral @n@ applied to
+-- a Church numeral @m@ normalises to the Church numeral for @m^n@ (see
+-- 'Control.Monad.Free.Foil.Example.nf'), so @'power' n m@ forces a number of
+-- β-reductions that grows with @m^n@, each one a 'substitute' into a scoped
+-- term. This is the same shape of workload as the free-foil module of
+-- [lambda-n-ways](https://github.com/sweirich/lambda-n-ways) (Weirich's
+-- benchmark suite), from the Free Foil paper.
+--
+-- There is no substitution or normalisation benchmark elsewhere in the package —
+-- the @zipmatchk@ benchmark only exercises 'Control.Monad.Free.Foil.alphaEquiv' —
+-- so this is the one that would show a change to term-building (a strict @AST@,
+-- a substitution that skips unaffected subterms, and so on).
+module Main (main) where
+
+import           Test.Tasty.Bench
+
+import           Control.Monad.Foil            (S (VoidS))
+import           Control.Monad.Free.Foil       (pattern Var)
+import           Control.Monad.Free.Foil.Example (Expr, churchN, nf', pattern AppE, pattern LamE)
+
+-- | The size of a term, used to force the whole normal form (rather than just
+-- its outermost constructor) without a 'Control.DeepSeq.NFData' instance.
+sizeOf :: Expr n -> Int
+sizeOf = \case
+  Var{}       -> 1
+  AppE f x    -> 1 + sizeOf f + sizeOf x
+  LamE _ body -> 1 + sizeOf body
+
+-- | @'power' n m@ is @m@ raised to the @n@: the Church numeral @n@ applied to
+-- the Church numeral @m@, which normalises to the Church numeral for @m^n@.
+power :: Int -> Int -> Expr VoidS
+power n m = AppE (churchN n) (churchN m)
+
+-- | Normalise, then walk the whole result so the benchmark forces it fully.
+normalized :: Expr VoidS -> Int
+normalized = sizeOf . nf'
+
+main :: IO ()
+main = defaultMain
+  [ bgroup "nf of Church m^n"
+      [ bench "8^2  = 64"   $ whnf normalized (power 2 8)
+      , bench "4^3  = 64"   $ whnf normalized (power 3 4)
+      , bench "12^2 = 144"  $ whnf normalized (power 2 12)
+      , bench "2^8  = 256"  $ whnf normalized (power 8 2)
+      , bench "2^10 = 1024" $ whnf normalized (power 10 2)
+      ]
+  ]
diff --git a/bench/zipmatchk/Main.hs b/bench/zipmatchk/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/zipmatchk/Main.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | What the generic 'ZipMatchK' instance costs, and how that cost scales with
+-- the size of the signature.
+--
+-- For each size, two structurally identical signatures differing only in how
+-- their 'ZipMatchK' instance is obtained: @SigNG@ takes the generic default
+-- (via "Generics.Kind"), @SigNH@ has the instance derived by
+-- 'deriveZipMatchK'. Both are compared on 'alphaEquiv' of a large closed term
+-- against itself, which is the worst case (no early exit) and the one a
+-- typechecker actually hits.
+--
+-- The generic representation of a constructor is a chain of @L1@\/@R1@ wrappers
+-- as long as the constructor's index, so a term built from constructors spread
+-- 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.
+module Main (main) where
+
+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.TH       (deriveZipMatchK)
+import           Generics.Kind.TH        (deriveGenericK)
+
+import           Signature               (mkSig)
+
+-- * Signatures of three sizes, twice over
+
+mkSig "Sig2G" 2
+mkSig "Sig2H" 2
+mkSig "Sig10G" 10
+mkSig "Sig10H" 10
+mkSig "Sig44G" 44
+mkSig "Sig44H" 44
+
+deriveBifunctor ''Sig2G
+deriveBifoldable ''Sig2G
+deriveBitraversable ''Sig2G
+deriveGenericK ''Sig2G
+instance ZipMatchK Sig2G
+
+deriveBifunctor ''Sig2H
+deriveBifoldable ''Sig2H
+deriveBitraversable ''Sig2H
+deriveZipMatchK ''Sig2H
+
+deriveBifunctor ''Sig10G
+deriveBifoldable ''Sig10G
+deriveBitraversable ''Sig10G
+deriveGenericK ''Sig10G
+instance ZipMatchK Sig10G
+
+deriveBifunctor ''Sig10H
+deriveBifoldable ''Sig10H
+deriveBitraversable ''Sig10H
+deriveZipMatchK ''Sig10H
+
+deriveBifunctor ''Sig44G
+deriveBifoldable ''Sig44G
+deriveBitraversable ''Sig44G
+deriveGenericK ''Sig44G
+instance ZipMatchK Sig44G
+
+deriveBifunctor ''Sig44H
+deriveBifoldable ''Sig44H
+deriveBitraversable ''Sig44H
+deriveZipMatchK ''Sig44H
+
+-- * A large closed term
+
+-- | A closed term of the given depth: an application tree with a λ every other
+-- level, cycling through the signature's application constructors so that the
+-- whole signature is on the hot path.
+mkTerm
+  :: forall sig
+   . (forall scope term. Int -> term -> term -> sig scope term)  -- ^ Application nodes.
+  -> (forall scope term. scope -> sig scope term)                -- ^ λ-abstraction node.
+  -> Int
+  -> AST Foil.NameBinder sig Foil.VoidS
+mkTerm app lam maxDepth = Foil.withFresh Foil.emptyScope $ \binder ->
+  let scope = Foil.extendScope binder Foil.emptyScope
+   in Node (lam (ScopedAST binder (go scope (Foil.nameOf binder) maxDepth)))
+  where
+    go :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Int -> AST Foil.NameBinder sig n
+    go _scope x 0 = Var x
+    go scope x d
+      | even d = Node (app d (go scope x (d - 1)) (go scope x (d - 1)))
+      | otherwise = Foil.withFresh scope $ \binder ->
+          let scope' = Foil.extendScope binder scope
+           in Node (lam (ScopedAST binder (go scope' (Foil.sink x) (d - 1))))
+
+-- | ~4000 leaves.
+depth :: Int
+depth = 24
+
+main :: IO ()
+main = defaultMain
+  [ bgroup "alphaEquiv, term against itself"
+      [ bgroup "2 constructors"
+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t) t
+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u) u
+          ]
+      , bgroup "10 constructors"
+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t10) t10
+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u10) u10
+          ]
+      , bgroup "44 constructors"
+          [ bench "generic" $ whnf (alphaEquiv Foil.emptyScope t44) t44
+          , bench "derived" $ whnf (alphaEquiv Foil.emptyScope u44) u44
+          ]
+      ]
+  ]
+  where
+    t = mkTerm appSig2G lamSig2G depth
+    u = mkTerm appSig2H lamSig2H depth
+    t10 = mkTerm appSig10G lamSig10G depth
+    u10 = mkTerm appSig10H lamSig10H depth
+    t44 = mkTerm appSig44G lamSig44G depth
+    u44 = mkTerm appSig44H lamSig44H depth
diff --git a/bench/zipmatchk/Signature.hs b/bench/zipmatchk/Signature.hs
new file mode 100644
--- /dev/null
+++ b/bench/zipmatchk/Signature.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TemplateHaskell #-}
+-- | A generator for signature bifunctors of a given size.
+--
+-- The cost of the generic 'Data.ZipMatchK.ZipMatchK' instance is expected to
+-- grow with the number of constructors — a constructor is represented as a
+-- chain of @L1@\/@R1@ wrappers as long as its index — so the benchmark needs
+-- signatures of several sizes, and hand-writing them would defeat the purpose.
+module Signature (mkSig) where
+
+import           Language.Haskell.TH
+
+-- | @mkSig \"Sig\" n@ declares a signature bifunctor @Sig@ with @n@
+-- constructors: @n-1@ application-like nodes (two terms) and one λ-like node
+-- (one scoped term), with 'Bifunctor', 'Bifoldable' and 'Bitraversable'
+-- instances. It also declares two builders,
+--
+-- > appSig :: Int -> term -> term -> Sig scope term   -- the i-th application node
+-- > lamSig :: scope -> Sig scope term
+--
+-- named after the type (@appSig@ and @lamSig@ for @Sig@), so that one term
+-- builder can serve every signature.
+--
+-- The 'Data.Bifunctor.Bifunctor' and 'Data.ZipMatchK.ZipMatchK' instances are
+-- left to the caller: they need a splice of their own, as Template Haskell
+-- cannot reify a type declared in the same declaration group.
+mkSig :: String -> Int -> Q [Dec]
+mkSig name n = do
+  scope <- newName "scope"
+  term <- newName "term"
+  let typeName = mkName name
+      appName i = mkName (name ++ "App" ++ show i)
+      lamName = mkName (name ++ "Lam")
+      appCon i = NormalC (appName i)
+        [ (noBang, VarT term), (noBang, VarT term) ]
+      lamCon = NormalC lamName [ (noBang, VarT scope) ]
+      noBang = Bang NoSourceUnpackedness NoSourceStrictness
+      cons = map appCon [0 .. n - 2] ++ [lamCon]
+      dataDec = DataD [] typeName [PlainTV scope BndrReq, PlainTV term BndrReq] Nothing cons
+        [DerivClause Nothing [ConT ''Functor, ConT ''Foldable, ConT ''Traversable]]
+
+  -- appSig i = the i-th application constructor, cycling.
+  i <- newName "i"
+  let sigType t = ForallT [PlainTV scope SpecifiedSpec, PlainTV term SpecifiedSpec] [] t
+      appType = sigType (arrows [ConT ''Int, VarT term, VarT term] result)
+      lamType = sigType (arrows [VarT scope] result)
+      result = AppT (AppT (ConT typeName) (VarT scope)) (VarT term)
+      arrows args res = foldr (\a b -> AppT (AppT ArrowT a) b) res args
+      appFn = mkName ("app" ++ name)
+      appDec = FunD appFn
+        [ Clause [VarP i]
+            (NormalB (CaseE (InfixE (Just (VarE i)) (VarE 'mod) (Just (LitE (IntegerL (toInteger (n - 1))))))
+              ([ Match (LitP (IntegerL (toInteger k))) (NormalB (ConE (appName k))) []
+               | k <- [0 .. n - 3] ]
+               ++ [ Match WildP (NormalB (ConE (appName (n - 2)))) [] ])))
+            [] ]
+      lamFn = mkName ("lam" ++ name)
+      lamDec = FunD lamFn [ Clause [] (NormalB (ConE lamName)) [] ]
+
+  return [dataDec, SigD appFn appType, appDec, SigD lamFn lamType, lamDec]
diff --git a/free-foil.cabal b/free-foil.cabal
--- a/free-foil.cabal
+++ b/free-foil.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           free-foil
-version:        0.3.1
+version:        0.3.2
 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
@@ -40,6 +40,7 @@
       Control.Monad.Foil.TH.MkToFoil
       Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
+      Control.Monad.Free.Foil.Annotated
       Control.Monad.Free.Foil.Example
       Control.Monad.Free.Foil.TH
       Control.Monad.Free.Foil.TH.Convert
@@ -51,6 +52,7 @@
       Data.ZipMatchK.Functor
       Data.ZipMatchK.Generic
       Data.ZipMatchK.Mappings
+      Data.ZipMatchK.TH
   other-modules:
       Paths_free_foil
   hs-source-dirs:
@@ -58,7 +60,7 @@
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-depends:
       array >=0.5.3.0 && <0.6
-    , base >=4.7 && <5
+    , base >=4.19 && <5
     , bifunctors >=5.5 && <5.7
     , containers >=0.6 && <0.9
     , deepseq >=1.4 && <1.6
@@ -76,7 +78,7 @@
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
   build-depends:
       array >=0.5.3.0 && <0.6
-    , base >=4.7 && <5
+    , base >=4.19 && <5
     , bifunctors >=5.5 && <5.7
     , containers >=0.6 && <0.9
     , deepseq >=1.4 && <1.6
@@ -93,16 +95,18 @@
   other-modules:
       Control.Monad.Foil.NameMapSpec
       Control.Monad.Foil.UnifyNameBindersSpec
+      Control.Monad.Free.Foil.AnnotatedSpec
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config
       Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax
+      Data.ZipMatchK.THSpec
       Paths_free_foil
   hs-source-dirs:
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       array >=0.5.3.0 && <0.6
-    , base >=4.7 && <5
+    , base >=4.19 && <5
     , bifunctors >=5.5 && <5.7
     , containers >=0.6 && <0.9
     , deepseq >=1.4 && <1.6
@@ -111,6 +115,50 @@
     , hspec-discover
     , kind-generics >=0.5.0 && <0.6
     , kind-generics-th
+    , template-haskell >=2.21.0.0 && <2.24
+    , text >=1.2.3.1 && <2.2
+  default-language: Haskell2010
+
+benchmark normalize
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Paths_free_foil
+  hs-source-dirs:
+      bench/normalize
+  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
+    , containers >=0.6 && <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 zipmatchk
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Signature
+      Paths_free_foil
+  hs-source-dirs:
+      bench/zipmatchk
+  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
+    , containers >=0.6 && <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
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
@@ -40,6 +40,7 @@
   CoSinkable(..),
   HasNameBinders(getNameBinders),
   sink,
+  sinkContainer,
   extendRenaming,
   extendNameBinderRenaming,
   composeNameBinderRenamings,
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
@@ -48,6 +48,7 @@
 import           Control.DeepSeq    (NFData (..))
 import           Data.Bifunctor
 import           Data.Coerce        (coerce)
+import           Data.Functor.Compose (Compose (..))
 import           Data.IntMap
 import qualified Data.IntMap        as IntMap
 import           Data.IntSet
@@ -59,6 +60,12 @@
 
 import Control.Monad.Foil.Internal.ValidNameBinders
 
+-- $setup
+-- >>> :set -XDataKinds
+-- >>> :set -XFlexibleContexts
+-- >>> :set -Wno-simplifiable-class-constraints
+-- >>> import qualified Data.Map as Map
+
 -- * Safe types and operations
 
 -- | 'S' is a data kind of scope indices.
@@ -662,12 +669,41 @@
 instance Sinkable Name where
   sinkabilityProof rename = rename
 
+-- | A container of sinkable expressions is sinkable, elementwise.
+--
+-- The point of this instance is 'sinkContainer': since the proof typechecks,
+-- sinking the whole container is a coercion, and does not walk its spine.
+instance (Functor f, Sinkable e) => Sinkable (Compose f e) where
+  sinkabilityProof rename (Compose xs) = Compose (fmap (sinkabilityProof rename) xs)
+
 -- | Efficient version of 'sinkabilityProof'.
 -- In fact, once 'sinkabilityProof' typechecks,
 -- it is safe to 'sink' by coercion.
 -- See Section 3.5 in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details.
 sink :: (Sinkable e, DExt n l) => e n -> e l
 sink = unsafeCoerce
+
+-- | Sink an entire container of sinkable expressions, in \(O(1)\).
+--
+-- The soundness argument for 'sink' extends to a container of sinkables — an
+-- 'Data.IntMap.IntMap' of terms, a 'Data.Map.Map' keyed by something else, a
+-- list of them — so there is no need to walk the spine with @'fmap' 'sink'@, and
+-- entering a binder need not be \(O(size)\).
+--
+-- >>> :{
+-- sinkEnv :: DExt n l => Map.Map String (Name n) -> Map.Map String (Name l)
+-- sinkEnv = sinkContainer
+-- :}
+--
+-- Two things this does /not/ cover:
+--
+-- * A 'Scope' is __not__ sinkable, and must not be sunk: it is the set of names
+--   /in/ scope @n@, and it has to grow when a binder is entered (see 'extendScope').
+-- * A 'NameMap' must stay __total__ on the names in scope ('lookupName' errors
+--   otherwise), so sinking one has to be paired with adding the new binder's
+--   entry (see 'addNameBinder').
+sinkContainer :: (Functor f, Sinkable e, DExt n l) => f (e n) -> f (e l)
+sinkContainer = getCompose . sink . Compose
 
 -- | Extend renaming when going under a 'CoSinkable' pattern (generalized binder).
 -- Note that the scope under pattern is independent of the codomain of the renaming.
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
@@ -34,7 +34,6 @@
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
 import           Data.Maybe                  (mapMaybe)
-import           Data.Monoid                 (All (..))
 import           GHC.Generics                (Generic)
 import           Unsafe.Coerce               (unsafeCoerce)
 
@@ -83,6 +82,7 @@
 -- * Substitution
 
 -- | Substitution for free (scoped monads).
+{-# INLINABLE substitute #-}
 substitute
   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
@@ -108,6 +108,7 @@
 -- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst
 --
 -- In general, 'substitute' is more efficient since it does not always refresh binders.
+{-# INLINABLE substituteRefreshed #-}
 substituteRefreshed
   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
@@ -158,6 +159,7 @@
 -- * \(\alpha\)-equivalence
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.
+{-# INLINABLE refreshAST #-}
 refreshAST
   :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
@@ -168,6 +170,7 @@
   Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)
 
 -- | Similar to `refreshAST`, but for scoped terms.
+{-# INLINABLE refreshScopedAST #-}
 refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
@@ -183,6 +186,7 @@
 --
 -- Compared to 'alphaEquiv', this function may perform some unnecessary
 -- changes of bound variables when the binders are the same on both sides.
+{-# INLINABLE alphaEquivRefreshed #-}
 alphaEquivRefreshed
   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
@@ -196,6 +200,7 @@
 --
 -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
 -- changes of bound variables when both binders in two matching scoped terms coincide.
+{-# INLINABLE alphaEquiv #-}
 alphaEquiv
   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
@@ -204,12 +209,15 @@
   -> Bool
 alphaEquiv _scope (Var x) (Var y) = x == coerce y
 alphaEquiv scope (Node l) (Node r) =
-  case zipMatch2 l r of
+  case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of
     Nothing -> False
-    Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)
+    Just _  -> True
+  where
+    unit f x = if f x then Just () else Nothing
 alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
+{-# INLINABLE alphaEquivScoped #-}
 alphaEquivScoped
   :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
@@ -255,6 +263,7 @@
 -- This check ignores the possibility that two terms might have different
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
+{-# INLINABLE unsafeEqAST #-}
 unsafeEqAST
   :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
@@ -262,12 +271,15 @@
   -> Bool
 unsafeEqAST (Var x) (Var y) = x == coerce y
 unsafeEqAST (Node t1) (Node t2) =
-  case zipMatch2 t1 t2 of
+  case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of
     Nothing -> False
-    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
+    Just _  -> True
+  where
+    unit f x = if f x then Just () else Nothing
 unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
+{-# INLINABLE unsafeEqScopedAST #-}
 unsafeEqScopedAST
   :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
diff --git a/src/Control/Monad/Free/Foil/Annotated.hs b/src/Control/Monad/Free/Foil/Annotated.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/Annotated.hs
@@ -0,0 +1,182 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-- | Annotating every node of a free foil term.
+--
+-- A node can be annotated with anything: a source position, a type, a memoised
+-- normal form. 'AnnSig' turns a signature into an annotated one, and
+-- 'AnnAST' is the annotated syntax it generates.
+--
+-- The annotation is a /functor of the term/, and that is what lets it depend on
+-- the node's scope. In @'AST' binder sig n@ the signature's term parameter /is/
+-- the AST at the node's own scope, so an annotation built from it holds terms in
+-- that scope — which is what a type annotation in a dependent language needs.
+-- An annotation that ignores the term (a source position, say) is @'Const' a@.
+--
+-- Whether two annotations must agree for their nodes to match is a property of
+-- @ann@, not of 'AnnSig'. Two examples, and they are the two you will want:
+--
+-- An annotation that ignores the term (a source position) and /is/ compared:
+--
+-- > instance Eq a => ZipMatchK (Const (a :: Type)) where
+-- >   zipMatchWithK _ (Const l) (Const r)
+-- >     | l == r    = Just (Const l)
+-- >     | otherwise = Nothing
+--
+-- An annotation that holds terms (a type, say) and is /ignored/, so that two
+-- terms differing only in their types are α-equivalent. Make the held term
+-- optional, so that pairing can fail /without/ failing the match:
+--
+-- > newtype TypeOf term = TypeOf (Maybe term)
+-- >
+-- > instance ZipMatchK TypeOf where
+-- >   zipMatchWithK (f :^: M0) (TypeOf l) (TypeOf r) =
+-- >     Just (TypeOf (do { a <- l; b <- r; f a b }))
+--
+-- __The instance must return 'Just' unconditionally, and lazily.__ Matching is
+-- annotation-blind, so it must succeed whatever the annotations are; the paired
+-- annotation is a thunk the (annotation-skipping) 'Bifoldable' never forces. A
+-- /strict/ shape — @TypeOf '<$>' f l r@, or anything that yields 'Nothing' when
+-- @f@ fails — is a footgun twice over: it breaks blindness (two nodes with
+-- different types would fail to match), and it /diverges/ for a finite or
+-- lazily-bottomed annotation (a universe tower ending in 'error', say), because
+-- forcing the annotation runs off the end. This is why the held term is a 'Maybe':
+-- a plain @term@ field would have no value to pair when @f@ fails, forcing a
+-- bottom into the result.
+--
+-- __Do not reach for the generic instance here.__ It compares the annotation's
+-- /shape/, so a node carrying a memoised normal form would fail to match the same
+-- node without one. (Nor is 'zipMatchViaChooseLeft' available: an annotation
+-- holding terms must /construct/ a value at the result index, and cannot simply
+-- pick a side.)
+--
+-- __Note the asymmetry__ in the instances below: 'Bifunctor' and 'Bitraversable'
+-- traverse the annotation, but 'Bifoldable' does /not/. This is deliberate — see
+-- 'AnnSig'.
+module Control.Monad.Free.Foil.Annotated (
+  AnnSig(..),
+  AnnAST,
+  AnnScopedAST,
+  pattern AnnNode,
+  annotationOf,
+  freeVarsOfAnnotated,
+) where
+
+import           Data.Bifoldable
+import           Data.Bifunctor
+import           Data.Bitraversable
+import           Data.Kind             (Type)
+import           Data.Maybe            (mapMaybe)
+import           Data.ZipMatchK.TH     (deriveZipMatchK2)
+import           Generics.Kind         (GenericK (..), Field, Var0, Var1, (:$:),
+                                        Atom ((:@:)), (:*:))
+import qualified GHC.Generics          as GHC
+
+import qualified Control.Monad.Foil    as Foil
+import           Control.Monad.Free.Foil
+
+-- | A signature, with every node annotated by an @ann@ built from the node's term.
+--
+-- The annotation is applied to the /term/ parameter, so in an
+-- @'AST' binder ('AnnSig' ann sig) n@ it holds terms in the node's own scope.
+--
+-- 'Bifoldable' deliberately __skips the annotation__. That is what makes
+-- α-equivalence annotation-blind: 'Control.Monad.Free.Foil.alphaEquiv' consumes a
+-- zipped node with 'bifoldMap', so a type annotation is never compared, and two
+-- terms that differ only in their annotations are α-equivalent. The price is that
+-- 'Control.Monad.Free.Foil.freeVarsOf', which is also 'Bifoldable', does not see
+-- variables occurring inside annotations. Use 'freeVarsOfAnnotated' when those
+-- matter.
+data AnnSig (ann :: Type -> Type) (sig :: Type -> Type -> Type) scope term
+  = AnnSig (ann term) (sig scope term)
+  deriving (GHC.Generic)
+
+deriving instance (Functor ann, Functor (sig scope))
+  => Functor (AnnSig ann sig scope)
+deriving instance (Foldable ann, Foldable (sig scope))
+  => Foldable (AnnSig ann sig scope)
+deriving instance (Traversable ann, Traversable (sig scope))
+  => Traversable (AnnSig ann sig scope)
+
+instance (Functor ann, Bifunctor sig) => Bifunctor (AnnSig ann sig) where
+  bimap f g (AnnSig ann sig) = AnnSig (fmap g ann) (bimap f g sig)
+
+-- | __The annotation is not folded.__ See 'AnnSig'.
+instance Bifoldable sig => Bifoldable (AnnSig ann sig) where
+  bifoldMap f g (AnnSig _ann sig) = bifoldMap f g sig
+
+instance (Traversable ann, Bitraversable sig) => Bitraversable (AnnSig ann sig) where
+  bitraverse f g (AnnSig ann sig) = AnnSig <$> traverse g ann <*> bitraverse f g sig
+
+instance GenericK (AnnSig ann sig) where
+  type RepK (AnnSig ann sig) =
+    Field (ann :$: Var1) :*: Field ((sig :$: Var0) :@: Var1)
+
+-- | Matching for 'AnnSig' is /derived/, not left to the generic default.
+--
+-- The generic default would rebuild the "Generics.Kind" view of every node on
+-- every comparison, and comparing terms is most of what a typechecker does, so
+-- for an annotated signature — where it lands on the hottest path — that is a
+-- measurable cost. 'Data.ZipMatchK.TH.deriveZipMatchK2' generates the
+-- written-out instance instead: the annotation matched with the term zipper (an
+-- annotation is a functor of the term), the inner signature with both. Write
+-- @deriveZipMatchK2 ''YourAnnSig@ for a bespoke annotated signature.
+deriveZipMatchK2 ''AnnSig
+
+-- | An annotated scope-safe term.
+type AnnAST binder ann sig = AST binder (AnnSig ann sig)
+
+-- | An annotated scope-safe term under a binder.
+type AnnScopedAST binder ann sig = ScopedAST binder (AnnSig ann sig)
+
+-- | An annotated node.
+pattern AnnNode
+  :: ann (AnnAST binder ann sig n)
+  -> sig (AnnScopedAST binder ann sig n) (AnnAST binder ann sig n)
+  -> AnnAST binder ann sig n
+pattern AnnNode ann sig = Node (AnnSig ann sig)
+
+{-# COMPLETE Var, AnnNode #-}
+
+-- | The annotation of a term, unless it is a variable (which is not a node, so it
+-- carries none).
+annotationOf :: AnnAST binder ann sig n -> Maybe (ann (AnnAST binder ann sig n))
+annotationOf = \case
+  Var _         -> Nothing
+  AnnNode ann _ -> Just ann
+
+-- | The free variables of an annotated term, __including__ those occurring inside
+-- annotations.
+--
+-- 'Control.Monad.Free.Foil.freeVarsOf' misses the latter, since 'Bifoldable' skips
+-- the annotation (see 'AnnSig').
+freeVarsOfAnnotated
+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig, Foldable ann)
+  => AnnAST binder ann sig n -> [Foil.Name n]
+freeVarsOfAnnotated = \case
+  Var name -> [name]
+  AnnNode ann sig ->
+    foldMap freeVarsOfAnnotated ann
+      <> bifoldMap freeVarsOfAnnotatedScoped freeVarsOfAnnotated sig
+
+-- | The free variables of an annotated scoped term, including those inside
+-- annotations.
+freeVarsOfAnnotatedScoped
+  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig, Foldable ann)
+  => AnnScopedAST binder ann sig n -> [Foil.Name n]
+freeVarsOfAnnotatedScoped (ScopedAST binder body) =
+  case Foil.assertDistinct binder of
+    Foil.Distinct ->
+      mapMaybe (Foil.unsinkNamePattern binder) (freeVarsOfAnnotated body)
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
@@ -29,6 +29,16 @@
 --
 -- Note: @f@ is expected to be a traversable n-functor,
 -- but at the moment we lack a @TraversableK@ constraint.
+--
+-- The default implementation is generic, via 'Generics.Kind.RepK'. It is
+-- convenient, but it reflects each node into a representation and back on every
+-- comparison, and a constructor is represented as a chain of @L1@\/@R1@ wrappers
+-- as long as its index, so the cost grows with the size of the signature. On a
+-- 44-constructor signature it costs about 1.8 times the time and 2.3 times the
+-- allocation of the written-out instance, and comparing terms is most of what a
+-- typechecker does. Use 'Data.ZipMatchK.TH.deriveZipMatchK' (or
+-- 'Data.ZipMatchK.TH.deriveZipMatchK2', for a signature bifunctor with extra
+-- parameters) to generate the written-out instance instead.
 class ZipMatchK (f :: k) where
   -- | Perform one level of equality testing:
   --
diff --git a/src/Data/ZipMatchK/TH.hs b/src/Data/ZipMatchK/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ZipMatchK/TH.hs
@@ -0,0 +1,267 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns    #-}
+-- | Template Haskell derivation of 'ZipMatchK' instances.
+--
+-- The generic instance (the one you get by writing @instance ZipMatchK TermSig@
+-- with no body) converts a node into its "Generics.Kind" representation on
+-- every comparison, and converts the result back. The representation of a
+-- constructor is a chain of @L1@\/@R1@ wrappers as long as that constructor's
+-- index, so the cost grows with the number of constructors in the signature,
+-- and comparing terms is most of what a typechecker does.
+--
+-- The derivers here generate the instance that one would otherwise write out by
+-- hand: a @case@ over the two nodes, allocating only its result. On a
+-- 44-constructor signature that is worth a factor of 1.8 in time and 2.3 in
+-- allocation on 'Control.Monad.Free.Foil.alphaEquiv' (see the @zipmatchk@
+-- benchmark), and the derived instance does not get slower as the signature
+-- grows.
+--
+-- The module the splice appears in needs at least
+--
+-- > {-# LANGUAGE GADTs #-}
+-- > {-# LANGUAGE TemplateHaskell #-}
+-- > {-# LANGUAGE TypeFamilies #-}
+--
+-- Signatures that refer to one another — as the ones generated by
+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil' from a grammar with
+-- several syntactic categories do — have to be derived in a __single splice__,
+-- since a top-level splice ends a declaration group and an instance from a later
+-- group is not visible to an earlier one:
+--
+-- > concat <$> traverse deriveZipMatchK2 [''Term'Sig, ''OpArg'Sig, ''Type'Sig]
+module Data.ZipMatchK.TH (
+  deriveZipMatchK,
+  deriveZipMatchK1,
+  deriveZipMatchK2,
+  deriveZipMatchKWith,
+) where
+
+import           Data.List             (foldl')
+import qualified Data.Set              as Set
+import           Language.Haskell.TH
+
+import           Control.Monad.Foil.TH.Util (removeName, tvarName)
+import           Data.ZipMatchK.Generic    (ZipMatchK (..))
+import           Data.ZipMatchK.Mappings   (Mappings (..))
+
+-- | Derive a 'ZipMatchK' instance, zipping /all/ type parameters.
+--
+-- For a signature bifunctor
+--
+-- > data TermSig scope term = AppSig term term | LamSig scope
+-- > deriveZipMatchK ''TermSig
+--
+-- this generates
+--
+-- > instance ZipMatchK TermSig where
+-- >   zipMatchWithK (f :^: g :^: M0) x y = case (x, y) of
+-- >     (AppSig l1 l2, AppSig r1 r2) -> AppSig <$> g l1 r1 <*> g l2 r2
+-- >     (LamSig l1, LamSig r1)       -> LamSig <$> f l1 r1
+-- >     _                            -> Nothing
+--
+-- Use 'deriveZipMatchK2' when the type has extra parameters that should stay
+-- fixed (an annotation, say), as a signature generated by
+-- "Control.Monad.Free.Foil.TH.MkFreeFoil" does.
+deriveZipMatchK :: Name -> Q [Dec]
+deriveZipMatchK = deriveZipMatchKWith Nothing
+
+-- | Derive a 'ZipMatchK' instance for a functor, zipping the last type parameter
+-- and fixing the rest.
+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.
+--
+-- For a signature with an extra parameter (a source position, for instance)
+--
+-- > data Term'Sig a scope term = AppSig a term term | LamSig a scope
+-- > deriveZipMatchK2 ''Term'Sig
+--
+-- this generates
+--
+-- > instance ZipMatchK a => ZipMatchK (Term'Sig a) where
+-- >   zipMatchWithK (f :^: g :^: M0) x y = case (x, y) of
+-- >     (AppSig l1 l2 l3, AppSig r1 r2 r3) ->
+-- >       AppSig <$> zipMatchWithK M0 l1 r1 <*> g l2 r2 <*> g l3 r3
+-- >     ...
+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.
+--
+-- Every fixed parameter that occurs in a field gets a 'ZipMatchK' constraint in
+-- the instance context.
+deriveZipMatchKWith :: Maybe Int -> Name -> Q [Dec]
+deriveZipMatchKWith arity typeName = do
+  (tvars, cons) <- reifyDataType typeName
+  let params = map tvarName tvars
+      n = case arity of
+            Nothing -> length params
+            Just k  -> k
+  if n > length params
+    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
+
+      -- 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
+
+      fieldsOf <- concat <$> mapM (constructorFields params zippedSet) cons
+      clauses <- mapM (conClause zippedSet mappings) 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 'zipMatchWithK
+            [Clause [mappingsPat, VarP x, VarP y] (NormalB body) []]
+
+          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 type parameters and constructors of a @data@ or @newtype@ declaration.
+reifyDataType :: Name -> Q ([TyVarBndr BndrVis], [Con])
+reifyDataType typeName = reify typeName >>= \case
+  TyConI (DataD _ _ tvars _ cons _)      -> return (tvars, cons)
+  TyConI (NewtypeD _ _ tvars _ con _)    -> return (tvars, [con])
+  _ -> fail (show typeName ++ " is not a data type or a newtype")
+
+-- | A constructor's name and the types of its fields, in terms of the type
+-- parameters of the declaration it belongs to.
+--
+-- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil' declares its signatures in
+-- GADT syntax, and 'reify' returns such a constructor wrapped in a 'ForallC',
+-- with variable names of its own. So the fields are renamed through the
+-- constructor's return type before anything else looks at them.
+constructorFields :: [Name] -> Set.Set Name -> Con -> Q [(Name, [Type])]
+constructorFields params zipped = \case
+  NormalC conName types      -> return [(conName, map snd types)]
+  RecC conName types         -> return [(conName, map (snd . removeName) types)]
+  InfixC l conName r         -> return [(conName, [snd l, snd r])]
+  RecGadtC conNames types r  -> constructorFields params zipped
+                                  (GadtC conNames (map removeName types) r)
+  ForallC _ context_ con
+    | null context_ -> constructorFields params zipped con
+    | otherwise -> fail "constructor contexts are not supported by deriveZipMatchK"
+  GadtC conNames types retType -> do
+    rename <- renaming retType
+    let fields = map (substTypeVars rename . snd) types
+        escaping = foldMap freeVarsOfType fields `Set.difference` Set.fromList params
+    if Set.null escaping
+      then return [ (conName, fields) | conName <- conNames ]
+      else fail ("existentials are not supported by deriveZipMatchK: "
+                  ++ show (Set.toList escaping))
+  where
+    -- The constructor's variables, named as the declaration names them.
+    renaming retType = do
+      let (_, args) = unApply retType
+      if length args /= length params
+        then fail "the constructor does not return the type being derived for"
+        else sequence
+          [ case stripType arg of
+              VarT v -> return (v, param)
+              _ | param `Set.member` zipped ->
+                    fail ("the constructor fixes the type parameter "
+                           ++ show param ++ ", which is being zipped")
+                | otherwise -> return (param, param)  -- a fixed index; no field can mention it
+          | (arg, param) <- zip args params ]
+
+-- | One @case@ alternative, zipping a constructor with itself.
+conClause :: Set.Set Name -> [(Name, Exp)] -> (Name, [Type]) -> Q Match
+conClause zipped mappings (conName, types) = do
+  lvars <- mapM (const (newName "l")) types
+  rvars <- mapM (const (newName "r")) types
+  zippers <- mapM (fieldZipper zipped mappings) types
+  -- Con <$> z1 l1 r1 <*> z2 l2 r2 <*> ...
+  let zipField z l r = AppE (AppE z (VarE l)) (VarE r)
+      apply acc (op, (z, (l, r))) = InfixE (Just acc) op (Just (zipField z l r))
+      fields = zip (VarE '(<$>) : repeat (VarE '(<*>)))
+                   (zip zippers (zip lvars rvars))
+      body
+        | null fields = AppE (ConE 'Just) (ConE conName)
+        | otherwise   = foldl' apply (ConE conName) fields
+  return (Match
+            (TupP [ ConP conName [] (map VarP lvars)
+                  , ConP conName [] (map VarP rvars) ])
+            (NormalB body) [])
+
+-- | Rename type variables.
+substTypeVars :: [(Name, Name)] -> Type -> Type
+substTypeVars rename = go
+  where
+    go = \case
+      VarT v        -> VarT (maybe v id (lookup v rename))
+      AppT f x      -> AppT (go f) (go x)
+      AppKindT t k  -> AppKindT (go t) k
+      SigT t k      -> SigT (go t) k
+      ParensT t     -> ParensT (go t)
+      InfixT l n r  -> InfixT (go l) n (go r)
+      UInfixT l n r -> UInfixT (go l) n (go r)
+      t             -> t
+
+-- | Compile a field type into a zipping function @a -> b -> Maybe c@.
+--
+-- This mirrors what @ZipMatchFields@ does for the generic instance, but at
+-- compile time, so nothing is reflected into a representation type:
+--
+-- * a zipped type parameter becomes the corresponding zipping function;
+-- * any other type is zipped by its own 'ZipMatchK' instance, with the
+--   arguments that mention zipped parameters passed as further zipping
+--   functions.
+--
+-- So a field @[term]@ becomes @zipMatchWithK (g :^: M0)@ (asking for
+-- @ZipMatchK []@), a field @Either a term@ becomes @zipMatchWithK (g :^: M0)@
+-- (asking for @ZipMatchK (Either a)@), and a field @VarIdent@ becomes
+-- @zipMatchWithK M0@ (asking for @ZipMatchK VarIdent@).
+fieldZipper :: Set.Set Name -> [(Name, Exp)] -> Type -> Q Exp
+fieldZipper zipped mappings type_ = case stripType type_ of
+  VarT v | Just f <- lookup v mappings -> return f
+  t -> do
+    let (_headType, args) = unApply t
+        zippedArgs = dropWhile (not . mentionsZipped zipped) args
+    argZippers <- mapM (fieldZipper zipped mappings) zippedArgs
+    let ms = foldr (\z m -> InfixE (Just z) (ConE '(:^:)) (Just m)) (ConE 'M0) argZippers
+    return (AppE (VarE 'zipMatchWithK) ms)
+
+-- | Does the type mention any of the zipped type parameters?
+mentionsZipped :: Set.Set Name -> Type -> Bool
+mentionsZipped zipped t = not (Set.null (Set.intersection zipped (freeVarsOfType t)))
+
+-- | Split a type into its head and its arguments.
+unApply :: Type -> (Type, [Type])
+unApply = 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)
+
+-- | Drop parentheses and kind signatures.
+stripType :: Type -> Type
+stripType (ParensT t) = stripType t
+stripType (SigT t _)  = stripType t
+stripType t           = t
+
+freeVarsOfType :: Type -> Set.Set Name
+freeVarsOfType = \case
+  VarT v      -> Set.singleton v
+  AppT f x    -> freeVarsOfType f <> freeVarsOfType x
+  AppKindT t _-> freeVarsOfType t
+  SigT t _    -> freeVarsOfType t
+  ParensT t   -> freeVarsOfType t
+  InfixT l _ r-> freeVarsOfType l <> freeVarsOfType r
+  UInfixT l _ r -> freeVarsOfType l <> freeVarsOfType r
+  _           -> Set.empty
diff --git a/test/Control/Monad/Free/Foil/AnnotatedSpec.hs b/test/Control/Monad/Free/Foil/AnnotatedSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Monad/Free/Foil/AnnotatedSpec.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Annotated syntax: one 'AnnSig' serving two annotations with opposite matching
+-- behaviour, and the 'Bifoldable' asymmetry that α-equivalence relies on.
+module Control.Monad.Free.Foil.AnnotatedSpec (spec) where
+
+import           Data.Bifunctor.TH
+import           Data.Functor.Const                (Const (..))
+import           Data.Kind                         (Type)
+import           Data.ZipMatchK
+import           Generics.Kind.TH                  (deriveGenericK)
+import qualified GHC.Generics                      as GHC
+import           Test.Hspec
+
+import qualified Control.Monad.Foil                as Foil
+import           Control.Monad.Free.Foil
+import           Control.Monad.Free.Foil.Annotated
+
+-- | A minimal λ-calculus signature.
+data LamSig scope term = AppSig term term | LamSig scope
+  deriving (GHC.Generic, Functor, Foldable, Traversable)
+
+deriveBifunctor ''LamSig
+deriveBifoldable ''LamSig
+deriveBitraversable ''LamSig
+deriveGenericK ''LamSig
+instance ZipMatchK LamSig
+
+instance ZipMatchK Int where zipMatchWithK = zipMatchViaEq
+
+-- | An annotation that ignores the term — a source position, say — and __is
+-- compared__ when matching.
+instance Eq a => ZipMatchK (Const (a :: Type)) where
+  zipMatchWithK _ (Const l) (Const r)
+    | l == r    = Just (Const l)
+    | otherwise = Nothing
+
+type Positioned = AnnAST Foil.NameBinder (Const Int) LamSig
+
+-- | An annotation that holds a term at the node's own scope — a type, say.
+--
+-- It is optional, and it has to be: an annotation holding a term needs a term to
+-- hold, so a closed annotated term could not be built at all without either a
+-- 'Maybe' or a knot.
+newtype TypeOf term = TypeOf (Maybe term)
+  deriving (GHC.Generic, Functor, Foldable, Traversable)
+
+deriveGenericK ''TypeOf
+
+-- | Matching __ignores__ the annotation: it always succeeds, pairing the terms it
+-- can and dropping what it cannot.
+--
+-- The /generic/ instance would not do: it compares the annotation's shape, so a
+-- node with a memoised type would fail to match the same node without one.
+instance ZipMatchK TypeOf where
+  zipMatchWithK (f :^: M0) (TypeOf l) (TypeOf r) =
+    Just (TypeOf (do { a <- l; b <- r; f a b }))
+
+type Typed = AnnAST Foil.NameBinder TypeOf LamSig
+
+-- | @\\x. x x@, annotated at every node with a source position.
+positioned :: Int -> Positioned Foil.VoidS
+positioned k = Foil.withFresh Foil.emptyScope $ \binder ->
+  case Foil.assertDistinct binder of
+    Foil.Distinct ->
+      let x = Var (Foil.nameOf binder)
+       in AnnNode (Const k)
+            (LamSig (ScopedAST binder (AnnNode (Const k) (AppSig x x))))
+
+-- | @\\x. x@, carrying the given type annotation at its root.
+typed :: Maybe (Typed Foil.VoidS) -> Typed Foil.VoidS
+typed ty = Foil.withFresh Foil.emptyScope $ \binder ->
+  case Foil.assertDistinct binder of
+    Foil.Distinct ->
+      AnnNode (TypeOf ty) (LamSig (ScopedAST binder (Var (Foil.nameOf binder))))
+
+-- | @\\x. x x@, with no type annotations, to have a structurally different term.
+selfApp :: Typed Foil.VoidS
+selfApp = Foil.withFresh Foil.emptyScope $ \binder ->
+  case Foil.assertDistinct binder of
+    Foil.Distinct ->
+      let x = Var (Foil.nameOf binder)
+       in AnnNode (TypeOf Nothing)
+            (LamSig (ScopedAST binder (AnnNode (TypeOf Nothing) (AppSig x x))))
+
+spec :: Spec
+spec = do
+  describe "an annotation that ignores the term (Const)" $ do
+    it "matches when the annotations agree" $
+      alphaEquiv Foil.emptyScope (positioned 1) (positioned 1) `shouldBe` True
+
+    it "does not match when they differ" $
+      alphaEquiv Foil.emptyScope (positioned 1) (positioned 2) `shouldBe` False
+
+  describe "an annotation that holds a term (a type)" $ do
+    it "is ignored when matching: terms differing only in their types are alpha-equivalent" $
+      -- The property a dependent typechecker needs. It works because Bifoldable
+      -- skips the annotation, so alphaEquiv never walks into it.
+      alphaEquiv Foil.emptyScope (typed Nothing) (typed (Just (typed Nothing)))
+        `shouldBe` True
+
+    it "still distinguishes terms that differ in the term itself" $
+      alphaEquiv Foil.emptyScope (typed Nothing) selfApp `shouldBe` False
+
+    it "never forces the annotation: matching is lazy in it" $
+      -- The blind instance returns 'Just' unconditionally with a thunked
+      -- annotation, so an annotation that is bottom must not break the match.
+      -- A strict instance would throw here instead of returning True.
+      alphaEquiv Foil.emptyScope
+        (typed (Just (error "annotation forced")))
+        (typed (Just (error "annotation forced")))
+        `shouldBe` True
+
+  describe "freeVarsOfAnnotated" $
+    it "sees a variable that freeVarsOf misses, because it occurs in an annotation" $
+      Foil.withFresh Foil.emptyScope $ \outer ->
+        case Foil.assertDistinct outer of
+          Foil.Distinct ->
+            let x = Var (Foil.nameOf outer)                      -- free at this scope
+                scope = Foil.extendScope outer Foil.emptyScope
+             in Foil.withFresh scope $ \inner ->
+                  case Foil.assertDistinct inner of
+                    Foil.Distinct ->
+                      -- \y. y, annotated with a type that mentions x
+                      let node = AnnNode (TypeOf (Just x))
+                                   (LamSig (ScopedAST inner (Var (Foil.nameOf inner))))
+                       in do
+                            freeVarsOf node `shouldBe` []
+                            length (freeVarsOfAnnotated node) `shouldBe` 1
diff --git a/test/Data/ZipMatchK/THSpec.hs b/test/Data/ZipMatchK/THSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/ZipMatchK/THSpec.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DeriveGeneric         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-- | The derived 'ZipMatchK' instance must agree with the generic one.
+--
+-- 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.
+module Data.ZipMatchK.THSpec (spec) where
+
+import           Data.List.NonEmpty      (NonEmpty (..))
+import           Generics.Kind           (LoT (..))
+import qualified GHC.Generics            as GHC
+import           Generics.Kind.TH        (deriveGenericK)
+import           Test.Hspec
+
+import           Data.ZipMatchK
+import           Data.ZipMatchK.Generic  (genericZipMatchWithK)
+import           Data.ZipMatchK.TH
+
+-- | An annotation, standing for the extra parameter a generated signature has.
+newtype Ann = Ann Int deriving (Eq, Show)
+instance ZipMatchK Ann where zipMatchWithK = zipMatchViaEq
+
+-- | A signature exercising every field shape the deriver has to compile: a
+-- term, a scoped term, a constant, the extra parameter, a container of terms,
+-- a container of scoped terms, and a nest of containers.
+data RichSig a scope term
+  = AppSig term term
+  | LamSig scope
+  | LitSig Ann
+  | AnnSig a term
+  | ManySig [term]
+  | SomeSig (Maybe scope)
+  | NestSig [Maybe term]
+  | NonEmptySig (NonEmpty term)
+  | EitherSig (Either Ann term)
+  | PairSig (scope, term)
+  | NullarySig
+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)
+
+deriveGenericK ''RichSig
+deriveZipMatchK2 ''RichSig
+
+-- | A plain signature bifunctor, with no extra parameters.
+data LamSig scope term = App term term | Lam scope
+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)
+
+deriveGenericK ''LamSig
+deriveZipMatchK ''LamSig
+
+-- | A functor, as an annotation would be.
+newtype Boxed term = Boxed [term]
+  deriving (GHC.Generic, Functor, Foldable, Traversable, Eq, Show)
+
+deriveGenericK ''Boxed
+deriveZipMatchK1 ''Boxed
+
+-- | Zip two values by equality, so that a zipped signature has the same type as
+-- the signatures it came from, and can be compared with '=='.
+zipEq :: Eq a => a -> a -> Maybe a
+zipEq x y
+  | x == y    = Just x
+  | otherwise = Nothing
+
+richSamples :: [RichSig Ann String String]
+richSamples =
+  [ AppSig "x" "y"
+  , AppSig "x" "z"
+  , LamSig "s"
+  , LamSig "t"
+  , LitSig (Ann 1)
+  , LitSig (Ann 2)
+  , AnnSig (Ann 1) "x"
+  , AnnSig (Ann 2) "x"
+  , ManySig []
+  , ManySig ["x"]
+  , ManySig ["x", "y"]
+  , SomeSig Nothing
+  , SomeSig (Just "s")
+  , NestSig [Just "x", Nothing]
+  , NestSig [Just "y", Nothing]
+  , NonEmptySig ("x" :| [])
+  , NonEmptySig ("x" :| ["y"])
+  , EitherSig (Left (Ann 1))
+  , EitherSig (Right "x")
+  , PairSig ("s", "x")
+  , NullarySig
+  ]
+
+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 "deriveZipMatchK2" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @(RichSig Ann) mappings x y
+            `shouldBe` genericZipMatchWithK @(RichSig Ann) mappings x y
+        | x <- richSamples, y <- richSamples ]
+
+  describe "deriveZipMatchK" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @LamSig mappings x y
+            `shouldBe` genericZipMatchWithK @LamSig mappings x y
+        | x <- lamSamples, y <- lamSamples ]
+
+  describe "deriveZipMatchK1" $
+    it "agrees with the generic instance on every pair of samples" $
+      sequence_
+        [ zipMatchWithK @_ @Boxed (zipEq :^: M0) x y
+            `shouldBe` genericZipMatchWithK @Boxed (zipEq :^: M0) x y
+        | x <- boxedSamples, y <- boxedSamples ]
+  where
+    mappings :: Mappings (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0) (String ':&&: String ':&&: 'LoT0)
+    mappings = zipEq :^: zipEq :^: M0