Derive UnifiablePattern via CoSinkable

fizruk · Oct 29, 2024 · b57f373 · b57f373
1 parent 4d0a4ab
commit b57f373
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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