diff --git a/haskell/free-foil/src/Control/Monad/Foil.hs b/haskell/free-foil/src/Control/Monad/Foil.hs
index 7e2228ef..8ba51866 100644
--- a/haskell/free-foil/src/Control/Monad/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil.hs
@@ -54,6 +54,9 @@ module Control.Monad.Foil (
   unifyNameBinders,
   andThenUnifyPatterns,
   UnifiablePattern(..),
+  NameBinders,
+  emptyNameBinders,
+  mergeNameBinders,
   -- ** Eliminating impossible unification
   V2, absurd2,
   -- * Name maps
diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
index 1fabc0f6..cfe5299b 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
@@ -329,91 +329,156 @@ unsinkNamePattern pat = withPattern @_ @n
 -- extending some common scope to scopes @l@ and @r@ respectively.
 --
 -- Due to the implementation of the foil,
-data UnifyNameBinders pattern n l r where
+data UnifyNameBinders (pattern :: S -> S -> Type) n l r where
   -- | Binders are the same, proving that type parameters @l@ and @r@
   -- are in fact equivalent.
-  SameNameBinders :: UnifyNameBinders pattern n l l
+  SameNameBinders :: NameBinders n l -> UnifyNameBinders pattern 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 pattern n l r
+  RenameLeftNameBinder :: NameBinders n r -> (NameBinder n l -> NameBinder n r) -> UnifyNameBinders pattern 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 pattern n l r
+  RenameRightNameBinder :: NameBinders n l -> (NameBinder n r -> NameBinder n l) -> UnifyNameBinders pattern n l r
   -- | It is necessary to rename both binders.
-  RenameBothBinders :: pattern n lr -> (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> UnifyNameBinders pattern n l r
+  RenameBothBinders :: NameBinders n lr -> (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> UnifyNameBinders pattern n l r
   -- | Cannot unify to (sub)patterns.
-  NotUnifiable :: pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
+  NotUnifiable :: UnifyNameBinders pattern 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 pattern.
-     NameBinder i l
+  :: forall i l r pattern. Distinct i
+  => NameBinder i l
   -> NameBinder i r
   -> UnifyNameBinders pattern 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'')) ->
+unifyNameBinders l@(UnsafeNameBinder (UnsafeName i1)) r@(UnsafeNameBinder (UnsafeName i2))
+  | i1 == i2  = case assertDistinct l of
+      Distinct -> unsafeCoerce (SameNameBinders (nameBindersSingleton l))  -- equal names extend scopes equally
+  | i1 < i2   = RenameRightNameBinder (nameBindersSingleton l) $ \(UnsafeNameBinder (UnsafeName i'')) ->
       if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')
-  | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->
+  | otherwise = RenameLeftNameBinder (nameBindersSingleton r) $ \(UnsafeNameBinder (UnsafeName i')) ->
       if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')
 
-unsafeMergeUnifyBinders :: UnifyNameBinders binder a a' a'' -> UnifyNameBinders binder b b' b'' -> UnifyNameBinders binder c c' c''
+unsafeMergeUnifyBinders :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''
 unsafeMergeUnifyBinders = \case
-  SameNameBinders -> unsafeCoerce
-  u@(RenameLeftNameBinder f) -> \case
-    SameNameBinders -> unsafeCoerce u
-    RenameLeftNameBinder g -> RenameLeftNameBinder (unsafeCoerce f . unsafeCoerce g)
-    RenameRightNameBinder g -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g)
-    RenameBothBinders _ f' g -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
-    NotUnifiable _ _ -> NotUnifiable undefined undefined
-  u@(RenameRightNameBinder f) -> \case
-    SameNameBinders -> unsafeCoerce u
-    RenameLeftNameBinder g -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g)
-    RenameRightNameBinder g -> RenameRightNameBinder (unsafeCoerce f . unsafeCoerce g)
-    RenameBothBinders _ g f' -> RenameBothBinders undefined (unsafeCoerce g) (unsafeCoerce f . unsafeCoerce f')
-    NotUnifiable _ _ -> NotUnifiable undefined undefined
-  u@(RenameBothBinders _ f g) -> \case
-    SameNameBinders -> unsafeCoerce u
-    RenameLeftNameBinder f' -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
-    RenameRightNameBinder g' -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')
-    RenameBothBinders _ f' g' -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g . unsafeCoerce g')
-    NotUnifiable _ _ -> NotUnifiable undefined undefined
-  NotUnifiable _ _ -> const (NotUnifiable undefined undefined)
-
-andThenUnifyPatterns :: (UnifiablePattern binder) => UnifyNameBinders binder n l l' -> (binder l r, binder l' r') -> UnifyNameBinders binder n r r'
-andThenUnifyPatterns u = case u of
-  SameNameBinders -> uncurry (unsafeCoerce . unifyPatterns)
-  RenameLeftNameBinder renameL -> \(l, r) ->
-    extendNameBinderRenaming renameL l $ \_renameL' l' ->
-      unsafeMergeUnifyBinders u (unifyPatterns l' r)
-  RenameRightNameBinder renameR -> \(l, r) ->
-    extendNameBinderRenaming renameR r $ \_renameR' r' ->
-      unsafeMergeUnifyBinders u (unifyPatterns l r')
-  RenameBothBinders _ renameL renameR -> \(l, r) ->
-    extendNameBinderRenaming renameL l $ \_renameL' l' ->
-      extendNameBinderRenaming renameR r $ \_renameR' r' ->
-        unsafeMergeUnifyBinders u (unifyPatterns l' r')
-  NotUnifiable{} -> const (NotUnifiable undefined undefined)
+
+  SameNameBinders x -> \case
+    SameNameBinders y -> SameNameBinders (x `unsafeMergeNameBinders` y)
+    RenameLeftNameBinder y f -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)
+    RenameRightNameBinder y g -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)
+    RenameBothBinders y f g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)
+    NotUnifiable -> NotUnifiable
+
+  RenameLeftNameBinder x f -> \case
+    SameNameBinders y -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)
+    RenameLeftNameBinder y g -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce g)
+    RenameRightNameBinder y g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)
+    RenameBothBinders y f' g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
+    NotUnifiable -> NotUnifiable
+
+  RenameRightNameBinder x g -> \case
+    SameNameBinders y -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)
+    RenameLeftNameBinder y f -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)
+    RenameRightNameBinder y g' -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g . unsafeCoerce g')
+    RenameBothBinders y f g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')
+    NotUnifiable -> NotUnifiable
+
+  RenameBothBinders x f g -> \case
+    SameNameBinders y -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)
+    RenameLeftNameBinder y f' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
+    RenameRightNameBinder y g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')
+    RenameBothBinders y f' g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g . unsafeCoerce g')
+    NotUnifiable -> NotUnifiable
+
+  NotUnifiable -> const (NotUnifiable)
+
+andThenUnifyPatterns :: (UnifiablePattern pattern, Distinct l, Distinct l') => UnifyNameBinders pattern n l l' -> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
+andThenUnifyPatterns u (l, r) = unsafeMergeUnifyBinders u (unifyPatterns (unsafeCoerce l) r)
+
+newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet
+
+unsafeMergeNameBinders :: NameBinders a b -> NameBinders c d -> NameBinders n l
+unsafeMergeNameBinders (UnsafeNameBinders x) (UnsafeNameBinders y) = UnsafeNameBinders (x <> y)
+
+emptyNameBinders :: NameBinders n n
+emptyNameBinders = UnsafeNameBinders IntSet.empty
+
+mergeNameBinders :: NameBinders n i -> NameBinders i l -> NameBinders n l
+mergeNameBinders = unsafeMergeNameBinders
+
+nameBindersSingleton :: NameBinder n l -> NameBinders n l
+nameBindersSingleton binder = UnsafeNameBinders (IntSet.singleton (nameId (nameOf binder)))
+
+data NameBinderList n l where
+  NameBinderListEmpty :: NameBinderList n n
+  NameBinderListCons :: NameBinder n i -> NameBinderList i l -> NameBinderList n l
+
+nameBindersList :: NameBinders n l -> NameBinderList n l
+nameBindersList (UnsafeNameBinders names) = go (IntSet.toList names)
+  where
+    go [] = unsafeCoerce NameBinderListEmpty
+    go (x:xs) = NameBinderListCons (UnsafeNameBinder (UnsafeName x)) (go xs)
+
+fromNameBindersList :: NameBinderList n l -> NameBinders n l
+fromNameBindersList = UnsafeNameBinders . IntSet.fromList . go
+  where
+    go :: NameBinderList n l -> [RawName]
+    go NameBinderListEmpty = []
+    go (NameBinderListCons binder binders) = nameId (nameOf binder) : go binders
+
+instance CoSinkable NameBinders where
+  coSinkabilityProof _rename (UnsafeNameBinders names) cont =
+    cont unsafeCoerce (UnsafeNameBinders names)
+
+  withPattern withBinder unit comp scope binders cont =
+    withPattern withBinder unit comp scope (nameBindersList binders) $ \f binders' ->
+      cont f (fromNameBindersList binders')
+
+instance CoSinkable NameBinderList where
+  coSinkabilityProof rename NameBinderListEmpty cont = cont rename NameBinderListEmpty
+  coSinkabilityProof rename (NameBinderListCons binder binders) cont =
+    coSinkabilityProof rename binder $ \rename' binder' ->
+      coSinkabilityProof rename' binders $ \rename'' binders' ->
+        cont rename'' (NameBinderListCons binder' binders')
+
+  withPattern withBinder unit comp scope binders cont = case binders of
+    NameBinderListEmpty -> cont unit NameBinderListEmpty
+    NameBinderListCons x xs ->
+      withBinder scope x $ \f x' ->
+        let scope' = extendScopePattern x' scope
+        in withPattern withBinder unit comp scope' xs $ \f' xs' ->
+            cont (comp f f') (NameBinderListCons x' xs')
 
 data V2 (n :: S) (l :: S)
 
 absurd2 :: V2 n l -> a
 absurd2 v2 = case v2 of {}
 
+instance CoSinkable V2 where
+  coSinkabilityProof _ v2 _ = absurd2 v2
+  withPattern _ _ _ _ v2 _ = absurd2 v2
+instance UnifiablePattern V2 where
+  unifyPatterns = absurd2
+
+data U2 (n :: S) (l :: S) where
+  U2 :: U2 n n
+
+instance CoSinkable U2 where
+  coSinkabilityProof rename U2 cont = cont rename U2
+  withPattern _withBinder unit _combine _scope U2 cont = cont unit U2
+instance UnifiablePattern U2 where
+  unifyPatterns U2 U2 = SameNameBinders emptyNameBinders
+
 class CoSinkable pattern => UnifiablePattern pattern where
-  unifyPatterns
-    :: pattern i l
-    -> pattern i r
-    -> UnifyNameBinders pattern i l r
+  unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
 
 instance UnifiablePattern NameBinder where
   unifyPatterns = unifyNameBinders
 
-unsafeEqPattern :: UnifiablePattern pattern => pattern n l -> pattern n' l' -> Bool
+unsafeEqPattern :: (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool
 unsafeEqPattern l r =
   case unifyPatterns l (unsafeCoerce r) of
-    SameNameBinders -> True
+    SameNameBinders{} -> True
     _ -> False
 
 -- * Safe sinking
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
index 302b27a0..e4d4cfd7 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
@@ -188,19 +188,19 @@ alphaEquivScoped scope
   (ScopedAST binder2 body2) =
     case Foil.unifyPatterns 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
+      Foil.SameNameBinders{} ->  -- after seeing this we know that body scopes are the same
         case Foil.assertDistinct binder1 of
           Foil.Distinct ->
             let scope1 = Foil.extendScopePattern binder1 scope
             in alphaEquiv scope1 body1 body2
       -- if we can safely rename first binder into second
-      Foil.RenameLeftNameBinder rename1to2 ->
+      Foil.RenameLeftNameBinder _ rename1to2 ->
         case Foil.assertDistinct binder2 of
           Foil.Distinct ->
             let scope2 = Foil.extendScopePattern 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 ->
+      Foil.RenameRightNameBinder _ rename2to1 ->
         case Foil.assertDistinct binder1 of
           Foil.Distinct ->
             let scope1 = Foil.extendScopePattern binder1 scope
@@ -214,7 +214,7 @@ alphaEquivScoped scope
                 (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename1) body1)
                 (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename2) body2)
       -- if we cannot unify patterns then scopes are not alpha-equivalent
-      Foil.NotUnifiable _ _ -> False
+      Foil.NotUnifiable -> False
 
 -- ** Unsafe equality checks
 
@@ -223,7 +223,7 @@ alphaEquivScoped scope
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
 unsafeEqAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder)
+  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
@@ -236,13 +236,14 @@ unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
 unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder)
+  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
 unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
   [ Foil.unsafeEqPattern binder1 binder2
-  , body1 `unsafeEqAST` body2
+  , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of
+      (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2
   ]
 
 -- ** Syntactic matching (unification)
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
index 5dd597d4..db706a3d 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE BlockArguments        #-}
-{-# LANGUAGE EmptyCase        #-}
 {-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE EmptyCase             #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE KindSignatures        #-}
@@ -33,13 +33,11 @@
 -- 3. "Language.LambdaPi.Impl.FreeFoilTH" combines the benefits of the above, when it is possible to generate the signature automatically.
 module Language.LambdaPi.Impl.Foil where
 
-import           Control.Monad.Foil hiding (unifyPatterns)
-import           Control.Monad                   (join)
+import           Control.Monad.Foil
 import           Control.Monad.Foil.Relative
 import           Data.Coerce                     (coerce)
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
-import           Data.Maybe                      (fromMaybe)
 import           Data.String
 import qualified Language.LambdaPi.Syntax.Abs    as Raw
 import           Language.LambdaPi.Syntax.Layout (resolveLayout)
@@ -118,6 +116,13 @@ instance CoSinkable Pattern where
         in withPattern withNameBinder id' combine scope' r $ \fr r' ->
               cont (combine fl fr) (PatternPair l' r')
 
+instance UnifiablePattern Pattern where
+  unifyPatterns PatternWildcard PatternWildcard = SameNameBinders emptyNameBinders
+  unifyPatterns (PatternVar x) (PatternVar x') = unifyNameBinders x x'
+  unifyPatterns (PatternPair l r) (PatternPair l' r') = case (assertDistinct l, assertDistinct l') of
+    (Distinct, Distinct) -> unifyPatterns l l' `andThenUnifyPatterns` (r, r')
+  unifyPatterns _ _ = NotUnifiable
+
 instance InjectName Expr where
   injectName = VarE
 
@@ -484,48 +489,41 @@ unsafeEqExpr e1 e2 = case (e1, e2) of
   (UniverseE, UniverseE) -> True
   _ -> False
 
-unifyPatterns
-  :: Distinct n
-  => Pattern n l
-  -> Pattern n r
-  -> (forall lr. DExt n lr => (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> Pattern n lr -> result)
-  -> Maybe result
-unifyPatterns PatternWildcard PatternWildcard cont =
-  Just (cont id id PatternWildcard)
-unifyPatterns (PatternVar x) (PatternVar x') cont =
-  case unifyNameBinders x x' of
-    SameNameBinders ->
-      case assertDistinct x of
-        Distinct -> case assertExt x of
-          Ext -> Just (cont id id (PatternVar x))
-    RenameLeftNameBinder renameL ->
-      case (assertExt x', assertDistinct x') of
-        (Ext, Distinct) -> Just (cont renameL id (PatternVar x'))
-    RenameRightNameBinder renameR ->
-      case (assertExt x, assertDistinct x) of
-        (Ext, Distinct) -> Just (cont id renameR (PatternVar x))
-    RenameBothBinders v2 _ _ -> absurd2 v2
-    NotUnifiable v2 _ -> absurd2 v2
-unifyPatterns (PatternPair l r) (PatternPair l' r') cont = join $
-  unifyPatterns l l' $ \renameL renameL' l'' ->
-    extendNameBinderRenaming renameL r $ \renameLext rext ->
-      extendNameBinderRenaming renameL' r' $ \renameL'ext r'ext ->
-        unifyPatterns rext r'ext $ \renameR renameR' r'' ->
-          let rename = renameL `composeNameBinderRenamings` (renameR . renameLext)
-              rename' = renameL' `composeNameBinderRenamings` (renameR' . renameL'ext)
-           in cont rename rename' (PatternPair l'' r'')
-unifyPatterns _ _ _ = Nothing
-
 alphaEquiv :: Distinct n => Scope n -> Expr n -> Expr n -> Bool
 alphaEquiv scope e1 e2 = case (e1, e2) of
   (VarE x, VarE x') -> x == coerce x'
   (AppE t1 t2, AppE t1' t2') -> alphaEquiv scope t1 t1' && alphaEquiv scope t2 t2'
-  (LamE x body, LamE x' body') -> fromMaybe False $ unifyPatterns x x' $ \renameL renameR x'' ->
-    let scope' = extendScopePattern x'' scope
-     in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) body) (liftRM scope' (fromNameBinderRenaming renameR) body')
-  (PiE x a b, PiE x' a' b') -> fromMaybe False $ unifyPatterns x x' $ \renameL renameR x'' ->
-    let scope' = extendScopePattern x'' scope
-     in alphaEquiv scope a a' && alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) b) (liftRM scope' (fromNameBinderRenaming renameR) b')
+  (LamE x body, LamE x' body') -> case unifyPatterns x x' of
+    SameNameBinders z    -> case assertDistinct z of
+      Distinct -> alphaEquiv (extendScopePattern z scope) body body'
+    RenameLeftNameBinder z renameL -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) body) body'
+    RenameRightNameBinder z renameR -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' body (liftRM scope' (fromNameBinderRenaming renameR) body')
+    RenameBothBinders z renameL renameR -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) body) (liftRM scope' (fromNameBinderRenaming renameR) body')
+    NotUnifiable -> False
+  (PiE x a b, PiE x' a' b') -> alphaEquiv scope a a' && case unifyPatterns x x' of
+    SameNameBinders z    -> case assertDistinct z of Distinct -> alphaEquiv (extendScopePattern z scope) b b'
+    RenameLeftNameBinder z renameL -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) b) b'
+    RenameRightNameBinder z renameR -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' b (liftRM scope' (fromNameBinderRenaming renameR) b')
+    RenameBothBinders z renameL renameR -> case assertDistinct z of
+      Distinct ->
+        let scope' = extendScopePattern z scope
+        in alphaEquiv scope' (liftRM scope' (fromNameBinderRenaming renameL) b) (liftRM scope' (fromNameBinderRenaming renameR) b')
+    NotUnifiable -> False
   (PairE l r, PairE l' r') -> alphaEquiv scope l l' && alphaEquiv scope r r'
   (FirstE t, FirstE t') -> alphaEquiv scope t t'
   (SecondE t, SecondE t') -> alphaEquiv scope t t'
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
index 7692a1d0..bdaab7b5 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -80,11 +80,12 @@ mkFromFoilPattern ''Raw.VarIdent ''Raw.Pattern'
 -- * User-defined code
 
 instance Foil.UnifiablePattern FoilPattern where
-  unifyPatterns (FoilPatternWildcard _loc) (FoilPatternWildcard _loc') = Foil.SameNameBinders
+  unifyPatterns (FoilPatternWildcard _loc) (FoilPatternWildcard _loc') = Foil.SameNameBinders Foil.emptyNameBinders
   unifyPatterns (FoilPatternVar _loc x) (FoilPatternVar _loc' x') = Foil.unifyNameBinders x x'
   unifyPatterns (FoilPatternPair _loc l r) (FoilPatternPair _loc' l' r') =
-    Foil.unifyPatterns l l' `Foil.andThenUnifyPatterns` (r, r')
-  unifyPatterns l r = Foil.NotUnifiable l r
+    case (Foil.assertDistinct l, Foil.assertDistinct l') of
+      (Foil.Distinct, Foil.Distinct) -> Foil.unifyPatterns l l' `Foil.andThenUnifyPatterns` (r, r')
+  unifyPatterns _ _ = Foil.NotUnifiable
 
 type Term' a = AST (FoilPattern' a) (Term'Sig a)
 type Term = Term' Raw.BNFC'Position