{-# language DefaultSignatures, UndecidableInstances, GADTs, MultiWayIf, AllowAmbiguousTypes #-}
-- | Unification for @unbound-generics@
module Unbound.Generics.Unify (
  -- * Main unification functions
  unify', Unify(..),
  -- ** Information about errors
  UnificationError, UnificationErrorCause(..),
  Path, PathElement(..),
  -- * Unification as a monad
  Unification(..),
  -- ** Base implementation
  UnificationM, runUnification,
  -- ** Including fresh creation
  UnificationFreshM, runUnificationFresh,
  -- ** As a monad transformer
  UnificationMT(..), runUnificationT,
  -- * Generic methods
  GUnify(..)
) where

import Data.Bifunctor
import Control.Monad (forM)
import Control.Monad.Trans.State
import Data.Functor.Identity
import Data.Map
import GHC.Generics
import Unbound.Generics.LocallyNameless

-- | Path to navigate to a unification error.
type UnificationError = (Path, UnificationErrorCause)

-- | Potential causes for unification errors.
data UnificationErrorCause where
  OccursCheck          :: (Name t) -> t -> UnificationErrorCause
  DifferentConstructor :: UnificationErrorCause
  DifferentListLength  :: UnificationErrorCause

instance Show UnificationErrorCause where
  show :: UnificationErrorCause -> String
show OccursCheck {}       = String
"OccursCheck"
  show UnificationErrorCause
DifferentConstructor = String
"DifferentConstructor"
  show UnificationErrorCause
DifferentListLength  = String
"DifferentListLength"

type Path = [PathElement]
-- | Ways to navigate within a value.
data PathElement
  = PathConstructor String | PathSelector String | PathIndex Int
  deriving (PathElement -> PathElement -> Bool
(PathElement -> PathElement -> Bool)
-> (PathElement -> PathElement -> Bool) -> Eq PathElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PathElement -> PathElement -> Bool
== :: PathElement -> PathElement -> Bool
$c/= :: PathElement -> PathElement -> Bool
/= :: PathElement -> PathElement -> Bool
Eq, Int -> PathElement -> ShowS
[PathElement] -> ShowS
PathElement -> String
(Int -> PathElement -> ShowS)
-> (PathElement -> String)
-> ([PathElement] -> ShowS)
-> Show PathElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PathElement -> ShowS
showsPrec :: Int -> PathElement -> ShowS
$cshow :: PathElement -> String
show :: PathElement -> String
$cshowList :: [PathElement] -> ShowS
showList :: [PathElement] -> ShowS
Show)

-- | Stateful storage of substitutions as required for unification.
--
-- The substitution operates only on terms and variables of type 't'.
class Monad m => Unification t m where
  -- | Obtain the current substitution.
  currentSubst :: m (Map (Name t) t)
  -- | Add a new substitution.
  recordSubst  :: Name t -> t -> m ()

applySubst :: forall t a m. (Unification t m, Subst t a) => a -> m a
applySubst :: forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst a
term = do
  current <- forall t (m :: * -> *). Unification t m => m (Map (Name t) t)
currentSubst @t @m
  pure $ foldlWithKey (\a
t Name t
v t
u -> Name t -> t -> a -> a
forall b a. Subst b a => Name b -> b -> a -> a
subst Name t
v t
u a
t) term current

type UnificationM t = UnificationMT t Identity
type UnificationFreshM t = UnificationMT t FreshM

runUnification :: forall t a. UnificationM t a -> (a, Map (Name t) t)
runUnification :: forall t a. UnificationM t a -> (a, Map (Name t) t)
runUnification UnificationM t a
action = Identity (a, Map (Name t) t) -> (a, Map (Name t) t)
forall a. Identity a -> a
runIdentity (UnificationM t a -> Identity (a, Map (Name t) t)
forall t (m :: * -> *) a.
Monad m =>
UnificationMT t m a -> m (a, Map (Name t) t)
runUnificationT UnificationM t a
action)

runUnificationFresh :: forall t a. UnificationFreshM t a -> (a, Map (Name t) t)
runUnificationFresh :: forall t a. UnificationFreshM t a -> (a, Map (Name t) t)
runUnificationFresh UnificationFreshM t a
action = FreshM (a, Map (Name t) t) -> (a, Map (Name t) t)
forall a. FreshM a -> a
runFreshM (UnificationFreshM t a -> FreshM (a, Map (Name t) t)
forall t (m :: * -> *) a.
Monad m =>
UnificationMT t m a -> m (a, Map (Name t) t)
runUnificationT UnificationFreshM t a
action)

runUnificationT :: forall t m a. Monad m => UnificationMT t m a -> m (a, Map (Name t) t)
runUnificationT :: forall t (m :: * -> *) a.
Monad m =>
UnificationMT t m a -> m (a, Map (Name t) t)
runUnificationT UnificationMT t m a
action = StateT (Map (Name t) t) m a
-> Map (Name t) t -> m (a, Map (Name t) t)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (UnificationMT t m a -> StateT (Map (Name t) t) m a
forall t (m :: * -> *) a.
UnificationMT t m a -> StateT (Map (Name t) t) m a
unUnificationMT UnificationMT t m a
action) Map (Name t) t
forall k a. Map k a
empty

newtype UnificationMT t m a 
  = UnificationMT { forall t (m :: * -> *) a.
UnificationMT t m a -> StateT (Map (Name t) t) m a
unUnificationMT :: StateT (Map (Name t) t) m a }
  deriving ((forall a b.
 (a -> b) -> UnificationMT t m a -> UnificationMT t m b)
-> (forall a b. a -> UnificationMT t m b -> UnificationMT t m a)
-> Functor (UnificationMT t m)
forall a b. a -> UnificationMT t m b -> UnificationMT t m a
forall a b. (a -> b) -> UnificationMT t m a -> UnificationMT t m b
forall t (m :: * -> *) a b.
Functor m =>
a -> UnificationMT t m b -> UnificationMT t m a
forall t (m :: * -> *) a b.
Functor m =>
(a -> b) -> UnificationMT t m a -> UnificationMT t m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall t (m :: * -> *) a b.
Functor m =>
(a -> b) -> UnificationMT t m a -> UnificationMT t m b
fmap :: forall a b. (a -> b) -> UnificationMT t m a -> UnificationMT t m b
$c<$ :: forall t (m :: * -> *) a b.
Functor m =>
a -> UnificationMT t m b -> UnificationMT t m a
<$ :: forall a b. a -> UnificationMT t m b -> UnificationMT t m a
Functor, Functor (UnificationMT t m)
Functor (UnificationMT t m) =>
(forall a. a -> UnificationMT t m a)
-> (forall a b.
    UnificationMT t m (a -> b)
    -> UnificationMT t m a -> UnificationMT t m b)
-> (forall a b c.
    (a -> b -> c)
    -> UnificationMT t m a
    -> UnificationMT t m b
    -> UnificationMT t m c)
-> (forall a b.
    UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b)
-> (forall a b.
    UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a)
-> Applicative (UnificationMT t m)
forall a. a -> UnificationMT t m a
forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a
forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
forall a b.
UnificationMT t m (a -> b)
-> UnificationMT t m a -> UnificationMT t m b
forall a b c.
(a -> b -> c)
-> UnificationMT t m a
-> UnificationMT t m b
-> UnificationMT t m c
forall t (m :: * -> *). Monad m => Functor (UnificationMT t m)
forall t (m :: * -> *) a. Monad m => a -> UnificationMT t m a
forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a
forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m (a -> b)
-> UnificationMT t m a -> UnificationMT t m b
forall t (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> UnificationMT t m a
-> UnificationMT t m b
-> UnificationMT t m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall t (m :: * -> *) a. Monad m => a -> UnificationMT t m a
pure :: forall a. a -> UnificationMT t m a
$c<*> :: forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m (a -> b)
-> UnificationMT t m a -> UnificationMT t m b
<*> :: forall a b.
UnificationMT t m (a -> b)
-> UnificationMT t m a -> UnificationMT t m b
$cliftA2 :: forall t (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> UnificationMT t m a
-> UnificationMT t m b
-> UnificationMT t m c
liftA2 :: forall a b c.
(a -> b -> c)
-> UnificationMT t m a
-> UnificationMT t m b
-> UnificationMT t m c
$c*> :: forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
*> :: forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
$c<* :: forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a
<* :: forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a
Applicative, Applicative (UnificationMT t m)
Applicative (UnificationMT t m) =>
(forall a b.
 UnificationMT t m a
 -> (a -> UnificationMT t m b) -> UnificationMT t m b)
-> (forall a b.
    UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b)
-> (forall a. a -> UnificationMT t m a)
-> Monad (UnificationMT t m)
forall a. a -> UnificationMT t m a
forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
forall a b.
UnificationMT t m a
-> (a -> UnificationMT t m b) -> UnificationMT t m b
forall t (m :: * -> *). Monad m => Applicative (UnificationMT t m)
forall t (m :: * -> *) a. Monad m => a -> UnificationMT t m a
forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a
-> (a -> UnificationMT t m b) -> UnificationMT t m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a
-> (a -> UnificationMT t m b) -> UnificationMT t m b
>>= :: forall a b.
UnificationMT t m a
-> (a -> UnificationMT t m b) -> UnificationMT t m b
$c>> :: forall t (m :: * -> *) a b.
Monad m =>
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
>> :: forall a b.
UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b
$creturn :: forall t (m :: * -> *) a. Monad m => a -> UnificationMT t m a
return :: forall a. a -> UnificationMT t m a
Monad)

instance (Monad m) => Unification t (UnificationMT t m) where
  currentSubst :: UnificationMT t m (Map (Name t) t)
currentSubst = StateT (Map (Name t) t) m (Map (Name t) t)
-> UnificationMT t m (Map (Name t) t)
forall t (m :: * -> *) a.
StateT (Map (Name t) t) m a -> UnificationMT t m a
UnificationMT (StateT (Map (Name t) t) m (Map (Name t) t)
 -> UnificationMT t m (Map (Name t) t))
-> StateT (Map (Name t) t) m (Map (Name t) t)
-> UnificationMT t m (Map (Name t) t)
forall a b. (a -> b) -> a -> b
$ StateT (Map (Name t) t) m (Map (Name t) t)
forall (m :: * -> *) s. Monad m => StateT s m s
get
  recordSubst :: Name t -> t -> UnificationMT t m ()
recordSubst Name t
v t
t = StateT (Map (Name t) t) m () -> UnificationMT t m ()
forall t (m :: * -> *) a.
StateT (Map (Name t) t) m a -> UnificationMT t m a
UnificationMT (StateT (Map (Name t) t) m () -> UnificationMT t m ())
-> StateT (Map (Name t) t) m () -> UnificationMT t m ()
forall a b. (a -> b) -> a -> b
$ (Map (Name t) t -> Map (Name t) t) -> StateT (Map (Name t) t) m ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (Name t -> t -> Map (Name t) t -> Map (Name t) t
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert Name t
v t
t)

instance (Fresh m) => Fresh (UnificationMT t m) where
  fresh :: forall a. Name a -> UnificationMT t m (Name a)
fresh = StateT (Map (Name t) t) m (Name a) -> UnificationMT t m (Name a)
forall t (m :: * -> *) a.
StateT (Map (Name t) t) m a -> UnificationMT t m a
UnificationMT (StateT (Map (Name t) t) m (Name a) -> UnificationMT t m (Name a))
-> (Name a -> StateT (Map (Name t) t) m (Name a))
-> Name a
-> UnificationMT t m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> StateT (Map (Name t) t) m (Name a)
forall a. Name a -> StateT (Map (Name t) t) m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

-- | Tries to unify two terms, giving back a common term, or a unification error.
--
-- This variant requires the terms to be of the same type 't' as the variables within them.
unify' :: forall t m. (Unification t m, Unify t t) => t -> t -> m (Either UnificationError t)
unify' :: forall t (m :: * -> *).
(Unification t m, Unify t t) =>
t -> t -> m (Either UnificationError t)
unify' = forall t a (m :: * -> *).
(Unify t a, Unification t m) =>
a -> a -> m (Either UnificationError a)
unify @t

-- | Declares the ability to unify values of type 'a' containing variables of type 't'.
class Subst t a => Unify t a where
  -- | Tries to unify two terms, giving back a common term, or a unification error.
  unify :: Unification t m => a -> a -> m (Either UnificationError a)

  default unify :: forall m. (Generic a, GUnify t (Rep a), Unification t m)
                 => a -> a -> m (Either UnificationError a)
  unify a
x a
y = do
    x' <- forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
x
    y' <- applySubst @t y
    result <- unifyIsvar x' y'
    case result of
      Left UnificationError
e -> Either UnificationError a -> m (Either UnificationError a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError a -> m (Either UnificationError a))
-> Either UnificationError a -> m (Either UnificationError a)
forall a b. (a -> b) -> a -> b
$ UnificationError -> Either UnificationError a
forall a b. a -> Either a b
Left UnificationError
e
      Right a
r -> a -> Either UnificationError a
forall a b. b -> Either a b
Right (a -> Either UnificationError a)
-> m a -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
r

    where
      unifyIsvar :: a -> a -> m (Either UnificationError a)
unifyIsvar a
x a
y
        | Just (SubstName Name a
v1) <- forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar @t @a a
x
        , Just (SubstName Name a
v2) <- forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar @t @a a
y
        = if | Name a
v1 Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name a
v2  -> a -> Either UnificationError a
forall a b. b -> Either a b
Right (a -> Either UnificationError a)
-> m a -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
x
             | Name a
v1  Name a -> Name a -> Bool
forall a. Ord a => a -> a -> Bool
< Name a
v2  -> do { Name a -> a -> m ()
forall t (m :: * -> *). Unification t m => Name t -> t -> m ()
recordSubst Name a
v1 a
y ; a -> Either UnificationError a
forall a b. b -> Either a b
Right (a -> Either UnificationError a)
-> m a -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
x }
             | Bool
otherwise -> do { Name a -> a -> m ()
forall t (m :: * -> *). Unification t m => Name t -> t -> m ()
recordSubst Name a
v2 a
x ; t -> Either UnificationError t
forall a b. b -> Either a b
Right (t -> Either UnificationError t)
-> m t -> m (Either UnificationError t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t t
a
y }
        -- do occurs check!!
        | Just (SubstName Name a
v) <- forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar @t @a a
x = do { Name a -> a -> m ()
forall t (m :: * -> *). Unification t m => Name t -> t -> m ()
recordSubst Name a
v a
y ; a -> Either UnificationError a
forall a b. b -> Either a b
Right (a -> Either UnificationError a)
-> m a -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
x }
        | Just (SubstName Name a
v) <- forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar @t @a a
y = do { Name a -> a -> m ()
forall t (m :: * -> *). Unification t m => Name t -> t -> m ()
recordSubst Name a
v a
x ; a -> Either UnificationError a
forall a b. b -> Either a b
Right (a -> Either UnificationError a)
-> m a -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *). (Unification t m, Subst t a) => a -> m a
applySubst @t a
y }
        | Bool
otherwise = a -> a -> m (Either UnificationError a)
unify_ a
x a
y

      unify_ :: a -> a -> m (Either UnificationError a)
      unify_ :: a -> a -> m (Either UnificationError a)
unify_ a
x a
y = (Rep a Any -> a)
-> Either UnificationError (Rep a Any) -> Either UnificationError a
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Either UnificationError (Rep a Any) -> Either UnificationError a)
-> m (Either UnificationError (Rep a Any))
-> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: * -> *) (m :: * -> *) a.
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t @(Rep a) @m (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y)

instance {-# overlaps #-} Unify t (Name t) where
  unify :: forall (m :: * -> *).
Unification t m =>
Name t -> Name t -> m (Either UnificationError (Name t))
unify = String -> Name t -> Name t -> m (Either UnificationError (Name t))
forall a. HasCallStack => String -> a
error String
"should have never arrived here"

-- required because otherwise strings are matched as lists
instance {-# overlaps #-} Unify t String where
  unify :: forall (m :: * -> *).
Unification t m =>
String -> String -> m (Either UnificationError String)
unify String
x String
y
    | String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
y    = Either UnificationError String
-> m (Either UnificationError String)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError String
 -> m (Either UnificationError String))
-> Either UnificationError String
-> m (Either UnificationError String)
forall a b. (a -> b) -> a -> b
$ String -> Either UnificationError String
forall a b. b -> Either a b
Right String
x
    | Bool
otherwise = Either UnificationError String
-> m (Either UnificationError String)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError String
 -> m (Either UnificationError String))
-> Either UnificationError String
-> m (Either UnificationError String)
forall a b. (a -> b) -> a -> b
$ UnificationError -> Either UnificationError String
forall a b. a -> Either a b
Left ([], UnificationErrorCause
DifferentConstructor)

instance {-# overlaps #-} (Unify t a) => Unify t [a] where
  unify :: forall (m :: * -> *).
Unification t m =>
[a] -> [a] -> m (Either UnificationError [a])
unify [a]
xlst [a]
ylst
    | [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xlst Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ylst = Either UnificationError [a] -> m (Either UnificationError [a])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError [a] -> m (Either UnificationError [a]))
-> Either UnificationError [a] -> m (Either UnificationError [a])
forall a b. (a -> b) -> a -> b
$ UnificationError -> Either UnificationError [a]
forall a b. a -> Either a b
Left ([], UnificationErrorCause
DifferentListLength)
    | Bool
otherwise = [Either UnificationError a] -> Either UnificationError [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Either UnificationError a] -> Either UnificationError [a])
-> m [Either UnificationError a] -> m (Either UnificationError [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, a, a)]
-> ((Int, a, a) -> m (Either UnificationError a))
-> m [Either UnificationError a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [a] -> [a] -> [(Int, a, a)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 .. ] [a]
xlst [a]
ylst) (\(Int
i, a
x,  a
y) -> (UnificationError -> UnificationError)
-> Either UnificationError a -> Either UnificationError a
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (([PathElement] -> [PathElement])
-> UnificationError -> UnificationError
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int -> PathElement
PathIndex Int
i PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
:)) (Either UnificationError a -> Either UnificationError a)
-> m (Either UnificationError a) -> m (Either UnificationError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *).
(Unify t a, Unification t m) =>
a -> a -> m (Either UnificationError a)
unify @t a
x a
y)

