    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Rules.LHS.Unify.Types where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Monad.Writer (WriterT(..), MonadWriter(..))

    import Data.Foldable (toList)
    import Data.DList (DList)
    import qualified Data.List as List

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Level (reallyUnLevelView)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import Agda.TypeChecking.Rules.LHS.Problem

    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    ----------------------------------------------------
    -- Equalities
    ----------------------------------------------------

    data Equality = Equal
      { Equality -> Dom' Term Type
    _eqType  :: Dom Type
      , Equality -> Term
    _eqLeft  :: Term
      , Equality -> Term
    _eqRight :: Term
      }

    -- Jesper, 2020-01-19: The type type lives in the context of the
    -- variables+equations, while the lhs/rhs only depend on the
    -- variables, so there is no way to give a correct Reduce instance.
    -- WRONG:
    -- instance Reduce Equality where
    --   reduce' (Equal a u v) = Equal <$> reduce' a <*> reduce' u <*> reduce' v

    eqConstructorForm :: HasBuiltins m => Equality -> m Equality
    eqConstructorForm :: forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqConstructorForm (Equal Dom' Term Type
    a Term
    u Term
    v) = Dom' Term Type -> Term -> Term -> Equality
    Equal Dom' Term Type
    a (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    u m (Term -> Equality) -> m Term -> m Equality
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm Term
    v

    eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality
    eqUnLevel :: forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    Equality -> m Equality
    eqUnLevel (Equal Dom' Term Type
    a Term
    u Term
    v) = Dom' Term Type -> Term -> Term -> Equality
    Equal Dom' Term Type
    a (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    unLevel Term
    u m (Term -> Equality) -> m Term -> m Equality
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    unLevel Term
    v
      where
        unLevel :: Term -> m Term
    unLevel (Level Level
    l) = Level -> m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    l
        unLevel Term
    u         = Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u

    ----------------------------------------------------
    -- Unify state
    ----------------------------------------------------

    data UnifyState = UState
      { UnifyState -> Telescope
    varTel   :: Telescope     -- ^ Don't reduce!
      , UnifyState -> FlexibleVars
    flexVars :: FlexibleVars
      , UnifyState -> Telescope
    eqTel    :: Telescope     -- ^ Can be reduced eagerly.
      , UnifyState -> [Arg Term]
    eqLHS    :: [Arg Term]    -- ^ Ends up in dot patterns (should not be reduced eagerly).
      , UnifyState -> [Arg Term]
    eqRHS    :: [Arg Term]    -- ^ Ends up in dot patterns (should not be reduced eagerly).
      } deriving (Int -> UnifyState -> ShowS
    [UnifyState] -> ShowS
    UnifyState -> String
    (Int -> UnifyState -> ShowS)
    -> (UnifyState -> String)
    -> ([UnifyState] -> ShowS)
    -> Show UnifyState
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnifyState -> ShowS
    showsPrec :: Int -> UnifyState -> ShowS
    $cshow :: UnifyState -> String
    show :: UnifyState -> String
    $cshowList :: [UnifyState] -> ShowS
    showList :: [UnifyState] -> ShowS
    Show)
    -- Issues #3578 and #4125: avoid unnecessary reduction in unifier.

    lensVarTel   :: Lens' UnifyState Telescope
    lensVarTel :: Lens' UnifyState Telescope
    lensVarTel   Telescope -> f Telescope
    f UnifyState
    s = Telescope -> f Telescope
    f (UnifyState -> Telescope
    varTel UnifyState
    s) f Telescope -> (Telescope -> UnifyState) -> f UnifyState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Telescope
    tel -> UnifyState
    s { varTel = tel }
    {-# INLINE lensVarTel #-}
    --UNUSED Liang-Ting Chen 2019-07-16
    --lensFlexVars :: Lens' UnifyState FlexibleVars
    --lensFlexVars f s = f (flexVars s) <&> \ flex -> s { flexVars = flex }

    lensEqTel    :: Lens' UnifyState Telescope
    lensEqTel :: Lens' UnifyState Telescope
    lensEqTel    Telescope -> f Telescope
    f UnifyState
    s = Telescope -> f Telescope
    f (UnifyState -> Telescope
    eqTel UnifyState
    s) f Telescope -> (Telescope -> UnifyState) -> f UnifyState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Telescope
    x -> UnifyState
    s { eqTel = x }
    {-# INLINE lensEqTel #-}

    --UNUSED Liang-Ting Chen 2019-07-16
    --lensEqLHS    :: Lens' UnifyState Args
    --lensEqLHS    f s = f (eqLHS s) <&> \ x -> s { eqLHS = x }

    --UNUSED Liang-Ting Chen 2019-07-16
    --lensEqRHS    :: Lens' UnifyState Args
    --lensEqRHS    f s = f (eqRHS s) <&> \ x -> s { eqRHS = x }

    -- UNUSED Andreas, 2019-10-14
    -- instance Reduce UnifyState where
    --   reduce' (UState var flex eq lhs rhs) =
    --     UState <$> reduce' var
    --            <*> pure flex
    --            <*> reduce' eq
    --            <*> reduce' lhs
    --            <*> reduce' rhs

    -- Andreas, 2019-10-14, issues #3578 and #4125:
    -- | Don't ever reduce the whole 'varTel', as it will destroy
    -- readability of the context in interactive editing!
    -- To make sure this insight is not lost, the following
    -- dummy instance should prevent a proper 'Reduce' instance for 'UnifyState'.
    instance Reduce UnifyState where
      reduce' :: UnifyState -> ReduceM UnifyState
    reduce' = UnifyState -> ReduceM UnifyState
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    --UNUSED Liang-Ting Chen 2019-07-16
    --reduceEqTel :: UnifyState -> TCM UnifyState
    --reduceEqTel = lensEqTel reduce

    -- UNUSED Andreas, 2019-10-14
    -- instance Normalise UnifyState where
    --   normalise' (UState var flex eq lhs rhs) =
    --     UState <$> normalise' var
    --            <*> pure flex
    --            <*> normalise' eq
    --            <*> normalise' lhs
    --            <*> normalise' rhs

    instance PrettyTCM UnifyState where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
    prettyTCM UnifyState
    state = m Doc
    "UnifyState" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
        [ m Doc
    "variable tel:  " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    gamma
        , m Doc
    "flexible vars: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(Int, IsForced)] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
    pshow ((FlexibleVar Int -> (Int, IsForced))
    -> FlexibleVars -> [(Int, IsForced)]
    forall a b. (a -> b) -> [a] -> [b]
    map FlexibleVar Int -> (Int, IsForced)
    forall {a}. FlexibleVar a -> (a, IsForced)
    flexVarF (FlexibleVars -> [(Int, IsForced)])
    -> FlexibleVars -> [(Int, IsForced)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> FlexibleVars
    flexVars UnifyState
    state)
        , m Doc
    "equation tel:  " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    delta)
        , m Doc
    "equations:     " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> Arg Term -> m Doc)
    -> [Arg Term] -> [Arg Term] -> [m Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Arg Term -> Arg Term -> m Doc
    forall {m :: * -> *} {a} {a}.
    (MonadFresh NameId m, MonadInteractionPoints m,
     MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
     Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
    a -> a -> m Doc
    prettyEquality (UnifyState -> [Arg Term]
    eqLHS UnifyState
    state) (UnifyState -> [Arg Term]
    eqRHS UnifyState
    state)))
        ])
        where
          flexVarF :: FlexibleVar a -> (a, IsForced)
    flexVarF FlexibleVar a
    fi = (FlexibleVar a -> a
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar a
    fi, FlexibleVar a -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar a
    fi)
          gamma :: Telescope
    gamma = UnifyState -> Telescope
    varTel UnifyState
    state
          delta :: Telescope
    delta = UnifyState -> Telescope
    eqTel UnifyState
    state
          prettyEquality :: a -> a -> m Doc
    prettyEquality a
    x a
    y = a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    x m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "=?=" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    y

    initUnifyState
      :: PureTCM m
      => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
    initUnifyState :: forall (m :: * -> *).
    PureTCM m =>
    Telescope
    -> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
    initUnifyState Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    lhs [Arg Term]
    rhs = do
      (tel, a, lhs, rhs) <- (Telescope, Type, [Arg Term], [Arg Term])
    -> m (Telescope, Type, [Arg Term], [Arg Term])
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Telescope
    tel, Type
    a, [Arg Term]
    lhs, [Arg Term]
    rhs)
      let n = [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    lhs
      unless (n == size rhs) __IMPOSSIBLE__
      TelV eqTel _ <- telView a
      unless (n == size eqTel) __IMPOSSIBLE__
      return $ UState tel flex eqTel lhs rhs
      -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
      -- reduce $ UState tel flex eqTel lhs rhs

    isUnifyStateSolved :: UnifyState -> Bool
    isUnifyStateSolved :: UnifyState -> Bool
    isUnifyStateSolved = Telescope -> Bool
    forall a. Null a => a -> Bool
    null (Telescope -> Bool)
    -> (UnifyState -> Telescope) -> UnifyState -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . UnifyState -> Telescope
    eqTel

    varCount :: UnifyState -> Int
    varCount :: UnifyState -> Int
    varCount = Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int)
    -> (UnifyState -> Telescope) -> UnifyState -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . UnifyState -> Telescope
    varTel

    -- | Get the type of the i'th variable in the given state
    getVarType :: Int -> UnifyState -> Dom Type
    getVarType :: Int -> UnifyState -> Dom' Term Type
    getVarType Int
    i UnifyState
    s = Dom' Term Type -> [Dom' Term Type] -> Int -> Dom' Term Type
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom' Term Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> [Dom' Term Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Telescope -> [Dom' Term Type]) -> Telescope -> [Dom' Term Type]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    varTel UnifyState
    s) Int
    i

    getVarTypeUnraised :: Int -> UnifyState -> Dom Type
    getVarTypeUnraised :: Int -> UnifyState -> Dom' Term Type
    getVarTypeUnraised Int
    i UnifyState
    s = (String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type)
    -> Dom' Term (String, Type) -> Dom' Term Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term (String, Type)
    -> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom' Term (String, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList (Telescope -> [Dom' Term (String, Type)])
    -> Telescope -> [Dom' Term (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    varTel UnifyState
    s) Int
    i

    eqCount :: UnifyState -> Int
    eqCount :: UnifyState -> Int
    eqCount = Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int)
    -> (UnifyState -> Telescope) -> UnifyState -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . UnifyState -> Telescope
    eqTel

    -- | Get the k'th equality in the given state. The left- and right-hand sides
    --   of the equality live in the varTel telescope, and the type of the equality
    --   lives in the varTel++eqTel telescope
    getEquality :: Int -> UnifyState -> Equality
    getEquality :: Int -> UnifyState -> Equality
    getEquality Int
    k UState { eqTel :: UnifyState -> Telescope
    eqTel = Telescope
    eqs, eqLHS :: UnifyState -> [Arg Term]
    eqLHS = [Arg Term]
    lhs, eqRHS :: UnifyState -> [Arg Term]
    eqRHS = [Arg Term]
    rhs } =
        Dom' Term Type -> Term -> Term -> Equality
    Equal (Dom' Term Type -> [Dom' Term Type] -> Int -> Dom' Term Type
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom' Term Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> [Dom' Term Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    eqs) Int
    k)
              (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> [Arg Term] -> Int -> Arg Term
    forall a. a -> [a] -> Int -> a
    indexWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    lhs Int
    k)
              (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> [Arg Term] -> Int -> Arg Term
    forall a. a -> [a] -> Int -> a
    indexWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    rhs Int
    k)

    getReducedEquality
      :: (MonadReduce m, MonadAddContext m)
      => Int -> UnifyState -> m Equality
    getReducedEquality :: forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> UnifyState -> m Equality
    getReducedEquality Int
    k UnifyState
    s = do
      let Equal Dom' Term Type
    a Term
    u Term
    v = Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      Telescope -> m Equality -> m Equality
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m Equality -> m Equality) -> m Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Term -> Term -> Equality
    Equal
        (Dom' Term Type -> Term -> Term -> Equality)
    -> m (Dom' Term Type) -> m (Term -> Term -> Equality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    eqTel UnifyState
    s) (Dom' Term Type -> m (Dom' Term Type)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Dom' Term Type
    a)
        m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
        m (Term -> Equality) -> m Term -> m Equality
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v

    -- | As getEquality, but with the unraised type
    getEqualityUnraised :: Int -> UnifyState -> Equality
    getEqualityUnraised :: Int -> UnifyState -> Equality
    getEqualityUnraised Int
    k UState { eqTel :: UnifyState -> Telescope
    eqTel = Telescope
    eqs, eqLHS :: UnifyState -> [Arg Term]
    eqLHS = [Arg Term]
    lhs, eqRHS :: UnifyState -> [Arg Term]
    eqRHS = [Arg Term]
    rhs } =
        Dom' Term Type -> Term -> Term -> Equality
    Equal ((String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type)
    -> Dom' Term (String, Type) -> Dom' Term Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term (String, Type)
    -> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom' Term (String, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    eqs) Int
    k)
              (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> [Arg Term] -> Int -> Arg Term
    forall a. a -> [a] -> Int -> a
    indexWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    lhs Int
    k)
              (Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> [Arg Term] -> Int -> Arg Term
    forall a. a -> [a] -> Int -> a
    indexWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    rhs Int
    k)

    getReducedEqualityUnraised
      :: (MonadReduce m, MonadAddContext m)
      => Int -> UnifyState -> m Equality
    getReducedEqualityUnraised :: forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> UnifyState -> m Equality
    getReducedEqualityUnraised Int
    k UnifyState
    s = do
      let Equal Dom' Term Type
    a Term
    u Term
    v = Int -> UnifyState -> Equality
    getEqualityUnraised Int
    k UnifyState
    s
      Telescope -> m Equality -> m Equality
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m Equality -> m Equality) -> m Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Term -> Term -> Equality
    Equal
        (Dom' Term Type -> Term -> Term -> Equality)
    -> m (Dom' Term Type) -> m (Term -> Term -> Equality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext ([Dom' Term (String, Type)] -> Telescope
    telFromList ([Dom' Term (String, Type)] -> Telescope)
    -> [Dom' Term (String, Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
    forall a. Int -> [a] -> [a]
    take Int
    k ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
    -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList (Telescope -> [Dom' Term (String, Type)])
    -> Telescope -> [Dom' Term (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s) (Dom' Term Type -> m (Dom' Term Type)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Dom' Term Type
    a)
        m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
        m (Term -> Equality) -> m Term -> m Equality
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v

    --UNUSED Liang-Ting Chen 2019-07-16
    --getEqInfo :: Int -> UnifyState -> ArgInfo
    --getEqInfo k UState { eqTel = eqs } =
    --  domInfo $ indexWithDefault __IMPOSSIBLE__ (telToList eqs) k
    --
    ---- | Add a list of equations to the front of the equation telescope
    --addEqs :: Telescope -> [Arg Term] -> [Arg Term] -> UnifyState -> UnifyState
    --addEqs tel us vs s =
    --  s { eqTel = tel `abstract` eqTel s
    --    , eqLHS = us ++ eqLHS s
    --    , eqRHS = vs ++ eqRHS s
    --    }
    --  where k = size tel
    --
    --addEq :: Type -> Arg Term -> Arg Term -> UnifyState -> UnifyState
    --addEq a u v = addEqs (ExtendTel (defaultDom a) (Abs underscore EmptyTel)) [u] [v]

    -- | Instantiate the k'th variable with the given value.
    --   Returns Nothing if there is a cycle.
    solveVar :: Int             -- ^ Index @k@
             -> DeBruijnPattern -- ^ Solution @u@
             -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
    solveVar :: Int
    -> Pattern' DBPatVar
    -> UnifyState
    -> Maybe (UnifyState, PatternSubstitution)
    solveVar Int
    k Pattern' DBPatVar
    u UnifyState
    s = case Telescope
    -> Int
    -> Pattern' DBPatVar
    -> Maybe (Telescope, PatternSubstitution, Permutation)
    instantiateTelescope (UnifyState -> Telescope
    varTel UnifyState
    s) Int
    k Pattern' DBPatVar
    u of
      Maybe (Telescope, PatternSubstitution, Permutation)
    Nothing -> Maybe (UnifyState, PatternSubstitution)
    forall a. Maybe a
    Nothing
      Just (Telescope
    tel' , PatternSubstitution
    sigma , Permutation
    rho) -> (UnifyState, PatternSubstitution)
    -> Maybe (UnifyState, PatternSubstitution)
    forall a. a -> Maybe a
    Just ((UnifyState, PatternSubstitution)
     -> Maybe (UnifyState, PatternSubstitution))
    -> (UnifyState, PatternSubstitution)
    -> Maybe (UnifyState, PatternSubstitution)
    forall a b. (a -> b) -> a -> b
    $ (,PatternSubstitution
    sigma) (UnifyState -> (UnifyState, PatternSubstitution))
    -> UnifyState -> (UnifyState, PatternSubstitution)
    forall a b. (a -> b) -> a -> b
    $ UState
          { varTel :: Telescope
    varTel   = Telescope
    tel'
          , flexVars :: FlexibleVars
    flexVars = Permutation -> FlexibleVars -> FlexibleVars
    permuteFlex (Permutation -> Permutation
    reverseP Permutation
    rho) (FlexibleVars -> FlexibleVars) -> FlexibleVars -> FlexibleVars
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> FlexibleVars
    flexVars UnifyState
    s
          , eqTel :: Telescope
    eqTel    = PatternSubstitution -> Telescope -> Telescope
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    sigma (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
          , eqLHS :: [Arg Term]
    eqLHS    = PatternSubstitution -> [Arg Term] -> [Arg Term]
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
          , eqRHS :: [Arg Term]
    eqRHS    = PatternSubstitution -> [Arg Term] -> [Arg Term]
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
          }
      where
        permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
        permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
    permuteFlex Permutation
    perm =
          (FlexibleVar Int -> Maybe (FlexibleVar Int))
    -> FlexibleVars -> FlexibleVars
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((FlexibleVar Int -> Maybe (FlexibleVar Int))
     -> FlexibleVars -> FlexibleVars)
    -> (FlexibleVar Int -> Maybe (FlexibleVar Int))
    -> FlexibleVars
    -> FlexibleVars
    forall a b. (a -> b) -> a -> b
    $ \(FlexibleVar ArgInfo
    ai IsForced
    fc FlexibleVarKind
    k Maybe Int
    p Int
    x) ->
            ArgInfo
    -> IsForced
    -> FlexibleVarKind
    -> Maybe Int
    -> Int
    -> FlexibleVar Int
    forall a.
    ArgInfo
    -> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
    FlexibleVar ArgInfo
    ai IsForced
    fc FlexibleVarKind
    k Maybe Int
    p (Int -> FlexibleVar Int) -> Maybe Int -> Maybe (FlexibleVar Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    x (Permutation -> [Int]
    permPicks Permutation
    perm)

    applyUnder :: Int -> Telescope -> Term -> Telescope
    applyUnder :: Int -> Telescope -> Term -> Telescope
    applyUnder Int
    k Telescope
    tel Term
    u
     | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0     = Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__
     | Int
    k Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    = Telescope
    tel Telescope -> Term -> Telescope
    forall t. Apply t => t -> Term -> t
    `apply1` Term
    u
     | Bool
    otherwise = case Telescope
    tel of
        Telescope
    EmptyTel         -> Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        ExtendTel Dom' Term Type
    a Abs Telescope
    tel' -> Dom' Term Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom' Term Type
    a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $
          String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Abs Telescope -> String
    forall a. Abs a -> String
    absName Abs Telescope
    tel') (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> Telescope -> Term -> Telescope
    applyUnder (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Abs Telescope -> Telescope
    forall a. Subst a => Abs a -> a
    absBody Abs Telescope
    tel') Term
    u

    dropAt :: Int -> [a] -> [a]
    dropAt :: forall a. Int -> [a] -> [a]
    dropAt Int
    _ [] = [a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    dropAt Int
    k (a
    x:[a]
    xs)
     | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0     = [a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
     | Int
    k Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    = [a]
    xs
     | Bool
    otherwise = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    dropAt (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) [a]
    xs

    -- | Solve the k'th equation with the given value, which can depend on
    --   regular variables but not on other equation variables.
    solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
    solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
    solveEq Int
    k Term
    u UnifyState
    s = (,PatternSubstitution
    sigma) (UnifyState -> (UnifyState, PatternSubstitution))
    -> UnifyState -> (UnifyState, PatternSubstitution)
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s
        { eqTel    = applyUnder k (eqTel s) u'
        , eqLHS    = dropAt k $ eqLHS s
        , eqRHS    = dropAt k $ eqRHS s
        }
      where
        u' :: Term
    u'    = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    k Term
    u
        n :: Int
    n     = UnifyState -> Int
    eqCount UnifyState
    s
        sigma :: PatternSubstitution
    sigma = Int -> PatternSubstitution -> PatternSubstitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (PatternSubstitution -> PatternSubstitution)
    -> PatternSubstitution -> PatternSubstitution
    forall a b. (a -> b) -> a -> b
    $ Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS (Term -> Pattern' DBPatVar
    forall a. Term -> Pattern' a
    dotP Term
    u') PatternSubstitution
    forall a. Substitution' a
    idS

    --UNUSED Liang-Ting Chen 2019-07-16
    ---- | Simplify the k'th equation with the given value (which can depend on other
    ----   equation variables). Returns Nothing if there is a cycle.
    --simplifyEq :: Int -> Term -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
    --simplifyEq k u s = case instantiateTelescope (eqTel s) k u of
    --  Nothing -> Nothing
    --  Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState
    --    { varTel   = varTel s
    --    , flexVars = flexVars s
    --    , eqTel    = tel'
    --    , eqLHS    = permute rho $ eqLHS s
    --    , eqRHS    = permute rho $ eqRHS s
    --    }
    --
    ----------------------------------------------------
    -- Unification strategies
    ----------------------------------------------------

    data UnifyStep
      = Deletion
        { UnifyStep -> Int
    deleteAt           :: Int
        , UnifyStep -> Type
    deleteType         :: Type
        , UnifyStep -> Term
    deleteLeft         :: Term
        , UnifyStep -> Term
    deleteRight        :: Term
        }
      | Solution
        { UnifyStep -> Int
    solutionAt         :: Int
        , UnifyStep -> Dom' Term Type
    solutionType       :: Dom Type
        , UnifyStep -> FlexibleVar Int
    solutionVar        :: FlexibleVar Int
        , UnifyStep -> Term
    solutionTerm       :: Term
        , UnifyStep -> Either () ()
    solutionSide       :: Either () ()
          -- ^ side of the equation where the variable is.
        }
      | Injectivity
        { UnifyStep -> Int
    injectAt           :: Int
        , UnifyStep -> Type
    injectType         :: Type
        , UnifyStep -> QName
    injectDatatype     :: QName
        , UnifyStep -> [Arg Term]
    injectParameters   :: Args
        , UnifyStep -> [Arg Term]
    injectIndices      :: Args
        , UnifyStep -> ConHead
    injectConstructor  :: ConHead
        }
      | Conflict
        { UnifyStep -> Int
    conflictAt         :: Int
        , UnifyStep -> Type
    conflictType       :: Type
        , UnifyStep -> QName
    conflictDatatype   :: QName
        , UnifyStep -> [Arg Term]
    conflictParameters :: Args
        , UnifyStep -> Term
    conflictLeft       :: Term
        , UnifyStep -> Term
    conflictRight      :: Term
        }
      | Cycle
        { UnifyStep -> Int
    cycleAt            :: Int
        , UnifyStep -> Type
    cycleType          :: Type
        , UnifyStep -> QName
    cycleDatatype      :: QName
        , UnifyStep -> [Arg Term]
    cycleParameters    :: Args
        , UnifyStep -> Int
    cycleVar           :: Int
        , UnifyStep -> Term
    cycleOccursIn      :: Term
        }
      | EtaExpandVar
        { UnifyStep -> FlexibleVar Int
    expandVar           :: FlexibleVar Int
        , UnifyStep -> QName
    expandVarRecordType :: QName
        , UnifyStep -> [Arg Term]
    expandVarParameters :: Args
        }
      | EtaExpandEquation
        { UnifyStep -> Int
    expandAt           :: Int
        , UnifyStep -> QName
    expandRecordType   :: QName
        , UnifyStep -> [Arg Term]
    expandParameters   :: Args
        }
      | LitConflict
        { UnifyStep -> Int
    litConflictAt      :: Int
        , UnifyStep -> Type
    litType            :: Type
        , UnifyStep -> Literal
    litConflictLeft    :: Literal
        , UnifyStep -> Literal
    litConflictRight   :: Literal
        }
      | StripSizeSuc
        { UnifyStep -> Int
    stripAt            :: Int
        , UnifyStep -> Term
    stripArgLeft       :: Term
        , UnifyStep -> Term
    stripArgRight      :: Term
        }
      | SkipIrrelevantEquation
        { UnifyStep -> Int
    skipIrrelevantAt   :: Int
        }
      | TypeConInjectivity
        { UnifyStep -> Int
    typeConInjectAt    :: Int
        , UnifyStep -> QName
    typeConstructor    :: QName
        , UnifyStep -> [Arg Term]
    typeConArgsLeft    :: Args
        , UnifyStep -> [Arg Term]
    typeConArgsRight   :: Args
        } deriving (Int -> UnifyStep -> ShowS
    [UnifyStep] -> ShowS
    UnifyStep -> String
    (Int -> UnifyStep -> ShowS)
    -> (UnifyStep -> String)
    -> ([UnifyStep] -> ShowS)
    -> Show UnifyStep
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnifyStep -> ShowS
    showsPrec :: Int -> UnifyStep -> ShowS
    $cshow :: UnifyStep -> String
    show :: UnifyStep -> String
    $cshowList :: [UnifyStep] -> ShowS
    showList :: [UnifyStep] -> ShowS
    Show)

    instance PrettyTCM UnifyStep where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    prettyTCM UnifyStep
    step = case UnifyStep
    step of
        Deletion Int
    k Type
    a Term
    u Term
    v -> m Doc
    "Deletion" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , m Doc
    "lhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          , m Doc
    "rhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          ])
        Solution Int
    k Dom' Term Type
    a FlexibleVar Int
    i Term
    u Either () ()
    s -> m Doc
    "Solution" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom' Term Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
    prettyTCM Dom' Term Type
    a
          , m Doc
    "variable:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text ((Int, Maybe Int, IsForced, FlexibleVarKind) -> String
    forall a. Show a => a -> String
    show (FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Int
    i, FlexibleVar Int -> Maybe Int
    forall a. FlexibleVar a -> Maybe Int
    flexPos FlexibleVar Int
    i, FlexibleVar Int -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar Int
    i, FlexibleVar Int -> FlexibleVarKind
    forall a. FlexibleVar a -> FlexibleVarKind
    flexKind FlexibleVar Int
    i))
          , m Doc
    "term:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          , m Doc
    "side:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Either () () -> String
    forall a. Show a => a -> String
    show Either () ()
    s)
          ])
        Injectivity Int
    k Type
    a QName
    d [Arg Term]
    pars [Arg Term]
    ixs ConHead
    c -> m Doc
    "Injectivity" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , m Doc
    "datatype:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
          , m Doc
    "parameters: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    pars)
          , m Doc
    "indices:    " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    ixs)
          , m Doc
    "constructor:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c
          ])
        Conflict Int
    k Type
    a QName
    d [Arg Term]
    pars Term
    u Term
    v -> m Doc
    "Conflict" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , m Doc
    "datatype:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
          , m Doc
    "parameters: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    pars)
          , m Doc
    "lhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          , m Doc
    "rhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          ])
        Cycle Int
    k Type
    a QName
    d [Arg Term]
    pars Int
    i Term
    u -> m Doc
    "Cycle" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , m Doc
    "datatype:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
          , m Doc
    "parameters: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    pars)
          , m Doc
    "variable:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    i)
          , m Doc
    "term:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          ])
        EtaExpandVar FlexibleVar Int
    fi QName
    r [Arg Term]
    pars -> m Doc
    "EtaExpandVar" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "variable:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (FlexibleVar Int -> String
    forall a. Show a => a -> String
    show FlexibleVar Int
    fi)
          , m Doc
    "record type:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    r
          , m Doc
    "parameters: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
    prettyTCM [Arg Term]
    pars
          ])
        EtaExpandEquation Int
    k QName
    r [Arg Term]
    pars -> m Doc
    "EtaExpandEquation" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "record type:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    r
          , m Doc
    "parameters: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
    prettyTCM [Arg Term]
    pars
          ])
        LitConflict Int
    k Type
    a Literal
    u Literal
    v -> m Doc
    "LitConflict" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "type:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , m Doc
    "lhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Literal -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Literal -> m Doc
    prettyTCM Literal
    u
          , m Doc
    "rhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Literal -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Literal -> m Doc
    prettyTCM Literal
    v
          ])
        StripSizeSuc Int
    k Term
    u Term
    v -> m Doc
    "StripSizeSuc" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "lhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          , m Doc
    "rhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          ])
        SkipIrrelevantEquation Int
    k -> m Doc
    "SkipIrrelevantEquation" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          ])
        TypeConInjectivity Int
    k QName
    d [Arg Term]
    us [Arg Term]
    vs -> m Doc
    "TypeConInjectivity" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
          [ m Doc
    "position:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    k)
          , m Doc
    "datatype:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
          , m Doc
    "lhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    us)
          , m Doc
    "rhs:        " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    vs)
          ])

    ----------------------------------------------------
    -- Unify Log and monad
    ----------------------------------------------------

    data UnifyLogEntry
     -- = UnificationDone  UnifyState
      = UnificationStep UnifyState UnifyStep UnifyOutput

    type UnifyLog = [(UnifyLogEntry,UnifyState)]

    -- | This variant of 'UnifyLog' is used to ensure that 'tell' is not
    -- expensive.
    type UnifyLog' = DList (UnifyLogEntry, UnifyState)

    -- Given varΓ ⊢ eqΓ, varΓ ⊢ us, vs : eqΓ
    data UnifyOutput = UnifyOutput
      { UnifyOutput -> PatternSubstitution
    unifySubst :: PatternSubstitution -- varΓ' ⊢ σ : varΓ
      , UnifyOutput -> PatternSubstitution
    unifyProof :: PatternSubstitution -- varΓ',eqΓ' ⊢ ps : eqΓ[σ]
                                          -- varΓ', us' =_eqΓ' vs' ⊢ ap(ps) : us[σ] =_{eqΓ[σ]} vs[σ]
    --  , unifyLog   :: UnifyLog
      }

    instance Semigroup UnifyOutput where
      UnifyOutput
    x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
    <> UnifyOutput
    y = UnifyOutput
        { unifySubst :: PatternSubstitution
    unifySubst = UnifyOutput -> PatternSubstitution
    unifySubst UnifyOutput
    y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` UnifyOutput -> PatternSubstitution
    unifySubst UnifyOutput
    x
        , unifyProof :: PatternSubstitution
    unifyProof = UnifyOutput -> PatternSubstitution
    unifyProof UnifyOutput
    y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` UnifyOutput -> PatternSubstitution
    unifyProof UnifyOutput
    x
    --    , unifyLog   = unifyLog x ++ unifyLog y
        }

    instance Monoid UnifyOutput where
      mempty :: UnifyOutput
    mempty  = PatternSubstitution -> PatternSubstitution -> UnifyOutput
    UnifyOutput PatternSubstitution
    forall a. Substitution' a
    IdS PatternSubstitution
    forall a. Substitution' a
    IdS -- []
      mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
    mappend = UnifyOutput -> UnifyOutput -> UnifyOutput
    forall a. Semigroup a => a -> a -> a
    (<>)

    type UnifyLogT m a = WriterT UnifyLog' m a

    type UnifyStepT m a = WriterT UnifyOutput m a

    tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
    tellUnifySubst :: forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifySubst PatternSubstitution
    sub = UnifyOutput -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
    forall a b. (a -> b) -> a -> b
    $ PatternSubstitution -> PatternSubstitution -> UnifyOutput
    UnifyOutput PatternSubstitution
    sub PatternSubstitution
    forall a. Substitution' a
    IdS

    tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
    tellUnifyProof :: forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    sub = UnifyOutput -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
    forall a b. (a -> b) -> a -> b
    $ PatternSubstitution -> PatternSubstitution -> UnifyOutput
    UnifyOutput PatternSubstitution
    forall a. Substitution' a
    IdS PatternSubstitution
    sub

    writeUnifyLog ::
      MonadWriter UnifyLog' m => (UnifyLogEntry, UnifyState) -> m ()
    writeUnifyLog :: forall (m :: * -> *).
    MonadWriter UnifyLog' m =>
    (UnifyLogEntry, UnifyState) -> m ()
    writeUnifyLog (UnifyLogEntry, UnifyState)
    x = UnifyLog' -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ((UnifyLogEntry, UnifyState) -> UnifyLog'
    forall el coll. Singleton el coll => el -> coll
    singleton (UnifyLogEntry, UnifyState)
    x) -- UnifyOutput IdS IdS [x]

    runUnifyLogT :: Functor m => UnifyLogT m a -> m (a, UnifyLog)
    runUnifyLogT :: forall (m :: * -> *) a.
    Functor m =>
    UnifyLogT m a -> m (a, UnifyLog)
    runUnifyLogT UnifyLogT m a
    m = (UnifyLog' -> UnifyLog) -> (a, UnifyLog') -> (a, UnifyLog)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd UnifyLog' -> UnifyLog
    forall a. DList a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList ((a, UnifyLog') -> (a, UnifyLog))
    -> m (a, UnifyLog') -> m (a, UnifyLog)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> UnifyLogT m a -> m (a, UnifyLog')
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT UnifyLogT m a
    m