diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal
index 41748029..e9f83e8a 100644
--- a/haskell/free-foil/free-foil.cabal
+++ b/haskell/free-foil/free-foil.cabal
@@ -31,6 +31,7 @@ library
       Control.Monad.Foil
       Control.Monad.Foil.Example
       Control.Monad.Foil.Internal
+      Control.Monad.Foil.Internal.ValidNameBinders
       Control.Monad.Foil.Relative
       Control.Monad.Foil.TH
       Control.Monad.Foil.TH.MkFoilData
diff --git a/haskell/free-foil/src/Control/Monad/Foil.hs b/haskell/free-foil/src/Control/Monad/Foil.hs
index 70831de2..8bc63a3a 100644
--- a/haskell/free-foil/src/Control/Monad/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil.hs
@@ -35,8 +35,10 @@ module Control.Monad.Foil (
   unsinkName,
   unsinkNamePattern,
   -- * Safe (co)sinking and renaming
+  SinkableK(..),
   Sinkable(..),
   CoSinkable(..),
+  HasNameBinders(getNameBinders),
   sink,
   extendRenaming,
   extendNameBinderRenaming,
diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
index 67c7b2a1..b2d2210d 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
@@ -1,17 +1,25 @@
+{-# OPTIONS_GHC -Wno-missing-methods #-}  -- disabled to avoid overlapping type instances
+{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-inaccessible-code #-}  -- disabled because I think GHC is wrong
+{-# LANGUAGE AllowAmbiguousTypes        #-}
 {-# LANGUAGE BlockArguments             #-}
 {-# LANGUAGE ConstraintKinds            #-}
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DeriveTraversable          #-}
 {-# LANGUAGE EmptyCase                  #-}
+{-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE InstanceSigs               #-}
 {-# LANGUAGE KindSignatures             #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE QuantifiedConstraints      #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
 {-# LANGUAGE UndecidableInstances       #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
@@ -37,15 +45,20 @@
 -- — the number of bits in an 'Int' (32 or 64).
 module Control.Monad.Foil.Internal where
 
-import           Control.DeepSeq (NFData (..))
-import           Data.Coerce     (coerce)
+import           Control.DeepSeq    (NFData (..))
+import           Data.Bifunctor
+import           Data.Coerce        (coerce)
 import           Data.IntMap
-import qualified Data.IntMap     as IntMap
+import qualified Data.IntMap        as IntMap
 import           Data.IntSet
-import qualified Data.IntSet     as IntSet
-import           Data.Kind       (Type)
+import qualified Data.IntSet        as IntSet
+import           Data.Kind          (Type)
+import qualified Data.Type.Equality as Type
+import           Generics.Kind
 import           Unsafe.Coerce
 
+import Control.Monad.Foil.Internal.ValidNameBinders
+
 -- * Safe types and operations
 
 -- | 'S' is a data kind of scope indices.
@@ -564,6 +577,16 @@ instance UnifiablePattern U2 where
 class CoSinkable pattern => UnifiablePattern pattern where
   -- | Unify two patterns and decide which binders need to be renamed.
   unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
+  default unifyPatterns
+    :: (CoSinkable pattern, Distinct n)
+    => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
+  unifyPatterns l r = coerce (unifyPatterns (nameBinderListOf l) (nameBinderListOf r))
+
+instance UnifiablePattern NameBinderList where
+  unifyPatterns NameBinderListEmpty NameBinderListEmpty = SameNameBinders emptyNameBinders
+  unifyPatterns (NameBinderListCons x xs) (NameBinderListCons y ys) =
+    case (assertDistinct x, assertDistinct y) of
+      (Distinct, Distinct) -> unifyNameBinders x y `andThenUnifyPatterns` (xs, ys)
 
 -- | Unification of values in patterns.
 -- By default, 'Eq' instance is used, but it may be useful to ignore
@@ -600,6 +623,10 @@ class Sinkable (e :: S -> Type) where
     -> e n                  -- ^ Expression with free variables in scope @n@.
     -> e l
 
+  default sinkabilityProof
+    :: (GenericK e, GSinkableK (RepK e)) => (Name n -> Name l) -> e n -> e l
+  sinkabilityProof rename = toK . gsinkabilityProof1 rename . fromK
+
 -- | Sinking a 'Name' is as simple as applying the renaming.
 instance Sinkable Name where
   sinkabilityProof rename = rename
@@ -689,6 +716,14 @@ class CoSinkable (pattern :: S -> S -> Type) where
     -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
     -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
     -> r
+  default coSinkabilityProof
+    :: (GenericK pattern, GSinkableK (RepK pattern))
+    => (Name n -> Name n')
+    -> pattern n l
+    -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)
+    -> r
+  coSinkabilityProof rename p cont = gsinkabilityProof2 rename (fromK @_ @pattern p) $ \rename' p' ->
+    cont rename' (toK @_ @pattern p')
 
   -- | Generalized processing of a pattern.
   --
@@ -708,6 +743,16 @@ class CoSinkable (pattern :: S -> S -> Type) where
     -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
     -> r
+  default withPattern
+    :: (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))
+    => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')
+    -> (forall x z z'. DExt z z' => f x x z z')
+    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')
+    -> Scope o
+    -> pattern n l
+    -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
+    -> r
+  withPattern = gunsafeWithPatternViaHasNameBinders
 
 -- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'.
 newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
@@ -912,3 +957,378 @@ type DExt n l = (Distinct l, Ext n l)
 class InjectName (e :: S -> Type) where
   -- | Inject names into expressions.
   injectName :: Name n -> e n
+
+-- * Kind-polymorphic sinkability
+
+data RenamingsK (as :: LoT k) (bs :: LoT k) where
+  RNil :: RenamingsK LoT0 LoT0
+  RCons :: (Name a -> Name b) -> RenamingsK as bs -> RenamingsK (a :&&: as) (b :&&: bs)
+  RSkip :: RenamingsK as bs -> RenamingsK (k :&&: as) (k :&&: bs)
+
+class SinkableK (f :: S -> k) where
+  sinkabilityProofK
+    :: forall as bs r.
+       RenamingsK as bs
+    -> f :@@: as
+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)
+    -> r
+  default sinkabilityProofK :: forall as bs r.
+      (GenericK f, GSinkableK (RepK f))
+    => RenamingsK as bs
+    -> f :@@: as
+    -> (forall cs. RenamingsK as cs -> f :@@: cs -> r)
+    -> r
+  sinkabilityProofK rename e cont =
+    gsinkabilityProofK rename (fromK @_ @f e) $ \rename' e' ->
+      cont rename' (toK @_ @f e')
+
+sinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f :@@: as -> f :@@: bs
+sinkK _ _ = unsafeCoerce
+
+instance SinkableK Name where
+  sinkabilityProofK renameK@(RCons rename RNil) name cont = cont renameK (rename name)
+instance SinkableK NameBinder where
+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinder name) cont =
+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinder name)
+instance SinkableK NameBinders where
+  sinkabilityProofK (RCons _ RNil) (UnsafeNameBinders s) cont =
+    cont (RCons unsafeCoerce RNil) (UnsafeNameBinders s)
+
+instance GenericK NameBinderList where
+  type RepK NameBinderList = ((Var0 :~~: Var1) :=>: U1) :+: Exists S
+    (Field (NameBinder :$: Var1 :@: Var0) :*: Field (NameBinderList :$: Var0 :@: Var2))
+  toK (L1 (SuchThat U1))                   = NameBinderListEmpty
+  toK (R1 (Exists (Field x :*: Field xs))) = NameBinderListCons x xs
+  fromK NameBinderListEmpty       = L1 (SuchThat U1)
+  fromK (NameBinderListCons x xs) = R1 (Exists (Field x :*: Field xs))
+
+instance GenericK V2 where
+  type RepK V2 = V1
+  toK _v1 = error "absurd: Generics.Kind.V1"
+  fromK = absurd2
+
+instance GenericK U2 where
+  type RepK U2 = ((Var0 :~~: Var1) :=>: U1)
+  toK (SuchThat U1) = U2
+  fromK U2 = SuchThat U1
+
+instance SinkableK NameBinderList
+instance SinkableK V2
+instance SinkableK U2
+
+sinkabilityProof1 :: SinkableK f => (Name n -> Name n') -> f n -> f n'
+sinkabilityProof1 rename e = sinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'
+
+gsinkabilityProof1 :: GSinkableK f => (Name n -> Name n') -> f (n :&&: LoT0) -> f (n' :&&: LoT0)
+gsinkabilityProof1 rename e = gsinkabilityProofK (RCons rename RNil) e $ \_ e' -> unsafeCoerce e'
+
+gsinkabilityProof2
+  :: forall f n n' l r. GSinkableK f
+  => (Name n -> Name n') -> f (n :&&: l :&&: LoT0)
+  -> (forall l'. (Name l -> Name l') -> f (n' :&&: l' :&&: LoT0) -> r)
+  -> r
+gsinkabilityProof2 rename e cont =
+  gsinkabilityProofK (RCons rename (RCons id RNil)) e $ \case
+    RCons (_ :: Name n -> Name n'') (RCons rename' RNil) -> \e' ->
+      case unsafeCoerce (Type.Refl :: n' Type.:~: n') :: n' Type.:~: n'' of
+        Type.Refl -> cont rename' e'
+
+gsinkabilityProofK' :: GSinkableK f => RenamingsK as bs -> f as -> f bs
+gsinkabilityProofK' renameK e = gsinkabilityProofK renameK e $ \_ e' -> unsafeCoerce e'
+
+class GSinkableK p where
+  gsinkabilityProofK
+    :: forall as bs r.
+       RenamingsK as bs
+    -> p as
+    -> (forall cs. RenamingsK as cs -> p cs -> r)
+    -> r
+
+gsinkK :: GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f as -> f bs
+gsinkK _ _ = unsafeCoerce
+
+instance GSinkableK V1 where
+  gsinkabilityProofK irename _v1 cont =
+    cont irename (error "absurd: Generics.Kind.V1")
+
+instance GSinkableK U1 where
+  gsinkabilityProofK irename U1 cont =
+    cont irename U1
+
+instance GSinkableK f => GSinkableK (M1 i c f) where
+  gsinkabilityProofK irename (M1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (M1 x')
+
+instance (GSinkableK f, GSinkableK g) => GSinkableK (f :+: g) where
+  gsinkabilityProofK irename (L1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (L1 x')
+  gsinkabilityProofK irename (R1 x) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      cont irename' (R1 x')
+
+instance (GSinkableK f, GSinkableK g) => GSinkableK (f :*: g) where
+  gsinkabilityProofK irename (x :*: y) cont =
+    gsinkabilityProofK irename x $ \irename' x' ->
+      gsinkabilityProofK irename' y $ \irename'' y' ->
+        cont irename'' (gsinkK irename' irename'' x' :*: y')
+
+instance GSinkableK f => GSinkableK (Exists S f) where
+  gsinkabilityProofK irename (Exists x) cont =
+    gsinkabilityProofK (RCons id irename) x $ \case
+      RCons _ irename' -> \x' ->
+        cont irename' (Exists x')
+
+instance {-# OVERLAPPABLE #-} GSinkableK f => GSinkableK (Exists k f) where
+  gsinkabilityProofK irename (Exists x) cont =
+    gsinkabilityProofK (RSkip irename) x $ \case
+      RSkip irename' -> \x' ->
+        cont irename' (Exists x')
+
+instance GSinkableK f => GSinkableK ((a :~~: b) :=>: f) where
+  gsinkabilityProofK irename (SuchThat x) cont =
+    gsinkabilityProofK irename x $ \(irename' :: RenamingsK as cs) x' ->
+      -- this is sort of safe...
+      case unsafeCoerce (Type.Refl :: Interpret a cs Type.:~: Interpret a cs) :: Interpret a cs Type.:~: Interpret b cs of
+        Type.Refl -> cont irename' (SuchThat x')
+
+instance GSinkableK (Field (Kon a)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field x)
+
+instance GSinkableK (Field (Var a)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (unsafeCoerce x)) -- FIXME: unsafeCoerce?
+
+instance (SinkableK f, ExtractRenamingK i) => GSinkableK (Field (Kon f :@: Var i)) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (RCons (extractRenamingK @_ @i irename) RNil) x $ \case
+      RCons rename' RNil -> \x' ->
+        cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce?
+
+instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where
+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
+    sinkabilityProofK irename x $ \rename' x' ->
+      cont rename' (Field x')
+
+instance SinkableK (f a b) => GSinkableK (Field (Kon f :@: Kon a :@: Kon b :@: Var0)) where
+  gsinkabilityProofK irename@(RCons _ RNil) (Field x) cont =
+    sinkabilityProofK irename x $ \rename' x' ->
+      cont rename' (Field x')
+
+class ExtractRenamingK (i :: TyVar k S) where
+  extractRenamingK :: forall (as :: LoT k) (bs :: LoT k).
+    RenamingsK as bs -> Name (Interpret (Var i) as) -> Name (Interpret (Var i) bs)
+  putBackRenamingK :: forall c (as :: LoT k) (bs :: LoT k).
+       (Name (Interpret (Var i) as) -> Name c)
+    -> RenamingsK as bs
+    -> RenamingsK as (PutBackLoT i c bs)
+
+instance ExtractRenamingK VZ where
+  extractRenamingK (RCons f _fs) = f
+  putBackRenamingK f (RCons _ gs) = RCons f gs
+
+instance ExtractRenamingK x => ExtractRenamingK (VS x) where
+  extractRenamingK (RCons _f fs) = extractRenamingK @_ @x fs
+  putBackRenamingK f (RCons g gs) = RCons g (putBackRenamingK @_ @x f gs)
+
+extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK as bs
+  -> RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (Interpret (Var i) bs :&&: Interpret (Var j) bs :&&: LoT0)
+extractTwoRenamingsK irename =
+  (RCons (extractRenamingK @_ @i irename) (RCons (extractRenamingK @_ @j irename) RNil))
+
+putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) c1 c2 (as :: LoT k) (bs :: LoT k).
+    (ExtractRenamingK i, ExtractRenamingK j)
+  => RenamingsK
+      (Interpret (Var i) as :&&: Interpret (Var j) as :&&: LoT0)
+      (c1 :&&: c2 :&&: LoT0)
+  -> RenamingsK as bs
+  -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs))
+putBackTwoRenamingsK (RCons f1 (RCons f2 RNil)) rename
+  = putBackRenamingK @_ @j f2 (putBackRenamingK @_ @i f1 rename)
+
+instance (SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field (Kon f :@: Var (i :: TyVar k S) :@: Var (j :: TyVar k S))) where
+  gsinkabilityProofK irename (Field x) cont =
+    sinkabilityProofK (extractTwoRenamingsK @_ @i @j irename) x $ \rename' x' ->
+      case rename' of
+        RCons _ (RCons _ RNil) ->
+          cont (putBackTwoRenamingsK @_ @i @j rename' irename)
+              (Field (unsafeCoerce x'))  -- FIXME: can we do better than unsafeCoerce?
+
+instance (Functor f, GSinkableK (Field x)) => GSinkableK (Field (Kon f :@: x)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (fmap
+      (unField . gsinkabilityProofK' @(Field x) irename . Field)
+      x))
+
+instance (Bifunctor f, GSinkableK (Field x), GSinkableK (Field y)) => GSinkableK (Field (Kon f :@: x :@: y)) where
+  gsinkabilityProofK irename (Field x) cont =
+    cont irename (Field (bimap
+      (unField . gsinkabilityProofK' @(Field x) irename . Field)
+      (unField . gsinkabilityProofK' @(Field y) irename . Field)
+      x))
+
+-- * Kind-polymorphic types with binders
+
+-- ** Generic version of 'withPattern'
+
+-- | Generic generalized processing of a pattern via 'GHasNameBinders'.
+--
+-- This can be used as a default implementation of 'withPattern'.
+gunsafeWithPatternViaHasNameBinders
+  :: forall pattern f o n l r.
+      (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))
+  => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')
+  -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern.
+  -> (forall x z z'. DExt z z' => f x x z z')
+  -- ^ Result in case no binders are present. This can be seen as scope-indexed 'mempty'.
+  -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')
+  -- ^ Composition of results for nested binders/patterns. This can be seen as scope-indexed 'mappend'.
+  -> Scope o
+  -- ^ Ambient scope.
+  -> pattern n l
+  -- ^ Pattern to process.
+  -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
+  -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
+  -> r
+gunsafeWithPatternViaHasNameBinders withBinder id_ comp_ scope pat cont =
+  withPattern withBinder id_ comp_ scope (ggetNameBinders pat) $ \result binders ->
+    cont result (gunsafeSetNameBinders (unsafeCoerce pat) binders) -- FIXME: safer version
+
+-- ** Manipulating nested 'NameBinder's
+-- | If @'HasNameBinders' f@, then @f n l@ is expected to act as a binder,
+-- introducing into scope @n@ some local variables, extending it to scope @l@.
+-- This class allows to extract and modify the set of binders.
+class HasNameBinders f where
+  -- | Extract a set of binders from a pattern.
+  getNameBinders :: f n l -> NameBinders n l
+  getNameBinders = UnsafeNameBinders . IntSet.fromList . getNameBindersRaw
+
+  -- | Replace binders in a pattern.
+  --
+  -- This function is unsafe, because it does not check if the new set of binders
+  -- has the same size. It can therefore crash at runtime.
+  --
+  -- You should probably not use this.
+  -- This is only used for 'gunsafeWithPatternViaHasNameBinders', which is then safe to use.
+  unsafeSetNameBinders :: f n l -> NameBinders n l' -> f n l'
+  unsafeSetNameBinders e (UnsafeNameBinders m) = fst (reallyUnsafeSetNameBindersRaw e (IntSet.toList m))
+
+  -- | Extract 'RawName's of all binders occurring in a pattern.
+  getNameBindersRaw :: f n l -> [RawName]
+  default getNameBindersRaw :: forall n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> [RawName]
+  getNameBindersRaw = ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)
+
+  -- | This is a version of 'unsafeSetNameBinders'
+  -- that takes in a list of 'RawName's.
+  --
+  -- It does not check if the given list has enough elements.
+  -- It does not check if the raw names are fresh in the scope @n@.
+  -- It does not check if the raw names given are distinct.
+  --
+  -- You should never use this. This is only used for generic implementation of 'HasNameBinders'.
+  reallyUnsafeSetNameBindersRaw :: f n l -> [RawName] -> (f n l', [RawName])
+  default reallyUnsafeSetNameBindersRaw :: forall n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName])
+  reallyUnsafeSetNameBindersRaw e names =
+    let (e', names') = greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) names
+     in (toK @_ @f @(n :&&: l' :&&: LoT0) e', names')
+
+instance HasNameBinders NameBinder where
+  getNameBindersRaw (UnsafeNameBinder (UnsafeName name)) = [name]
+  reallyUnsafeSetNameBindersRaw _ (name:names) = (UnsafeNameBinder (UnsafeName name), names)
+
+instance HasNameBinders NameBinderList
+
+-- ** Generic
+
+ggetNameBinders :: forall f n l. (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l
+ggetNameBinders = UnsafeNameBinders . IntSet.fromList . ggetNameBindersRaw . fromK @_ @f @(n :&&: l :&&: LoT0)
+
+gunsafeSetNameBinders :: forall f n l l'. (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l'
+gunsafeSetNameBinders e (UnsafeNameBinders m) = toK @_ @f @(n :&&: l' :&&: LoT0) $
+  fst (greallyUnsafeSetNameBindersRaw (fromK @_ @f @(n :&&: l :&&: LoT0) e) (IntSet.toList m))
+
+class GHasNameBinders f where
+  ggetNameBindersRaw :: f as -> [RawName]
+  greallyUnsafeSetNameBindersRaw :: f as -> [RawName] -> (f bs, [RawName])
+
+instance GHasNameBinders V1 where
+  ggetNameBindersRaw _ = error "absurd: Generics.Kind.V1"
+  greallyUnsafeSetNameBindersRaw _ _ = error "absurd: Generics.Kind.V1"
+instance GHasNameBinders U1 where
+  ggetNameBindersRaw U1 = []
+  greallyUnsafeSetNameBindersRaw U1 names = (U1, names)
+
+instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :+: g) where
+  ggetNameBindersRaw (L1 x) = ggetNameBindersRaw x
+  ggetNameBindersRaw (R1 x) = ggetNameBindersRaw x
+
+  greallyUnsafeSetNameBindersRaw (L1 x) names = first L1 (greallyUnsafeSetNameBindersRaw x names)
+  greallyUnsafeSetNameBindersRaw (R1 x) names = first R1 (greallyUnsafeSetNameBindersRaw x names)
+
+-- | FIXME: this is, perhaps, the most "unsafe" place for the user
+-- since it does not reject "parallel" binders:
+--
+--    data BadPattern n l = BadPattern (NameBinder n l) (NameBinder n l)
+--
+-- This instance will treat both binders in the same way as "nested":
+--
+--    data GoodPattern n l = forall i. GoodPattern (NameBinder n i) (NameBinder i l)
+--
+-- However, Template Haskell code at the moment will never generate "parallel" binders,
+-- and the very user is unlikely to misuse this instance, since "parallel" binders
+-- require extra effort to support it.
+--
+-- Still, it would be better to detect and reject any "parallel" or otherwise improper binders.
+instance (GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :*: g) where
+  ggetNameBindersRaw (x :*: y) = ggetNameBindersRaw x <> ggetNameBindersRaw y
+  greallyUnsafeSetNameBindersRaw (x :*: y) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+        (y', names'') = greallyUnsafeSetNameBindersRaw y names'
+     in (x' :*: y', names'')
+
+instance GHasNameBinders f => GHasNameBinders (M1 i c f) where
+  ggetNameBindersRaw (M1 x) = ggetNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (M1 x) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+     in (M1 x', names')
+
+instance GHasNameBinders f => GHasNameBinders (Var i :~~: Var j :=>: f) where
+  ggetNameBindersRaw (SuchThat x) = ggetNameBindersRaw x
+
+  greallyUnsafeSetNameBindersRaw :: forall as bs. (Var i :~~: Var j :=>: f) as -> [RawName] -> ((Var i :~~: Var j :=>: f) bs, [RawName])
+  greallyUnsafeSetNameBindersRaw (SuchThat x) names =
+    -- this is sort of safe...
+    case unsafeCoerce (Type.Refl :: Interpret (Var i) bs Type.:~: Interpret (Var i) bs) :: Interpret (Var i) bs Type.:~: Interpret (Var j) bs of
+      Type.Refl ->
+        let (x', names') = greallyUnsafeSetNameBindersRaw x names
+         in (SuchThat x', names')
+
+instance GHasNameBinders f => GHasNameBinders (Exists k f) where
+  ggetNameBindersRaw (Exists x) = ggetNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (Exists x) names =
+    let (x', names') = greallyUnsafeSetNameBindersRaw x names
+     in (Exists x', names')
+
+instance GHasNameBinders (Field (Kon a)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field x, names)
+
+instance GHasNameBinders (Field (Var x)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names)  -- FIXME: unsafeCoerce?
+
+instance GHasNameBinders (Field (Kon f :@: Var i)) where
+  ggetNameBindersRaw (Field _x) = []
+  greallyUnsafeSetNameBindersRaw (Field x) names = (Field (unsafeCoerce x), names) -- FIXME: unsafeCoerce?
+
+instance HasNameBinders f => GHasNameBinders (Field (Kon f :@: Var i :@: Var j)) where
+  ggetNameBindersRaw (Field x) = getNameBindersRaw x
+  greallyUnsafeSetNameBindersRaw (Field x) names =
+    let (x', names') = reallyUnsafeSetNameBindersRaw x names
+     in (Field (unsafeCoerce x'), names') -- FIXME: safer version?
diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs
new file mode 100644
index 00000000..a562950d
--- /dev/null
+++ b/haskell/free-foil/src/Control/Monad/Foil/Internal/ValidNameBinders.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE StandaloneKindSignatures  #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators  #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE TypeFamilies  #-}
+{-# LANGUAGE PolyKinds  #-}
+{-# LANGUAGE DataKinds  #-}
+module Control.Monad.Foil.Internal.ValidNameBinders where
+
+import Data.Kind (Type, Constraint)
+import GHC.TypeError
+import GHC.TypeLits
+import Generics.Kind
+import qualified GHC.Generics as GHC
+
+type SubstInRepK :: TyVar d k -> Atom d k -> (LoT d -> Type) -> LoT d -> Type
+type family SubstInRepK i atom f where
+  SubstInRepK i atom V1 = V1
+  SubstInRepK i atom U1 = U1
+  SubstInRepK i atom (M1 info c f) = M1 info c (SubstInRepK i atom f)
+  SubstInRepK i atom (Field field) = Field (SubstInAtom i atom field)
+  SubstInRepK i atom f =
+    TypeError
+      ('Text "cannot substitute variable"
+      :$$: 'Text "  " :<>: 'ShowType (Var i)
+      :$$: 'Text "with atom"
+      :$$: 'Text "  " :<>: 'ShowType atom
+      :$$: 'Text "in"
+      :$$: 'Text "  " :<>: 'ShowType f)
+
+type SubstInAtom :: TyVar d k -> Atom d k -> Atom d k1 -> Atom d k1
+type family SubstInAtom i atom f where
+  SubstInAtom i atom (Var i) = atom
+  SubstInAtom i atom (Var j) = Var j
+  SubstInAtom i atom (Kon a) = Kon a
+  SubstInAtom i atom (f :@: x) = SubstInAtom i atom f :@: SubstInAtom i atom x
+  -- SubstInAtom i atom atom' = atom'
+  SubstInAtom i atom atom' =
+    TypeError
+      ('Text "cannot substitute variable"
+      :$$: 'Text "  " :<>: 'ShowType (Var i)
+      :$$: 'Text "with atom"
+      :$$: 'Text "  " :<>: 'ShowType atom
+      :$$: 'Text "in an atom"
+      :$$: 'Text "  " :<>: 'ShowType atom')
+
+type ShowKindedScope oo n ll = ShowScope oo n ll :<>: 'Text " : S"
+
+type ShowScope :: Atom d s -> Atom d s -> Atom d s -> ErrorMessage
+type family ShowScope oo n ll where
+  ShowScope oo ll ll = 'Text "innerScope"
+  ShowScope oo oo ll = 'Text "outerScope"
+  ShowScope oo n  ll = ShowScopeN 1 n
+
+type ShowScopeN :: Natural -> Atom d s -> ErrorMessage
+type family ShowScopeN i n where
+  ShowScopeN i (Var VZ) = 'Text "scope" :<>: 'ShowType i
+  ShowScopeN i (Var (VS x)) = ShowScopeN (i + 1) (Var x)
+
+type ShowSaturatedPatternType pattern oo n l ll =
+  'ShowType pattern :<>: 'Text " " :<>: ShowScope oo n ll :<>: 'Text " " :<>: ShowScope oo l ll
+
+type GInnerScopeOfAtom :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> Atom d Type -> Atom d s -> Atom d s -> Atom d s -> Atom d s
+type family GInnerScopeOfAtom msg icon ifield pattern atom oo n ll where
+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: n :@: l) oo n ll = l
+  GInnerScopeOfAtom msg icon ifield pattern (Kon f :@: o :@: i) oo n ll =
+    TypeError
+      ('Text "Unexpected Foil scope extension in the binder/pattern"
+      :$$: 'Text "  " :<>: ShowSaturatedPatternType f oo o i ll
+      :$$: 'Text "the binder/pattern tries to extend scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo o ll
+      :$$: 'Text "to scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo i ll
+      :$$: 'Text "but it is expected to extend the current (outer) scope"
+      :$$: 'Text "  " :<>: ShowKindedScope oo n ll
+      :$$: ShowLocalizeError msg icon ifield pattern oo ll
+      )
+  GInnerScopeOfAtom msg icon ifield pattern atom oo n ll = n
+
+type SameInnerScope :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom k s -> Atom k s -> Atom k s
+type family SameInnerScope msg icon pattern n l where
+  SameInnerScope msg icon pattern l l = l
+  SameInnerScope msg icon pattern n l =
+    TypeError
+      ('Text "Unexpected extended (inner) Foil scope in the data type"
+      :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l
+      :$$: 'Text "expecting extended (inner) scope to be"
+      :$$: 'Text "  " :<>: ShowKindedScope n l l
+      :$$: 'Text "but the inferred extended (inner) scope is"
+      :$$: 'Text "  " :<>: ShowKindedScope n n l
+      :$$: ShowLocalizeError msg icon 0 pattern n l
+      )
+
+type GValidNameBinders :: (s -> s -> Type) -> (LoT (s -> s -> Type) -> Type) -> Constraint
+type family GValidNameBinders pattern f :: Constraint where
+  GValidNameBinders pattern (f :: LoT (s -> s -> Type) -> Type) =
+    (GInnerScopeOfRepK ('Text "") 0 0 pattern f Var0 Var0 Var1)
+    ~ (Var1 :: Atom (s -> s -> Type) s)
+
+type AtomSucc :: Atom d k1 -> Atom (k -> d) k1
+type family AtomSucc atom where
+  AtomSucc (Var i) = Var (VS i)
+
+type AtomUnSucc :: ErrorMessage -> Nat -> (s -> s -> Type) -> Atom d s -> Atom d s -> Atom (k -> d) k1 -> Atom d k1
+type family AtomUnSucc msg icon pattern oo ll atom where
+  AtomUnSucc msg icon pattern oo ll (Var (VS i)) = Var i
+  AtomUnSucc msg icon pattern oo ll (Var VZ) = TypeError
+    ('Text "Intermediate scope escapes existential quantification for data type"
+      :$$: ShowLocalizeError msg icon 0 pattern oo ll
+      )
+
+type family First x y where
+  First (Var x) (Var y) = Var x
+
+type family AndShowFieldNumber ifield msg where
+  AndShowFieldNumber 0 msg = msg
+  AndShowFieldNumber n msg =
+    'Text "when checking field number " :<>: 'ShowType n
+    :$$: msg
+
+type family AndShowConNumber icon msg where
+  AndShowConNumber 0 msg = msg
+  AndShowConNumber n msg =
+    'Text "when checking constructor number " :<>: 'ShowType n
+    :$$: msg
+
+type AndShowDataType pattern n l msg =
+  'Text "when tracking Foil scopes for the data type"
+  :$$: 'Text "  " :<>: ShowSaturatedPatternType pattern n n l l
+  :$$: msg
+
+type ShowLocalizeError msg icon ifield pattern o l =
+    AndShowFieldNumber ifield
+      (AndShowConNumber icon
+        (AndShowDataType pattern o l
+          msg))
+
+type family CountCons f where
+  CountCons (f :+: g) = CountCons f + CountCons g
+  CountCons (M1 GHC.C c f) = 1
+
+type family CountFields f where
+  CountFields (f :*: g) = CountFields f + CountFields g
+  CountFields (M1 GHC.S c f) = 1
+
+type GInnerScopeOfRepK :: ErrorMessage -> Nat -> Nat -> (s -> s -> Type) -> (LoT k -> Type) -> Atom k s -> Atom k s -> Atom k s -> Atom k s
+type family GInnerScopeOfRepK msg icon ifield pattern f o n l where
+  GInnerScopeOfRepK msg icon ifield pattern V1 o n l = l
+  GInnerScopeOfRepK msg icon ifield pattern U1 o n l = n
+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.C c f) o n l =
+    GInnerScopeOfRepK msg icon 1 pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (M1 GHC.D c f) o n l =
+    GInnerScopeOfRepK msg 1 ifield pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (M1 i c f) o n l =
+    GInnerScopeOfRepK msg icon ifield pattern f o n l
+  GInnerScopeOfRepK msg icon ifield pattern (f :+: g) o n l = First
+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg icon ifield pattern f o n l) l)
+    (SameInnerScope msg icon pattern (GInnerScopeOfRepK msg (icon + CountCons f) ifield pattern g o n l) l)
+  GInnerScopeOfRepK msg icon ifield pattern (f :*: g) o n l =
+    GInnerScopeOfRepK msg icon (ifield + CountFields f) pattern g o
+      (GInnerScopeOfRepK msg icon ifield pattern f o n l) l
+  GInnerScopeOfRepK msg icon ifield pattern (Var i :~~: Var j :=>: f) o n l =
+    GInnerScopeOfRepK msg icon ifield pattern (SubstInRepK i (Var j) f)
+      (SubstInAtom i (Var j) o) (SubstInAtom i (Var j) n) (SubstInAtom i (Var j) l)
+  GInnerScopeOfRepK msg icon ifield pattern (Exists k f) o n l =
+    AtomUnSucc msg icon pattern o l
+      (GInnerScopeOfRepK msg icon ifield pattern f (AtomSucc o) (AtomSucc n) (AtomSucc l))
+  GInnerScopeOfRepK msg icon ifield pattern (Field atom) o n l = GInnerScopeOfAtom msg icon ifield pattern atom o n l
+  GInnerScopeOfRepK msg icon ifield pattern f o n l =
+    TypeError
+      ('Text "Unsupported structure in a binder/pattern"
+      :$$: 'Text "  " :<>: 'ShowType f
+      :$$: ShowLocalizeError msg icon 0 pattern n l)
+
+type PutBackLoT :: TyVar d s -> s -> LoT k -> LoT k
+type family PutBackLoT i c bs where
+  PutBackLoT VZ c (b :&&: bs) = c :&&: bs
+  PutBackLoT (VS x) c (b :&&: bs) = b :&&: PutBackLoT x c bs
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
index eeb77ddd..9d310755 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -26,6 +28,8 @@ import           Data.Bifoldable
 import           Data.Bitraversable
 import           Data.Bifunctor
 import Data.ZipMatchK
+import qualified Generics.Kind as Kind
+import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))
 import           Data.Coerce                 (coerce)
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
@@ -53,14 +57,25 @@ deriving instance Generic (AST binder sig n)
 deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
   => NFData (AST binder sig n)
 
-instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) where
-  sinkabilityProof rename = \case
-    Var name -> Var (rename name)
-    Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)
-    where
-      f (ScopedAST binder body) =
-        Foil.extendRenaming rename binder $ \rename' binder' ->
-          ScopedAST binder' (Foil.sinkabilityProof rename' body)
+instance GenericK (ScopedAST binder sig) where
+  type RepK (ScopedAST binder sig) =
+    Exists Foil.S
+      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))
+  toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast
+  fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)
+
+instance GenericK (AST binder sig) where
+  type RepK (AST binder sig) =
+    Field (Foil.Name :$: Var0)
+    :+: Field (sig
+                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)
+                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))
+
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)
+
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)
 
 instance Foil.InjectName (AST binder sig) where
   injectName = Var
@@ -69,7 +84,7 @@ instance Foil.InjectName (AST binder sig) where
 
 -- | Substitution for free (scoped monads).
 substitute
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
   -> Foil.Substitution (AST binder sig) i o
   -> AST binder sig i
@@ -94,7 +109,7 @@ substitute scope subst = \case
 --
 -- In general, 'substitute' is more efficient since it does not always refresh binders.
 substituteRefreshed
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o
   -> Foil.Substitution (AST binder sig) i o
   -> AST binder sig i
@@ -111,7 +126,8 @@ substituteRefreshed scope subst = \case
         in ScopedAST binder' body'
 
 -- | @'AST' sig@ is a monad relative to 'Foil.Name'.
-instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST binder sig) where
+instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)
+  => Foil.RelMonad Foil.Name (AST binder sig) where
   rreturn = Var
   rbind scope term subst =
     case term of
