module Unify where

newtype UVar

class Unifiable t where
  -- True if two things are considered structurally equal. i.e. toplevelEqual TyArr{} TyArr{} = True
  -- Must obey the law: forall t u, toplevelEqual t u ==> (lengthOf plate t == lengthOf plate u)
  -- In other words, structurally equal things must have the same number of subterms
  toplevelEqual :: t -> t -> Bool

class HasVar t a | t -> a where
  _Var :: Prism' t a

class AsUnificationError e t | e -> t where
  _OccursError :: Prism' e (UVar, t)
  _MismatchError :: Prism' e (t, t)

newtype Unify t m a

instance Functor m => Functor (Unify t m) where
instance (Applicative m, Monad m) => Applicative (Unify t m) where -- artifact of equivalence :(
instance Monad m => Monad (Unify t m) where
instance MonadState s m => MonadState s (Unify t m) where
instance MonadError e m => MonadError e (Unify t m) where
instance MonadWriter w m => MonadWriter w (Unify t m) where
instance MonadReader r m => MonadReader r (Unify t m) where

fresh :: Monad m => Unify t m UVar

occurs :: (HasVar t (Either UVar a), Plated t) => UVar -> t -> Bool

union :: (Monad m, Ord t) => t -> t -> Unify t m ()

find :: (Plated t, Ord t, Monad m) => t -> Unify t m t

unify
  :: ( HasVar t (Either UVar a)
     , Unifiable t
     , Plated t
     , Ord t
     , AsUnificationError e t
     , MonadError e m
     )
  => t
  -> t
  -> Unify t m ()

runUnify :: (HasVar t (Either UVar v), Monad m, Plated t) => Unify t m res -> m res