From b57f37331ff4817b1a29337230711e2a4914fe64 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 30 Oct 2024 00:50:44 +0300
Subject: [PATCH] Derive UnifiablePattern via CoSinkable

---
 haskell/free-foil/src/Control/Monad/Foil/Internal.hs   | 10 ++++++++++
 .../lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs |  2 +-
 haskell/soas/src/Language/SOAS/Impl/Generated.hs       |  9 +--------
 3 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
index ddb45eb..869433a 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
@@ -576,6 +576,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
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
index 8174fab..90789fc 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -92,10 +92,10 @@ 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/Generated.hs b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
index dcc7429..67d3976 100644
--- a/haskell/soas/src/Language/SOAS/Impl/Generated.hs
+++ b/haskell/soas/src/Language/SOAS/Impl/Generated.hs
@@ -94,14 +94,7 @@ instance ZipMatchK a => ZipMatchK (Term'Sig a)
 instance ZipMatchK a => ZipMatchK (OpArg'Sig a)
 instance ZipMatchK a => ZipMatchK (Type'Sig a)
 
--- TODO: infer via GenericK
-instance Foil.UnifiablePattern (Binders' a) where
-  unifyPatterns (NoBinders _loc) (NoBinders _loc') = Foil.SameNameBinders Foil.emptyNameBinders
-  unifyPatterns (SomeBinders _loc x xs) (SomeBinders _loc' y ys) =
-    case (Foil.assertDistinct x, Foil.assertDistinct y) of
-      (Foil.Distinct, Foil.Distinct) ->
-        Foil.unifyNameBinders x y `Foil.andThenUnifyPatterns` (xs, ys)
-  unifyPatterns _ _ = Foil.NotUnifiable
+instance Foil.UnifiablePattern (Binders' a)
 
 -- |
 -- >>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS