Factor out Data.ZipMatchK, remove ZipMatch

haskell/free-foil/free-foil.cabal

@@ -40,13 +40,15 @@ library
       Control.Monad.Foil.TH.Util
       Control.Monad.Free.Foil
       Control.Monad.Free.Foil.Example
-      Control.Monad.Free.Foil.Generic
       Control.Monad.Free.Foil.TH
       Control.Monad.Free.Foil.TH.Convert
       Control.Monad.Free.Foil.TH.MkFreeFoil
       Control.Monad.Free.Foil.TH.PatternSynonyms
       Control.Monad.Free.Foil.TH.Signature
-      Control.Monad.Free.Foil.TH.ZipMatch
+      Data.ZipMatchK
+      Data.ZipMatchK.Bifunctor
+      Data.ZipMatchK.Generic
+      Data.ZipMatchK.Mappings
   other-modules:
       Paths_free_foil
   hs-source-dirs:

haskell/free-foil/src/Control/Monad/Free/Foil.hs

@@ -24,7 +24,7 @@ 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.ZipMatchK
 import           Data.Coerce                 (coerce)
 import           Data.Map                    (Map)
 import qualified Data.Map                    as Map
@@ -165,7 +165,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
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,21 +178,21 @@ 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
-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
   -> Bool
 alphaEquiv _scope (Var x) (Var y) = x == coerce y
 alphaEquiv scope (Node l) (Node r) =
-  case zipMatch l r of
+  case zipMatch2 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.UnifiablePattern binder)
+  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,20 +237,20 @@ 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, Foil.Distinct n, Foil.Distinct l)
+  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
 unsafeEqAST (Var x) (Var y) = x == coerce y
 unsafeEqAST (Node t1) (Node t2) =
-  case zipMatch t1 t2 of
+  case zipMatch2 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, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool
@@ -260,20 +260,6 @@ unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
       (Foil.Distinct, Foil.Distinct) -> 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

haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs

@@ -2,10 +2,8 @@ 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

haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs

@@ -83,7 +83,7 @@ mkPatternSynonym signatureType scope term = \case
       where
         l = mkName ("l" ++ show i)
 
-    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))
+    mkPatternName conName = mkName (dropEnd (length ("Sig" :: String)) (nameBase conName))
     dropEnd k = reverse . drop k . reverse
 
     collapse = \case

haskell/free-foil/src/Data/ZipMatchK.hs

@@ -0,0 +1,36 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.ZipMatchK (
+  module Data.ZipMatchK.Mappings,
+  ZipMatchK(..),
+  zipMatchK,
+  zipMatch2,
+  zipMatchViaEq,
+  zipMatchViaChooseLeft,
+) where
+
+import           Generics.Kind
+
+import Data.ZipMatchK.Generic
+import Data.ZipMatchK.Mappings
+
+zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
+zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings
+
+zipMatch2 :: forall f a b a' b'. (ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
+zipMatch2 = zipMatchK @f @(a :&&: b :&&: LoT0) @(a' :&&: b' :&&: LoT0)
+
+zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaEq _ x y
+  | x == y = Just x
+  | otherwise = Nothing
+
+zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
+zipMatchViaChooseLeft _ x _ = Just x

haskell/free-foil/src/Data/ZipMatchK/Bifunctor.hs

@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.ZipMatchK.Bifunctor where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Data.Bifunctor.Sum
+import Data.Bifunctor.Product
+
+import Data.ZipMatchK
+
+instance GenericK (Sum f g) where
+  type RepK (Sum f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :+: Field ((Kon g :@: Var0) :@: Var1)
+instance GenericK (Product f g) where
+  type RepK (Product f g) =
+    Field ((Kon f :@: Var0) :@: Var1)
+    :*: Field ((Kon g :@: Var0) :@: Var1)
+
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum (f :: Type -> Type -> Type) g)
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product (f :: Type -> Type -> Type) g)

haskell/free-foil/src/Control/Monad/Free/Foil/Generic.hs → haskell/free-foil/src/Data/ZipMatchK/Generic.hs

@@ -16,41 +16,20 @@
 {-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE UndecidableInstances     #-}
-module Control.Monad.Free.Foil.Generic where
+module Data.ZipMatchK.Generic where
 
 import           Data.Kind              (Constraint, Type)
 import           Generics.Kind
 import           Generics.Kind.Examples ()
 import           GHC.TypeError
+import           Data.ZipMatchK.Mappings
 
-type ZipLoT :: LoT k -> LoT k -> LoT k
-type family ZipLoT as bs where
-  ZipLoT LoT0 LoT0 = LoT0
-  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)
-
-type Mappings :: LoT k -> LoT k -> LoT k -> Type
-data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
-  M0 :: Mappings LoT0 LoT0 LoT0
-  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
-
-class PairMappings (as :: LoT k) (bs :: LoT k) where
-  pairMappings :: Mappings as bs (ZipLoT as bs)
-
-instance PairMappings LoT0 LoT0 where
-  pairMappings = M0
-
-instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where
-  pairMappings = (\x y -> Just (x, y)) :^: pairMappings
-
-class ApplyMappings (v :: TyVar d Type) where
-  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
-    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)
-
-instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
-  applyMappings (f :^: _) x y = f x y
-
-instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where
-  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y
+class ZipMatchK (f :: k) where
+  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
+  default zipMatchWithK :: forall as bs cs.
+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
+  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs
 
 genericZipMatchK :: forall f as bs.
     (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)
@@ -70,24 +49,6 @@ genericZipMatch2
    => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
 genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)
 
-zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
-zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings
-
-class ZipMatchK (f :: k) where
-  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
-  default zipMatchWithK :: forall as bs cs.
-    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
-    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
-  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs
-
-zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
-zipMatchViaEq _ x y
-  | x == y = Just x
-  | otherwise = Nothing
-
-zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
-zipMatchViaChooseLeft _ x _ = Just x
-
 -- instance ZipMatchK (,)     -- missing GenericK instance upstream
 instance ZipMatchK []
 instance ZipMatchK Maybe
@@ -153,12 +114,12 @@ instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where
   type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
 
   zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>
-    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon k :@: t) cs)
+    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon (k :: Type -> Type) :@: t) cs)
   zipMatchFieldsWith g (Field l) (Field r) =
     Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)
       ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r
 
-instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: t1) :@: t2) where
+instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where
   type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)
 
   zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>
@@ -169,7 +130,12 @@ instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields (
         :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))
         :^: M0)) l r
 
-instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: t) where
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (f :@: t)
+  :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))
+  => ZipMatchFields ((f :: Atom d (k1 -> Type)) :@: t) where
   -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")
   zipMatchFieldsWith = undefined