Improve documentation and type errors

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

@@ -23,6 +23,7 @@ import           Control.DeepSeq
 import qualified Control.Monad.Foil.Internal as Foil
 import qualified Control.Monad.Foil.Relative as Foil
 import           Data.Bifoldable
+import           Data.Bitraversable
 import           Data.Bifunctor
 import Data.ZipMatchK
 import           Data.Coerce                 (coerce)
@@ -165,7 +166,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, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -178,7 +179,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
-  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> AST binder sig n
   -> AST binder sig n
@@ -192,7 +193,7 @@ alphaEquiv _ _ _ = False
 
 -- | Same as 'alphaEquiv' but for scoped terms.
 alphaEquivScoped
-  :: (Bifunctor sig, Bifoldable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder)
   => Foil.Scope n
   -> ScopedAST binder sig n
   -> ScopedAST binder sig n
@@ -237,7 +238,7 @@ alphaEquivScoped scope
 -- scope extensions under binders (which might happen due to substitution
 -- under a binder in absence of name conflicts).
 unsafeEqAST
-  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => AST binder sig n
   -> AST binder sig l
   -> Bool
@@ -250,7 +251,7 @@ unsafeEqAST _ _ = False
 
 -- | A version of 'unsafeEqAST' for scoped terms.
 unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
+  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
   => ScopedAST binder sig n
   -> ScopedAST binder sig l
   -> Bool

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

@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE RankNTypes #-}
@@ -7,30 +8,73 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+-- | Kind-polymorphic syntactic (first-order) unification.
 module Data.ZipMatchK (
   module Data.ZipMatchK.Mappings,
   ZipMatchK(..),
   zipMatchK,
-  zipMatch2,
+  -- * Specializations
+  -- ** Unification of plain 'Type's
   zipMatchViaEq,
   zipMatchViaChooseLeft,
+  -- ** Unification of 'Functor's
+  zipMatchWith1,
+  zipMatch1,
+  -- ** Unification of 'Data.Bifunctor.Bifunctor's
+  zipMatchWith2,
+  zipMatch2,
 ) where
 
 import           Generics.Kind
+import Data.Bitraversable
 
 import Data.ZipMatchK.Generic
 import Data.ZipMatchK.Mappings
 
+-- | Perform one level of equality testing for two values and pair up components using @(,)@:
+--
+-- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)
 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)
-
+-- | Unify values via 'Eq'.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Type'@.
 zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
 zipMatchViaEq _ x y
   | x == y = Just x
   | otherwise = Nothing
 
+-- | Always successfully unify any two values of type @a@ by preferring the left value.
+-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Type'@.
 zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
 zipMatchViaChooseLeft _ x _ = Just x
+
+-- | 'zipMatchWithK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatchWith1
+  :: (Traversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> f a -> f a' -> Maybe (f a'')
+zipMatchWith1 f = zipMatchWithK (f :^: M0)
+
+-- | 'zipMatchK' specialised to functors.
+--
+-- Note: 'Traversable' is a morally correct constraint here.
+zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))
+zipMatch1 = zipMatchWith1 pairA
+-- | 'zipMatchWithK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatchWith2
+  :: (Bitraversable f, ZipMatchK f)
+  => (a -> a' -> Maybe a'')
+  -> (b -> b' -> Maybe b'')
+  -> f a b -> f a' b' -> Maybe (f a'' b'')
+zipMatchWith2 f g = zipMatchWithK (f :^: g :^: M0)
+
+-- | 'zipMatchK' specialised to bifunctors.
+--
+-- Note: 'Bitraversable' is a morally correct constraint here.
+zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
+zipMatch2 = zipMatchWith2 pairA pairA

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

@@ -8,6 +8,8 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+-- | This module provides 'GenericK' and 'ZipMatchK' instances for 'Sum' and 'Product',
+-- to enable the use of 'ZipMatchK' with the data types à la carte approach.
 module Data.ZipMatchK.Bifunctor where
 
 import Data.Kind (Type)
@@ -26,5 +28,7 @@ instance GenericK (Product f g) where
     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)
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Sum f (g :: Type -> Type -> Type))
+-- | Note: instance is limited to 'Type'-kinded bifunctors @f@ and @g@.
+instance (ZipMatchK f, ZipMatchK g) => ZipMatchK (Product f (g :: Type -> Type -> Type))

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

@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -Wno-missing-methods #-}
+{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-}
 {-# LANGUAGE AllowAmbiguousTypes      #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
@@ -24,32 +24,44 @@ import           Generics.Kind.Examples ()
 import           GHC.TypeError
 import           Data.ZipMatchK.Mappings
 
+-- | Kind-polymorphic syntactic (first-order) unification of two values.
+--
+-- Note: @f@ is expected to be a traversable n-functor,
+-- but at the moment we lack a @TraversableK@ constraint.
 class ZipMatchK (f :: k) where
+  -- | Perform one level of equality testing:
+  --
+  -- * when @k = 'Type'@, values are compared directly (e.g. via 'Eq');
+  -- * when @k = 'Type' -> 'Type'@, we compare term constructors;
+  --   if term constructors are unequal, we return 'Nothing';
+  --   otherwise, we pair up all components with a given function.
   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
 
+-- | Generic implementation of 'Data.ZipMatch.zipMatchK'.
 genericZipMatchK :: forall f as bs.
     (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)
     => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))
 genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings
 
