diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,31 @@
+# CHANGELOG for `free-foil`
+
+# 0.0.3 — 2024-06-20
+
+- Add α-equivalence checks and α-normalization (see [#12](https://github.com/fizruk/free-foil/pull/12)):
+
+  - `Control.Monad.Foil` now offers more helpers to work with binder renaming and binder unification.
+    These helpers can be used to implement (efficient) α-equivalence.
+  - In `Control.Monad.Free.Foil` general implementation of α-equivalence and α-normalization is provided.
+
+- Add general conversion functions for free foil (see [#14](https://github.com/fizruk/free-foil/pull/14)):
+
+  - `Control.Monad.Free.Foil` now offers `convertToAST` and `convertFromAST` functions
+    enabling easier implementation of conversions raw and scope-safe representations.
+
+- Add Template Haskell functions for free foil (see [#14](https://github.com/fizruk/free-foil/pull/14)):
+
+  - `Control.Monad.Free.Foil.TH` contains many useful functions to generate free foil from
+    a raw representation (e.g. generated via BNFC), including generation of the signature,
+    convenient pattern synonyms, `ZipMatch` instance, and conversion helpers.
+
+# 0.0.2 — 2024-06-18
+
+- Improve TH to support parametrized data types (see [#11](https://github.com/fizruk/free-foil/pull/11))
+- Split `lambda-pi` into its own package (see [#10](https://github.com/fizruk/free-foil/pull/10))
+- Switch to `template-haskell >= 2.21.0.0` (to support latest Stackage Nightly)
+- Fix doctests (see [#9](https://github.com/fizruk/free-foil/pull/9))
+
+# 0.0.1 — 2024-06-08
+
+First release, corresponding to the ICCQ 2024 paper.
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.0.2
+version:        0.0.3
 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
@@ -19,6 +19,7 @@
 build-type:     Simple
 extra-source-files:
     README.md
+    ChangeLog.md
     LICENSE
 
 source-repository head
@@ -39,6 +40,11 @@
       Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
       Control.Monad.Free.Foil.Example
+      Control.Monad.Free.Foil.TH
+      Control.Monad.Free.Foil.TH.Convert
+      Control.Monad.Free.Foil.TH.PatternSynonyms
+      Control.Monad.Free.Foil.TH.Signature
+      Control.Monad.Free.Foil.TH.ZipMatch
   other-modules:
       Paths_free_foil
   hs-source-dirs:
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
@@ -28,11 +28,14 @@
   withFresh,
   withRefreshed,
   unsinkName,
-  -- * Safe (co)sinking
+  -- * Safe (co)sinking and renaming
   Sinkable(..),
   CoSinkable(..),
   sink,
   extendRenaming,
+  extendNameBinderRenaming,
+  composeNameBinderRenamings,
+  fromNameBinderRenaming,
   extendRenamingNameBinder,
   -- * Safe substitutions
   Substitution,
@@ -40,6 +43,9 @@
   identitySubst,
   addSubst,
   addRename,
+  -- * Unification of binders
+  UnifyNameBinders(..),
+  unifyNameBinders,
   -- * Name maps
   NameMap,
   emptyNameMap,
@@ -51,6 +57,7 @@
   Distinct,
   DistinctEvidence(..),
   assertDistinct,
+  assertExt,
   DExt,
   InjectName(..),
 ) where
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
@@ -40,6 +40,7 @@
 import qualified Data.IntSet     as IntSet
 import           Data.Kind       (Type)
 import           Unsafe.Coerce
+import Data.Coerce (coerce)
 
 -- * Safe types and operations
 
@@ -134,6 +135,10 @@
 assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l
 assertDistinct _ = unsafeDistinct
 
+-- | A distinct scope extended with a 'NameBinder' is also distinct.
+assertExt :: NameBinder n l -> ExtEvidence n l
+assertExt _ = unsafeExt
+
 -- | Safely rename (if necessary) a given name to extend a given scope.
 -- This is similar to 'withFresh', except if the name does not clash with
 -- the scope, it can be used immediately, without renaming.
@@ -155,6 +160,37 @@
   | nameOf binder == name = Nothing
   | otherwise = Just (UnsafeName raw)
 
+-- * Unification of binders
+
+-- | Unification result for two binders,
+-- extending some common scope to scopes @l@ and @r@ respectively.
+--
+-- Due to the implementation of the foil,
+data UnifyNameBinders n l r where
+  -- | Binders are the same, proving that type parameters @l@ and @r@
+  -- are in fact equivalent.
+  SameNameBinders :: UnifyNameBinders n l l
+  -- | It is possible to safely rename the left binder
+  -- to match the right one.
+  RenameLeftNameBinder :: (NameBinder n l -> NameBinder n r) -> UnifyNameBinders n l r
+  -- | It is possible to safely rename the right binder
+  -- to match the left one.
+  RenameRightNameBinder :: (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r
+
+-- | Unify binders either by asserting that they are the same,
+-- or by providing a /safe/ renaming function to convert one binder to another.
+unifyNameBinders
+  :: forall i l r.
+     NameBinder i l
+  -> NameBinder i r
+  -> UnifyNameBinders i l r
+unifyNameBinders (UnsafeNameBinder (UnsafeName i1)) (UnsafeNameBinder (UnsafeName i2))
+  | i1 == i2  = unsafeCoerce (SameNameBinders @l)  -- equal names extend scopes equally
+  | i1 < i2   = RenameRightNameBinder $ \(UnsafeNameBinder (UnsafeName i'')) ->
+      if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')
+  | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->
+      if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')
+
 -- * Safe sinking
 
 -- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,
@@ -195,6 +231,31 @@
   -> r
 extendRenaming _ pattern cont =
   cont unsafeCoerce (unsafeCoerce pattern)
+
+-- | Extend renaming of binders when going under a 'CoSinkable' pattern (generalized binder).
+-- Note that the scope under pattern is independent of the codomain of the renaming.
+extendNameBinderRenaming
+  :: CoSinkable pattern
+  => (NameBinder i n -> NameBinder i n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
+  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.
+  -> (forall l'. (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r )
+  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
+  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
+  -> r
+extendNameBinderRenaming _ pattern cont =
+  cont unsafeCoerce (unsafeCoerce pattern)
+
+-- | Safely compose renamings of name binders.
+-- The underlying implementation is
+composeNameBinderRenamings
+  :: (NameBinder n i -> NameBinder n i')    -- ^ Rename binders extending scope @n@ from @i@ to @i'@.
+  -> (NameBinder i' l -> NameBinder i' l')  -- ^ Rename binders extending scope @i'@ from @l@ to @l'@.
+  -> (NameBinder n l -> NameBinder n l')
+composeNameBinderRenamings = unsafeCoerce (flip (.))
+
+-- | Convert renaming of name binders into renaming of names in the inner scopes.
+fromNameBinderRenaming :: (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
+fromNameBinderRenaming = coerce
 
 -- | Extend renaming when going under a 'NameBinder'.
 -- Note that the scope under binder is independent of the codomain of the renaming.
diff --git a/src/Control/Monad/Foil/Relative.hs b/src/Control/Monad/Foil/Relative.hs
--- a/src/Control/Monad/Foil/Relative.hs
+++ b/src/Control/Monad/Foil/Relative.hs
@@ -21,3 +21,7 @@
   -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,
   -- preserving the more general type signature for 'rbind'.
   rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b
+
+-- | Relative version of 'liftM' (an 'fmap' restricted to 'Monad').
+liftRM :: (RelMonad f m, Distinct b) => Scope b -> (f a -> f b) -> m a -> m b
+liftRM scope f m = rbind scope m (rreturn . f)
diff --git a/src/Control/Monad/Foil/TH/Util.hs b/src/Control/Monad/Foil/TH/Util.hs
--- a/src/Control/Monad/Foil/TH/Util.hs
+++ b/src/Control/Monad/Foil/TH/Util.hs
@@ -24,3 +24,6 @@
 tvarName = \case
   PlainTV name _ -> name
   KindedTV name _ _ -> name
+
+removeName :: VarBangType -> BangType
+removeName (_name, bang_, type_) = (bang_, type_)
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
@@ -8,6 +8,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE UndecidableInstances  #-}
 -- | This module defines a variation of
@@ -20,7 +21,13 @@
 import           Control.DeepSeq
 import qualified Control.Monad.Foil.Internal as Foil
 import qualified Control.Monad.Foil.Relative as Foil
+import           Data.Bifoldable
 import           Data.Bifunctor
+import           Data.Bifunctor.Sum
+import           Data.Coerce                 (coerce)
+import           Data.Map                    (Map)
+import qualified Data.Map                    as Map
+import           Data.Monoid                 (All (..))
 import           GHC.Generics                (Generic)
 
 -- | Scoped term under a (single) name binder.
@@ -53,6 +60,8 @@
 instance Foil.InjectName (AST sig) where
   injectName = Var
 
+-- * Substitution
+
 -- | Substitution for free (scoped monads).
 substitute
   :: (Bifunctor sig, Foil.Distinct o)
@@ -71,6 +80,31 @@
             body' = substitute scope' subst' body
         in ScopedAST binder' body'
 
+-- | Substitution for free (scoped monads).
+--
+-- This is a version of 'substitute' that forces refreshing of all name binders,
+-- resulting in a term with normalized binders:
+--
+-- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst
+--
+-- In general, 'substitute' is more efficient since it does not always refresh binders.
+substituteRefreshed
+  :: (Bifunctor sig, Foil.Distinct o)
+  => Foil.Scope o
+  -> Foil.Substitution (AST sig) i o
+  -> AST sig i
+  -> AST sig o
+substituteRefreshed scope subst = \case
+  Var name -> Foil.lookupSubst subst name
+  Node node -> Node (bimap f (substituteRefreshed scope subst) node)
+  where
+    f (ScopedAST binder body) =
+      Foil.withFresh scope $ \binder' ->
+        let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder')
+            scope' = Foil.extendScope binder' scope
+            body' = substituteRefreshed scope' subst' body
+        in ScopedAST binder' body'
+
 -- | @'AST' sig@ is a monad relative to 'Foil.Name'.
 instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where
   rreturn = Var
@@ -87,3 +121,200 @@
                           Nothing -> Foil.rreturn (Foil.nameOf binder')
                           Just n  -> Foil.sink (subst n)
            in ScopedAST binder' (Foil.rbind scope' body subst')
+
+-- * \(\alpha\)-equivalence
+
+-- | Refresh (force) all binders in a term, minimizing the used indices.
+refreshAST
+  :: (Bifunctor sig, Foil.Distinct n)
+  => Foil.Scope n
+  -> AST sig n
+  -> AST sig n
+refreshAST scope = \case
+  t@Var{} -> t
+  Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)
+
+-- | Similar to `refreshAST`, but for scoped terms.
+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n)
+  => Foil.Scope n
+  -> ScopedAST sig n
+  -> ScopedAST sig n
+refreshScopedAST scope (ScopedAST binder body) =
+  Foil.withFresh scope $ \binder' ->
+    let scope' = Foil.extendScope binder' scope
+        subst = Foil.addRename (Foil.sink Foil.identitySubst) binder (Foil.nameOf binder')
+    in ScopedAST binder' (substituteRefreshed scope' subst body)
+
+-- | \(\alpha\)-equivalence check for two terms in one scope
+-- via normalization of bound identifiers (via 'refreshAST').
+--
+-- Compared to 'alphaEquiv', this function may perform some unnecessary
+-- changes of bound variables when the binders are the same on both sides.
+alphaEquivRefreshed
+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
+  => Foil.Scope n
+  -> AST sig n
+  -> AST sig n
+  -> Bool
+alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2
+
+-- | \(\alpha\)-equivalence check for two terms in one scope
+-- via unification of bound variables (via 'unifyNameBinders').
+--
+-- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
+-- changes of bound variables when both binders in two matching scoped terms coincide.
+alphaEquiv
+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
+  => Foil.Scope n
+  -> AST sig n
+  -> AST sig n
+  -> Bool
+alphaEquiv _scope (Var x) (Var y) = x == coerce y
+alphaEquiv scope (Node l) (Node r) =
+  case zipMatch l r of
+    Nothing -> False
+    Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)
+alphaEquiv _ _ _ = False
+
+-- | Same as 'alphaEquiv' but for scoped terms.
+alphaEquivScoped
+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
+  => Foil.Scope n
+  -> ScopedAST sig n
+  -> ScopedAST sig n
+  -> Bool
+alphaEquivScoped scope
+  (ScopedAST binder1 body1)
+  (ScopedAST binder2 body2) =
+    case Foil.unifyNameBinders binder1 binder2 of
+      -- if binders are the same, then we can safely compare bodies
+      Foil.SameNameBinders ->  -- after seeing this we know that body scopes are the same
+        case Foil.assertDistinct binder1 of
+          Foil.Distinct ->
+            let scope1 = Foil.extendScope binder1 scope
+            in alphaEquiv scope1 body1 body2
+      -- if we can safely rename first binder into second
+      Foil.RenameLeftNameBinder rename1to2 ->
+        case Foil.assertDistinct binder2 of
+          Foil.Distinct ->
+            let scope2 = Foil.extendScope binder2 scope
+            in alphaEquiv scope2 (Foil.liftRM scope2 (Foil.fromNameBinderRenaming rename1to2) body1) body2
+      -- if we can safely rename second binder into first
+      Foil.RenameRightNameBinder rename2to1 ->
+        case Foil.assertDistinct binder1 of
+          Foil.Distinct ->
+            let scope1 = Foil.extendScope binder1 scope
+            in alphaEquiv scope1 body1 (Foil.liftRM scope1 (Foil.fromNameBinderRenaming rename2to1) body2)
+
+-- ** Unsafe equality checks
+
+-- | /Unsafe/ equality check for two terms.
+-- 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).
+unsafeEqAST
+  :: (Bifoldable sig, ZipMatch sig)
+  => AST sig n
+  -> AST sig l
+  -> Bool
+unsafeEqAST (Var x) (Var y) = x == coerce y
+unsafeEqAST (Node t1) (Node t2) =
+  case zipMatch t1 t2 of
+    Nothing -> False
+    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
+unsafeEqAST _ _ = False
+
+-- | A version of 'unsafeEqAST' for scoped terms.
+unsafeEqScopedAST
+  :: (Bifoldable sig, ZipMatch sig)
+  => ScopedAST sig n
+  -> ScopedAST sig l
+  -> Bool
+unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
+  [ binder1 == coerce binder2
+  , body1 `unsafeEqAST` body2
+  ]
+
+-- ** Syntactic matching (unification)
+
+-- | Perform one-level matching for the two (non-variable) terms.
+class ZipMatch sig where
+  zipMatch
+    :: sig scope term     -- ^ Left non-variable term.
+    -> sig scope' term'   -- ^ Right non-variable term.
+    -> Maybe (sig (scope, scope') (term, term'))
+
+instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
+  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'
+  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'
+  zipMatch _ _            = Nothing
+
+-- * Converting to and from free foil
+
+-- ** Convert to free foil
+
+convertToAST
+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)
+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
+  -> (rawPattern -> Maybe rawIdent)
+  -> (rawScopedTerm -> rawTerm)
+  -> Foil.Scope n
+  -> Map rawIdent (Foil.Name n) -> rawTerm -> AST sig n
+convertToAST toSig getPatternBinder getScopedTerm scope names t =
+  case toSig t of
+    Left x ->
+      case Map.lookup x names of
+        Nothing   -> error "undefined variable"
+        Just name -> Var name
+    Right node -> Node $
+      bimap
+        (convertToScopedAST toSig getPatternBinder getScopedTerm scope names)
+        (convertToAST toSig getPatternBinder getScopedTerm scope names)
+        node
+
+convertToScopedAST
+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)
+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
+  -> (rawPattern -> Maybe rawIdent)
+  -> (rawScopedTerm -> rawTerm)
+  -> Foil.Scope n
+  -> Map rawIdent (Foil.Name n)
+  -> (rawPattern, rawScopedTerm)
+  -> ScopedAST sig n
+convertToScopedAST toSig getPatternBinder getScopedTerm scope names (pat, scopedTerm) =
+  Foil.withFresh scope $ \binder ->
+    let scope' = Foil.extendScope binder scope
+        names' =
+          case getPatternBinder pat of
+            Nothing -> Foil.sink <$> names
+            Just x  -> Map.insert x (Foil.nameOf binder) (Foil.sink <$> names)
+     in ScopedAST binder (convertToAST toSig getPatternBinder getScopedTerm scope' names' (getScopedTerm scopedTerm))
+
+-- ** Convert from free foil
+
+convertFromAST
+  :: Bifunctor sig
+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
+  -> (rawIdent -> rawTerm)
+  -> (rawIdent -> rawPattern)
+  -> (rawTerm -> rawScopedTerm)
+  -> (Int -> rawIdent) -> AST sig n -> rawTerm
+convertFromAST fromSig fromVar makePattern makeScoped f = \case
+  Var x -> fromVar (f (Foil.nameId x))
+  Node node -> fromSig $
+    bimap
+      (convertFromScopedAST fromSig fromVar makePattern makeScoped f)
+      (convertFromAST fromSig fromVar makePattern makeScoped f)
+      node
+
+convertFromScopedAST
+  :: Bifunctor sig
+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
+  -> (rawIdent -> rawTerm)
+  -> (rawIdent -> rawPattern)
+  -> (rawTerm -> rawScopedTerm)
+  -> (Int -> rawIdent) -> ScopedAST sig n -> (rawPattern, rawScopedTerm)
+convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case
+  ScopedAST binder body ->
+    ( makePattern (f (Foil.nameId (Foil.nameOf binder)))
+    , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))
diff --git a/src/Control/Monad/Free/Foil/TH.hs b/src/Control/Monad/Free/Foil/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/TH.hs
@@ -0,0 +1,11 @@
+module Control.Monad.Free.Foil.TH (
+  module Control.Monad.Free.Foil.TH.Signature,
+  module Control.Monad.Free.Foil.TH.PatternSynonyms,
+  module Control.Monad.Free.Foil.TH.Convert,
+  module Control.Monad.Free.Foil.TH.ZipMatch,
+) where
+
+import Control.Monad.Free.Foil.TH.Signature
+import Control.Monad.Free.Foil.TH.PatternSynonyms
+import Control.Monad.Free.Foil.TH.Convert
+import Control.Monad.Free.Foil.TH.ZipMatch
diff --git a/src/Control/Monad/Free/Foil/TH/Convert.hs b/src/Control/Monad/Free/Foil/TH/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/TH/Convert.hs
@@ -0,0 +1,272 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Control.Monad.Free.Foil.TH.Convert where
+
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Syntax
+
+import           Control.Monad.Foil.TH.Util
+
+-- * Bulk generators
+
+-- | Generate helpers for conversion to scope-safe representation.
+-- Includes 'mkConvertToSig', 'mkGetPatternBinder', and 'mkGetScopedTerm'.
+mkConvertToFreeFoil
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkConvertToFreeFoil termT nameT scopeT patternT = concat <$> sequence
+  [ mkConvertToSig termT nameT scopeT patternT
+  , mkGetPatternBinder nameT patternT
+  , mkGetScopedTerm termT scopeT
+  ]
+
+-- | Generate helpers for conversion from scope-safe representation.
+-- Includes 'mkConvertFromSig'.
+mkConvertFromFreeFoil
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkConvertFromFreeFoil termT nameT scopeT patternT = concat <$> sequence
+  [ mkConvertFromSig termT nameT scopeT patternT
+  ]
+
+-- * Individual generators
+
+-- | Generate conversion helper that goes unpeels one node from a raw term.
+mkConvertToSig
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkConvertToSig termT nameT scopeT patternT = do
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
+  TyConI (NewtypeD _ctx _name nameTVars _kind _nameCons _deriv) <- reify nameT
+
+  convertTermToSigClauses <- concat <$> mapM toClause termCons
+
+  let params = map (VarT . tvarName) termTVars
+      termType = return $ PeelConT termT params
+      nameType = return $ PeelConT nameT (map (VarT . tvarName) nameTVars)
+      scopeType = return $ PeelConT scopeT params
+      patternType = return $ PeelConT patternT params
+      signatureType = return $ PeelConT signatureT params
+  convertTermToSigClausesType <-
+    [t| $termType -> Either $nameType ($signatureType ($patternType, $scopeType) $termType) |]
+
+  addModFinalizer $ putDoc (DeclDoc convertTermToSigT)
+    ("/Generated/ with '" ++ show 'mkConvertToFreeFoil ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")
+  return
+    [ SigD convertTermToSigT convertTermToSigClausesType
+    , FunD convertTermToSigT convertTermToSigClauses
+    ]
+  where
+    signatureT = mkName (nameBase termT ++ "Sig")
+    convertTermToSigT = mkName ("convertTo" ++ nameBase signatureT)
+
+    toClause :: Con -> Q [Clause]
+    toClause = \case
+      NormalC conName types | any isVarP pats
+        -> return [Clause [ConP conName [] pats] (NormalB (AppE (ConE 'Left) (VarE x))) []]
+        where
+          x = mkName "x"
+          isVarP VarP{} = True
+          isVarP _ = False
+          pats =
+            [ case type_ of
+                PeelConT typeName _ | typeName == nameT -> VarP x
+                _ -> WildP
+            | (_bang, type_) <- types ]
+      NormalC conName types -> mkClause conName conName' types
+        where
+          conName' = mkName (nameBase conName ++ "Sig")
+      RecC conName types -> toClause (NormalC conName (map removeName types))
+      InfixC l conName r -> mkClause conName conName' [l, r]
+        where
+          conName' = mkName (nameBase conName ++ "---")
+      ForallC _ _ con -> toClause con
+      GadtC conNames types _retType -> concat <$> mapM (\conName -> toClause (NormalC conName types)) conNames
+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)
+
+    mkClause conName conName' types = return
+      [ Clause [ConP conName [] pats] (NormalB (AppE (ConE 'Right) (foldl AppE (ConE conName') (concat args)))) [] ]
+      where
+        p = mkName "p"
+        (pats, args) = unzip
+          [ case type_ of
+              PeelConT typeName _
+                | typeName == patternT -> (VarP p, [])
+                | typeName == scopeT -> (VarP x, [TupE [Just (VarE p), Just (VarE x)]])
+              _ -> (VarP x, [VarE x])
+          | (i, (_bang, type_)) <- zip [0..] types
+          , let x = mkName ("x" ++ show i)
+          ]
+
+-- | Generate conversion helper that peels back one node to a raw term.
+mkConvertFromSig
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkConvertFromSig termT nameT scopeT patternT = do
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
+  TyConI (NewtypeD _ctx _name _nameTVars _kind _nameCons _deriv) <- reify nameT
+
+  convertTermFromSigClauses <- concat <$> mapM toClause termCons
+
+  let params = map (VarT . tvarName) termTVars
+      termType = return $ PeelConT termT params
+      scopeType = return $ PeelConT scopeT params
+      patternType = return $ PeelConT patternT params
+      signatureType = return $ PeelConT signatureT params
+  convertTermFromSigClausesType <-
+    [t| $signatureType ($patternType, $scopeType) $termType -> $termType |]
+
+  addModFinalizer $ putDoc (DeclDoc convertTermFromSigT)
+    ("/Generated/ with '" ++ show 'mkConvertToFreeFoil ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")
+  return
+    [ SigD convertTermFromSigT convertTermFromSigClausesType
+    , FunD convertTermFromSigT convertTermFromSigClauses
+    ]
+  where
+    signatureT = mkName (nameBase termT ++ "Sig")
+    convertTermFromSigT = mkName ("convertFrom" ++ nameBase signatureT)
+
+    toClause :: Con -> Q [Clause]
+    toClause = \case
+      NormalC _conName types | or [ typeName == nameT | (_bang, PeelConT typeName _typeParams) <- types ]
+        -> pure []
+      NormalC conName types -> mkClause conName conName' types
+        where
+          conName' = mkName (nameBase conName ++ "Sig")
+      RecC conName types -> toClause (NormalC conName (map removeName types))
+      InfixC l conName r -> mkClause conName conName' [l, r]
+        where
+          conName' = mkName (nameBase conName ++ "---")
+      ForallC _ _ con -> toClause con
+      GadtC conNames types _retType -> concat <$> mapM (\conName -> toClause (NormalC conName types)) conNames
+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)
+
+    mkClause conName conName' types = return
+      [ Clause [ConP conName' [] (concat pats)] (NormalB (foldl AppE (ConE conName) args)) [] ]
+      where
+        p = mkName "p"
+        (args, pats) = unzip
+          [ case type_ of
+              PeelConT typeName _
+                | typeName == patternT -> (VarE p, [])
+                | typeName == scopeT -> (VarE x, [TupP [VarP p, VarP x]])
+              _ -> (VarE x, [VarP x])
+          | (i, (_bang, type_)) <- zip [0..] types
+          , let x = mkName ("x" ++ show i)
+          ]
+
+-- | Generate a helper that extracts at most one binder from a pattern.
+mkGetPatternBinder
+  :: Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkGetPatternBinder nameT patternT = do
+  TyConI (NewtypeD _ctx _name nameTVars _kind _nameCons _deriv) <- reify nameT
+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
+
+  getPatternBinderClauses <- concat <$> mapM toClause patternCons
+
+  let nameType = return $ PeelConT nameT (map (VarT . tvarName) nameTVars)
+      patternType = return $ PeelConT patternT (map (VarT . tvarName) patternTVars)
+  getPatternBinderClausesType <-
+    [t| $patternType -> Maybe $nameType |]
+
+  addModFinalizer $ putDoc (DeclDoc getPatternBinderT)
+    ("/Generated/ with '" ++ show 'mkGetPatternBinder ++ "'. Extract at most one binder from a pattern or __crash__.")
+  return
+    [ SigD getPatternBinderT getPatternBinderClausesType
+    , FunD getPatternBinderT getPatternBinderClauses
+    ]
+  where
+    getPatternBinderT = mkName ("get" ++ nameBase patternT ++ "Binder")
+
+    toClause :: Con -> Q [Clause]
+    toClause = \case
+      NormalC conName types -> mkClause conName types
+      RecC conName types -> toClause (NormalC conName (map removeName types))
+      InfixC l conName r -> toClause (NormalC conName [l, r])
+      ForallC _ _ con -> toClause con
+      GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames
+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)
+
+    mkClause :: Name -> [BangType] -> Q [Clause]
+    mkClause conName types = do
+      body <- case concat vars of
+        [] -> [e| Nothing |]
+        [Just y] -> [e| Just $y |]
+        _ -> [e| error "complex patterns are not supported" |]
+      return [ Clause [ConP conName [] pats] (NormalB body) [] ]
+      where
+        x = mkName "x"
+        (pats, vars) = unzip
+          [ case type_ of
+              PeelConT typeName _
+                | typeName == nameT -> (VarP x, [Just (return (VarE x))])
+                | typeName == patternT -> (WildP, [Nothing])
+              _ -> (WildP, [])
+          | (_bang, type_) <- types
+          ]
+
+-- | Generate a helper that extracts a term from a scoped term.
+mkGetScopedTerm
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Q [Dec]
+mkGetScopedTerm termT scopeT = do
+  TyConI (DataD _ctx _name termTVars _kind _termCons _deriv) <- reify termT
+  TyConI (DataD _ctx _name _scopeTVars _kind scopeCons _deriv) <- reify scopeT
+
+  getScopedTermClauses <- concat <$> mapM toClause scopeCons
+
+  let params = map (VarT . tvarName) termTVars
+      termType = return $ PeelConT termT params
+      scopeType = return $ PeelConT scopeT params
+  getScopedTermClausesType <-
+    [t| $scopeType -> $termType |]
+
+  addModFinalizer $ putDoc (DeclDoc getScopedTermT)
+    ("/Generated/ with '" ++ show 'mkGetScopedTerm ++ "'. Extract scoped term or __crash__.")
+  return
+    [ SigD getScopedTermT getScopedTermClausesType
+    , FunD getScopedTermT getScopedTermClauses
+    ]
+  where
+    getScopedTermT = mkName ("get" ++ nameBase termT ++ "From" ++ nameBase scopeT)
+
+    toClause :: Con -> Q [Clause]
+    toClause = \case
+      NormalC conName types -> mkClause conName types
+      RecC conName types -> toClause (NormalC conName (map removeName types))
+      InfixC l conName r -> toClause (NormalC conName [l, r])
+      ForallC _ _ con -> toClause con
+      GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames
+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)
+
+    mkClause :: Name -> [BangType] -> Q [Clause]
+    mkClause conName types = do
+      body <- case concat vars of
+        [y] -> [e| $y |]
+        _ -> [e| error "complex patterns are not supported" |]
+      return [ Clause [ConP conName [] pats] (NormalB body) [] ]
+      where
+        x = mkName "x"
+        (pats, vars) = unzip
+          [ case type_ of
+              PeelConT typeName _
+                | typeName == termT -> (VarP x, [return (VarE x)])
+              _ -> (WildP, [])
+          | (_bang, type_) <- types
+          ]
diff --git a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns    #-}
+module Control.Monad.Free.Foil.TH.PatternSynonyms where
+
+import Control.Monad (forM_)
+import qualified Control.Monad.Foil         as Foil
+import           Control.Monad.Foil.TH.Util
+import           Control.Monad.Free.Foil
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Syntax
+
+-- | Generate helpful pattern synonyms given a signature bifunctor.
+mkPatternSynonyms
+  :: Name -- ^ Type name for the signature bifunctor.
+  -> Q [Dec]
+mkPatternSynonyms signatureT = do
+  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT
+
+  case reverse signatureTVars of
+    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do
+      concat <$> mapM (mkPatternSynonym (PeelConT signatureT (map (VarT . tvarName) params)) scope term) signatureCons
+    _ -> fail "cannot generate pattern synonyms"
+
+mkPatternSynonym :: Type -> Name -> Name -> Con -> Q [Dec]
+mkPatternSynonym signatureType scope term = \case
+  NormalC conName types -> mkPatternSynonym signatureType scope term
+    (GadtC [conName] types (AppT (AppT signatureType (VarT scope)) (VarT term)))
+
+  RecC conName types -> mkPatternSynonym signatureType scope term (NormalC conName (map removeName types))
+
+  InfixC l conName r -> mkPatternSynonym signatureType scope term (NormalC conName [l, r])
+
+  ForallC params ctx con -> do
+    [ PatSynSigD patName patType, patD ] <- mkPatternSynonym signatureType scope term con
+    return
+      [ PatSynSigD patName (ForallT params ctx patType)
+      , patD
+      ]
+
+  GadtC conNames types _retType -> do
+    let argsWithTypes = zipWith toPatternArgType [0..] types
+        argsWithTypes' = foldMap collapse argsWithTypes
+        pats   = map toArg argsWithTypes
+        args  = map fst argsWithTypes'
+        types' = map snd argsWithTypes'
+    forM_ conNames $ \conName ->
+      addModFinalizer $ putDoc (DeclDoc (mkPatternName conName))
+        ("/Generated/ with '" ++ show 'mkPatternSynonyms ++ "'. Pattern synonym for an '" ++ show ''AST ++ "' node of type '" ++ show conName ++ "'.")
+    return $ concat
+      [ [ PatSynSigD patternName (foldr (AppT . AppT ArrowT) termType types')
+        , PatSynD  patternName (PrefixPatSyn args) ImplBidir (ConP 'Node [] [ConP conName [] pats])
+        ]
+      | conName <- conNames
+      , let patternName = mkPatternName conName
+      ]
+
+  RecGadtC conNames types retType -> mkPatternSynonym signatureType scope term (GadtC conNames (map removeName types) retType)
+
+  where
+    n = mkName "n"
+    termType = PeelConT ''AST [signatureType, VarT n]
+    toArg = \case
+      Left ((b, _), (x, _)) -> ConP 'ScopedAST [] [VarP b, VarP x]
+      Right (x, _) -> VarP x
+
+    toPatternArgType i (_bang, VarT typeName)
+      | typeName == scope =
+          Left
+            ( (mkName ("b" ++ show i), PeelConT ''Foil.NameBinder [VarT n, VarT l])
+            , (mkName ("x" ++ show i), PeelConT ''AST [signatureType, VarT l]))
+      | typeName == term =
+          Right (mkName ("x" ++ show i), PeelConT ''AST [signatureType, VarT n])
+      where
+        l = mkName ("l" ++ show i)
+    toPatternArgType i (_bang, type_)
+      = Right (mkName ("z" ++ show i), type_)
+
+    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))
+    dropEnd k = reverse . drop k . reverse
+
+    collapse = \case
+      Left (x, y) -> [x, y]
+      Right x -> [x]
diff --git a/src/Control/Monad/Free/Foil/TH/Signature.hs b/src/Control/Monad/Free/Foil/TH/Signature.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/TH/Signature.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Control.Monad.Free.Foil.TH.Signature where
+
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Syntax
+
+import           Control.Monad              (forM_)
+import           Control.Monad.Foil.TH.Util
+import           Data.Maybe                 (catMaybes)
+
+-- | Generate a signature for the free foil (or free scoped monads)
+-- based on a naïve recursive abstract syntax representation,
+-- with clearly separated types for terms, variable identifiers, scoped terms,
+-- and patterns (binders).
+mkSignature
+  :: Name -- ^ Type name for raw terms.
+  -> Name -- ^ Type name for raw variable identifiers.
+  -> Name -- ^ Type name for raw scoped terms.
+  -> Name -- ^ Type name for raw patterns.
+  -> Q [Dec]
+mkSignature termT nameT scopeT patternT = do
+  scope <- newName "scope"
+  term <- newName "term"
+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT
+
+  signatureCons <- catMaybes <$> mapM (toSignatureCons scope term) termCons
+
+  addModFinalizer $ putDoc (DeclDoc signatureT)
+    ("/Generated/ with '" ++ show 'mkSignature ++ "'. A signature bifunctor, specifying the nodes of a syntax tree corresponding to '" ++ show termT ++ "'.")
+  return
+    [ DataD [] signatureT (termTVars ++ [PlainTV scope BndrReq, PlainTV term BndrReq]) Nothing signatureCons
+      [DerivClause Nothing [ConT ''Functor, ConT ''Foldable, ConT ''Traversable]]
+    ]
+  where
+    signatureT = mkName (nameBase termT ++ "Sig")
+
+    toSignatureCons :: Name -> Name -> Con -> Q (Maybe Con)
+    toSignatureCons scope term con' = case con' of
+      -- treat constructors with a single variable field as variable constructor and ignore
+      NormalC _conName types | or [ typeName == nameT | (_bang, PeelConT typeName _typeParams) <- types ]
+        -> pure Nothing
+      RecC _conName types | or [ typeName == nameT | (_name, _bang, PeelConT typeName _typeParams) <- types ]
+        -> pure Nothing
+
+      NormalC conName params -> do
+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")
+        Just . NormalC conName' . catMaybes <$> mapM toSignatureParam params
+        where
+          conName' = mkName (nameBase conName ++ "Sig")
+      RecC conName params -> do
+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")
+        Just . RecC conName' . catMaybes <$> mapM toSignatureParam' params
+        where
+          conName' = mkName (nameBase conName ++ "Sig")
+      InfixC l conName r -> do
+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")
+        Just <$> (flip InfixC conName' <$> toInfixParam l <*> toInfixParam r)
+        where
+          conName' = mkName (nameBase conName ++ "---")
+      ForallC params ctx con -> fmap (ForallC params ctx) <$> toSignatureCons scope term con
+      GadtC conNames argTypes retType -> do
+        let conNames' = map (\conName -> mkName (nameBase conName ++ "---")) conNames
+        forM_ (zip conNames conNames') $ \(conName, conName') ->
+          addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")
+        Just <$> (GadtC conNames' <$> (catMaybes <$> mapM toSignatureParam argTypes) <*> retType')
+        where
+          retType' = case retType of
+            PeelConT typeName typeParams
+              | typeName == termT -> return (PeelConT signatureT (typeParams ++ [VarT scope, VarT term]))
+            _ -> fail "unexpected return type in a GADT constructor"
+      RecGadtC conNames argTypes retType -> do
+        let conNames' = map (\conName -> mkName (nameBase conName ++ "---")) conNames
+        forM_ (zip conNames conNames') $ \(conName, conName') ->
+          addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")
+        Just <$> (RecGadtC conNames' <$> (catMaybes <$> mapM toSignatureParam' argTypes) <*> retType')
+        where
+          retType' = case retType of
+            PeelConT typeName typeParams
+              | typeName == termT -> return (PeelConT signatureT (typeParams ++ [VarT scope, VarT term]))
+            _ -> fail "unexpected return type in a GADT constructor"
+
+      where
+        toInfixParam (bang_, type_) = toSignatureParam (bang_, type_) >>= \case
+          Nothing -> pure (bang_, VarT ''())
+          Just bt -> pure bt
+
+        toSignatureParam' (name, bang_, type_) = fmap k <$> toSignatureParam (bang_, type_)
+          where
+            k (x, y) = (name, x, y)
+
+        toSignatureParam (bang_, PeelConT typeName _typeParams)
+          | typeName == nameT = fail ("variable with other stuff in constructor: " ++ show con')
+          | typeName == patternT = pure Nothing -- skip binders, they will be inserted automatically with each scoped term
+          | typeName == scopeT = pure (Just (bang_, VarT scope))
+          | typeName == termT = pure (Just (bang_, VarT term))
+        toSignatureParam bt = pure (Just bt)  -- everything else remains as is
diff --git a/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
+{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Control.Monad.Free.Foil.TH.ZipMatch where
+
+import           Language.Haskell.TH
+
+import           Control.Monad.Foil.TH.Util
+import           Control.Monad.Free.Foil
+
+-- | Generate 'ZipMatch' instance for a given bifunctor.
+deriveZipMatch
+  :: Name -- ^ Type name for the signature bifunctor.
+  -> Q [Dec]
+deriveZipMatch signatureT = do
+  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT
+
+  case reverse signatureTVars of
+    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do
+      let signatureType = PeelConT signatureT (map (VarT . tvarName) params)
+      clauses <- concat <$> mapM (toClause scope term) signatureCons
+      let defaultClause = Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []
+      let instType = AppT (ConT ''ZipMatch) signatureType
+
+      return
+        [ InstanceD Nothing [] instType
+          [ FunD 'zipMatch (clauses ++ [defaultClause]) ]
+        ]
+    _ -> fail "cannot generate pattern synonyms"
+
+  where
+    toClause :: Name -> Name -> Con -> Q [Clause]
+    toClause scope term = go
+      where
+        go = \case
+          NormalC conName types -> mkClause conName types
+          RecC conName types -> go (NormalC conName (map removeName types))
+          InfixC l conName r -> go (NormalC conName [l, r])
+          ForallC _ _ con -> go con
+          GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames
+          RecGadtC conNames types retType -> go (GadtC conNames (map removeName types) retType)
+
+        mkClause :: Name -> [BangType] -> Q [Clause]
+        mkClause conName types = return
+          [Clause [ConP conName [] lpats, ConP conName [] rpats]
+            (NormalB (AppE (ConE 'Just) (foldl AppE (ConE conName) args))) []]
+          where
+            (lpats, rpats, args) = unzip3
+              [ case type_ of
+                  VarT typeName
+                    | typeName `elem` [scope, term] -> (VarP l, VarP r, TupE [Just (VarE l), Just (VarE r)])
+                  _ -> (VarP l, WildP, VarE l)
+              | (i, (_bang, type_)) <- zip [0..] types
+              , let l = mkName ("l" ++ show i)
+              , let r = mkName ("r" ++ show i)
+              ]