-- | Implementation of unification using @GHC.Generics@.
class GUnify t f where
  gunify :: Unification t m => f a -> f a -> m (Either UnificationError (f a))

instance GUnify t U1 where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
U1 a -> U1 a -> m (Either UnificationError (U1 a))
gunify U1 a
_ U1 a
_ = Either UnificationError (U1 a)
-> m (Either UnificationError (U1 a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError (U1 a)
 -> m (Either UnificationError (U1 a)))
-> Either UnificationError (U1 a)
-> m (Either UnificationError (U1 a))
forall a b. (a -> b) -> a -> b
$ U1 a -> Either UnificationError (U1 a)
forall a b. b -> Either a b
Right U1 a
forall k (p :: k). U1 p
U1

instance (Unify t a) => GUnify t (K1 i a) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
K1 i a a -> K1 i a a -> m (Either UnificationError (K1 i a a))
gunify (K1 a
x) (K1 a
y) = (a -> K1 i a a)
-> Either UnificationError a -> Either UnificationError (K1 i a a)
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (Either UnificationError a -> Either UnificationError (K1 i a a))
-> m (Either UnificationError a)
-> m (Either UnificationError (K1 i a a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a (m :: * -> *).
(Unify t a, Unification t m) =>
a -> a -> m (Either UnificationError a)
unify @t a
x a
y

instance GUnify t f => GUnify t (D1 d f) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
D1 d f a -> D1 d f a -> m (Either UnificationError (D1 d f a))
gunify (M1 f a
x) (M1 f a
y) = (f a -> M1 D d f a)
-> Either UnificationError (f a)
-> Either UnificationError (M1 D d f a)
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> M1 D d f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Either UnificationError (f a)
 -> Either UnificationError (M1 D d f a))
-> m (Either UnificationError (f a))
-> m (Either UnificationError (M1 D d f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x f a
y

instance (Constructor c, GUnify t f) => GUnify t (C1 c f) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
C1 c f a -> C1 c f a -> m (Either UnificationError (C1 c f a))
gunify c :: C1 c f a
c@(M1 f a
x) (M1 f a
y) = (UnificationError -> UnificationError)
-> (f a -> C1 c f a)
-> Either UnificationError (f a)
-> Either UnificationError (C1 c f a)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([PathElement] -> [PathElement])
-> UnificationError -> UnificationError
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> PathElement
PathConstructor (C1 c f a -> String
forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> String
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t c f a -> String
conName C1 c f a
c) PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
:)) f a -> C1 c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Either UnificationError (f a)
 -> Either UnificationError (C1 c f a))
-> m (Either UnificationError (f a))
-> m (Either UnificationError (C1 c f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x f a
y

instance (Selector s, GUnify t f) => GUnify t (S1 s f) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
S1 s f a -> S1 s f a -> m (Either UnificationError (S1 s f a))
gunify c :: S1 s f a
c@(M1 f a
x) (M1 f a
y) = 
    case S1 s f a -> String
forall {k} (s :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Selector s =>
t s f a -> String
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t s f a -> String
selName S1 s f a
c of
      String
""  -> (f a -> S1 s f a)
-> Either UnificationError (f a)
-> Either UnificationError (S1 s f a)
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> S1 s f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Either UnificationError (f a)
 -> Either UnificationError (S1 s f a))
-> m (Either UnificationError (f a))
-> m (Either UnificationError (S1 s f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x f a
y
      String
con -> (UnificationError -> UnificationError)
-> (f a -> S1 s f a)
-> Either UnificationError (f a)
-> Either UnificationError (S1 s f a)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([PathElement] -> [PathElement])
-> UnificationError -> UnificationError
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> PathElement
PathSelector String
con PathElement -> [PathElement] -> [PathElement]
forall a. a -> [a] -> [a]
:)) f a -> S1 s f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Either UnificationError (f a)
 -> Either UnificationError (S1 s f a))
-> m (Either UnificationError (f a))
-> m (Either UnificationError (S1 s f a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x f a
y

instance (GUnify t f, GUnify t g) => GUnify t (f :*: g) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
(:*:) f g a
-> (:*:) f g a -> m (Either UnificationError ((:*:) f g a))
gunify (f a
x1 :*: g a
x2) (f a
y1 :*: g a
y2) = do
    r1 <- forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x1 f a
y1
    r2 <- gunify @t x2 y2
    pure $ (:*:) <$> r1 <*> r2

instance (GUnify t f, GUnify t g) => GUnify t (f :+: g) where
  gunify :: forall (m :: * -> *) (a :: k).
Unification t m =>
(:+:) f g a
-> (:+:) f g a -> m (Either UnificationError ((:+:) f g a))
gunify (R1 g a
x) (R1 g a
y) = (g a -> (:+:) f g a)
-> Either UnificationError (g a)
-> Either UnificationError ((:+:) f g a)
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Either UnificationError (g a)
 -> Either UnificationError ((:+:) f g a))
-> m (Either UnificationError (g a))
-> m (Either UnificationError ((:+:) f g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t g a
x g a
y
  gunify (L1 f a
x) (L1 f a
y) = (f a -> (:+:) f g a)
-> Either UnificationError (f a)
-> Either UnificationError ((:+:) f g a)
forall a b.
(a -> b) -> Either UnificationError a -> Either UnificationError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Either UnificationError (f a)
 -> Either UnificationError ((:+:) f g a))
-> m (Either UnificationError (f a))
-> m (Either UnificationError ((:+:) f g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
forall t (f :: k -> *) (m :: * -> *) (a :: k).
(GUnify t f, Unification t m) =>
f a -> f a -> m (Either UnificationError (f a))
gunify @t f a
x f a
y
  gunify (:+:) f g a
_ (:+:) f g a
_ = Either UnificationError ((:+:) f g a)
-> m (Either UnificationError ((:+:) f g a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UnificationError ((:+:) f g a)
 -> m (Either UnificationError ((:+:) f g a)))
-> Either UnificationError ((:+:) f g a)
-> m (Either UnificationError ((:+:) f g a))
forall a b. (a -> b) -> a -> b
$ UnificationError -> Either UnificationError ((:+:) f g a)
forall a b. a -> Either a b
Left ([], UnificationErrorCause
DifferentConstructor)