+-- | Generic implementation of 'zipMatchWithK'.
 genericZipMatchWithK :: forall f 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)
 genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings
   (fromK @_ @f @as x)
   (fromK @_ @f @bs y)
 
-genericZipMatch2
-   :: forall sig scope scope' term term'.
-   (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0))
-   => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
-genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)
+instance GenericK (,) where
+  type RepK (,) = Field Var0 :*: Field Var1
+instance GenericK ((,) a) where
+  type RepK ((,) a) = Field (Kon a) :*: Field Var0
 
--- instance ZipMatchK (,)     -- missing GenericK instance upstream
+instance ZipMatchK (,)
+instance ZipMatchK a => ZipMatchK ((,) a)
 instance ZipMatchK []
 instance ZipMatchK Maybe
 instance ZipMatchK Either
@@ -110,7 +122,7 @@ instance ZipMatchK k => ZipMatchFields (Kon k) where
   type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()
   zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r
 
-instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where
+instance {-# OVERLAPPING #-} (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 =>
@@ -130,6 +142,24 @@ instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k)
         :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))
         :^: M0)) l r
 
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "The type constructor is kind-polymorphic:"
+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type)
+  :$$: 'Text "Possible fix:"
+  :$$: 'Text "  add an explicit kind signature"
+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type))
+  => ZipMatchFields (Kon (k :: kk -> Type) :@: t) where
+  zipMatchFieldsWith = undefined
+
+instance {-# OVERLAPPABLE #-} TypeError
+  ('Text "The type constructor is kind-polymorphic:"
+  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type)
+  :$$: 'Text "Possible fix:"
+  :$$: 'Text "  add an explicit kind signature"
+  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type))
+  => ZipMatchFields ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where
+  zipMatchFieldsWith = undefined
+
 instance {-# OVERLAPPABLE #-} TypeError
   ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"
   :$$: 'Text "  when attempting to use a generic instance for"
@@ -139,24 +169,21 @@ instance {-# OVERLAPPABLE #-} TypeError
   -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")
   zipMatchFieldsWith = undefined
 
-instance TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") => ZipMatchFields (ForAll a) where
+instance TypeError
+  ('Text "Atom ForAll is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (ForAll a)) => ZipMatchFields (ForAll a) where
   type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-instance TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") => ZipMatchFields (c :=>>: a) where
+instance TypeError
+  ('Text "Atom :=>>: is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (c :=>>: a)) => ZipMatchFields (c :=>>: a) where
   type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-instance TypeError ('Text "Atom Eval is not supported by ZipMatchFields") => ZipMatchFields (Eval a) where
+instance TypeError
+  ('Text "Atom Eval is not supported by ZipMatchFields"
+  :$$: 'Text "  when attempting to use a generic instance for"
+  :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where
   type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")
   zipMatchFieldsWith = undefined
-
--- instance ZipMatchFields (ForAll f) where
---   type ReqsZipMatchFields (ForAll f) as bs = ???
---   zipMatchFields = ???
-
--- instance ZipMatchFields (c :=>>: f) where
---   type ReqsZipMatchFields (c :=>>: f) as bs = ???
---   zipMatchFields = ???
-
--- instance ZipMatchFields (Eval f) where
---   type ReqsZipMatchFields (Eval f) as bs = ???
---   zipMatchFields = ???

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

@@ -14,31 +14,47 @@ module Data.ZipMatchK.Mappings where
 import           Data.Kind              (Type)
 import           Generics.Kind
 
+-- | Zip to lists of types into a single list of pair types.
 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)
 
+infixr 5 :^:
 type Mappings :: LoT k -> LoT k -> LoT k -> Type
+-- | A collection of zipping functions for 'Data.ZipMatchK.zipMatchWithK'.
 data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
+  -- | An empty collection (when there no (more) type parameters).
   M0 :: Mappings LoT0 LoT0 LoT0
-  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
+  -- | A non-empty collection (when there is at least one type parameter).
+  (:^:) :: (a -> b -> Maybe c)    -- ^ Zipping for the first type parameter.
+        -> Mappings as bs cs      -- ^ Zipping for other type parameters.
+        -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)
 
 class PairMappings (as :: LoT k) (bs :: LoT k) where
+  -- | A collection of pairing functions @(\\x y -> Just (x, y))@ for 'Data.ZipMatchK.zipMatchK'.
   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
+  pairMappings = pairA :^: pairMappings
 
 class ApplyMappings (v :: TyVar d Type) where
+  -- | Apply a collection of zipping functions to collections of values.
   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)
+       Mappings as bs cs      -- ^ A collection of zipping functions.
+    -> Interpret (Var v) as   -- ^ First collection of values (one per type parameter).
+    -> Interpret (Var v) bs   -- ^ Second collection of values (one per type parameter).
+    -> 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
+
+-- | Pair two values in a context.
+pairA :: Applicative f => a -> b -> f (a, b)
+pairA x y = pure (x, y)