@@ -127,7 +143,7 @@ instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST
 
 -- | Substitution for a single generalized pattern.
 substitutePattern
-  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope o                           -- ^ Resulting scope.
   -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.
   -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.
@@ -143,7 +159,7 @@ substitutePattern scope env binders args body =
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.
 refreshAST
-  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
+  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -152,7 +168,7 @@ refreshAST scope = \case
   Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)
 
 -- | Similar to `refreshAST`, but for scoped terms.
-refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -168,7 +184,7 @@ refreshScopedAST scope (ScopedAST binder body) =
 -- Compared to 'alphaEquiv', this function may perform some unnecessary
 -- changes of bound variables when the binders are the same on both sides.
 alphaEquivRefreshed
-  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -181,7 +197,7 @@ alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST s
 -- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
 -- changes of bound variables when both binders in two matching scoped terms coincide.
 alphaEquiv
-  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -195,7 +211,7 @@ alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
 alphaEquivScoped
-  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
index 043c773e..7e7242ea 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -13,13 +14,18 @@
 {-# LANGUAGE TemplateHaskell            #-}
 {-# LANGUAGE TypeApplications           #-}
 -- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs)
--- using Template Haskell to reduce boilerplate.
+-- using Template Haskell and "Generics.Kind" to reduce boilerplate.
 --
 -- Template Haskell helpers __generate__ the following:
 --
 -- 1. Scope-safe AST, generated from a raw definition. See 'FoilTerm', 'FoilScopedTerm', and 'FoilPattern'.
--- 2. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm' and 'fromFoilTerm'.
--- 3. Helper functions for patterns. See 'extendScopeFoilPattern' and 'withRefreshedFoilPattern'.
+-- 2. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm'' and 'fromFoilTerm''.
+-- 3. Helper functions for patterns. See 'extendScopeFoilPattern'' and 'withRefreshedFoilPattern''.
+--
+-- The following is provided via kind-polymophic generics (see "Generics.Kind"):
+--
+-- 1. 'Sinkable' instance for 'FoilTerm''.
+-- 2. 'CoSinkable' instance for 'FoilPattern'', giving access to 'extendScopePattern' and 'withRefreshedPattern' (among other utilities).
 --
 -- The following is implemented __manually__ in this module:
 --
@@ -43,13 +49,25 @@ import qualified Language.LambdaPi.Syntax.Layout as Raw
 import qualified Language.LambdaPi.Syntax.Lex    as Raw
 import qualified Language.LambdaPi.Syntax.Par    as Raw
 import qualified Language.LambdaPi.Syntax.Print  as Raw
+import           Generics.Kind.TH
 import           System.Exit                     (exitFailure)
 
 -- * Generated code
 
 -- ** Scope-safe AST
 mkFoilData ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
-mkInstancesFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
+-- mkInstancesFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
+
+deriveGenericK ''FoilTerm'
+deriveGenericK ''FoilScopedTerm'
+deriveGenericK ''FoilPattern'
+instance SinkableK (FoilTerm' a)
+instance SinkableK (FoilScopedTerm' a)
+instance SinkableK (FoilPattern' a)
+instance HasNameBinders (FoilPattern' a)
+
+instance Sinkable (FoilTerm' a)
+instance CoSinkable (FoilPattern' a)
 
 -- ** Conversion from raw to scope-safe AST
 mkToFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
@@ -79,14 +97,14 @@ substitute :: Distinct o => Scope o -> Substitution FoilTerm i o -> FoilTerm i -
 substitute scope subst = \case
     FoilVar _loc name -> lookupSubst subst name
     FoilApp loc f x -> FoilApp loc (substitute scope subst f) (substitute scope subst x)
-    FoilLam loc1 pattern (FoilAScopedTerm loc2 body) -> withRefreshedFoilPattern' scope pattern $ \extendSubst pattern' ->
+    FoilLam loc1 pattern (FoilAScopedTerm loc2 body) -> withRefreshedPattern scope pattern $ \extendSubst pattern' ->
       let subst' = extendSubst subst
-          scope' = extendScopeFoilPattern' pattern' scope
+          scope' = extendScopePattern pattern' scope
           body' = substitute scope' subst' body
        in FoilLam loc1 pattern' (FoilAScopedTerm loc2 body')
-    FoilPi loc1 pattern a (FoilAScopedTerm loc2 b) -> withRefreshedFoilPattern' scope pattern $ \extendSubst pattern' ->
+    FoilPi loc1 pattern a (FoilAScopedTerm loc2 b) -> withRefreshedPattern scope pattern $ \extendSubst pattern' ->
       let subst' = extendSubst subst
-          scope' = extendScopeFoilPattern' pattern' scope
+          scope' = extendScopePattern pattern' scope
           a' = substitute scope subst a
           b' = substitute scope' subst' b
        in FoilPi loc1 pattern' a' (FoilAScopedTerm loc2 b')
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
index 948db1f5..90789fcc 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -20,11 +20,16 @@
 -- 3. Correct \(\alpha\)-equivalence checks (see 'alphaEquiv' and 'alphaEquivRefreshed') as well as \(\alpha\)-normalization (see 'refreshAST').
 -- 4. Conversion helpers (see 'convertToAST' and 'convertFromAST').
 --
+-- The following is provided via __generic__ representation via [kind-generics](https://hackage.haskell.org/package/kind-generics) (see "Generics.Kind"):
+-- 1. 'ZipMatch' instances for signatures (enabling general \(\alpha\)-equivalence).
+-- 2. 'Sinkable' instances for terms.
+-- 3. 'CoSinkable' instances for patterns.
+--
 -- The following is __generated__ using Template Haskell:
 --
--- 1. Convenient pattern synonyms.
--- 2. 'ZipMatch' instances (enabling general \(\alpha\)-equivalence).
--- 3. Conversion between scope-safe and raw term representation.
+-- 1. Signature bifunctor for terms.
+-- 2. Convenient pattern synonyms.
+-- 4. Conversion between scope-safe and raw term representation.
 --
 -- The following is implemented __manually__ in this module:
 --
@@ -80,14 +85,17 @@ mkConvertFromFreeFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern
 -- ** Scope-safe patterns
 
 mkFoilPattern ''Raw.VarIdent ''Raw.Pattern'
-deriveCoSinkable ''Raw.VarIdent ''Raw.Pattern'
+deriveGenericK ''FoilPattern'
+instance Foil.SinkableK (FoilPattern' a)
+instance Foil.HasNameBinders (FoilPattern' a)
+instance Foil.CoSinkable (FoilPattern' a)
 mkToFoilPattern ''Raw.VarIdent ''Raw.Pattern'
 mkFromFoilPattern ''Raw.VarIdent ''Raw.Pattern'
 
+instance Foil.UnifiablePattern (FoilPattern' a)
 -- | Ignoring location information when unifying patterns.
 instance Foil.UnifiableInPattern Raw.BNFC'Position where
   unifyInPattern _ _  = True
-deriveUnifiablePattern ''Raw.VarIdent ''Raw.Pattern'
 
 -- | Deriving 'GHC.Generic' and 'GenericK' instances.
 deriving instance GHC.Generic (Term'Sig a scope term)
diff --git a/haskell/soas/src/Language/SOAS/Impl.hs b/haskell/soas/src/Language/SOAS/Impl.hs
index f6f06298..c082b1c6 100644
--- a/haskell/soas/src/Language/SOAS/Impl.hs
+++ b/haskell/soas/src/Language/SOAS/Impl.hs
@@ -62,12 +62,16 @@ lookupSubst m = find $ \(Subst _loc m' _ _) -> m == m'
 -- | Apply meta variable substitutions to a term.
 --
 -- >>> applySubsts Foil.emptyScope ["?m[x y] ↦ Lam(z. App(z, App(x, y)))"] "Lam(x. ?m[App(x, ?m[x, x]), x])"
--- Lam (x0 . Lam (x2 . App (x2, App (App (x0, ?m [x0, x0]), x0))))
+-- Lam (x0 . Lam (x2 . App (x2, App (App (x0, Lam (x2 . App (x2, App (x0, x0)))), x0))))
+--
+-- >>> applySubsts Foil.emptyScope ["?m[x y] ↦ App(y, x)"] "Lam(f. Lam(x. ?m[?m[x, f], f]))"
+-- Lam (x0 . Lam (x1 . App (x0, App (x0, x1))))
 applySubsts :: Foil.Distinct n => Foil.Scope n -> [Subst] -> Term n -> Term n
 applySubsts scope substs term =
   case term of
     MetaVar _loc m args | Just (Subst _ _ binders body) <- lookupSubst m substs ->
-      substitutePattern scope Foil.voidSubst binders args body
+      let args' = map (applySubsts scope substs) args
+       in substitutePattern scope Foil.voidSubst binders args' body
     Var{} -> term
     -- NOTE: generic recursive processing!
     Node node -> Node (bimap goScoped (applySubsts scope substs) node)
@@ -78,6 +82,26 @@ applySubsts scope substs term =
           let scope' = Foil.extendScopePattern binders scope
            in ScopedAST binders (applySubsts scope' substs body)
 
+-- | Check if a (simultaneous) substitution is a solution to a set of constraints:
+--
+-- >>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x. ?m[?m[x, f], f] = App(f, App(f, x))"]
+-- True
+-- >>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x y. ?m[?m[x, f], f] = App(f, App(f, y))"]
+-- False
+--
+-- >>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, x))))"]
+-- True
+-- >>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ y x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, y))))"]
+-- False
+isSolutionFor :: [Subst] -> [Constraint] -> Bool
+isSolutionFor substs = all isSatisfied
+  where
+    isSatisfied (ConstraintEq _loc binders l r) =
+      case Foil.assertDistinct binders of
+        Foil.Distinct ->
+          let scope = Foil.extendScopePattern binders Foil.emptyScope
+          in alphaEquiv scope (applySubsts scope substs l) (applySubsts scope substs r)
+
 -- * Entrypoint
 
 -- | A SOAS interpreter implemented via the free foil.
diff --git a/haskell/soas/src/Language/SOAS/Impl/Generated.hs b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
index 6385487c..67d39764 100644
--- a/haskell/soas/src/Language/SOAS/Impl/Generated.hs
+++ b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
@@ -44,6 +44,11 @@ deriveGenericK ''OpArg'Sig
 deriveGenericK ''Term'Sig
 deriveGenericK ''OpArgTyping'Sig
 deriveGenericK ''Type'Sig
+deriveGenericK ''Subst'
+deriveGenericK ''Constraint'
+deriveGenericK ''OpTyping'
+deriveGenericK ''Binders'
+deriveGenericK ''TypeBinders'
 
 deriveBifunctor ''OpArg'Sig
 deriveBifunctor ''Term'Sig
@@ -51,45 +56,30 @@ deriveBifunctor ''OpArgTyping'Sig
 deriveBifunctor ''ScopedOpArgTyping'Sig
 deriveBifunctor ''Type'Sig
 
--- FIXME: derive via GenericK
-instance Foil.CoSinkable (Binders' a) where
-  coSinkabilityProof rename (NoBinders loc) cont = cont rename (NoBinders loc)
-  -- coSinkabilityProof rename (OneBinder loc binder) cont =
-  --   Foil.coSinkabilityProof rename binder $ \rename' binder' ->
-  --     cont rename' (OneBinder loc binder')
-  coSinkabilityProof rename (SomeBinders loc binder binders) cont =
-    Foil.coSinkabilityProof rename binder $ \rename' binder' ->
-      Foil.coSinkabilityProof rename' binders $ \rename'' binders' ->
-        cont rename'' (SomeBinders loc binder' binders')
-
-  withPattern withBinder unit comp scope binders cont =
-    case binders of
-      NoBinders loc -> cont unit (NoBinders loc)
-      -- OneBinder loc binder ->
-      --   Foil.withPattern withBinder unit comp scope binder $ \f binder' ->
-      --     cont f (OneBinder loc binder')
-      SomeBinders loc binder moreBinders ->
-        Foil.withPattern withBinder unit comp scope binder $ \f binder' ->
-          let scope' = Foil.extendScopePattern binder' scope
-           in Foil.withPattern withBinder unit comp scope' moreBinders $ \g moreBinders' ->
-                cont (comp f g) (SomeBinders loc binder' moreBinders')
-
--- FIXME: derive via GenericK
-instance Foil.CoSinkable (TypeBinders' a) where
-  coSinkabilityProof rename (NoTypeBinders loc) cont = cont rename (NoTypeBinders loc)
-  coSinkabilityProof rename (SomeTypeBinders loc binder binders) cont =
-    Foil.coSinkabilityProof rename binder $ \rename' binder' ->
-      Foil.coSinkabilityProof rename' binders $ \rename'' binders' ->
-        cont rename'' (SomeTypeBinders loc binder' binders')
-
-  withPattern withBinder unit comp scope binders cont =
-    case binders of
-      NoTypeBinders loc -> cont unit (NoTypeBinders loc)
-      SomeTypeBinders loc binder moreTypeBinders ->
-        Foil.withPattern withBinder unit comp scope binder $ \f binder' ->
-          let scope' = Foil.extendScopePattern binder' scope
-           in Foil.withPattern withBinder unit comp scope' moreTypeBinders $ \g moreTypeBinders' ->
-                cont (comp f g) (SomeTypeBinders loc binder' moreTypeBinders')
+deriveBifoldable ''OpArg'Sig
+deriveBifoldable ''Term'Sig
+deriveBifoldable ''OpArgTyping'Sig
+deriveBifoldable ''ScopedOpArgTyping'Sig
+deriveBifoldable ''Type'Sig
+
+deriveBitraversable ''OpArg'Sig
+deriveBitraversable ''Term'Sig
+deriveBitraversable ''OpArgTyping'Sig
+deriveBitraversable ''ScopedOpArgTyping'Sig
+deriveBitraversable ''Type'Sig
+
+instance Foil.Sinkable (Subst' a)
+instance Foil.Sinkable (Constraint' a)
+instance Foil.Sinkable (OpTyping' a)
+
+instance Foil.SinkableK (Binders' a)
+instance Foil.SinkableK (TypeBinders' a)
+
+instance Foil.HasNameBinders (Binders' a)
+instance Foil.CoSinkable (Binders' a)
+
+instance Foil.HasNameBinders (TypeBinders' a)
+instance Foil.CoSinkable (TypeBinders' a)
 
 mkFreeFoilConversions soasConfig
 
@@ -104,6 +94,8 @@ instance ZipMatchK a => ZipMatchK (Term'Sig a)
 instance ZipMatchK a => ZipMatchK (OpArg'Sig a)
 instance ZipMatchK a => ZipMatchK (Type'Sig a)
 
+instance Foil.UnifiablePattern (Binders' a)
+
 -- |
 -- >>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS
 -- ?m [App (Lam (x0 . x0), Lam (x0 . x0))]