    {-# LANGUAGE NondecreasingIndentation #-}

    -- | Unification algorithm for specializing datatype indices, as described in
    --     \"Unifiers as Equivalences: Proof-Relevant Unification of Dependently
    --     Typed Data\" by Jesper Cockx, Dominique Devriese, and Frank Piessens
    --     (ICFP 2016).
    --
    --   This is the unification algorithm used for checking the left-hand side
    --   of clauses (see @Agda.TypeChecking.Rules.LHS@), coverage checking (see
    --   @Agda.TypeChecking.Coverage@) and indirectly also for interactive case
    --   splitting (see @Agda.Interaction.MakeCase@).
    --
    --   A unification problem (of type @UnifyState@) consists of:
    --
    --   1. A telescope @varTel@ of free variables, some or all of which are
    --      flexible (as indicated by @flexVars@).
    --
    --   2. A telescope @eqTel@ containing the types of the equations.
    --
    --   3. Left- and right-hand sides for each equation:
    --      @varTel ⊢ eqLHS : eqTel@ and @varTel ⊢ eqRHS : eqTel@.
    --
    --   The unification algorithm can end in three different ways:
    --   (type @UnificationResult@):
    --
    --   - A *positive success* @Unifies (tel, sigma, ps)@ with @tel ⊢ sigma : varTel@,
    --     @tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel@,
    --     and @tel ⊢ ps : eqTel@. In this case, @sigma;ps@ is an *equivalence*
    --     between the telescopes @tel@ and @varTel(eqLHS ≡ eqRHS)@.
    --
    --   - A *negative success* @NoUnify err@ means that a conflicting equation
    --     was found (e.g an equation between two distinct constructors or a cycle).
    --
    --   - A *failure* @UnifyStuck err@ means that the unifier got stuck.
    --
    --   The unification algorithm itself consists of two parts:
    --
    --   1. A *unification strategy* takes a unification problem and produces a
    --      list of suggested unification rules (of type @UnifyStep@). Strategies
    --      can be constructed by composing simpler strategies (see for example the
    --      definition of @completeStrategyAt@).
    --
    --   2. The *unification engine* @unifyStep@ takes a unification rule and tries
    --      to apply it to the given state, writing the result to the UnifyOutput
    --      on a success.
    --
    --   The unification steps (of type @UnifyStep@) are the following:
    --
    --   - *Deletion* removes a reflexive equation @u =?= v : a@ if the left- and
    --     right-hand side @u@ and @v@ are (definitionally) equal. This rule results
    --     in a failure if --without-K is enabled (see \"Pattern Matching Without K\"
    --     by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014).
    --
    --   - *Solution* solves an equation if one side is (eta-equivalent to) a
    --     flexible variable. In case both sides are flexible variables, the
    --     unification strategy makes a choice according to the @chooseFlex@
    --     function in @Agda.TypeChecking.Rules.LHS.Problem@.
    --
    --   - *Injectivity* decomposes an equation of the form
    --     @c us =?= c vs : D pars is@ where @c : Δc → D pars js@ is a constructor
    --     of the inductive datatype @D@ into a sequence of equations
    --     @us =?= vs : delta@. In case @D@ is an indexed datatype,
    --     *higher-dimensional unification* is applied (see below).
    --
    --   - *Conflict* detects absurd equations of the form
    --     @c₁ us =?= c₂ vs : D pars is@ where @c₁@ and @c₂@ are two distinct
    --     constructors of the datatype @D@.
    --
    --   - *Cycle* detects absurd equations of the form @x =?= v : D pars is@ where
    --     @x@ is a variable of the datatype @D@ that occurs strongly rigid in @v@.
    --
    --   - *EtaExpandVar* eta-expands a single flexible variable @x : R@ where @R@
    --     is a (eta-expandable) record type, replacing it by one variable for each
    --     field of @R@.
    --
    --   - *EtaExpandEquation* eta-expands an equation @u =?= v : R@ where @R@ is a
    --     (eta-expandable) record type, replacing it by one equation for each field
    --     of @R@. The left- and right-hand sides of these equations are the
    --     projections of @u@ and @v@.
    --
    --   - *LitConflict* detects absurd equations of the form @l₁ =?= l₂ : A@ where
    --     @l₁@ and @l₂@ are distinct literal terms.
    --
    --   - *StripSizeSuc* simplifies an equation of the form
    --     @sizeSuc x =?= sizeSuc y : Size@ to @x =?= y : Size@.
    --
    --   - *SkipIrrelevantEquation@ removes an equation between irrelevant terms.
    --
    --   - *TypeConInjectivity* decomposes an equation of the form
    --     @D us =?= D vs : Set i@ where @D@ is a datatype. This rule is only used
    --     if --injective-type-constructors is enabled.
    --
    --   Higher-dimensional unification (new, does not yet appear in any paper):
    --   If an equation of the form @c us =?= c vs : D pars is@ is encountered where
    --   @c : Δc → D pars js@ is a constructor of an indexed datatype
    --   @D pars : Φ → Set ℓ@, it is in general unsound to just simplify this
    --   equation to @us =?= vs : Δc@. For this reason, the injectivity rule in the
    --   paper restricts the indices @is@ to be distinct variables that are bound in
    --   the telescope @eqTel@. But we can be more general by introducing new
    --   variables @ks@ to the telescope @eqTel@ and equating these to @is@:
    --   @
    --       Δ₁(x : D pars is)Δ₂
    --        ≃
    --       Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂
    --   @
    --   Since @ks@ are distinct variables, it's now possible to apply injectivity
    --   to the equation @x@, resulting in the following new equation telescope:
    --   @
    --     Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂
    --   @
    --   Now we can solve the equations @ps@ by recursively calling the unification
    --   algorithm with flexible variables @Δ₁(ys : Δc)@. This is called
    --   *higher-dimensional unification* since we are unifying equality proofs
    --   rather than terms. If the higher-dimensional unification succeeds, the
    --   resulting telescope serves as the new equation telescope for the original
    --   unification problem.

    module Agda.TypeChecking.Rules.LHS.Unify
      ( UnificationResult
      , UnificationResult'(..)
      , unifyIndices ) where

    import Prelude hiding (null)

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

    import Data.Semigroup hiding (Arg)
    import qualified Data.List as List
    import qualified Data.IntSet as IntSet
    import qualified Data.IntMap as IntMap
    import Data.IntMap (IntMap)

    import qualified Agda.Benchmarking as Bench

    import Agda.Interaction.Options (optInjectiveTypeConstructors)

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

    import Agda.TypeChecking.Monad
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Conversion.Pure
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Irrelevance
    import Agda.TypeChecking.Level (reallyUnLevelView)
    import Agda.TypeChecking.Reduce
    import qualified Agda.TypeChecking.Patterns.Match as Match
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Precompute
    import Agda.TypeChecking.Free.Reduce
    import Agda.TypeChecking.Records

    import Agda.TypeChecking.Rules.LHS.Problem

    import Agda.Utils.Benchmark
    import Agda.Utils.Either
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.ListT
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.PartialOrd
    import Agda.Utils.Permutation
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | Result of 'unifyIndices'.
    type UnificationResult = UnificationResult'
      ( Telescope                  -- @tel@
      , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
      , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
      )

    data UnificationResult' a
      = Unifies  a                        -- ^ Unification succeeded.
      | NoUnify  NegativeUnification      -- ^ Terms are not unifiable.
      | UnifyBlocked Blocker              -- ^ Unification got blocked on a metavariable
      | UnifyStuck   [UnificationFailure] -- ^ Some other error happened, unification got stuck.
      deriving (Int -> UnificationResult' a -> ShowS
    [UnificationResult' a] -> ShowS
    UnificationResult' a -> String
    (Int -> UnificationResult' a -> ShowS)
    -> (UnificationResult' a -> String)
    -> ([UnificationResult' a] -> ShowS)
    -> Show (UnificationResult' a)
    forall a. Show a => Int -> UnificationResult' a -> ShowS
    forall a. Show a => [UnificationResult' a] -> ShowS
    forall a. Show a => UnificationResult' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [UnificationResult' a] -> ShowS
    $cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
    show :: UnificationResult' a -> String
    $cshow :: forall a. Show a => UnificationResult' a -> String
    showsPrec :: Int -> UnificationResult' a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> UnificationResult' a -> ShowS
    Show, (forall a b.
     (a -> b) -> UnificationResult' a -> UnificationResult' b)
    -> (forall a b. a -> UnificationResult' b -> UnificationResult' a)
    -> Functor UnificationResult'
    forall a b. a -> UnificationResult' b -> UnificationResult' a
    forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
    $c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
    fmap :: forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    $cfmap :: forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    Functor, (forall m. Monoid m => UnificationResult' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
    -> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
    -> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
    -> (forall a. UnificationResult' a -> [a])
    -> (forall a. UnificationResult' a -> Bool)
    -> (forall a. UnificationResult' a -> Int)
    -> (forall a. Eq a => a -> UnificationResult' a -> Bool)
    -> (forall a. Ord a => UnificationResult' a -> a)
    -> (forall a. Ord a => UnificationResult' a -> a)
    -> (forall a. Num a => UnificationResult' a -> a)
    -> (forall a. Num a => UnificationResult' a -> a)
    -> Foldable UnificationResult'
    forall a. Eq a => a -> UnificationResult' a -> Bool
    forall a. Num a => UnificationResult' a -> a
    forall a. Ord a => UnificationResult' a -> a
    forall m. Monoid m => UnificationResult' m -> m
    forall a. UnificationResult' a -> Bool
    forall a. UnificationResult' a -> Int
    forall a. UnificationResult' a -> [a]
    forall a. (a -> a -> a) -> UnificationResult' a -> a
    forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => UnificationResult' a -> a
    $cproduct :: forall a. Num a => UnificationResult' a -> a
    sum :: forall a. Num a => UnificationResult' a -> a
    $csum :: forall a. Num a => UnificationResult' a -> a
    minimum :: forall a. Ord a => UnificationResult' a -> a
    $cminimum :: forall a. Ord a => UnificationResult' a -> a
    maximum :: forall a. Ord a => UnificationResult' a -> a
    $cmaximum :: forall a. Ord a => UnificationResult' a -> a
    elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
    $celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
    length :: forall a. UnificationResult' a -> Int
    $clength :: forall a. UnificationResult' a -> Int
    null :: forall a. UnificationResult' a -> Bool
    $cnull :: forall a. UnificationResult' a -> Bool
    toList :: forall a. UnificationResult' a -> [a]
    $ctoList :: forall a. UnificationResult' a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    fold :: forall m. Monoid m => UnificationResult' m -> m
    $cfold :: forall m. Monoid m => UnificationResult' m -> m
    Foldable, Functor UnificationResult'
    Foldable UnificationResult'
    Functor UnificationResult'
    -> Foldable UnificationResult'
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> UnificationResult' a -> f (UnificationResult' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        UnificationResult' (f a) -> f (UnificationResult' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> UnificationResult' a -> m (UnificationResult' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        UnificationResult' (m a) -> m (UnificationResult' a))
    -> Traversable UnificationResult'
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a)
    forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
    Traversable)

    -- | Unify indices.
    --
    --   In @unifyIndices gamma flex a us vs@,
    --
    --   * @us@ and @vs@ are the argument lists to unify, eliminating type @a@.
    --
    --   * @gamma@ is the telescope of free variables in @us@ and @vs@.
    --
    --   * @flex@ is the set of flexible (instantiable) variabes in @us@ and @vs@.
    --
    --   The result is the most general unifier of @us@ and @vs@.
    unifyIndices
      :: (PureTCM m, MonadBench m, BenchPhase m ~ Bench.Phase)
      => Telescope     -- ^ @gamma@
      -> FlexibleVars  -- ^ @flex@
      -> Type          -- ^ @a@
      -> Args          -- ^ @us@
      -> Args          -- ^ @vs@
      -> m UnificationResult
    unifyIndices :: forall (m :: * -> *).
    (PureTCM m, MonadBench m, BenchPhase m ~ Phase) =>
    Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    unifyIndices Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs =
      Account (BenchPhase m)
    -> m UnificationResult -> m UnificationResult
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase m
    Phase
    Bench.Typing, BenchPhase m
    Phase
    Bench.CheckLHS, BenchPhase m
    Phase
    Bench.UnifyIndices] (m UnificationResult -> m UnificationResult)
    -> m UnificationResult -> m UnificationResult
    forall a b. (a -> b) -> a -> b
    $
        Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    forall (m :: * -> *).
    PureTCM m =>
    Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    unifyIndices' Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs

    unifyIndices'
      :: (PureTCM m)
      => Telescope     -- ^ @gamma@
      -> FlexibleVars  -- ^ @flex@
      -> Type          -- ^ @a@
      -> Args          -- ^ @us@
      -> Args          -- ^ @vs@
      -> m UnificationResult
    unifyIndices' :: forall (m :: * -> *).
    PureTCM m =>
    Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    unifyIndices' Telescope
    tel FlexibleVars
    flex Type
    a [] [] = UnificationResult -> m UnificationResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult -> m UnificationResult)
    -> UnificationResult -> m UnificationResult
    forall a b. (a -> b) -> a -> b
    $ (Telescope, Substitution' (Pattern' DBPatVar),
     [NamedArg (Pattern' DBPatVar)])
    -> UnificationResult
    forall a. a -> UnificationResult' a
    Unifies (Telescope
    tel, Substitution' (Pattern' DBPatVar)
    forall a. Substitution' a
    idS, [])
    unifyIndices' Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs = do
        String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
          [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "unifyIndices"
              , (TCMT IO Doc
    "tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
              , (TCMT IO Doc
    "flex =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Int] -> String
    forall a. Show a => a -> String
    show ([Int] -> String) -> [Int] -> String
    forall a b. (a -> b) -> a -> b
    $ (FlexibleVar Int -> Int) -> FlexibleVars -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVars
    flex
              , (TCMT IO Doc
    "a    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a)
              , (TCMT IO Doc
    "us   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    us
              , (TCMT IO Doc
    "vs   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    vs
              ]
        UnifyState
    initialState    <- Telescope
    -> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
    forall (m :: * -> *).
    PureTCM m =>
    Telescope
    -> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
    initUnifyState Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs
        String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "initial unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> UnifyState -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM UnifyState
    initialState
        String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "initial unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (UnifyState -> String
    forall a. Show a => a -> String
    show UnifyState
    initialState)
        (UnificationResult' UnifyState
    result,UnifyOutput
    output) <- UnifyLogT m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState, UnifyOutput)
    forall (m :: * -> *) a. UnifyLogT m a -> m (a, UnifyOutput)
    runUnifyLogT (UnifyLogT m (UnificationResult' UnifyState)
     -> m (UnificationResult' UnifyState, UnifyOutput))
    -> UnifyLogT m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState, UnifyOutput)
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    -> UnifyStrategy -> UnifyLogT m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
    unify UnifyState
    initialState UnifyStrategy
    rightToLeftStrategy
        let ps :: [NamedArg (Pattern' DBPatVar)]
    ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifyProof UnifyOutput
    output) ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs (UnifyState -> Telescope
    eqTel UnifyState
    initialState)
        UnificationResult -> m UnificationResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult -> m UnificationResult)
    -> UnificationResult -> m UnificationResult
    forall a b. (a -> b) -> a -> b
    $ (UnifyState
     -> (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)]))
    -> UnificationResult' UnifyState -> UnificationResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\UnifyState
    s -> (UnifyState -> Telescope
    varTel UnifyState
    s , UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifySubst UnifyOutput
    output , [NamedArg (Pattern' DBPatVar)]
    ps)) UnificationResult' UnifyState
    result

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

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

    instance Reduce Equality where
      reduce' :: Equality -> ReduceM Equality
    reduce' (Equal Dom' Term Type
    a Term
    u Term
    v) = Dom' Term Type -> Term -> Term -> Equality
    Equal (Dom' Term Type -> Term -> Term -> Equality)
    -> ReduceM (Dom' Term Type) -> ReduceM (Term -> Term -> Equality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Type -> ReduceM (Dom' Term Type)
    forall t. Reduce t => t -> ReduceM t
    reduce' Dom' Term Type
    a ReduceM (Term -> Term -> Equality)
    -> ReduceM Term -> ReduceM (Term -> Equality)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> ReduceM Term
    forall t. Reduce t => t -> ReduceM t
    reduce' Term
    u ReduceM (Term -> Equality) -> ReduceM Term -> ReduceM Equality
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> ReduceM Term
    forall t. Reduce t => t -> ReduceM t
    reduce' Term
    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 (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 => Equality -> m Equality
    eqUnLevel :: forall (m :: * -> *). HasBuiltins 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 (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 (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
    showList :: [UnifyState] -> ShowS
    $cshowList :: [UnifyState] -> ShowS
    show :: UnifyState -> String
    $cshow :: UnifyState -> String
    showsPrec :: Int -> UnifyState -> ShowS
    $cshowsPrec :: Int -> UnifyState -> ShowS
    Show)
    -- Issues #3578 and #4125: avoid unnecessary reduction in unifier.

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

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

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

    --UNUSED Liang-Ting Chen 2019-07-16
    --lensEqRHS    :: Lens' Args UnifyState
    --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
    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
    addContext Telescope
    gamma (Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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}.
    (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames 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
    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
    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
      (Telescope
    tel, Type
    a, [Arg Term]
    lhs, [Arg Term]
    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 :: Int
    n = [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    lhs
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    rhs) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      TelV Telescope
    eqTel Type
    _ <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      UnifyState -> m UnifyState
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> FlexibleVars
    -> Telescope
    -> [Arg Term]
    -> [Arg Term]
    -> UnifyState
    UState Telescope
    tel FlexibleVars
    flex Telescope
    eqTel [Arg Term]
    lhs [Arg Term]
    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)

    -- | 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)

    --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, Substitution' (Pattern' DBPatVar))
    solveVar Int
    k Pattern' DBPatVar
    u UnifyState
    s = case Telescope
    -> Int
    -> Pattern' DBPatVar
    -> Maybe
         (Telescope, Substitution' (Pattern' DBPatVar), Permutation)
    instantiateTelescope (UnifyState -> Telescope
    varTel UnifyState
    s) Int
    k Pattern' DBPatVar
    u of
      Maybe (Telescope, Substitution' (Pattern' DBPatVar), Permutation)
    Nothing -> Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    forall a. Maybe a
    Nothing
      Just (Telescope
    tel' , Substitution' (Pattern' DBPatVar)
    sigma , Permutation
    rho) -> (UnifyState, Substitution' (Pattern' DBPatVar))
    -> Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    forall a. a -> Maybe a
    Just ((UnifyState, Substitution' (Pattern' DBPatVar))
     -> Maybe (UnifyState, Substitution' (Pattern' DBPatVar)))
    -> (UnifyState, Substitution' (Pattern' DBPatVar))
    -> Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ (,Substitution' (Pattern' DBPatVar)
    sigma) (UnifyState -> (UnifyState, Substitution' (Pattern' DBPatVar)))
    -> UnifyState -> (UnifyState, Substitution' (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ UState :: Telescope
    -> FlexibleVars
    -> Telescope
    -> [Arg Term]
    -> [Arg Term]
    -> UnifyState
    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    = Substitution' (Pattern' DBPatVar) -> Telescope -> Telescope
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    sigma (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
          , eqLHS :: [Arg Term]
    eqLHS    = Substitution' (Pattern' DBPatVar) -> [Arg Term] -> [Arg Term]
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    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    = Substitution' (Pattern' DBPatVar) -> [Arg Term] -> [Arg Term]
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    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, Substitution' (Pattern' DBPatVar))
    solveEq Int
    k Term
    u UnifyState
    s = (,Substitution' (Pattern' DBPatVar)
    sigma) (UnifyState -> (UnifyState, Substitution' (Pattern' DBPatVar)))
    -> UnifyState -> (UnifyState, Substitution' (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s
        { eqTel :: Telescope
    eqTel    = Int -> Telescope -> Term -> Telescope
    applyUnder Int
    k (UnifyState -> Telescope
    eqTel UnifyState
    s) Term
    u'
        , eqLHS :: [Arg Term]
    eqLHS    = Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    dropAt Int
    k ([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    = Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    dropAt Int
    k ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    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 :: Substitution' (Pattern' DBPatVar)
    sigma = Int
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    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) (Substitution' (Pattern' DBPatVar)
     -> Substitution' (Pattern' DBPatVar))
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ Pattern' DBPatVar
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS (Term -> Pattern' DBPatVar
    forall a. Term -> Pattern' a
    dotP Term
    u') Substitution' (Pattern' DBPatVar)
    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
        }
      | 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
    showList :: [UnifyStep] -> ShowS
    $cshowList :: [UnifyStep] -> ShowS
    show :: UnifyStep -> String
    $cshow :: UnifyStep -> String
    showsPrec :: Int -> UnifyStep -> ShowS
    $cshowsPrec :: Int -> 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
    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
    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
    prettyTCM Term
    v
          ])
        Solution Int
    k Dom' Term Type
    a FlexibleVar Int
    i Term
    u -> 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
    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
    prettyTCM Term
    u
          ])
        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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    prettyTCM [Arg Term]
    vs)
          ])

    type UnifyStrategy = forall m. (PureTCM m, MonadPlus m) => UnifyState -> m UnifyStep

    --UNUSED Liang-Ting Chen 2019-07-16
    --leftToRightStrategy :: UnifyStrategy
    --leftToRightStrategy s =
    --    msum (for [0..n-1] $ \k -> completeStrategyAt k s)
    --  where n = size $ eqTel s

    rightToLeftStrategy :: UnifyStrategy
    rightToLeftStrategy :: UnifyStrategy
    rightToLeftStrategy UnifyState
    s =
        [m UnifyStep] -> m UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([Int] -> (Int -> m UnifyStep) -> [m UnifyStep]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) ((Int -> m UnifyStep) -> [m UnifyStep])
    -> (Int -> m UnifyStep) -> [m UnifyStep]
    forall a b. (a -> b) -> a -> b
    $ \Int
    k -> Int -> UnifyStrategy
    completeStrategyAt Int
    k UnifyState
    s)
      where n :: Int
    n = Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> Telescope -> Int
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s

    completeStrategyAt :: Int -> UnifyStrategy
    completeStrategyAt :: Int -> UnifyStrategy
    completeStrategyAt Int
    k UnifyState
    s = [m UnifyStep] -> m UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([m UnifyStep] -> m UnifyStep) -> [m UnifyStep] -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ ((Int -> UnifyState -> m UnifyStep) -> m UnifyStep)
    -> [Int -> UnifyState -> m UnifyStep] -> [m UnifyStep]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int -> UnifyState -> m UnifyStep
    strat -> Int -> UnifyState -> m UnifyStep
    strat Int
    k UnifyState
    s) ([Int -> UnifyState -> m UnifyStep] -> [m UnifyStep])
    -> [Int -> UnifyState -> m UnifyStep] -> [m UnifyStep]
    forall a b. (a -> b) -> a -> b
    $
    -- ASR (2021-02-07). The below eta-expansions are required by GHC >=
    -- 9.0.1 (see Issue #4955).
        [ (\Int
    n -> Int -> UnifyStrategy
    skipIrrelevantStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    basicUnifyStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    literalStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    dataStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    etaExpandVarStrategy  Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    etaExpandEquationStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    injectiveTypeConStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    injectivePragmaStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    simplifySizesStrategy Int
    n)
        , (\Int
    n -> Int -> UnifyStrategy
    checkEqualityStrategy Int
    n)
        ]

    -- | @isHom n x@ returns x lowered by n if the variables 0..n-1 don't occur in x.
    --
    -- This is naturally sensitive to normalization.
    isHom :: (Free a, Subst a) => Int -> a -> Maybe a
    isHom :: forall a. (Free a, Subst a) => Int -> a -> Maybe a
    isHom Int
    n a
    x = do
      Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $ SingleVar All -> IgnoreSorts -> a -> All
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree (Bool -> All
    All (Bool -> All) -> (Int -> Bool) -> SingleVar All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n)) IgnoreSorts
    IgnoreNot a
    x
      a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> a
    forall a. Subst a => Int -> a -> a
    raise (-Int
    n) a
    x

    findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
    findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    i FlexibleVars
    flex = (FlexibleVar Int -> Bool)
    -> FlexibleVars -> Maybe (FlexibleVar Int)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Int -> Bool)
    -> (FlexibleVar Int -> Int) -> FlexibleVar Int -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar) FlexibleVars
    flex

    basicUnifyStrategy :: Int -> UnifyStrategy
    basicUnifyStrategy :: Int -> UnifyStrategy
    basicUnifyStrategy Int
    k UnifyState
    s = do
      Equal dom :: Dom' Term Type
    dom@Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s)
        -- Andreas, 2019-02-23: reduce equality for the sake of isHom?
      Type
    ha <- Maybe Type -> m Type
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe Type -> m Type) -> Maybe Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Maybe Type
    forall a. (Free a, Subst a) => Int -> a -> Maybe a
    isHom Int
    n Type
    a
      (Maybe Int
    mi, Maybe Int
    mj) <- Telescope -> m (Maybe Int, Maybe Int) -> m (Maybe Int, Maybe Int)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m (Maybe Int, Maybe Int) -> m (Maybe Int, Maybe Int))
    -> m (Maybe Int, Maybe Int) -> m (Maybe Int, Maybe Int)
    forall a b. (a -> b) -> a -> b
    $ (,) (Maybe Int -> Maybe Int -> (Maybe Int, Maybe Int))
    -> m (Maybe Int) -> m (Maybe Int -> (Maybe Int, Maybe Int))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Type -> m (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    u Type
    ha m (Maybe Int -> (Maybe Int, Maybe Int))
    -> m (Maybe Int) -> m (Maybe Int, Maybe Int)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> Type -> m (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    v Type
    ha
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "isEtaVar results: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text ([Maybe Int] -> String
    forall a. Show a => a -> String
    show [Maybe Int
    mi,Maybe Int
    mj])
      case (Maybe Int
    mi, Maybe Int
    mj) of
        (Just Int
    i, Just Int
    j)
         | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero -- Taken care of by checkEqualityStrategy
        (Just Int
    i, Just Int
    j)
         | Just FlexibleVar Int
    fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    i FlexibleVars
    flex
         , Just FlexibleVar Int
    fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    j FlexibleVars
    flex -> do
           let choice :: FlexChoice
    choice = FlexibleVar Int -> FlexibleVar Int -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex FlexibleVar Int
    fi FlexibleVar Int
    fj
               firstTryLeft :: m UnifyStep
    firstTryLeft  = [m UnifyStep] -> m UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum [ UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fi Term
    v)
                                    , UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fj Term
    u)]
               firstTryRight :: m UnifyStep
    firstTryRight = [m UnifyStep] -> m UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum [ UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fj Term
    u)
                                    , UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fi Term
    v)]
           String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "fi = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (FlexibleVar Int -> String
    forall a. Show a => a -> String
    show FlexibleVar Int
    fi)
           String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "fj = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (FlexibleVar Int -> String
    forall a. Show a => a -> String
    show FlexibleVar Int
    fj)
           String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "chooseFlex: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (FlexChoice -> String
    forall a. Show a => a -> String
    show FlexChoice
    choice)
           case FlexChoice
    choice of
             FlexChoice
    ChooseLeft   -> m UnifyStep
    firstTryLeft
             FlexChoice
    ChooseRight  -> m UnifyStep
    firstTryRight
             FlexChoice
    ExpandBoth   -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero -- This should be taken care of by etaExpandEquationStrategy
             FlexChoice
    ChooseEither -> m UnifyStep
    firstTryRight
        (Just Int
    i, Maybe Int
    _)
         | Just FlexibleVar Int
    fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    i FlexibleVars
    flex -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fi Term
    v
        (Maybe Int
    _, Just Int
    j)
         | Just FlexibleVar Int
    fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    j FlexibleVars
    flex -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
    Solution Int
    k Dom' Term Type
    dom{unDom :: Type
    unDom = Type
    ha} FlexibleVar Int
    fj Term
    u
        (Maybe Int, Maybe Int)
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      where
        flex :: FlexibleVars
    flex = UnifyState -> FlexibleVars
    flexVars UnifyState
    s
        n :: Int
    n = UnifyState -> Int
    eqCount UnifyState
    s

    dataStrategy :: Int -> UnifyStrategy
    dataStrategy :: Int -> UnifyStrategy
    dataStrategy Int
    k UnifyState
    s = do
      Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqConstructorForm (Equality -> m Equality) -> m Equality -> m Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Equality -> m Equality) -> m Equality -> m Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Int -> UnifyState -> Equality
    getEqualityUnraised Int
    k UnifyState
    s)
      Sort
    sa <- Sort -> m Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    a
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
        Def QName
    d Elims
    es | Type{} <- Sort
    sa -> do
          Int
    npars <- m (Maybe Int) -> m Int
    forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
    catMaybesMP (m (Maybe Int) -> m Int) -> m (Maybe Int) -> m Int
    forall a b. (a -> b) -> a -> b
    $ QName -> m (Maybe Int)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
    getNumberOfParameters QName
    d
          let ([Arg Term]
    pars,[Arg Term]
    ixs) = Int -> [Arg Term] -> ([Arg Term], [Arg Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    npars ([Arg Term] -> ([Arg Term], [Arg Term]))
    -> [Arg Term] -> ([Arg Term], [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` UnifyState -> Telescope
    eqTel UnifyState
    s) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Found equation at datatype " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d
             TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " with parameters " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Int -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size (UnifyState -> Telescope
    eqTel UnifyState
    s) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k) [Arg Term]
    pars)
          case (Term
    u, Term
    v) of
            (Con ConHead
    c ConInfo
    _ Elims
    _   , Con ConHead
    c' ConInfo
    _ Elims
    _  ) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c' -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int
    -> Type
    -> QName
    -> [Arg Term]
    -> [Arg Term]
    -> ConHead
    -> UnifyStep
    Injectivity Int
    k Type
    a QName
    d [Arg Term]
    pars [Arg Term]
    ixs ConHead
    c
            (Con ConHead
    c ConInfo
    _ Elims
    _   , Con ConHead
    c' ConInfo
    _ Elims
    _  ) -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> QName -> [Arg Term] -> Term -> Term -> UnifyStep
    Conflict Int
    k Type
    a QName
    d [Arg Term]
    pars Term
    u Term
    v
            (Var Int
    i []  , Term
    v         ) -> Int -> Term -> m UnifyStep -> m UnifyStep
    forall {m :: * -> *} {a} {b}.
    (ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
    Int -> a -> m b -> m b
    ifOccursStronglyRigid Int
    i Term
    v (m UnifyStep -> m UnifyStep) -> m UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> QName -> [Arg Term] -> Int -> Term -> UnifyStep
    Cycle Int
    k Type
    a QName
    d [Arg Term]
    pars Int
    i Term
    v
            (Term
    u         , Var Int
    j []  ) -> Int -> Term -> m UnifyStep -> m UnifyStep
    forall {m :: * -> *} {a} {b}.
    (ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
    Int -> a -> m b -> m b
    ifOccursStronglyRigid Int
    j Term
    u (m UnifyStep -> m UnifyStep) -> m UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> QName -> [Arg Term] -> Int -> Term -> UnifyStep
    Cycle Int
    k Type
    a QName
    d [Arg Term]
    pars Int
    j Term
    u
            (Term, Term)
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        Term
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      where
        ifOccursStronglyRigid :: Int -> a -> m b -> m b
    ifOccursStronglyRigid Int
    i a
    u m b
    ret = do
            -- Call forceNotFree to reduce u as far as possible
            -- around any occurrences of i
            (IntMap IsFree
    _ , a
    u) <- IntSet -> a -> m (IntMap IsFree, a)
    forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree (Int -> IntSet
    forall el coll. Singleton el coll => el -> coll
    singleton Int
    i) a
    u
            case Int -> a -> Maybe (FlexRig' ())
    forall a. Free a => Int -> a -> Maybe (FlexRig' ())
    flexRigOccurrenceIn Int
    i a
    u of
              Just FlexRig' ()
    StronglyRigid -> m b
    ret
              Maybe (FlexRig' ())
    _ -> m b
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    checkEqualityStrategy :: Int -> UnifyStrategy
    checkEqualityStrategy :: Int -> UnifyStrategy
    checkEqualityStrategy Int
    k UnifyState
    s = do
      let Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v = Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
          n :: Int
    n = UnifyState -> Int
    eqCount UnifyState
    s
      Type
    ha <- Maybe Type -> m Type
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe Type -> m Type) -> Maybe Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Maybe Type
    forall a. (Free a, Subst a) => Int -> a -> Maybe a
    isHom Int
    n Type
    a
      UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Term -> Term -> UnifyStep
    Deletion Int
    k Type
    ha Term
    u Term
    v

    literalStrategy :: Int -> UnifyStrategy
    literalStrategy :: Int -> UnifyStrategy
    literalStrategy Int
    k UnifyState
    s = do
      let n :: Int
    n = UnifyState -> Int
    eqCount UnifyState
    s
      Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      Type
    ha <- Maybe Type -> m Type
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe Type -> m Type) -> Maybe Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Maybe Type
    forall a. (Free a, Subst a) => Int -> a -> Maybe a
    isHom Int
    n Type
    a
      (Term
    u, Term
    v) <- (Term, Term) -> m (Term, Term)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term
    u, Term
    v)
      case (Term
    u , Term
    v) of
        (Lit Literal
    l1 , Lit Literal
    l2)
         | Literal
    l1 Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l2  -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Term -> Term -> UnifyStep
    Deletion Int
    k Type
    ha Term
    u Term
    v
         | Bool
    otherwise -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Literal -> Literal -> UnifyStep
    LitConflict Int
    k Type
    ha Literal
    l1 Literal
    l2
        (Term, Term)
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    etaExpandVarStrategy :: Int -> UnifyStrategy
    etaExpandVarStrategy :: Int -> UnifyStrategy
    etaExpandVarStrategy Int
    k UnifyState
    s = do
      Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Equality -> m Equality)
    -> (Equality -> m Equality) -> Equality -> m Equality
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      Term -> Term -> Type -> UnifyStrategy
    shouldEtaExpand Term
    u Term
    v Type
    a UnifyState
    s m UnifyStep -> m UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Term -> Term -> Type -> UnifyStrategy
    shouldEtaExpand Term
    v Term
    u Type
    a UnifyState
    s
      where
        -- TODO: use IsEtaVar to check if the term is a variable
        shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
        shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
    shouldEtaExpand (Var Int
    i Elims
    es) Term
    v Type
    a UnifyState
    s = do
          FlexibleVar Int
    fi       <- Maybe (FlexibleVar Int) -> m (FlexibleVar Int)
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe (FlexibleVar Int) -> m (FlexibleVar Int))
    -> Maybe (FlexibleVar Int) -> m (FlexibleVar Int)
    forall a b. (a -> b) -> a -> b
    $ Int -> FlexibleVars -> Maybe (FlexibleVar Int)
    findFlexible Int
    i (UnifyState -> FlexibleVars
    flexVars UnifyState
    s)
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Found flexible variable " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    i)
          -- Issue 2888: Do this if there are only projections or if it's a singleton
          -- record or if it's unified against a record constructor term. Basically
          -- we need to avoid EtaExpandEquation if EtaExpandVar is possible, or the
          -- forcing translation is unhappy.
          Type
    b         <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom' Term Type -> Type) -> Dom' Term Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Dom' Term Type
    getVarTypeUnraised (UnifyState -> Int
    varCount UnifyState
    s Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) UnifyState
    s
          (QName
    d, [Arg Term]
    pars) <- m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term])
    forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
    catMaybesMP (m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term]))
    -> m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ Type -> m (Maybe (QName, [Arg Term]))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, [Arg Term]))
    isEtaRecordType Type
    b
          [(ProjOrigin, QName)]
    ps        <- Maybe [(ProjOrigin, QName)] -> m [(ProjOrigin, QName)]
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe [(ProjOrigin, QName)] -> m [(ProjOrigin, QName)])
    -> Maybe [(ProjOrigin, QName)] -> m [(ProjOrigin, QName)]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [(ProjOrigin, QName)]
    forall t. [Elim' t] -> Maybe [(ProjOrigin, QName)]
    allProjElims Elims
    es
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> m Bool -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    orM
            [ Bool -> m Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [(ProjOrigin, QName)] -> Bool
    forall a. Null a => a -> Bool
    null [(ProjOrigin, QName)]
    ps
            , Term -> m Bool
    forall {f :: * -> *}. HasConstInfo f => Term -> f Bool
    isRecCon Term
    v  -- is the other term a record constructor?
            , (Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right Bool
    True Either Blocker Bool -> Either Blocker Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Either Blocker Bool -> Bool) -> m (Either Blocker Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (QName -> [Arg Term] -> BlockT m Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> [Arg Term] -> m Bool
    isSingletonRecord QName
    d [Arg Term]
    pars)
            ]
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "with projections " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (ProjOrigin, QName) -> QName
    forall a b. (a, b) -> b
    snd [(ProjOrigin, QName)]
    ps)
          String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "at record type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d
          UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ FlexibleVar Int -> QName -> [Arg Term] -> UnifyStep
    EtaExpandVar FlexibleVar Int
    fi QName
    d [Arg Term]
    pars
        shouldEtaExpand Term
    _ Term
    _ Type
    _ UnifyState
    _ = m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        isRecCon :: Term -> f Bool
    isRecCon (Con ConHead
    c ConInfo
    _ Elims
    _) = Maybe (QName, Defn) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (QName, Defn) -> Bool) -> f (Maybe (QName, Defn)) -> f Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> f (Maybe (QName, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor (ConHead -> QName
    conName ConHead
    c)
        isRecCon Term
    _           = Bool -> f Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    etaExpandEquationStrategy :: Int -> UnifyStrategy
    etaExpandEquationStrategy :: Int -> UnifyStrategy
    etaExpandEquationStrategy Int
    k UnifyState
    s = do
      -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
      Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEqualityUnraised Int
    k UnifyState
    s
      (QName
    d, [Arg Term]
    pars) <- m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term])
    forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
    catMaybesMP (m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term]))
    -> m (Maybe (QName, [Arg Term])) -> m (QName, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> m (Maybe (QName, [Arg Term])) -> m (Maybe (QName, [Arg Term]))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m (Maybe (QName, [Arg Term])) -> m (Maybe (QName, [Arg Term])))
    -> m (Maybe (QName, [Arg Term])) -> m (Maybe (QName, [Arg Term]))
    forall a b. (a -> b) -> a -> b
    $ Type -> m (Maybe (QName, [Arg Term]))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, [Arg Term]))
    isEtaRecordType Type
    a
      Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> m Bool -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    orM
        [ (Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right Bool
    True Either Blocker Bool -> Either Blocker Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Either Blocker Bool -> Bool) -> m (Either Blocker Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (QName -> [Arg Term] -> BlockT m Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> [Arg Term] -> m Bool
    isSingletonRecord QName
    d [Arg Term]
    pars)
        , Term -> m Bool
    forall (m :: * -> *). PureTCM m => Term -> m Bool
    shouldProject Term
    u
        , Term -> m Bool
    forall (m :: * -> *). PureTCM m => Term -> m Bool
    shouldProject Term
    v
        ]
      UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> QName -> [Arg Term] -> UnifyStep
    EtaExpandEquation Int
    k QName
    d [Arg Term]
    pars
      where
        shouldProject :: PureTCM m => Term -> m Bool
        shouldProject :: forall (m :: * -> *). PureTCM m => Term -> m Bool
    shouldProject = \case
          Def QName
    f Elims
    es   -> QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    usesCopatterns QName
    f
          Con ConHead
    c ConInfo
    _ Elims
    _  -> Maybe (QName, Defn) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (QName, Defn) -> Bool) -> m (Maybe (QName, Defn)) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe (QName, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor (ConHead -> QName
    conName ConHead
    c)

          Var Int
    _ Elims
    _    -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Lam ArgInfo
    _ Abs Term
    _    -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lit Literal
    _      -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Pi Dom' Term Type
    _ Abs Type
    _     -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Sort Sort
    _     -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level Level
    _    -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaV MetaId
    _ Elims
    _  -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DontCare Term
    _ -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Dummy String
    s Elims
    _  -> String -> m Bool
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

        tel :: Telescope
    tel = UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` [Dom' Term (String, Type)] -> Telescope
    telFromList (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)

    simplifySizesStrategy :: Int -> UnifyStrategy
    simplifySizesStrategy :: Int -> UnifyStrategy
    simplifySizesStrategy Int
    k UnifyState
    s = do
      QName -> Bool
    isSizeName <- m (QName -> Bool)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (QName -> Bool)
    isSizeNameTest
      Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v <- Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
        Def QName
    d Elims
    _ -> do
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Bool
    isSizeName QName
    d
          SizeView
    su <- Term -> m SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
          SizeView
    sv <- Term -> m SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    v
          case (SizeView
    su, SizeView
    sv) of
            (SizeSuc Term
    u, SizeSuc Term
    v) -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term -> UnifyStep
    StripSizeSuc Int
    k Term
    u Term
    v
            (SizeSuc Term
    u, SizeView
    SizeInf  ) -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term -> UnifyStep
    StripSizeSuc Int
    k Term
    u Term
    v
            (SizeView
    SizeInf  , SizeSuc Term
    v) -> UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term -> UnifyStep
    StripSizeSuc Int
    k Term
    u Term
    v
            (SizeView, SizeView)
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        Term
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    injectiveTypeConStrategy :: Int -> UnifyStrategy
    injectiveTypeConStrategy :: Int -> UnifyStrategy
    injectiveTypeConStrategy Int
    k UnifyState
    s = do
      Bool
    injTyCon <- PragmaOptions -> Bool
    optInjectiveTypeConstructors (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    injTyCon
      Equality
    eq <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Equality -> m Equality)
    -> (Equality -> m Equality) -> Equality -> m Equality
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      case Equality
    eq of
        Equal Dom' Term Type
    a u :: Term
    u@(Def QName
    d Elims
    es) v :: Term
    v@(Def QName
    d' Elims
    es') | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' -> do
          -- d must be a data, record or axiom
          Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ case Definition -> Defn
    theDef Definition
    def of
                    Datatype{} -> Bool
    True
                    Record{}   -> Bool
    True
                    Axiom{}    -> Bool
    True
                    DataOrRecSig{} -> Bool
    True
                    AbstractDefn{} -> Bool
    False -- True triggers issue #2250
                    Function{}   -> Bool
    False
                    Primitive{}  -> Bool
    False
                    PrimitiveSort{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    GeneralizableVar{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Constructor{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- Never a type!
          let us :: [Arg Term]
    us = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              vs :: [Arg Term]
    vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es'
          UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
    TypeConInjectivity Int
    k QName
    d [Arg Term]
    us [Arg Term]
    vs
        Equality
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    injectivePragmaStrategy :: Int -> UnifyStrategy
    injectivePragmaStrategy :: Int -> UnifyStrategy
    injectivePragmaStrategy Int
    k UnifyState
    s = do
      Equality
    eq <- Equality -> m Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqUnLevel (Equality -> m Equality)
    -> (Equality -> m Equality) -> Equality -> m Equality
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Equality -> m Equality
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Equality -> m Equality) -> Equality -> m Equality
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
      case Equality
    eq of
        Equal Dom' Term Type
    a u :: Term
    u@(Def QName
    d Elims
    es) v :: Term
    v@(Def QName
    d' Elims
    es') | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' -> do
          -- d must have an injective pragma
          Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ Definition -> Bool
    defInjective Definition
    def
          let us :: [Arg Term]
    us = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              vs :: [Arg Term]
    vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es'
          UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
    TypeConInjectivity Int
    k QName
    d [Arg Term]
    us [Arg Term]
    vs
        Equality
    _ -> m UnifyStep
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    skipIrrelevantStrategy :: Int -> UnifyStrategy
    skipIrrelevantStrategy :: Int -> UnifyStrategy
    skipIrrelevantStrategy Int
    k UnifyState
    s = do
      let Equal Dom' Term Type
    a Term
    _ Term
    _ = Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s                               -- reduce not necessary
      Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ())
    -> (Either Blocker Bool -> Bool) -> Either Blocker Bool -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Either Blocker Bool -> Either Blocker Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right Bool
    True) (Either Blocker Bool -> m ()) -> m (Either Blocker Bool) -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (Dom' Term Type -> BlockT m Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM Dom' Term Type
    a)  -- reduction takes place here
      -- TODO: do something in case the above is blocked (i.e. `Left b`)
      UnifyStep -> m UnifyStep
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> m UnifyStep) -> UnifyStep -> m UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Int -> UnifyStep
    SkipIrrelevantEquation Int
    k

    ----------------------------------------------------
    -- Actually doing the unification
    ----------------------------------------------------

    data UnifyLogEntry
      = UnificationStep  UnifyState UnifyStep
    --  | UnificationDone  UnifyState -- unused?

    type UnifyLog = [UnifyLogEntry]

    data UnifyOutput = UnifyOutput
      { UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifySubst :: PatternSubstitution
      , UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifyProof :: PatternSubstitution
      , UnifyOutput -> UnifyLog
    unifyLog   :: UnifyLog
      }

    instance Semigroup UnifyOutput where
      UnifyOutput
    x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
    <> UnifyOutput
    y = UnifyOutput :: Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar) -> UnifyLog -> UnifyOutput
    UnifyOutput
        { unifySubst :: Substitution' (Pattern' DBPatVar)
    unifySubst = UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifySubst UnifyOutput
    y Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifySubst UnifyOutput
    x
        , unifyProof :: Substitution' (Pattern' DBPatVar)
    unifyProof = UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifyProof UnifyOutput
    y Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` UnifyOutput -> Substitution' (Pattern' DBPatVar)
    unifyProof UnifyOutput
    x
        , unifyLog :: UnifyLog
    unifyLog   = UnifyOutput -> UnifyLog
    unifyLog UnifyOutput
    x UnifyLog -> UnifyLog -> UnifyLog
    forall a. [a] -> [a] -> [a]
    ++ UnifyOutput -> UnifyLog
    unifyLog UnifyOutput
    y
        }

    instance Monoid UnifyOutput where
      mempty :: UnifyOutput
    mempty  = Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar) -> UnifyLog -> UnifyOutput
    UnifyOutput Substitution' (Pattern' DBPatVar)
    forall a. Substitution' a
    IdS Substitution' (Pattern' DBPatVar)
    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 UnifyOutput m a

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

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

    writeUnifyLog :: MonadWriter UnifyOutput m => UnifyLogEntry -> m ()
    writeUnifyLog :: forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    UnifyLogEntry -> m ()
    writeUnifyLog UnifyLogEntry
    x = UnifyOutput -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
    forall a b. (a -> b) -> a -> b
    $ Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar) -> UnifyLog -> UnifyOutput
    UnifyOutput Substitution' (Pattern' DBPatVar)
    forall a. Substitution' a
    IdS Substitution' (Pattern' DBPatVar)
    forall a. Substitution' a
    IdS [UnifyLogEntry
    x]

    runUnifyLogT :: UnifyLogT m a -> m (a,UnifyOutput)
    runUnifyLogT :: forall (m :: * -> *) a. UnifyLogT m a -> m (a, UnifyOutput)
    runUnifyLogT = WriterT UnifyOutput m a -> m (a, UnifyOutput)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT

    unifyStep
      :: (PureTCM m, MonadWriter UnifyOutput m)
      => UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)

    unifyStep :: forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    unifyStep UnifyState
    s Deletion{ deleteAt :: UnifyStep -> Int
    deleteAt = Int
    k , deleteType :: UnifyStep -> Type
    deleteType = Type
    a , deleteLeft :: UnifyStep -> Term
    deleteLeft = Term
    u , deleteRight :: UnifyStep -> Term
    deleteRight = Term
    v } = do
        -- Check definitional equality of u and v
        Either Blocker Bool
    isReflexive <- Telescope -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m (Either Blocker Bool) -> m (Either Blocker Bool))
    -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT m Bool -> m (Either Blocker Bool))
    -> BlockT m Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> BlockT m Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Term -> Term -> m Bool
    pureEqualTerm Type
    a Term
    u Term
    v
        Bool
    withoutK <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption
        Bool
    splitOnStrict <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envSplitOnStrict
        case Either Blocker Bool
    isReflexive of
          Left Blocker
    block   -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked Blocker
    block
          Right Bool
    False  -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []
          Right Bool
    True | Bool
    withoutK Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    splitOnStrict
                       -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [Telescope -> Type -> Term -> UnificationFailure
    UnifyReflexiveEq (UnifyState -> Telescope
    varTel UnifyState
    s) Type
    a Term
    u]
          Right Bool
    True   -> do
            let (UnifyState
    s', Substitution' (Pattern' DBPatVar)
    sigma) = Int
    -> Term
    -> UnifyState
    -> (UnifyState, Substitution' (Pattern' DBPatVar))
    solveEq Int
    k Term
    u UnifyState
    s
            Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    sigma
            UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> m UnifyState -> m (UnificationResult' UnifyState)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Telescope -> m Telescope) -> UnifyState -> m UnifyState
    Lens' Telescope UnifyState
    lensEqTel Telescope -> m Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce UnifyState
    s'

    unifyStep UnifyState
    s step :: UnifyStep
    step@Solution{} = RetryNormalised
    -> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    RetryNormalised
    -> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    solutionStep RetryNormalised
    RetryNormalised UnifyState
    s UnifyStep
    step

    unifyStep UnifyState
    s (Injectivity Int
    k Type
    a QName
    d [Arg Term]
    pars [Arg Term]
    ixs ConHead
    c) = do
      m Bool
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> m Bool) -> QName -> m Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (m (UnificationResult' UnifyState)
     -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
      Bool
    withoutK <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption

      -- Split equation telescope into parts before and after current equation
      let ([Dom' Term (String, Type)]
    eqListTel1, Dom' Term (String, Type)
    _ : [Dom' Term (String, Type)]
    eqListTel2) = Int
    -> [Dom' Term (String, Type)]
    -> ([Dom' Term (String, Type)], [Dom' Term (String, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    k ([Dom' Term (String, Type)]
     -> ([Dom' Term (String, Type)], [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
          (Telescope
    eqTel1, Telescope
    eqTel2) = ([Dom' Term (String, Type)] -> Telescope
    telFromList [Dom' Term (String, Type)]
    eqListTel1, [Dom' Term (String, Type)] -> Telescope
    telFromList [Dom' Term (String, Type)]
    eqListTel2)

      -- Get constructor telescope and target indices
      Definition
    cdef  <- ConHead -> m Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    c
      let ctype :: Type
    ctype  = Definition -> Type
    defType Definition
    cdef Type -> [Arg Term] -> Type
    `piApply` [Arg Term]
    pars
      Telescope -> m () -> m ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel1) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Constructor type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ctype
      TelV Telescope
    ctel Type
    ctarget <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    ctype
      let cixs :: [Arg Term]
    cixs = case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    ctarget of
                   Def QName
    d' Elims
    es | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d' ->
                     let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                     in  Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    drop ([Arg Term] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg Term]
    pars) [Arg Term]
    args
                   Term
    _ -> [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      -- Get index telescope of the datatype
      Type
    dtype    <- (Type -> [Arg Term] -> Type
    `piApply` [Arg Term]
    pars) (Type -> Type) -> (Definition -> Type) -> Definition -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      Telescope -> m () -> m ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel1) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Datatype type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    dtype

      -- This is where the magic of higher-dimensional unification happens
      -- We need to generalize the indices `ixs` to the target indices of the
      -- constructor `cixs`. This is done by calling the unification algorithm
      -- recursively (this doesn't get stuck in a loop because a type should
      -- never be indexed over itself). Note the similarity with the
      -- computeNeighbourhood function in Agda.TypeChecking.Coverage.
      let hduTel :: Telescope
    hduTel = Telescope
    eqTel1 Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    ctel
          notforced :: [IsForced]
    notforced = Int -> IsForced -> [IsForced]
    forall a. Int -> a -> [a]
    replicate (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    hduTel) IsForced
    NotForced
      UnificationResult
    res <- Telescope -> m UnificationResult -> m UnificationResult
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m UnificationResult -> m UnificationResult)
    -> m UnificationResult -> m UnificationResult
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    forall (m :: * -> *).
    PureTCM m =>
    Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> m UnificationResult
    unifyIndices'
               Telescope
    hduTel
               ([IsForced] -> Telescope -> FlexibleVars
    allFlexVars [IsForced]
    notforced Telescope
    hduTel)
               (Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ctel) Type
    dtype)
               (Int -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ctel) [Arg Term]
    ixs)
               [Arg Term]
    cixs
      case UnificationResult
    res of
        -- Higher-dimensional unification can never end in a conflict,
        -- because `cong c1 ...` and `cong c2 ...` don't even have the
        -- same type for distinct constructors c1 and c2.
        NoUnify NegativeUnification
    _ -> m (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Higher-dimensional unification is blocked: propagate
        UnifyBlocked Blocker
    block -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked Blocker
    block

        -- Higher-dimensional unification has failed. If not --without-K,
        -- we can simply ignore the higher-dimensional equations and
        -- simplify the equation as in the non-indexed case.
        UnifyStuck [UnificationFailure]
    _ | Bool -> Bool
    not Bool
    withoutK -> do
          -- using the same variable names as in the case where hdu succeeds.
          let eqTel1' :: Telescope
    eqTel1' = Telescope
    eqTel1 Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    ctel
              rho1 :: Substitution' (Pattern' DBPatVar)
    rho1    = Int -> Substitution' (Pattern' DBPatVar)
    forall a. Int -> Substitution' a
    raiseS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ctel)
              ceq :: Pattern' DBPatVar
    ceq     = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    noConPatternInfo ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
    -> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    ctel
              rho3 :: Substitution' (Pattern' DBPatVar)
    rho3    = Pattern' DBPatVar
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Pattern' DBPatVar
    ceq Substitution' (Pattern' DBPatVar)
    rho1
              eqTel2' :: Telescope
    eqTel2' = Substitution' (Pattern' DBPatVar) -> Telescope -> Telescope
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho3 Telescope
    eqTel2
              eqTel' :: Telescope
    eqTel'  = Telescope
    eqTel1' Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel2'
              rho :: Substitution' (Pattern' DBPatVar)
    rho     = Int
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel2) Substitution' (Pattern' DBPatVar)
    rho3

          Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    rho

          Telescope
    eqTel' <- Telescope -> m Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Telescope
    eqTel'

          -- Compute new lhs and rhs by matching the old ones against rho
          ([Arg Term]
    lhs', [Arg Term]
    rhs') <- do
            let ps :: [NamedArg (Pattern' DBPatVar)]
    ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (Pattern' DBPatVar)
    Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    rho ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs (Telescope -> [NamedArg (Pattern' DBPatVar)])
    -> Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
            (Match Term
    lhsMatch, [Arg Term]
    _) <- [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
    ps ([Arg Term] -> m (Match Term, [Arg Term]))
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
            (Match Term
    rhsMatch, [Arg Term]
    _) <- [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
    ps ([Arg Term] -> m (Match Term, [Arg Term]))
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
            case (Match Term
    lhsMatch, Match Term
    rhsMatch) of
              (Match.Yes Simplification
    _ IntMap (Arg Term)
    lhs', Match.Yes Simplification
    _ IntMap (Arg Term)
    rhs') -> ([Arg Term], [Arg Term]) -> m ([Arg Term], [Arg Term])
    forall (m :: * -> *) a. Monad m => a -> m a
    return
                ([Arg Term] -> [Arg Term]
    forall a. [a] -> [a]
    reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Empty -> Int -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel') IntMap (Arg Term)
    lhs',
                 [Arg Term] -> [Arg Term]
    forall a. [a] -> [a]
    reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Empty -> Int -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel') IntMap (Arg Term)
    rhs')
              (Match Term, Match Term)
    _ -> m ([Arg Term], [Arg Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> UnifyState -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s { eqTel :: Telescope
    eqTel = Telescope
    eqTel' , eqLHS :: [Arg Term]
    eqLHS = [Arg Term]
    lhs' , eqRHS :: [Arg Term]
    eqRHS = [Arg Term]
    rhs' }

        UnifyStuck [UnificationFailure]
    _ -> let n :: Int
    n           = UnifyState -> Int
    eqCount UnifyState
    s
                            Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v = Int -> UnifyState -> Equality
    getEquality Int
    k UnifyState
    s
                        in UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [Telescope
    -> Type -> Term -> Term -> [Arg Term] -> UnificationFailure
    UnifyIndicesNotVars
                             (UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` UnifyState -> Telescope
    eqTel UnifyState
    s) Type
    a
                             (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    n Term
    u) (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    n Term
    v) (Int -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Int -> a -> a
    raise (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    k) [Arg Term]
    ixs)]

        Unifies (Telescope
    eqTel1', Substitution' (Pattern' DBPatVar)
    rho0, [NamedArg (Pattern' DBPatVar)]
    _) -> do
          -- Split ps0 into parts for eqTel1 and ctel
          let (Substitution' (Pattern' DBPatVar)
    rho1, Substitution' (Pattern' DBPatVar)
    rho2) = Int
    -> Substitution' (Pattern' DBPatVar)
    -> (Substitution' (Pattern' DBPatVar),
        Substitution' (Pattern' DBPatVar))
    forall a.
    Int -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ctel) Substitution' (Pattern' DBPatVar)
    rho0

          -- Compute new equation telescope context and substitution
          let ceq :: Pattern' DBPatVar
    ceq     = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    noConPatternInfo ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
    -> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (Pattern' DBPatVar)
    Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    rho2 ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    ctel
              rho3 :: Substitution' (Pattern' DBPatVar)
    rho3    = Pattern' DBPatVar
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Pattern' DBPatVar
    ceq Substitution' (Pattern' DBPatVar)
    rho1
              eqTel2' :: Telescope
    eqTel2' = Substitution' (Pattern' DBPatVar) -> Telescope -> Telescope
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho3 Telescope
    eqTel2
              eqTel' :: Telescope
    eqTel'  = Telescope
    eqTel1' Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel2'
              rho :: Substitution' (Pattern' DBPatVar)
    rho     = Int
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel2) Substitution' (Pattern' DBPatVar)
    rho3

          Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    rho

          Telescope
    eqTel' <- Telescope -> m Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Telescope
    eqTel'

          -- Compute new lhs and rhs by matching the old ones against rho
          ([Arg Term]
    lhs', [Arg Term]
    rhs') <- do
            let ps :: [NamedArg (Pattern' DBPatVar)]
    ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (Pattern' DBPatVar)
    Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    rho ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs (Telescope -> [NamedArg (Pattern' DBPatVar)])
    -> Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
            (Match Term
    lhsMatch, [Arg Term]
    _) <- [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
    ps ([Arg Term] -> m (Match Term, [Arg Term]))
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
            (Match Term
    rhsMatch, [Arg Term]
    _) <- [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall (m :: * -> *).
    MonadMatch m =>
    [NamedArg (Pattern' DBPatVar)]
    -> [Arg Term] -> m (Match Term, [Arg Term])
    Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
    ps ([Arg Term] -> m (Match Term, [Arg Term]))
    -> [Arg Term] -> m (Match Term, [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
            case (Match Term
    lhsMatch, Match Term
    rhsMatch) of
              (Match.Yes Simplification
    _ IntMap (Arg Term)
    lhs', Match.Yes Simplification
    _ IntMap (Arg Term)
    rhs') -> ([Arg Term], [Arg Term]) -> m ([Arg Term], [Arg Term])
    forall (m :: * -> *) a. Monad m => a -> m a
    return
                ([Arg Term] -> [Arg Term]
    forall a. [a] -> [a]
    reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Empty -> Int -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel') IntMap (Arg Term)
    lhs',
                 [Arg Term] -> [Arg Term]
    forall a. [a] -> [a]
    reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Empty -> Int -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqTel') IntMap (Arg Term)
    rhs')
              (Match Term, Match Term)
    _ -> m ([Arg Term], [Arg Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> UnifyState -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s { eqTel :: Telescope
    eqTel = Telescope
    eqTel' , eqLHS :: [Arg Term]
    eqLHS = [Arg Term]
    lhs' , eqRHS :: [Arg Term]
    eqRHS = [Arg Term]
    rhs' }

    unifyStep UnifyState
    s Conflict
      { conflictLeft :: UnifyStep -> Term
    conflictLeft  = Term
    u
      , conflictRight :: UnifyStep -> Term
    conflictRight = Term
    v
      } =
      case Term
    u of
        Con ConHead
    h ConInfo
    _ Elims
    _ -> do
          m Bool
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> m Bool) -> QName -> m Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    h) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (m (UnificationResult' UnifyState)
     -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
            UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ NegativeUnification -> UnificationResult' UnifyState
    forall a. NegativeUnification -> UnificationResult' a
    NoUnify (NegativeUnification -> UnificationResult' UnifyState)
    -> NegativeUnification -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Term -> Term -> NegativeUnification
    UnifyConflict (UnifyState -> Telescope
    varTel UnifyState
    s) Term
    u Term
    v
        Term
    _ -> m (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    unifyStep UnifyState
    s Cycle
      { cycleVar :: UnifyStep -> Int
    cycleVar        = Int
    i
      , cycleOccursIn :: UnifyStep -> Term
    cycleOccursIn   = Term
    u
      } =
      case Term
    u of
        Con ConHead
    h ConInfo
    _ Elims
    _ -> do
          m Bool
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> m Bool) -> QName -> m Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    h) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (m (UnificationResult' UnifyState)
     -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
            UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ NegativeUnification -> UnificationResult' UnifyState
    forall a. NegativeUnification -> UnificationResult' a
    NoUnify (NegativeUnification -> UnificationResult' UnifyState)
    -> NegativeUnification -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int -> Term -> NegativeUnification
    UnifyCycle (UnifyState -> Telescope
    varTel UnifyState
    s) Int
    i Term
    u
        Term
    _ -> m (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unifyStep UnifyState
    s EtaExpandVar{ expandVar :: UnifyStep -> FlexibleVar Int
    expandVar = FlexibleVar Int
    fi, expandVarRecordType :: UnifyStep -> QName
    expandVarRecordType = QName
    d , expandVarParameters :: UnifyStep -> [Arg Term]
    expandVarParameters = [Arg Term]
    pars } = do
      Defn
    recd <- Defn -> Maybe Defn -> Defn
    forall a. a -> Maybe a -> a
    fromMaybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Defn -> Defn) -> m (Maybe Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    d
      let delta :: Telescope
    delta = Defn -> Telescope
    recTel Defn
    recd Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    pars
          c :: ConHead
    c     = Defn -> ConHead
    recConHead Defn
    recd
      let nfields :: Int
    nfields         = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta
          (Telescope
    varTel', Substitution' (Pattern' DBPatVar)
    rho)  = Telescope
    -> Int
    -> Telescope
    -> ConHead
    -> (Telescope, Substitution' (Pattern' DBPatVar))
    expandTelescopeVar (UnifyState -> Telescope
    varTel UnifyState
    s) (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    i) Telescope
    delta ConHead
    c
          projectFlexible :: FlexibleVars
    projectFlexible = [ ArgInfo
    -> IsForced
    -> FlexibleVarKind
    -> Maybe Int
    -> Int
    -> FlexibleVar Int
    forall a.
    ArgInfo
    -> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
    FlexibleVar (FlexibleVar Int -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo FlexibleVar Int
    fi) (FlexibleVar Int -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar Int
    fi) (Int -> FlexibleVarKind
    projFlexKind Int
    j) (FlexibleVar Int -> Maybe Int
    forall a. FlexibleVar a -> Maybe Int
    flexPos FlexibleVar Int
    fi) (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    j) | Int
    j <- [Int
    0..Int
    nfieldsInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] ]
      Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifySubst (Substitution' (Pattern' DBPatVar) -> m ())
    -> Substitution' (Pattern' DBPatVar) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Substitution' (Pattern' DBPatVar)
    rho
      UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> UnifyState -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ UState :: Telescope
    -> FlexibleVars
    -> Telescope
    -> [Arg Term]
    -> [Arg Term]
    -> UnifyState
    UState
        { varTel :: Telescope
    varTel   = Telescope
    varTel'
        , flexVars :: FlexibleVars
    flexVars = FlexibleVars
    projectFlexible FlexibleVars -> FlexibleVars -> FlexibleVars
    forall a. [a] -> [a] -> [a]
    ++ Int -> FlexibleVars -> FlexibleVars
    liftFlexibles Int
    nfields (UnifyState -> FlexibleVars
    flexVars UnifyState
    s)
        , eqTel :: Telescope
    eqTel    = Substitution' (Pattern' DBPatVar) -> Telescope -> Telescope
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
        , eqLHS :: [Arg Term]
    eqLHS    = Substitution' (Pattern' DBPatVar) -> [Arg Term] -> [Arg Term]
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho ([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    = Substitution' (Pattern' DBPatVar) -> [Arg Term] -> [Arg Term]
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
        }
      where
        i :: Int
    i = FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Int
    fi
        m :: Int
    m = UnifyState -> Int
    varCount UnifyState
    s

        projFlexKind :: Int -> FlexibleVarKind
        projFlexKind :: Int -> FlexibleVarKind
    projFlexKind Int
    j = case FlexibleVar Int -> FlexibleVarKind
    forall a. FlexibleVar a -> FlexibleVarKind
    flexKind FlexibleVar Int
    fi of
          RecordFlex [FlexibleVarKind]
    ks -> FlexibleVarKind -> [FlexibleVarKind] -> Int -> FlexibleVarKind
    forall a. a -> [a] -> Int -> a
    indexWithDefault FlexibleVarKind
    ImplicitFlex [FlexibleVarKind]
    ks Int
    j
          FlexibleVarKind
    ImplicitFlex  -> FlexibleVarKind
    ImplicitFlex
          FlexibleVarKind
    DotFlex       -> FlexibleVarKind
    DotFlex
          FlexibleVarKind
    OtherFlex     -> FlexibleVarKind
    OtherFlex

        liftFlexible :: Int -> Int -> Maybe Int
        liftFlexible :: Int -> Int -> Maybe Int
    liftFlexible Int
    n Int
    j = if Int
    j Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i then Maybe Int
    forall a. Maybe a
    Nothing else Int -> Maybe Int
    forall a. a -> Maybe a
    Just (if Int
    j Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    i then Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) else Int
    j)

        liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
        liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
    liftFlexibles Int
    n FlexibleVars
    fs = (FlexibleVar Int -> Maybe (FlexibleVar Int))
    -> FlexibleVars -> FlexibleVars
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int))
    -> (Int -> Maybe Int) -> FlexibleVar Int -> Maybe (FlexibleVar Int)
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> Maybe Int
    liftFlexible Int
    n) FlexibleVars
    fs

    unifyStep UnifyState
    s EtaExpandEquation{ expandAt :: UnifyStep -> Int
    expandAt = Int
    k, expandRecordType :: UnifyStep -> QName
    expandRecordType = QName
    d, expandParameters :: UnifyStep -> [Arg Term]
    expandParameters = [Arg Term]
    pars } = do
      Defn
    recd  <- Defn -> Maybe Defn -> Defn
    forall a. a -> Maybe a -> a
    fromMaybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Defn -> Defn) -> m (Maybe Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    d
      let delta :: Telescope
    delta = Defn -> Telescope
    recTel Defn
    recd Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    pars
          c :: ConHead
    c     = Defn -> ConHead
    recConHead Defn
    recd
      [Arg Term]
    lhs   <- [Arg Term] -> m [Arg Term]
    expandKth ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
      [Arg Term]
    rhs   <- [Arg Term] -> m [Arg Term]
    expandKth ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
      let (Telescope
    tel, Substitution' (Pattern' DBPatVar)
    sigma) = Telescope
    -> Int
    -> Telescope
    -> ConHead
    -> (Telescope, Substitution' (Pattern' DBPatVar))
    expandTelescopeVar (UnifyState -> Telescope
    eqTel UnifyState
    s) Int
    k Telescope
    delta ConHead
    c
      Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    sigma
      UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> m UnifyState -> m (UnificationResult' UnifyState)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
       (Telescope -> m Telescope) -> UnifyState -> m UnifyState
    Lens' Telescope UnifyState
    lensEqTel Telescope -> m Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s
        { eqTel :: Telescope
    eqTel    = Telescope
    tel
        , eqLHS :: [Arg Term]
    eqLHS    = [Arg Term]
    lhs
        , eqRHS :: [Arg Term]
    eqRHS    = [Arg Term]
    rhs
        }
      where
        expandKth :: [Arg Term] -> m [Arg Term]
    expandKth [Arg Term]
    us = do
          let ([Arg Term]
    us1,Arg Term
    v:[Arg Term]
    us2) = ([Arg Term], [Arg Term])
    -> Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term])
    forall a. a -> Maybe a -> a
    fromMaybe ([Arg Term], [Arg Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term]))
    -> Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term])
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Term] -> Maybe ([Arg Term], [Arg Term])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt Int
    k [Arg Term]
    us
          [Arg Term]
    vs <- (Telescope, [Arg Term]) -> [Arg Term]
    forall a b. (a, b) -> b
    snd ((Telescope, [Arg Term]) -> [Arg Term])
    -> m (Telescope, [Arg Term]) -> m [Arg Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> [Arg Term] -> Term -> m (Telescope, [Arg Term])
    forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m) =>
    QName -> [Arg Term] -> Term -> m (Telescope, [Arg Term])
    etaExpandRecord QName
    d [Arg Term]
    pars (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v)
          [Arg Term]
    vs <- [Arg Term] -> m [Arg Term]
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce [Arg Term]
    vs
          [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term]
    us1 [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    vs [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    us2

    unifyStep UnifyState
    s LitConflict
      { litType :: UnifyStep -> Type
    litType          = Type
    a
      , litConflictLeft :: UnifyStep -> Literal
    litConflictLeft  = Literal
    l
      , litConflictRight :: UnifyStep -> Literal
    litConflictRight = Literal
    l'
      } = UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ NegativeUnification -> UnificationResult' UnifyState
    forall a. NegativeUnification -> UnificationResult' a
    NoUnify (NegativeUnification -> UnificationResult' UnifyState)
    -> NegativeUnification -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Term -> Term -> NegativeUnification
    UnifyConflict (UnifyState -> Telescope
    varTel UnifyState
    s) (Literal -> Term
    Lit Literal
    l) (Literal -> Term
    Lit Literal
    l')

    unifyStep UnifyState
    s (StripSizeSuc Int
    k Term
    u Term
    v) = do
      Type
    sizeTy <- m Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
      Term
    sizeSu <- Int -> Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
    sizeSuc Int
    1 (Int -> Term
    var Int
    0)
      let n :: Int
    n          = UnifyState -> Int
    eqCount UnifyState
    s
          sub :: Substitution' Term
    sub        = Int -> Substitution' Term -> Substitution' Term
    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) (Substitution' Term -> Substitution' Term)
    -> Substitution' Term -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    sizeSu (Substitution' Term -> Substitution' Term)
    -> Substitution' Term -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Substitution' Term
    forall a. Int -> Substitution' a
    raiseS Int
    1
          eqFlatTel :: [Dom' Term Type]
    eqFlatTel  = 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
    eqTel UnifyState
    s
          eqFlatTel' :: [Dom' Term Type]
    eqFlatTel' = Substitution' (SubstArg [Dom' Term Type])
    -> [Dom' Term Type] -> [Dom' Term Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [Dom' Term Type])
    sub ([Dom' Term Type] -> [Dom' Term Type])
    -> [Dom' Term Type] -> [Dom' Term Type]
    forall a b. (a -> b) -> a -> b
    $ Int
    -> (Dom' Term Type -> Dom' Term Type)
    -> [Dom' Term Type]
    -> [Dom' Term Type]
    forall a. Int -> (a -> a) -> [a] -> [a]
    updateAt Int
    k ((Type -> Type) -> Dom' Term Type -> Dom' Term Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Type -> Type) -> Dom' Term Type -> Dom' Term Type)
    -> (Type -> Type) -> Dom' Term Type -> Dom' Term Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    forall a b. a -> b -> a
    const Type
    sizeTy) ([Dom' Term Type] -> [Dom' Term Type])
    -> [Dom' Term Type] -> [Dom' Term Type]
    forall a b. (a -> b) -> a -> b
    $ [Dom' Term Type]
    eqFlatTel
          eqTel' :: Telescope
    eqTel'     = [String] -> [Dom' Term Type] -> Telescope
    unflattenTel (Telescope -> [String]
    teleNames (Telescope -> [String]) -> Telescope -> [String]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s) [Dom' Term Type]
    eqFlatTel'
      -- TODO: tellUnifyProof sub
      -- but sizeSu is not a constructor, so sub is not a PatternSubstitution!
      UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> UnifyState -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s
        { eqTel :: Telescope
    eqTel = Telescope
    eqTel'
        , eqLHS :: [Arg Term]
    eqLHS = Int -> (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
    forall a. Int -> (a -> a) -> [a] -> [a]
    updateAt Int
    k (Arg Term -> Arg Term -> Arg Term
    forall a b. a -> b -> a
    const (Arg Term -> Arg Term -> Arg Term)
    -> Arg Term -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    u) ([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 = Int -> (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
    forall a. Int -> (a -> a) -> [a] -> [a]
    updateAt Int
    k (Arg Term -> Arg Term -> Arg Term
    forall a b. a -> b -> a
    const (Arg Term -> Arg Term -> Arg Term)
    -> Arg Term -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    v) ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> [Arg Term]
    eqRHS UnifyState
    s
        }

    unifyStep UnifyState
    s (SkipIrrelevantEquation Int
    k) = do
      let lhs :: [Arg Term]
    lhs = UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
          (UnifyState
    s', Substitution' (Pattern' DBPatVar)
    sigma) = Int
    -> Term
    -> UnifyState
    -> (UnifyState, Substitution' (Pattern' DBPatVar))
    solveEq Int
    k (Term -> Term
    DontCare (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ 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) UnifyState
    s
      Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    sigma
      UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies UnifyState
    s'

    unifyStep UnifyState
    s (TypeConInjectivity Int
    k QName
    d [Arg Term]
    us [Arg Term]
    vs) = do
      Type
    dtype <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      TelV Telescope
    dtel Type
    _ <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    dtype
      let deq :: Term
    deq = QName -> Elims -> Term
    Def QName
    d (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    dtel
      -- TODO: tellUnifyProof ???
      -- but d is not a constructor...
      UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> m UnifyState -> m (UnificationResult' UnifyState)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
       (Telescope -> m Telescope) -> UnifyState -> m UnifyState
    Lens' Telescope UnifyState
    lensEqTel Telescope -> m Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s
        { eqTel :: Telescope
    eqTel = Telescope
    dtel Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Int -> Telescope -> Term -> Telescope
    applyUnder Int
    k (UnifyState -> Telescope
    eqTel UnifyState
    s) (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    k Term
    deq)
        , eqLHS :: [Arg Term]
    eqLHS = [Arg Term]
    us [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    dropAt Int
    k (UnifyState -> [Arg Term]
    eqLHS UnifyState
    s)
        , eqRHS :: [Arg Term]
    eqRHS = [Arg Term]
    vs [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    dropAt Int
    k (UnifyState -> [Arg Term]
    eqRHS UnifyState
    s)
        }

    data RetryNormalised = RetryNormalised | DontRetryNormalised
      deriving (RetryNormalised -> RetryNormalised -> Bool
    (RetryNormalised -> RetryNormalised -> Bool)
    -> (RetryNormalised -> RetryNormalised -> Bool)
    -> Eq RetryNormalised
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: RetryNormalised -> RetryNormalised -> Bool
    $c/= :: RetryNormalised -> RetryNormalised -> Bool
    == :: RetryNormalised -> RetryNormalised -> Bool
    $c== :: RetryNormalised -> RetryNormalised -> Bool
    Eq, Int -> RetryNormalised -> ShowS
    [RetryNormalised] -> ShowS
    RetryNormalised -> String
    (Int -> RetryNormalised -> ShowS)
    -> (RetryNormalised -> String)
    -> ([RetryNormalised] -> ShowS)
    -> Show RetryNormalised
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [RetryNormalised] -> ShowS
    $cshowList :: [RetryNormalised] -> ShowS
    show :: RetryNormalised -> String
    $cshow :: RetryNormalised -> String
    showsPrec :: Int -> RetryNormalised -> ShowS
    $cshowsPrec :: Int -> RetryNormalised -> ShowS
    Show)

    solutionStep
      :: (PureTCM m, MonadWriter UnifyOutput m)
      => RetryNormalised
      -> UnifyState
      -> UnifyStep
      -> m (UnificationResult' UnifyState)
    solutionStep :: forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    RetryNormalised
    -> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    solutionStep RetryNormalised
    retry UnifyState
    s
      step :: UnifyStep
    step@Solution{ solutionAt :: UnifyStep -> Int
    solutionAt   = Int
    k
                   , solutionType :: UnifyStep -> Dom' Term Type
    solutionType = dom :: Dom' Term Type
    dom@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a }
                   , solutionVar :: UnifyStep -> FlexibleVar Int
    solutionVar  = fi :: FlexibleVar Int
    fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
    flexVar = Int
    i }
                   , solutionTerm :: UnifyStep -> Term
    solutionTerm = Term
    u } = do
      let m :: Int
    m = UnifyState -> Int
    varCount UnifyState
    s

      -- Now we have to be careful about forced variables in `u`. If they appear
      -- in pattern positions we need to bind them there rather in their forced positions. We can safely
      -- ignore non-pattern positions and forced pattern positions, because in that case there will be
      -- other equations where the variable can be bound.
      -- NOTE: If we're doing make-case we ignore forced variables. This is safe since we take the
      -- result of unification and build user clauses that will be checked again with forcing turned on.
      Bool
    inMakeCase <- Lens' Bool TCEnv -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Bool TCEnv
    eMakeCase
      let forcedVars :: IntMap Modality
    forcedVars | Bool
    inMakeCase = IntMap Modality
    forall a. IntMap a
    IntMap.empty
                     | Bool
    otherwise  = [(Int, Modality)] -> IntMap Modality
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList [ (FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Int
    fi, FlexibleVar Int -> Modality
    forall a. LensModality a => a -> Modality
    getModality FlexibleVar Int
    fi) | FlexibleVar Int
    fi <- UnifyState -> FlexibleVars
    flexVars UnifyState
    s,
                                                                                     FlexibleVar Int -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar Int
    fi IsForced -> IsForced -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsForced
    Forced ]
      (Pattern' DBPatVar
    p, IntMap Modality
    bound) <- IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
    forall (m :: * -> *).
    PureTCM m =>
    IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
    patternBindingForcedVars IntMap Modality
    forcedVars Term
    u

      -- To maintain the invariant that each variable in varTel is bound exactly once in the pattern
      -- substitution we need to turn the bound variables in `p` into dot patterns in the rest of the
      -- substitution.
      let dotSub :: Substitution' (Pattern' DBPatVar)
    dotSub = (Substitution' (Pattern' DBPatVar)
     -> Substitution' (Pattern' DBPatVar)
     -> Substitution' (Pattern' DBPatVar))
    -> Substitution' (Pattern' DBPatVar)
    -> [Substitution' (Pattern' DBPatVar)]
    -> Substitution' (Pattern' DBPatVar)
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' (Pattern' DBPatVar)
    forall a. Substitution' a
    idS [ Int -> Pattern' DBPatVar -> Substitution' (Pattern' DBPatVar)
    forall a. EndoSubst a => Int -> a -> Substitution' a
    inplaceS Int
    i (Term -> Pattern' DBPatVar
    forall a. Term -> Pattern' a
    dotP (Int -> Elims -> Term
    Var Int
    i [])) | Int
    i <- IntMap Modality -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys IntMap Modality
    bound ]

      -- We moved the binding site of some forced variables, so we need to update their modalities in
      -- the telescope. The new modality is the combination of the modality of the variable we are
      -- instantiating and the modality of the binding site in the pattern (returned by
      -- patternBindingForcedVars).
      let updModality :: Modality -> IntMap Modality -> Telescope -> Telescope
    updModality Modality
    md IntMap Modality
    vars Telescope
    tel
            | IntMap Modality -> Bool
    forall a. IntMap a -> Bool
    IntMap.null IntMap Modality
    vars = Telescope
    tel
            | Bool
    otherwise        = [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))
    -> [Int]
    -> [Dom' Term (String, Type)]
    -> [Dom' Term (String, Type)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Int -> Dom' Term (String, Type) -> Dom' Term (String, Type)
    upd (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) (Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel)
            where
              upd :: Int -> Dom' Term (String, Type) -> Dom' Term (String, Type)
    upd Int
    i Dom' Term (String, Type)
    a | Just Modality
    md' <- Int -> IntMap Modality -> Maybe Modality
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i IntMap Modality
    vars = Modality -> Dom' Term (String, Type) -> Dom' Term (String, Type)
    forall a. LensModality a => Modality -> a -> a
    setModality (Modality -> Modality -> Modality
    composeModality Modality
    md Modality
    md') Dom' Term (String, Type)
    a
                      | Bool
    otherwise                        = Dom' Term (String, Type)
    a
      UnifyState
    s <- UnifyState -> m UnifyState
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    s { varTel :: Telescope
    varTel = Modality -> IntMap Modality -> Telescope -> Telescope
    updModality (FlexibleVar Int -> Modality
    forall a. LensModality a => a -> Modality
    getModality FlexibleVar Int
    fi) IntMap Modality
    bound (UnifyState -> Telescope
    varTel UnifyState
    s) }

      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.force" Int
    45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "forcedVars =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (IntMap Modality -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys IntMap Modality
    forcedVars)
        , TCMT IO Doc
    "u          =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u
        , TCMT IO Doc
    "p          =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Pattern' DBPatVar -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Pattern' DBPatVar
    p
        , TCMT IO Doc
    "bound      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Int] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (IntMap Modality -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys IntMap Modality
    bound)
        , TCMT IO Doc
    "dotSub     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution' (Pattern' DBPatVar) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution' (Pattern' DBPatVar)
    dotSub ]

      -- Check that the type of the variable is equal to the type of the equation
      -- (not just a subtype), otherwise we cannot instantiate (see Issue 2407).
      let dom' :: Dom' Term Type
    dom'@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a' } = Int -> UnifyState -> Dom' Term Type
    getVarType (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    i) UnifyState
    s
      Either Blocker Bool
    equalTypes <- Telescope -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m (Either Blocker Bool) -> m (Either Blocker Bool))
    -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT m Bool -> m (Either Blocker Bool))
    -> BlockT m Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Int -> TCMT IO Doc -> BlockT m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    45 (TCMT IO Doc -> BlockT m ()) -> TCMT IO Doc -> BlockT m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Equation type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
        String -> Int -> TCMT IO Doc -> BlockT m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    45 (TCMT IO Doc -> BlockT m ()) -> TCMT IO Doc -> BlockT m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Variable type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a'
        Type -> Type -> BlockT m Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Type -> m Bool
    pureEqualType Type
    a Type
    a'

      -- The conditions on the relevances are as follows (see #2640):
      -- - If the type of the equation is relevant, then the solution must be
      --   usable in a relevant position.
      -- - If the type of the equation is (shape-)irrelevant, then the solution
      --   must be usable in a μ-relevant position where μ is the relevance
      --   of the variable being solved.
      --
      -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally
      -- always @Quantity0@, since the indices of the data type are runtime erased.
      -- Thus, we need not change the quantity of the solution.
      Modality
    envmod <- Lens' Modality TCEnv -> m Modality
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Modality TCEnv
    eModality
      let eqrel :: Relevance
    eqrel  = Dom' Term Type -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Dom' Term Type
    dom
          eqmod :: Modality
    eqmod  = Dom' Term Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom' Term Type
    dom
          varmod :: Modality
    varmod = Dom' Term Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom' Term Type
    dom'
          mod :: Modality
    mod    = Bool -> (Modality -> Modality) -> Modality -> Modality
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Relevance
    NonStrict Relevance -> Relevance -> Bool
    `moreRelevant` Relevance
    eqrel) (Relevance -> Modality -> Modality
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    eqrel)
                 (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $ Bool -> (Modality -> Modality) -> Modality -> Modality
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Modality -> Bool
    forall a. LensQuantity a => a -> Bool
    usableQuantity Modality
    envmod) (Quantity -> Modality -> Modality
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    zeroQuantity)
                 (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $ Modality
    varmod
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Equation modality: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Modality -> String
    forall a. Show a => a -> String
    show (Dom' Term Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom' Term Type
    dom)
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Variable modality: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Modality -> String
    forall a. Show a => a -> String
    show Modality
    varmod
      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Solution must be usable in a " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Modality -> String
    forall a. Show a => a -> String
    show Modality
    mod String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " position."
      -- Andreas, 2018-10-18
      -- Currently, the modality check has problems with meta-variables created in the type signature,
      -- and thus, in quantity 0, that get into terms using the unifier, and there are checked to be
      -- non-erased, i.e., have quantity ω.
      -- Ulf, 2019-12-13. We still do it though.
      -- Andrea, 2020-10-15: It looks at meta instantiations now.
      Either Blocker Bool
    eusable <- Telescope -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m (Either Blocker Bool) -> m (Either Blocker Bool))
    -> m (Either Blocker Bool) -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ ExceptT Blocker m Bool -> m (Either Blocker Bool)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT Blocker m Bool -> m (Either Blocker Bool))
    -> ExceptT Blocker m Bool -> m (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Modality -> Term -> ExceptT Blocker m Bool
    forall a (m :: * -> *).
    (UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
     MonadAddContext m, MonadDebug m, MonadReduce m,
     MonadError Blocker m) =>
    Modality -> a -> m Bool
    usableMod Modality
    mod Term
    u
      m (Either Blocker Bool)
    -> (Blocker -> m (UnificationResult' UnifyState))
    -> (Bool -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (Either Blocker Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Either Blocker Bool
    eusable) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> (Blocker -> UnificationResult' UnifyState)
    -> Blocker
    -> m (UnificationResult' UnifyState)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked) ((Bool -> m (UnificationResult' UnifyState))
     -> m (UnificationResult' UnifyState))
    -> (Bool -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ \ Bool
    usable -> do

      String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Modality ok: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Bool -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Bool
    usable
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    usable (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> String -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "tc.lhs.unify" Int
    65 (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Rejected solution: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Term -> String
    forall a. Show a => a -> String
    show Term
    u

      -- We need a Flat equality to solve a Flat variable.
      -- This also ought to take care of the need for a usableCohesion check.
      if Bool -> Bool
    not (Modality -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion Modality
    eqmod Cohesion -> Cohesion -> Bool
    `moreCohesion` Modality -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion Modality
    varmod) then UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [] else do

      case Either Blocker Bool
    equalTypes of
        Left Blocker
    block  -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked Blocker
    block
        Right Bool
    False -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []
        Right Bool
    True | Bool
    usable ->
          case Int
    -> Pattern' DBPatVar
    -> UnifyState
    -> Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    solveVar (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) Pattern' DBPatVar
    p UnifyState
    s of
            Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    Nothing | RetryNormalised
    retry RetryNormalised -> RetryNormalised -> Bool
    forall a. Eq a => a -> a -> Bool
    == RetryNormalised
    RetryNormalised -> do
              Term
    u <- Term -> m Term
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Term
    u
              UnifyState
    s <- (Telescope -> m Telescope) -> UnifyState -> m UnifyState
    Lens' Telescope UnifyState
    lensVarTel Telescope -> m Telescope
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise UnifyState
    s
              RetryNormalised
    -> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    RetryNormalised
    -> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    solutionStep RetryNormalised
    DontRetryNormalised UnifyState
    s UnifyStep
    step{ solutionTerm :: Term
    solutionTerm = Term
    u }
            Maybe (UnifyState, Substitution' (Pattern' DBPatVar))
    Nothing ->
              UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [Telescope -> Type -> Int -> Term -> UnificationFailure
    UnifyRecursiveEq (UnifyState -> Telescope
    varTel UnifyState
    s) Type
    a Int
    i Term
    u]
            Just (UnifyState
    s', Substitution' (Pattern' DBPatVar)
    sub) -> do
              let rho :: Substitution' (Pattern' DBPatVar)
    rho = Substitution' (Pattern' DBPatVar)
    sub Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    -> Substitution' (Pattern' DBPatVar)
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution' (Pattern' DBPatVar)
    dotSub
              Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifySubst Substitution' (Pattern' DBPatVar)
    rho
              let (UnifyState
    s'', Substitution' (Pattern' DBPatVar)
    sigma) = Int
    -> Term
    -> UnifyState
    -> (UnifyState, Substitution' (Pattern' DBPatVar))
    solveEq Int
    k (Substitution' (Pattern' DBPatVar) -> Term -> Term
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    applyPatSubst Substitution' (Pattern' DBPatVar)
    rho Term
    u) UnifyState
    s'
              Substitution' (Pattern' DBPatVar) -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    Substitution' (Pattern' DBPatVar) -> m ()
    tellUnifyProof Substitution' (Pattern' DBPatVar)
    sigma
              UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies UnifyState
    s''
              -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
              -- Unifies <$> liftTCM (reduce s'')
        Right Bool
    True -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [Telescope -> Type -> Int -> Term -> Modality -> UnificationFailure
    UnifyUnusableModality (UnifyState -> Telescope
    varTel UnifyState
    s) Type
    a Int
    i Term
    u Modality
    mod]
    solutionStep RetryNormalised
    _ UnifyState
    _ UnifyStep
    _ = m (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unify
      :: (PureTCM m, MonadWriter UnifyOutput m)
      => UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
    unify :: forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
    unify UnifyState
    s UnifyStrategy
    strategy = if UnifyState -> Bool
    isUnifyStateSolved UnifyState
    s
                       then UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies UnifyState
    s
                       else ListT m UnifyStep -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    ListT m UnifyStep -> m (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue (UnifyState -> ListT m UnifyStep
    UnifyStrategy
    strategy UnifyState
    s)
      where
        tryUnifyStepsAndContinue
          :: (PureTCM m, MonadWriter UnifyOutput m)
          => ListT m UnifyStep -> m (UnificationResult' UnifyState)
        tryUnifyStepsAndContinue :: forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    ListT m UnifyStep -> m (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue ListT m UnifyStep
    steps = do
          UnificationResult' UnifyState
    x <- (UnifyStep
     -> m (UnificationResult' UnifyState)
     -> m (UnificationResult' UnifyState))
    -> m (UnificationResult' UnifyState)
    -> ListT m UnifyStep
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT UnifyStep
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyStep
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    tryUnifyStep m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
    failure ListT m UnifyStep
    steps
          case UnificationResult' UnifyState
    x of
            Unifies UnifyState
    s'     -> UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
    unify UnifyState
    s' UnifyStrategy
    strategy
            NoUnify NegativeUnification
    err    -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ NegativeUnification -> UnificationResult' UnifyState
    forall a. NegativeUnification -> UnificationResult' a
    NoUnify NegativeUnification
    err
            UnifyBlocked Blocker
    b -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked Blocker
    b
            UnifyStuck [UnificationFailure]
    err -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [UnificationFailure]
    err

        tryUnifyStep :: (PureTCM m, MonadWriter UnifyOutput m)
                     => UnifyStep
                     -> m (UnificationResult' UnifyState)
                     -> m (UnificationResult' UnifyState)
        tryUnifyStep :: forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyStep
    -> m (UnificationResult' UnifyState)
    -> m (UnificationResult' UnifyState)
    tryUnifyStep UnifyStep
    step m (UnificationResult' UnifyState)
    fallback = do
          Telescope -> m () -> m ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
            String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "trying unifyStep" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> UnifyStep -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM UnifyStep
    step
          UnificationResult' UnifyState
    x <- UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    forall (m :: * -> *).
    (PureTCM m, MonadWriter UnifyOutput m) =>
    UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
    unifyStep UnifyState
    s UnifyStep
    step
          case UnificationResult' UnifyState
    x of
            Unifies UnifyState
    s'   -> do
              String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "unifyStep successful."
              String -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "new unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> UnifyState -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM UnifyState
    s'
              UnifyLogEntry -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    UnifyLogEntry -> m ()
    writeUnifyLog (UnifyLogEntry -> m ()) -> UnifyLogEntry -> m ()
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnifyStep -> UnifyLogEntry
    UnificationStep UnifyState
    s UnifyStep
    step
              UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    x
            NoUnify{}       -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    x
            UnifyBlocked Blocker
    b1 -> do
              UnificationResult' UnifyState
    y <- m (UnificationResult' UnifyState)
    fallback
              case UnificationResult' UnifyState
    y of
                UnifyStuck [UnificationFailure]
    _    -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked Blocker
    b1
                UnifyBlocked Blocker
    b2 -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> UnificationResult' UnifyState
    forall a. Blocker -> UnificationResult' a
    UnifyBlocked (Blocker -> UnificationResult' UnifyState)
    -> Blocker -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Blocker -> Blocker
    unblockOnEither Blocker
    b1 Blocker
    b2
                UnificationResult' UnifyState
    _               -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    y
            UnifyStuck [UnificationFailure]
    err1 -> do
              UnificationResult' UnifyState
    y <- m (UnificationResult' UnifyState)
    fallback
              case UnificationResult' UnifyState
    y of
                UnifyStuck [UnificationFailure]
    err2 -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> m (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> m (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck ([UnificationFailure] -> UnificationResult' UnifyState)
    -> [UnificationFailure] -> UnificationResult' UnifyState
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure]
    err1 [UnificationFailure]
    -> [UnificationFailure] -> [UnificationFailure]
    forall a. [a] -> [a] -> [a]
    ++ [UnificationFailure]
    err2
                UnificationResult' UnifyState
    _               -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    y

        failure :: Monad m => m (UnificationResult' a)
        failure :: forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
    failure = UnificationResult' a -> m (UnificationResult' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' a -> m (UnificationResult' a))
    -> UnificationResult' a -> m (UnificationResult' a)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' a
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []

    -- | Turn a term into a pattern while binding as many of the given forced variables as possible (in
    --   non-forced positions).
    patternBindingForcedVars :: PureTCM m => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
    patternBindingForcedVars :: forall (m :: * -> *).
    PureTCM m =>
    IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
    patternBindingForcedVars IntMap Modality
    forced Term
    v = do
      let v' :: Term
    v' = Term -> Term
    forall a. PrecomputeFreeVars a => a -> a
    precomputeFreeVars_ Term
    v
      WriterT (IntMap Modality) m (Pattern' DBPatVar)
    -> m (Pattern' DBPatVar, IntMap Modality)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (StateT
      (IntMap Modality) (WriterT (IntMap Modality) m) (Pattern' DBPatVar)
    -> IntMap Modality
    -> WriterT (IntMap Modality) m (Pattern' DBPatVar)
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT (Modality
    -> Term
    -> StateT
         (IntMap Modality) (WriterT (IntMap Modality) m) (Pattern' DBPatVar)
    forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
           {m :: * -> *} {a}.
    (MonadWriter (IntMap Modality) (t (t m)), HasConstInfo (t (t m)),
     DeBruijn a, MonadTrans t, MonadTrans t, Monad (t m), MonadReduce m,
     MonadState (IntMap Modality) (t (t m))) =>
    Modality -> Term -> t (t m) (Pattern' a)
    go Modality
    defaultModality Term
    v') IntMap Modality
    forced)
      where
        noForced :: a -> m Bool
    noForced a
    v = (IntMap a -> Bool) -> m Bool
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((IntMap a -> Bool) -> m Bool) -> (IntMap a -> Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ IntSet -> IntSet -> Bool
    IntSet.disjoint (a -> IntSet
    forall a. PrecomputeFreeVars a => a -> IntSet
    precomputedFreeVars a
    v) (IntSet -> Bool) -> (IntMap a -> IntSet) -> IntMap a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntMap a -> IntSet
    forall a. IntMap a -> IntSet
    IntMap.keysSet

        bind :: a -> Int -> m (Pattern' a)
    bind a
    md Int
    i = do
          (IntMap a -> Maybe a) -> m (Maybe a)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (Int -> IntMap a -> Maybe a
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i) m (Maybe a) -> (Maybe a -> m (Pattern' a)) -> m (Pattern' a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just a
    md' | a -> PartialOrdering -> a -> Bool
    forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
    related a
    md PartialOrdering
    POLE a
    md' -> do
              -- The new binding site must be more relevant (more relevant = smaller).
              -- "The forcing analysis guarantees that there exists such a position."
              -- Really? Andreas, 2021-08-18, issue #5506
              IntMap a -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell   (IntMap a -> m ()) -> IntMap a -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> IntMap a
    forall a. Int -> a -> IntMap a
    IntMap.singleton Int
    i a
    md
              (IntMap a -> IntMap a) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((IntMap a -> IntMap a) -> m ()) -> (IntMap a -> IntMap a) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> IntMap a -> IntMap a
    forall a. Int -> IntMap a -> IntMap a
    IntMap.delete Int
    i
              Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ a -> Pattern' a
    forall a. a -> Pattern' a
    varP (Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar Int
    i)
            Maybe a
    _ -> Pattern' a -> m (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP (Int -> Elims -> Term
    Var Int
    i [])

        go :: Modality -> Term -> t (t m) (Pattern' a)
    go Modality
    md Term
    v = t (t m) Bool
    -> t (t m) (Pattern' a)
    -> t (t m) (Pattern' a)
    -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Term -> t (t m) Bool
    forall {a} {m :: * -> *} {a}.
    (MonadState (IntMap a) m, PrecomputeFreeVars a) =>
    a -> m Bool
    noForced Term
    v) (Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v) (t (t m) (Pattern' a) -> t (t m) (Pattern' a))
    -> t (t m) (Pattern' a) -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ do
          Term
    v' <- t m Term -> t (t m) Term
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (t m Term -> t (t m) Term) -> t m Term -> t (t m) Term
    forall a b. (a -> b) -> a -> b
    $ m Term -> t m Term
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Term -> t m Term) -> m Term -> t m Term
    forall a b. (a -> b) -> a -> b
    $ Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          case Term
    v' of
            Var Int
    i [] -> Modality -> Int -> t (t m) (Pattern' a)
    forall {a} {m :: * -> *} {a}.
    (MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
     DeBruijn a) =>
    a -> Int -> m (Pattern' a)
    bind Modality
    md Int
    i  -- we know i is forced
            Con ConHead
    c ConInfo
    ci Elims
    es
              | Just [Arg Term]
    vs <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es -> do
                [IsForced]
    fs <- Definition -> [IsForced]
    defForced (Definition -> [IsForced])
    -> t (t m) Definition -> t (t m) [IsForced]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> t (t m) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    c)
                let goArg :: IsForced
    -> Arg Term -> t (t m) (Arg (Named NamedName (Pattern' a)))
    goArg IsForced
    Forced    Arg Term
    v = Arg (Named NamedName (Pattern' a))
    -> t (t m) (Arg (Named NamedName (Pattern' a)))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Arg (Named NamedName (Pattern' a))
     -> t (t m) (Arg (Named NamedName (Pattern' a))))
    -> Arg (Named NamedName (Pattern' a))
    -> t (t m) (Arg (Named NamedName (Pattern' a)))
    forall a b. (a -> b) -> a -> b
    $ (Term -> Named NamedName (Pattern' a))
    -> Arg Term -> Arg (Named NamedName (Pattern' a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern' a -> Named NamedName (Pattern' a)
    forall a name. a -> Named name a
    unnamed (Pattern' a -> Named NamedName (Pattern' a))
    -> (Term -> Pattern' a) -> Term -> Named NamedName (Pattern' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP) Arg Term
    v
                    goArg IsForced
    NotForced Arg Term
    v = (Pattern' a -> Named NamedName (Pattern' a))
    -> Arg (Pattern' a) -> Arg (Named NamedName (Pattern' a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' a -> Named NamedName (Pattern' a)
    forall a name. a -> Named name a
    unnamed (Arg (Pattern' a) -> Arg (Named NamedName (Pattern' a)))
    -> t (t m) (Arg (Pattern' a))
    -> t (t m) (Arg (Named NamedName (Pattern' a)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> t (t m) (Pattern' a))
    -> Arg Term -> t (t m) (Arg (Pattern' a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Modality -> Term -> t (t m) (Pattern' a)
    go (Modality -> Term -> t (t m) (Pattern' a))
    -> Modality -> Term -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Modality -> Modality -> Modality
    composeModality Modality
    md (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Modality
    forall a. LensModality a => a -> Modality
    getModality Arg Term
    v) Arg Term
    v
                ([Arg (Named NamedName (Pattern' a))]
    ps, IntMap Modality
    bound) <- t (t m) [Arg (Named NamedName (Pattern' a))]
    -> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality)
    forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
    listen (t (t m) [Arg (Named NamedName (Pattern' a))]
     -> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality))
    -> t (t m) [Arg (Named NamedName (Pattern' a))]
    -> t (t m) ([Arg (Named NamedName (Pattern' a))], IntMap Modality)
    forall a b. (a -> b) -> a -> b
    $ (IsForced
     -> Arg Term -> t (t m) (Arg (Named NamedName (Pattern' a))))
    -> [IsForced]
    -> [Arg Term]
    -> t (t m) [Arg (Named NamedName (Pattern' a))]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM IsForced
    -> Arg Term -> t (t m) (Arg (Named NamedName (Pattern' a)))
    goArg ([IsForced]
    fs [IsForced] -> [IsForced] -> [IsForced]
    forall a. [a] -> [a] -> [a]
    ++ IsForced -> [IsForced]
    forall a. a -> [a]
    repeat IsForced
    NotForced) [Arg Term]
    vs
                if IntMap Modality -> Bool
    forall a. IntMap a -> Bool
    IntMap.null IntMap Modality
    bound
                  then Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v  -- bound nothing
                  else do
                    let cpi :: ConPatternInfo
    cpi = (ConInfo -> ConPatternInfo
    toConPatternInfo ConInfo
    ci) { conPLazy :: Bool
    conPLazy   = Bool
    True } -- Not setting conPType. Is this a problem?
                    Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ ConHead
    -> ConPatternInfo
    -> [Arg (Named NamedName (Pattern' a))]
    -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    cpi ([Arg (Named NamedName (Pattern' a))] -> Pattern' a)
    -> [Arg (Named NamedName (Pattern' a))] -> Pattern' a
    forall a b. (a -> b) -> a -> b
    $ (Arg (Named NamedName (Pattern' a))
     -> Arg (Named NamedName (Pattern' a)))
    -> [Arg (Named NamedName (Pattern' a))]
    -> [Arg (Named NamedName (Pattern' a))]
    forall a b. (a -> b) -> [a] -> [b]
    map (Origin
    -> Arg (Named NamedName (Pattern' a))
    -> Arg (Named NamedName (Pattern' a))
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted) [Arg (Named NamedName (Pattern' a))]
    ps
              | Bool
    otherwise -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v   -- Higher constructor (es has IApply)

            -- Non-pattern positions
            Var Int
    _ (Elim' Term
    _:Elims
    _) -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Lam{}       -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Pi{}        -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Def{}       -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            MetaV{}     -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Sort{}      -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Level{}     -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            DontCare{}  -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Dummy{}     -> Pattern' a -> t (t m) (Pattern' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern' a -> t (t m) (Pattern' a))
    -> Pattern' a -> t (t m) (Pattern' a)
    forall a b. (a -> b) -> a -> b
    $ Term -> Pattern' a
    forall a. Term -> Pattern' a
    dotP Term
    v
            Lit{}       -> t (t m) (Pattern' a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__