    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# 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'(..)
      , NoLeftInv(..)
      , unifyIndices'
      , unifyIndices ) where

    import Prelude hiding (null)

    import Control.Monad.State  ( gets, modify, evalStateT )
    import Control.Monad.Writer ( WriterT(..), MonadWriter(..) )
    import Control.Monad.Except ( runExceptT )

    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.TypeChecking.Monad
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Conversion.Pure (pureEqualTermB, pureEqualTypeB)
    import Agda.TypeChecking.Constraints ()
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Irrelevance
    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.TypeChecking.Rules.LHS.Unify.Types
    import Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

    import Agda.Utils.Either
    import Agda.Utils.Function
    import Agda.Utils.Functor
    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.Singleton
    import Agda.Utils.Size

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

    type FullUnificationResult = UnificationResult'
      ( Telescope                  -- @tel@
      , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
      , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
      , Either NoLeftInv (Substitution, Substitution) -- (τ,leftInv)
      )

    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 (Nat -> UnificationResult' a -> ShowS
    [UnificationResult' a] -> ShowS
    UnificationResult' a -> String
    (Nat -> UnificationResult' a -> ShowS)
    -> (UnificationResult' a -> String)
    -> ([UnificationResult' a] -> ShowS)
    -> Show (UnificationResult' a)
    forall a. Show a => Nat -> UnificationResult' a -> ShowS
    forall a. Show a => [UnificationResult' a] -> ShowS
    forall a. Show a => UnificationResult' a -> String
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Nat -> UnificationResult' a -> ShowS
    showsPrec :: Nat -> UnificationResult' a -> ShowS
    $cshow :: forall a. Show a => UnificationResult' a -> String
    show :: UnificationResult' a -> String
    $cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
    showList :: [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
    $cfmap :: forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    fmap :: forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    $c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
    <$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
    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 -> Nat)
    -> (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 -> Nat
    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 -> Nat)
    -> (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
    $cfold :: forall m. Monoid m => UnificationResult' m -> m
    fold :: forall m. Monoid m => UnificationResult' m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
    $ctoList :: forall a. UnificationResult' a -> [a]
    toList :: forall a. UnificationResult' a -> [a]
    $cnull :: forall a. UnificationResult' a -> Bool
    null :: forall a. UnificationResult' a -> Bool
    $clength :: forall a. UnificationResult' a -> Nat
    length :: forall a. UnificationResult' a -> Nat
    $celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
    elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
    $cmaximum :: forall a. Ord a => UnificationResult' a -> a
    maximum :: forall a. Ord a => UnificationResult' a -> a
    $cminimum :: forall a. Ord a => UnificationResult' a -> a
    minimum :: forall a. Ord a => UnificationResult' a -> a
    $csum :: forall a. Num a => UnificationResult' a -> a
    sum :: forall a. Num a => UnificationResult' a -> a
    $cproduct :: forall a. Num a => UnificationResult' a -> a
    product :: forall a. Num a => UnificationResult' a -> a
    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)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a)
    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
      :: Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
      -> Telescope       -- ^ @gamma@
      -> FlexibleVars    -- ^ @flex@
      -> Type            -- ^ @a@
      -> Args            -- ^ @us@
      -> Args            -- ^ @vs@
      -> TCM UnificationResult
    unifyIndices :: Maybe NoLeftInv
    -> Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> TCM UnificationResult
    unifyIndices Maybe NoLeftInv
    linv Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs =
      Account (BenchPhase TCM)
    -> TCM UnificationResult -> TCM UnificationResult
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase TCM
    Phase
    Bench.Typing, BenchPhase TCM
    Phase
    Bench.CheckLHS, BenchPhase TCM
    Phase
    Bench.UnifyIndices] (TCM UnificationResult -> TCM UnificationResult)
    -> TCM UnificationResult -> TCM UnificationResult
    forall a b. (a -> b) -> a -> b
    $
        ((Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution))
     -> (Telescope, PatternSubstitution,
         [NamedArg (Pattern' DBPatVar)]))
    -> UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))
    -> UnificationResult
    forall a b.
    (a -> b) -> UnificationResult' a -> UnificationResult' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(Telescope
    a,PatternSubstitution
    b,[NamedArg (Pattern' DBPatVar)]
    c,Either NoLeftInv (Substitution, Substitution)
    _) -> (Telescope
    a,PatternSubstitution
    b,[NamedArg (Pattern' DBPatVar)]
    c)) (UnificationResult'
       (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
        Either NoLeftInv (Substitution, Substitution))
     -> UnificationResult)
    -> TCMT
         IO
         (UnificationResult'
            (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
             Either NoLeftInv (Substitution, Substitution)))
    -> TCM UnificationResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe NoLeftInv
    -> Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> TCMT
         IO
         (UnificationResult'
            (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
             Either NoLeftInv (Substitution, Substitution)))
    unifyIndices' Maybe NoLeftInv
    linv Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs

    unifyIndices'
      :: Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
      -> Telescope     -- ^ @gamma@
      -> FlexibleVars  -- ^ @flex@
      -> Type          -- ^ @a@
      -> Args          -- ^ @us@
      -> Args          -- ^ @vs@
      -> TCM FullUnificationResult
    unifyIndices' :: Maybe NoLeftInv
    -> Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> TCMT
         IO
         (UnificationResult'
            (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
             Either NoLeftInv (Substitution, Substitution)))
    unifyIndices' Maybe NoLeftInv
    linv Telescope
    tel FlexibleVars
    flex Type
    a [] [] = UnificationResult'
      (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
       Either NoLeftInv (Substitution, Substitution))
    -> TCMT
         IO
         (UnificationResult'
            (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
             Either NoLeftInv (Substitution, Substitution)))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult'
       (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
        Either NoLeftInv (Substitution, Substitution))
     -> TCMT
          IO
          (UnificationResult'
             (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
              Either NoLeftInv (Substitution, Substitution))))
    -> UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))
    -> TCMT
         IO
         (UnificationResult'
            (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
             Either NoLeftInv (Substitution, Substitution)))
    forall a b. (a -> b) -> a -> b
    $ (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
     Either NoLeftInv (Substitution, Substitution))
    -> UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))
    forall a. a -> UnificationResult' a
    Unifies (Telescope
    tel, PatternSubstitution
    forall a. Substitution' a
    idS, [], (Substitution, Substitution)
    -> Either NoLeftInv (Substitution, Substitution)
    forall a b. b -> Either a b
    Right (Substitution
    forall a. Substitution' a
    idS, Nat -> Substitution
    forall a. Nat -> Substitution' a
    raiseS Nat
    1))
    unifyIndices' Maybe NoLeftInv
    linv Telescope
    tel FlexibleVars
    flex Type
    a [Arg Term]
    us [Arg Term]
    vs = do
        String -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    $ [Nat] -> String
    forall a. Show a => a -> String
    show ([Nat] -> String) -> [Nat] -> String
    forall a b. (a -> b) -> a -> b
    $ (FlexibleVar Nat -> Nat) -> FlexibleVars -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map FlexibleVar Nat -> Nat
    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
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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, 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
    forall (m :: * -> *). MonadPretty m => Arg Term -> 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
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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, 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
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    vs
              ]
        initialState    <- Telescope
    -> FlexibleVars
    -> Type
    -> [Arg Term]
    -> [Arg Term]
    -> TCMT IO 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
        reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState
        (result,log) <- runUnifyLogT $ unify initialState rightToLeftStrategy
        forM result $ \ UnifyState
    s -> do -- Unifies case
            let output :: UnifyOutput
    output = [UnifyOutput] -> UnifyOutput
    forall a. Monoid a => [a] -> a
    mconcat [UnifyOutput
    output | (UnificationStep UnifyState
    _ UnifyStep
    _ UnifyOutput
    output,UnifyState
    _) <- UnifyLog
    log ]
            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 -> PatternSubstitution
    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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs (UnifyState -> Telescope
    eqTel UnifyState
    initialState)
            tauInv <- do
              strict     <- (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envSplitOnStrict
              cubicalCompatible <- cubicalCompatibleOption
              withoutK <- withoutKOption
              case linv of
                Just NoLeftInv
    reason -> Either NoLeftInv (Substitution, Substitution)
    -> TCMT IO (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    reason)
                Maybe NoLeftInv
    Nothing
                  | Bool
    strict            -> Either NoLeftInv (Substitution, Substitution)
    -> TCMT IO (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    SplitOnStrict)
                  | Bool
    cubicalCompatible -> UnifyState
    -> UnifyLog
    -> TCMT IO (Either NoLeftInv (Substitution, Substitution))
    forall (tcm :: * -> *).
    (PureTCM tcm, MonadError TCErr tcm) =>
    UnifyState
    -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
    buildLeftInverse UnifyState
    initialState UnifyLog
    log
                  | Bool
    withoutK          -> Either NoLeftInv (Substitution, Substitution)
    -> TCMT IO (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    NoCubical)
                  | Bool
    otherwise         -> Either NoLeftInv (Substitution, Substitution)
    -> TCMT IO (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    WithKEnabled)
            reportSDoc "tc.lhs.unify" 20 $ "ps:" <+> pretty ps
            return $ (varTel s, unifySubst output, ps, tauInv)

    type UnifyStrategy = UnifyState -> ListT TCM 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 =
        [ListT TCM UnifyStep] -> ListT TCM UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([Nat] -> (Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n) ((Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep])
    -> (Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
    forall a b. (a -> b) -> a -> b
    $ \Nat
    k -> Nat -> UnifyStrategy
    completeStrategyAt Nat
    k UnifyState
    s)
      where n :: Nat
    n = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size (Telescope -> Nat) -> Telescope -> Nat
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s

    completeStrategyAt :: Int -> UnifyStrategy
    completeStrategyAt :: Nat -> UnifyStrategy
    completeStrategyAt Nat
    k UnifyState
    s = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([ListT TCM UnifyStep] -> ListT TCM UnifyStep)
    -> [ListT TCM UnifyStep] -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ ((Nat -> UnifyStrategy) -> ListT TCM UnifyStep)
    -> [Nat -> UnifyStrategy] -> [ListT TCM UnifyStep]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Nat -> UnifyStrategy
    strat -> Nat -> UnifyStrategy
    strat Nat
    k UnifyState
    s) ([Nat -> UnifyStrategy] -> [ListT TCM UnifyStep])
    -> [Nat -> UnifyStrategy] -> [ListT TCM 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).
        [ (\Nat
    n -> Nat -> UnifyStrategy
    skipIrrelevantStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    basicUnifyStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    literalStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    dataStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    etaExpandVarStrategy  Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    etaExpandEquationStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    injectiveTypeConStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    injectivePragmaStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    simplifySizesStrategy Nat
    n)
        , (\Nat
    n -> Nat -> UnifyStrategy
    checkEqualityStrategy Nat
    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) => Nat -> a -> Maybe a
    isHom Nat
    n a
    x = do
      Bool -> Maybe ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    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) -> (Nat -> Bool) -> SingleVar All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    n)) IgnoreSorts
    IgnoreNot a
    x
      a -> Maybe a
    forall a. 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
    $ Nat -> a -> a
    forall a. Subst a => Nat -> a -> a
    raise (-Nat
    n) a
    x

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

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

    dataStrategy :: Int -> UnifyStrategy
    dataStrategy :: Nat -> UnifyStrategy
    dataStrategy Nat
    k UnifyState
    s = do
      Equal Dom{unDom = a} u v <- Equality -> ListT TCM Equality
    forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
    eqConstructorForm (Equality -> ListT TCM Equality)
    -> ListT TCM Equality -> ListT TCM Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Equality -> ListT TCM Equality
    forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    Equality -> m Equality
    eqUnLevel (Equality -> ListT TCM Equality)
    -> ListT TCM Equality -> ListT TCM Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Nat -> UnifyState -> ListT TCM Equality
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Nat -> UnifyState -> m Equality
    getReducedEqualityUnraised Nat
    k UnifyState
    s
      sortOk <- reduce (getSort a) <&> \case
        Type{} -> Bool
    True
        Inf{}  -> Bool
    True
        SSet{} -> Bool
    True
        Sort
    _      -> Bool
    False
      case unEl a of
        Def QName
    d Elims
    es | Bool
    sortOk -> do
          npars <- ListT TCM (Maybe Nat) -> ListT TCM Nat
    forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
    catMaybesMP (ListT TCM (Maybe Nat) -> ListT TCM Nat)
    -> ListT TCM (Maybe Nat) -> ListT TCM Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> ListT TCM (Maybe Nat)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Nat)
    getNumberOfParameters QName
    d
          let (pars,ixs) = splitAt npars $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
          reportSDoc "tc.lhs.unify" 40 $ addContext (varTel s `abstract` eqTel s) $
            "Found equation at datatype " <+> prettyTCM d
             <+> " with parameters " <+> prettyTCM (raise (size (eqTel s) - k) pars)
          case (u, 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 -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat
    -> Type
    -> QName
    -> [Arg Term]
    -> [Arg Term]
    -> ConHead
    -> UnifyStep
    Injectivity Nat
    k Type
    a QName
    d [Arg Term]
    pars [Arg Term]
    ixs ConHead
    c
            (Con ConHead
    c ConInfo
    _ Elims
    _   , Con ConHead
    c' ConInfo
    _ Elims
    _  ) -> UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> QName -> [Arg Term] -> Term -> Term -> UnifyStep
    Conflict Nat
    k Type
    a QName
    d [Arg Term]
    pars Term
    u Term
    v
            (Var Nat
    i []  , Term
    v         ) -> Nat -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
    forall {m :: * -> *} {a} {b}.
    (ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
    Nat -> a -> m b -> m b
    ifOccursStronglyRigid Nat
    i Term
    v (ListT TCM UnifyStep -> ListT TCM UnifyStep)
    -> ListT TCM UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> QName -> [Arg Term] -> Nat -> Term -> UnifyStep
    Cycle Nat
    k Type
    a QName
    d [Arg Term]
    pars Nat
    i Term
    v
            (Term
    u         , Var Nat
    j []  ) -> Nat -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
    forall {m :: * -> *} {a} {b}.
    (ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
    Nat -> a -> m b -> m b
    ifOccursStronglyRigid Nat
    j Term
    u (ListT TCM UnifyStep -> ListT TCM UnifyStep)
    -> ListT TCM UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> QName -> [Arg Term] -> Nat -> Term -> UnifyStep
    Cycle Nat
    k Type
    a QName
    d [Arg Term]
    pars Nat
    j Term
    u
            (Term, Term)
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        Term
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      where
        ifOccursStronglyRigid :: Nat -> a -> m b -> m b
    ifOccursStronglyRigid Nat
    i a
    u m b
    ret = do
            -- Call forceNotFree to reduce u as far as possible
            -- around any occurrences of i
            (_ , u) <- IntSet -> a -> m (IntMap IsFree, a)
    forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree (Nat -> IntSet
    forall el coll. Singleton el coll => el -> coll
    singleton Nat
    i) a
    u
            case flexRigOccurrenceIn i u of
              Just FlexRig
    StronglyRigid -> m b
    ret
              Maybe FlexRig
    _ -> m b
    forall a. m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

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

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

    etaExpandVarStrategy :: Int -> UnifyStrategy
    etaExpandVarStrategy :: Nat -> UnifyStrategy
    etaExpandVarStrategy Nat
    k UnifyState
    s = do
      Equal Dom{unDom = a} u v <- Equality -> ListT TCM Equality
    forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    Equality -> m Equality
    eqUnLevel (Equality -> ListT TCM Equality)
    -> ListT TCM Equality -> ListT TCM Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Nat -> UnifyState -> ListT TCM Equality
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Nat -> UnifyState -> m Equality
    getReducedEquality Nat
    k UnifyState
    s
      shouldEtaExpand u v a s `mplus` shouldEtaExpand v u a 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 Nat
    i Elims
    es) Term
    v Type
    a UnifyState
    s = do
          fi       <- Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat)
    forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
    fromMaybeMP (Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat))
    -> Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat)
    forall a b. (a -> b) -> a -> b
    $ Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
    findFlexible Nat
    i (UnifyState -> FlexibleVars
    flexVars UnifyState
    s)
          reportSDoc "tc.lhs.unify" 50 $
            "Found flexible variable " <+> text (show 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.
          let k  = UnifyState -> Nat
    varCount UnifyState
    s Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    i -- position of var i in telescope
              b0 = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type) -> Dom Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Nat -> UnifyState -> Dom Type
    getVarTypeUnraised Nat
    k UnifyState
    s
          b         <- addContext (telFromList $ take k $ telToList $ varTel s) $ reduce b0
          (d, pars) <- catMaybesMP $ isEtaRecordType b
          ps        <- fromMaybeMP $ allProjElims es
          guard =<< orM
            [ pure $ not $ null ps
            , isRecCon v  -- is the other term a record constructor?
            , (Right True ==) <$> runBlocked (isSingletonRecord d pars)
            ]
          reportSDoc "tc.lhs.unify" 50 $
            "with projections " <+> prettyTCM (map snd ps)
          reportSDoc "tc.lhs.unify" 50 $
            "at record type " <+> prettyTCM d
          return $ EtaExpandVar fi d pars
        shouldEtaExpand Term
    _ Term
    _ Type
    _ UnifyState
    _ = ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

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

    etaExpandEquationStrategy :: Int -> UnifyStrategy
    etaExpandEquationStrategy :: Nat -> UnifyStrategy
    etaExpandEquationStrategy Nat
    k UnifyState
    s = do
      -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
      Equal Dom{unDom = a} u v <- Nat -> UnifyState -> ListT TCM Equality
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Nat -> UnifyState -> m Equality
    getReducedEqualityUnraised Nat
    k UnifyState
    s
      (d, pars) <- catMaybesMP $ addContext tel $ isEtaRecordType a
      guard =<< orM
        [ (Right True ==) <$> runBlocked (isSingletonRecord d pars)
        , shouldProject u
        , shouldProject v
        ]
      return $ EtaExpandEquation k d 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, HasBuiltins m) =>
    QName -> m Bool
    usesCopatterns QName
    f
          Con ConHead
    c ConInfo
    _ Elims
    _  -> Maybe (QName, RecordData) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (QName, RecordData) -> Bool)
    -> m (Maybe (QName, RecordData)) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor (ConHead -> QName
    conName ConHead
    c)

          Var Nat
    _ Elims
    _    -> Bool -> m Bool
    forall a. a -> m a
    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 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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DontCare Term
    _ -> Bool -> m Bool
    forall a. a -> m a
    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` ListTel -> Telescope
    telFromList (Nat -> ListTel -> ListTel
    forall a. Nat -> [a] -> [a]
    take Nat
    k (ListTel -> ListTel) -> ListTel -> ListTel
    forall a b. (a -> b) -> a -> b
    $ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList (Telescope -> ListTel) -> Telescope -> ListTel
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s)

    simplifySizesStrategy :: Int -> UnifyStrategy
    simplifySizesStrategy :: Nat -> UnifyStrategy
    simplifySizesStrategy Nat
    k UnifyState
    s = do
      isSizeName <- ListT TCM (QName -> Bool)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    m (QName -> Bool)
    isSizeNameTest
      Equal Dom{unDom = a} u v <- getReducedEquality k s
      case unEl a of
        Def QName
    d Elims
    _ -> do
          Bool -> ListT TCM ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Bool
    isSizeName QName
    d
          su <- Term -> ListT TCM SizeView
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    Term -> m SizeView
    sizeView Term
    u
          sv <- sizeView v
          case (su, sv) of
            (SizeSuc Term
    u, SizeSuc Term
    v) -> UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term -> Term -> UnifyStep
    StripSizeSuc Nat
    k Term
    u Term
    v
            (SizeSuc Term
    u, SizeView
    SizeInf  ) -> UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term -> Term -> UnifyStep
    StripSizeSuc Nat
    k Term
    u Term
    v
            (SizeView
    SizeInf  , SizeSuc Term
    v) -> UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term -> Term -> UnifyStep
    StripSizeSuc Nat
    k Term
    u Term
    v
            (SizeView, SizeView)
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        Term
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    injectiveTypeConStrategy :: Int -> UnifyStrategy
    injectiveTypeConStrategy :: Nat -> UnifyStrategy
    injectiveTypeConStrategy Nat
    k UnifyState
    s = do
      injTyCon <- PragmaOptions -> Bool
    optInjectiveTypeConstructors (PragmaOptions -> Bool)
    -> ListT TCM PragmaOptions -> ListT TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ListT TCM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      guard injTyCon
      eq <- eqUnLevel =<< getReducedEquality k s
      case eq of
        Equal Dom 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
          def <- QName -> ListT TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          guard $ case theDef 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] -> 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] -> 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'
          return $ TypeConInjectivity k d us vs
        Equality
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    injectivePragmaStrategy :: Int -> UnifyStrategy
    injectivePragmaStrategy :: Nat -> UnifyStrategy
    injectivePragmaStrategy Nat
    k UnifyState
    s = do
      eq <- Equality -> ListT TCM Equality
    forall (m :: * -> *).
    (HasBuiltins m, HasOptions m) =>
    Equality -> m Equality
    eqUnLevel (Equality -> ListT TCM Equality)
    -> ListT TCM Equality -> ListT TCM Equality
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Nat -> UnifyState -> ListT TCM Equality
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Nat -> UnifyState -> m Equality
    getReducedEquality Nat
    k UnifyState
    s
      case eq of
        Equal Dom 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
          def <- QName -> ListT TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          guard $ defInjective def
          let 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] -> 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'
          return $ TypeConInjectivity k d us vs
        Equality
    _ -> ListT TCM UnifyStep
    forall a. ListT TCM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    skipIrrelevantStrategy :: Int -> UnifyStrategy
    skipIrrelevantStrategy :: Nat -> UnifyStrategy
    skipIrrelevantStrategy Nat
    k UnifyState
    s = do
      let Equal Dom Type
    a Term
    _ Term
    _ = Nat -> UnifyState -> Equality
    getEquality Nat
    k UnifyState
    s                                 -- reduce not necessary
      Telescope -> ListT TCM () -> ListT TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` UnifyState -> Telescope
    eqTel UnifyState
    s) (ListT TCM () -> ListT TCM ()) -> ListT TCM () -> ListT TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Bool -> ListT TCM ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard (Bool -> ListT TCM ())
    -> (Either Blocker Bool -> Bool)
    -> Either Blocker Bool
    -> ListT TCM ()
    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 -> ListT TCM ())
    -> ListT TCM (Either Blocker Bool) -> ListT TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< BlockT (ListT TCM) Bool -> ListT TCM (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (Dom Type -> BlockT (ListT TCM) Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM Dom Type
    a)  -- reduction takes place here
      -- TODO: do something in case the above is blocked (i.e. `Left b`)
      UnifyStep -> ListT TCM UnifyStep
    forall a. a -> ListT TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnifyStep -> ListT TCM UnifyStep)
    -> UnifyStep -> ListT TCM UnifyStep
    forall a b. (a -> b) -> a -> b
    $ Nat -> UnifyStep
    SkipIrrelevantEquation Nat
    k

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

    unifyStep
      :: UnifyState -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
    unifyStep :: UnifyState
    -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
    unifyStep UnifyState
    s Deletion{ deleteAt :: UnifyStep -> Nat
    deleteAt = Nat
    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
        isReflexive <- Telescope
    -> WriterT UnifyOutput TCM (Either Blocker Bool)
    -> WriterT UnifyOutput TCM (Either Blocker Bool)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (WriterT UnifyOutput TCM (Either Blocker Bool)
     -> WriterT UnifyOutput TCM (Either Blocker Bool))
    -> WriterT UnifyOutput TCM (Either Blocker Bool)
    -> WriterT UnifyOutput TCM (Either Blocker Bool)
    forall a b. (a -> b) -> a -> b
    $ Type
    -> Term -> Term -> WriterT UnifyOutput TCM (Either Blocker Bool)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Either Blocker Bool)
    pureEqualTermB Type
    a Term
    u Term
    v
        withoutK <- withoutKOption
        splitOnStrict <- asksTC envSplitOnStrict
        case isReflexive of
          Left Blocker
    block   -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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', PatternSubstitution
    sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
    solveEq Nat
    k Term
    u UnifyState
    s
            PatternSubstitution -> WriterT UnifyOutput TCM ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    sigma
            UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies (UnifyState -> UnificationResult' UnifyState)
    -> WriterT UnifyOutput TCM UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Telescope -> WriterT UnifyOutput TCM Telescope)
    -> UnifyState -> WriterT UnifyOutput TCM UnifyState
    Lens' UnifyState Telescope
    lensEqTel Telescope -> WriterT UnifyOutput TCM Telescope
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce UnifyState
    s'

    unifyStep UnifyState
    s step :: UnifyStep
    step@Solution{} = RetryNormalised
    -> UnifyState
    -> UnifyStep
    -> UnifyStepT TCM (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 Nat
    k Type
    a QName
    d [Arg Term]
    pars [Arg Term]
    ixs ConHead
    c) = do
      WriterT UnifyOutput TCM Bool
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> WriterT UnifyOutput TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> WriterT UnifyOutput TCM Bool)
    -> QName -> WriterT UnifyOutput TCM Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c) (UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (UnifyStepT TCM (UnificationResult' UnifyState)
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
      withoutK <- WriterT UnifyOutput TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption

      -- Split equation telescope into parts before and after current equation
      let (eqListTel1, _ : eqListTel2) = splitAt k $ telToList $ eqTel s
          (eqTel1, eqTel2) = (telFromList eqListTel1, telFromList eqListTel2)

      -- Get constructor telescope and target indices
      cdef  <- getConInfo c
      let ctype  = Definition -> Type
    defType Definition
    cdef Type -> [Arg Term] -> Type
    `piApply` [Arg Term]
    pars
      addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
        "Constructor type: " <+> prettyTCM ctype
      TelV ctel ctarget <- addContext (varTel s `abstract` eqTel1) $ telView ctype
      let 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  Nat -> [Arg Term] -> [Arg Term]
    forall a. Nat -> [a] -> [a]
    drop ([Arg Term] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Term]
    pars) [Arg Term]
    args
                   Term
    _ -> [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      -- Get index telescope of the datatype
      dtype    <- (`piApply` pars) . defType <$> getConstInfo d
      addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
        "Datatype type: " <+> prettyTCM 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
    eqTel1 Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    ctel
          notforced = Nat -> IsForced -> [IsForced]
    forall a. Nat -> a -> [a]
    replicate (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    hduTel) IsForced
    NotForced

      -- The left inverse computed here is not actually used when computing
      -- a left inverse for the overall match, so as a slight optimisation
      -- we just don't bother computing it. __IMPOSSIBLE__ because that
      -- field in the result is never evaluated.
      res <- lift $ addContext (varTel s) $ unifyIndices' (Just __IMPOSSIBLE__)
               hduTel
               (allFlexVars notforced hduTel)
               (raise (size ctel) dtype)
               (raise (size ctel) ixs)
               cixs
      case 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
    _ -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Higher-dimensional unification is blocked: propagate
        UnifyBlocked Blocker
    block -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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 :: PatternSubstitution
    rho1    = Nat -> PatternSubstitution
    forall a. Nat -> Substitution' a
    raiseS (Telescope -> Nat
    forall a. Sized a => a -> Nat
    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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Telescope
    ctel
              rho3 :: PatternSubstitution
    rho3    = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Pattern' DBPatVar
    ceq PatternSubstitution
    rho1
              eqTel2' :: Telescope
    eqTel2' = PatternSubstitution -> Telescope -> Telescope
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    rho3 Telescope
    eqTel2
              eqTel' :: Telescope
    eqTel'  = Telescope
    eqTel1' Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel2'
              rho :: PatternSubstitution
    rho     = Nat -> PatternSubstitution -> PatternSubstitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    eqTel2) PatternSubstitution
    rho3

          PatternSubstitution -> WriterT UnifyOutput TCM ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    rho

          eqTel' <- Telescope
    -> WriterT UnifyOutput TCM Telescope
    -> WriterT UnifyOutput TCM Telescope
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (WriterT UnifyOutput TCM Telescope
     -> WriterT UnifyOutput TCM Telescope)
    -> WriterT UnifyOutput TCM Telescope
    -> WriterT UnifyOutput TCM Telescope
    forall a b. (a -> b) -> a -> b
    $ Telescope -> WriterT UnifyOutput TCM 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
          (lhs', rhs') <- addContext (varTel s) $ do
            let ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst PatternSubstitution
    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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs (Telescope -> [NamedArg (Pattern' DBPatVar)])
    -> Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
            (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
            (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
            case (lhsMatch, rhsMatch) of
              (Match.Yes Simplification
    _ IntMap (Arg Term)
    lhs', Match.Yes Simplification
    _ IntMap (Arg Term)
    rhs') -> ([Arg Term], [Arg Term])
    -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
    forall a. a -> WriterT UnifyOutput TCM a
    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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Nat
    forall a. Sized a => a -> Nat
    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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    eqTel') IntMap (Arg Term)
    rhs')
              (Match Term, Match Term)
    _ -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }

        UnifyStuck [UnificationFailure]
    _ -> let n :: Nat
    n           = UnifyState -> Nat
    eqCount UnifyState
    s
                            Equal Dom{unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a} Term
    u Term
    v = Nat -> UnifyState -> Equality
    getEquality Nat
    k UnifyState
    s
                        in UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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
                             (Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n Term
    u) (Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n Term
    v) (Nat -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    k) [Arg Term]
    ixs)]

        Unifies (Telescope
    eqTel1', PatternSubstitution
    rho0, [NamedArg (Pattern' DBPatVar)]
    _, Either NoLeftInv (Substitution, Substitution)
    _) -> do
          -- Split ps0 into parts for eqTel1 and ctel
          let (PatternSubstitution
    rho1, PatternSubstitution
    rho2) = Nat
    -> PatternSubstitution
    -> (PatternSubstitution, PatternSubstitution)
    forall a.
    Nat -> Substitution' a -> (Substitution' a, Substitution' a)
    splitS (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    ctel) PatternSubstitution
    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 PatternSubstitution
    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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Telescope
    ctel
              rho3 :: PatternSubstitution
    rho3    = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Pattern' DBPatVar
    ceq PatternSubstitution
    rho1
              eqTel2' :: Telescope
    eqTel2' = PatternSubstitution -> Telescope -> Telescope
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    rho3 Telescope
    eqTel2
              eqTel' :: Telescope
    eqTel'  = Telescope
    eqTel1' Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    eqTel2'
              rho :: PatternSubstitution
    rho     = Nat -> PatternSubstitution -> PatternSubstitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    eqTel2) PatternSubstitution
    rho3

          PatternSubstitution -> WriterT UnifyOutput TCM ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    rho

          eqTel' <- Telescope
    -> WriterT UnifyOutput TCM Telescope
    -> WriterT UnifyOutput TCM Telescope
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (WriterT UnifyOutput TCM Telescope
     -> WriterT UnifyOutput TCM Telescope)
    -> WriterT UnifyOutput TCM Telescope
    -> WriterT UnifyOutput TCM Telescope
    forall a b. (a -> b) -> a -> b
    $ Telescope -> WriterT UnifyOutput TCM 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
          (lhs', rhs') <- addContext (varTel s) $ do
            let ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst PatternSubstitution
    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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs (Telescope -> [NamedArg (Pattern' DBPatVar)])
    -> Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
            (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
            (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
            case (lhsMatch, rhsMatch) of
              (Match.Yes Simplification
    _ IntMap (Arg Term)
    lhs', Match.Yes Simplification
    _ IntMap (Arg Term)
    rhs') -> ([Arg Term], [Arg Term])
    -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
    forall a. a -> WriterT UnifyOutput TCM a
    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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Nat
    forall a. Sized a => a -> Nat
    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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
    forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
    Match.matchedArgs Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    eqTel') IntMap (Arg Term)
    rhs')
              (Match Term, Match Term)
    _ -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = 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
          WriterT UnifyOutput TCM Bool
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> WriterT UnifyOutput TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> WriterT UnifyOutput TCM Bool)
    -> QName -> WriterT UnifyOutput TCM Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    h) (UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (UnifyStepT TCM (UnificationResult' UnifyState)
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
            UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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
    _ -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    unifyStep UnifyState
    s Cycle
      { cycleVar :: UnifyStep -> Nat
    cycleVar        = Nat
    i
      , cycleOccursIn :: UnifyStep -> Term
    cycleOccursIn   = Term
    u
      } =
      case Term
    u of
        Con ConHead
    h ConInfo
    _ Elims
    _ -> do
          WriterT UnifyOutput TCM Bool
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> WriterT UnifyOutput TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT (QName -> WriterT UnifyOutput TCM Bool)
    -> QName -> WriterT UnifyOutput TCM Bool
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    h) (UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck []) (UnifyStepT TCM (UnificationResult' UnifyState)
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ do
            UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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 -> Nat -> Term -> NegativeUnification
    UnifyCycle (UnifyState -> Telescope
    varTel UnifyState
    s) Nat
    i Term
    u
        Term
    _ -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unifyStep UnifyState
    s EtaExpandVar{ expandVar :: UnifyStep -> FlexibleVar Nat
    expandVar = FlexibleVar Nat
    fi, expandVarRecordType :: UnifyStep -> QName
    expandVarRecordType = QName
    d , expandVarParameters :: UnifyStep -> [Arg Term]
    expandVarParameters = [Arg Term]
    pars } = do
      recd <- RecordData -> Maybe RecordData -> RecordData
    forall a. a -> Maybe a -> a
    fromMaybe RecordData
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe RecordData -> RecordData)
    -> WriterT UnifyOutput TCM (Maybe RecordData)
    -> WriterT UnifyOutput TCM RecordData
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> WriterT UnifyOutput TCM (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    d
      let delta = RecordData -> Telescope
    _recTel RecordData
    recd Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    pars
          c     = RecordData -> ConHead
    _recConHead RecordData
    recd
      let nfields         = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    delta
          (varTel', rho)  = expandTelescopeVar (varTel s) (m-1-i) delta c
          projectFlexible = [ ArgInfo
    -> IsForced
    -> FlexibleVarKind
    -> Maybe Nat
    -> Nat
    -> FlexibleVar Nat
    forall a.
    ArgInfo
    -> IsForced -> FlexibleVarKind -> Maybe Nat -> a -> FlexibleVar a
    FlexibleVar (FlexibleVar Nat -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo FlexibleVar Nat
    fi) (FlexibleVar Nat -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar Nat
    fi) (Nat -> FlexibleVarKind
    projFlexKind Nat
    j) (FlexibleVar Nat -> Maybe Nat
    forall a. FlexibleVar a -> Maybe Nat
    flexPos FlexibleVar Nat
    fi) (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    j) | Nat
    j <- [Nat
    0 .. Nat
    nfields Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] ]
      tellUnifySubst $ rho
      return $ Unifies $ UState
        { varTel   = varTel'
        , flexVars = projectFlexible ++ liftFlexibles nfields (flexVars s)
        , eqTel    = applyPatSubst rho $ eqTel s
        , eqLHS    = applyPatSubst rho $ eqLHS s
        , eqRHS    = applyPatSubst rho $ eqRHS s
        }
      where
        i :: Nat
    i = FlexibleVar Nat -> Nat
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Nat
    fi
        m :: Nat
    m = UnifyState -> Nat
    varCount UnifyState
    s

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

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

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

    unifyStep UnifyState
    s EtaExpandEquation{ expandAt :: UnifyStep -> Nat
    expandAt = Nat
    k, expandRecordType :: UnifyStep -> QName
    expandRecordType = QName
    d, expandParameters :: UnifyStep -> [Arg Term]
    expandParameters = [Arg Term]
    pars } = do
      recd  <- RecordData -> Maybe RecordData -> RecordData
    forall a. a -> Maybe a -> a
    fromMaybe RecordData
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe RecordData -> RecordData)
    -> WriterT UnifyOutput TCM (Maybe RecordData)
    -> WriterT UnifyOutput TCM RecordData
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> WriterT UnifyOutput TCM (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    d
      let delta = RecordData -> Telescope
    _recTel RecordData
    recd Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    pars
          c     = RecordData -> ConHead
    _recConHead RecordData
    recd
      lhs   <- expandKth $ eqLHS s
      rhs   <- expandKth $ eqRHS s
      let (tel, sigma) = expandTelescopeVar (eqTel s) k delta c
      tellUnifyProof sigma
      Unifies <$> do
       lensEqTel reduce $ s
        { eqTel    = tel
        , eqLHS    = lhs
        , eqRHS    = rhs
        }
      where
        expandKth :: [Arg Term] -> WriterT UnifyOutput TCM [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
    $ Nat -> [Arg Term] -> Maybe ([Arg Term], [Arg Term])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt Nat
    k [Arg Term]
    us
          vs <- (Telescope, [Arg Term]) -> [Arg Term]
    forall a b. (a, b) -> b
    snd ((Telescope, [Arg Term]) -> [Arg Term])
    -> WriterT UnifyOutput TCM (Telescope, [Arg Term])
    -> WriterT UnifyOutput TCM [Arg Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> [Arg Term]
    -> Term
    -> WriterT UnifyOutput TCM (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)
          vs <- reduce vs
          return $ us1 ++ vs ++ 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
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (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 Nat
    k Term
    u Term
    v) = do
      sizeTy <- WriterT UnifyOutput TCM Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
    m Type
    sizeType
      sizeSu <- sizeSuc 1 (var 0)
      let n          = UnifyState -> Nat
    eqCount UnifyState
    s
          sub        = Nat -> Substitution -> Substitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    kNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1) (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Term -> Substitution -> Substitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    sizeSu (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution
    forall a. Nat -> Substitution' a
    raiseS Nat
    1
          eqFlatTel  = Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s
          eqFlatTel' = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [Dom Type])
    sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Nat -> (Dom Type -> Dom Type) -> [Dom Type] -> [Dom Type]
    forall a. Nat -> (a -> a) -> [a] -> [a]
    updateAt Nat
    k ((Type -> Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Type -> Type) -> Dom Type -> Dom Type)
    -> (Type -> Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    forall a b. a -> b -> a
    const Type
    sizeTy) ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ [Dom Type]
    eqFlatTel
          eqTel'     = [String] -> [Dom Type] -> Telescope
    unflattenTel (Telescope -> [String]
    teleNames (Telescope -> [String]) -> Telescope -> [String]
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    s) [Dom Type]
    eqFlatTel'
      -- TODO: tellUnifyProof sub
      -- but sizeSu is not a constructor, so sub is not a PatternSubstitution!
      return $ Unifies $ s
        { eqTel = eqTel'
        , eqLHS = updateAt k (const $ defaultArg u) $ eqLHS s
        , eqRHS = updateAt k (const $ defaultArg v) $ eqRHS s
        }

    unifyStep UnifyState
    s (SkipIrrelevantEquation Nat
    k) = do
      let lhs :: [Arg Term]
    lhs = UnifyState -> [Arg Term]
    eqLHS UnifyState
    s
          (UnifyState
    s', PatternSubstitution
    sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
    solveEq Nat
    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] -> Nat -> Arg Term
    forall a. a -> [a] -> Nat -> a
    indexWithDefault Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Arg Term]
    lhs Nat
    k) UnifyState
    s
      PatternSubstitution -> WriterT UnifyOutput TCM ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    sigma
      UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyOutput TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyStepT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies UnifyState
    s'

    unifyStep UnifyState
    s (TypeConInjectivity Nat
    k QName
    d [Arg Term]
    us [Arg Term]
    vs) = do
      dtype <- Definition -> Type
    defType (Definition -> Type)
    -> WriterT UnifyOutput TCM Definition
    -> WriterT UnifyOutput TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> WriterT UnifyOutput TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      TelV dtel _ <- telView dtype
      let deq = QName -> Elims -> Term
    Def QName
    d (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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...
      Unifies <$> do
       lensEqTel reduce $ s
        { eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq)
        , eqLHS = us ++ dropAt k (eqLHS s)
        , eqRHS = vs ++ dropAt k (eqRHS 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
    $c== :: RetryNormalised -> RetryNormalised -> Bool
    == :: RetryNormalised -> RetryNormalised -> Bool
    $c/= :: RetryNormalised -> RetryNormalised -> Bool
    /= :: RetryNormalised -> RetryNormalised -> Bool
    Eq, Nat -> RetryNormalised -> ShowS
    [RetryNormalised] -> ShowS
    RetryNormalised -> String
    (Nat -> RetryNormalised -> ShowS)
    -> (RetryNormalised -> String)
    -> ([RetryNormalised] -> ShowS)
    -> Show RetryNormalised
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Nat -> RetryNormalised -> ShowS
    showsPrec :: Nat -> RetryNormalised -> ShowS
    $cshow :: RetryNormalised -> String
    show :: RetryNormalised -> String
    $cshowList :: [RetryNormalised] -> ShowS
    showList :: [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 -> Nat
    solutionAt   = Nat
    k
                   , solutionType :: UnifyStep -> Dom Type
    solutionType = dom :: Dom Type
    dom@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a }
                   , solutionVar :: UnifyStep -> FlexibleVar Nat
    solutionVar  = fi :: FlexibleVar Nat
    fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
    flexVar = Nat
    i }
                   , solutionTerm :: UnifyStep -> Term
    solutionTerm = Term
    u } = do
      let m :: Nat
    m = UnifyState -> Nat
    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.
      inMakeCase <- Lens' TCEnv Bool -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eMakeCase
      let forcedVars | Bool
    inMakeCase = IntMap Modality
    forall a. IntMap a
    IntMap.empty
                     | Bool
    otherwise  = [(Nat, Modality)] -> IntMap Modality
    forall a. [(Nat, a)] -> IntMap a
    IntMap.fromList [ (FlexibleVar Nat -> Nat
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Nat
    fi, FlexibleVar Nat -> Modality
    forall a. LensModality a => a -> Modality
    getModality FlexibleVar Nat
    fi) | FlexibleVar Nat
    fi <- UnifyState -> FlexibleVars
    flexVars UnifyState
    s,
                                                                                     FlexibleVar Nat -> IsForced
    forall a. FlexibleVar a -> IsForced
    flexForced FlexibleVar Nat
    fi IsForced -> IsForced -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsForced
    Forced ]
      (p, bound) <- patternBindingForcedVars forcedVars 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 = (PatternSubstitution -> PatternSubstitution -> PatternSubstitution)
    -> PatternSubstitution
    -> [PatternSubstitution]
    -> PatternSubstitution
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr PatternSubstitution -> PatternSubstitution -> PatternSubstitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS PatternSubstitution
    forall a. Substitution' a
    idS [ Nat -> Pattern' DBPatVar -> PatternSubstitution
    forall a. EndoSubst a => Nat -> a -> Substitution' a
    inplaceS Nat
    i (Term -> Pattern' DBPatVar
    forall a. Term -> Pattern' a
    dotP (Nat -> Elims -> Term
    Var Nat
    i [])) | Nat
    i <- IntMap Modality -> [Nat]
    forall a. IntMap a -> [Nat]
    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
    md IntMap Modality
    vars Telescope
    tel
            | IntMap Modality -> Bool
    forall a. IntMap a -> Bool
    IntMap.null IntMap Modality
    vars = Telescope
    tel
            | Bool
    otherwise        = ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Dom (String, Type) -> Dom (String, Type))
    -> [Nat] -> ListTel -> ListTel
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> Dom (String, Type) -> Dom (String, Type)
    upd (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom (Nat -> [Nat]) -> Nat -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    tel) (Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel)
            where
              upd :: Nat -> Dom (String, Type) -> Dom (String, Type)
    upd Nat
    i Dom (String, Type)
    a | Just Modality
    md' <- Nat -> IntMap Modality -> Maybe Modality
    forall a. Nat -> IntMap a -> Maybe a
    IntMap.lookup Nat
    i IntMap Modality
    vars = Modality -> Dom (String, Type) -> Dom (String, Type)
    forall a. LensModality a => Modality -> a -> a
    setModality (Modality -> Modality -> Modality
    composeModality Modality
    md Modality
    md') Dom (String, Type)
    a
                      | Bool
    otherwise                        = Dom (String, Type)
    a
      s <- return $ s { varTel = updModality (getModality fi) bound (varTel s) }

      reportSDoc "tc.lhs.unify.force" 45 $ vcat
        [ "forcedVars =" <+> pretty (IntMap.keys forcedVars)
        , "u          =" <+> prettyTCM u
        , "p          =" <+> prettyTCM p
        , "bound      =" <+> pretty (IntMap.keys bound)
        , "dotSub     =" <+> pretty 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{ unDom = a' } = getVarType (m-1-i) s
      equalTypes <- addContext (varTel s) $ do
        reportSDoc "tc.lhs.unify" 45 $ "Equation type: " <+> prettyTCM a
        reportSDoc "tc.lhs.unify" 45 $ "Variable type: " <+> prettyTCM a'
        pureEqualTypeB a 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.
      envmod <- currentModality
      let eqrel  = Dom Type -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Dom Type
    dom
          eqmod  = Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom Type
    dom
          varmod = Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom Type
    dom'
          mod    = Bool -> (Modality -> Modality) -> Modality -> Modality
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Relevance
    shapeIrrelevant 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 b a. IsBool b => b -> (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
      reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom)
      reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod
      reportSDoc "tc.lhs.unify" 65 $ text $ "Solution must be usable in a " ++ show mod ++ " 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.
      eusable <- addContext (varTel s) $ runExceptT $ usableMod mod u
      caseEitherM (return eusable) (return . UnifyBlocked) $ \ Bool
    usable -> do

      String -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    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
    forall (m :: * -> *). MonadPretty m => Bool -> m Doc
    prettyTCM Bool
    usable
      Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless Bool
    usable (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ String -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Rejected solution: " 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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM 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 a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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 Nat
    -> Pattern' DBPatVar
    -> UnifyState
    -> Maybe (UnifyState, PatternSubstitution)
    solveVar (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    i) Pattern' DBPatVar
    p UnifyState
    s of
            Maybe (UnifyState, PatternSubstitution)
    Nothing | RetryNormalised
    retry RetryNormalised -> RetryNormalised -> Bool
    forall a. Eq a => a -> a -> Bool
    == RetryNormalised
    RetryNormalised -> do
              u <- Term -> m Term
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Term
    u
              s <- lensVarTel normalise s
              solutionStep DontRetryNormalised s step{ solutionTerm = u }
            Maybe (UnifyState, PatternSubstitution)
    Nothing ->
              UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall a. a -> m a
    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 -> Nat -> Term -> UnificationFailure
    UnifyRecursiveEq (UnifyState -> Telescope
    varTel UnifyState
    s) Type
    a Nat
    i Term
    u]
            Just (UnifyState
    s', PatternSubstitution
    sub) -> do
              let rho :: PatternSubstitution
    rho = PatternSubstitution
    sub PatternSubstitution -> PatternSubstitution -> PatternSubstitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` PatternSubstitution
    dotSub
              PatternSubstitution -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifySubst PatternSubstitution
    rho
              let (UnifyState
    s'', PatternSubstitution
    sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
    solveEq Nat
    k (PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    rho Term
    u) UnifyState
    s'
              PatternSubstitution -> m ()
    forall (m :: * -> *).
    MonadWriter UnifyOutput m =>
    PatternSubstitution -> m ()
    tellUnifyProof PatternSubstitution
    sigma
              UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
    forall a. a -> m a
    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 a. a -> m a
    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 -> Nat -> Term -> Modality -> UnificationFailure
    UnifyUnusableModality (UnifyState -> Telescope
    varTel UnifyState
    s) Type
    a Nat
    i Term
    u Modality
    mod]
    solutionStep RetryNormalised
    _ UnifyState
    _ UnifyStep
    _ = m (UnificationResult' UnifyState)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    unify :: UnifyState -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
    unify :: UnifyState
    -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
    unify UnifyState
    s UnifyStrategy
    strategy = if UnifyState -> Bool
    isUnifyStateSolved UnifyState
    s
                       then UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> UnificationResult' UnifyState
    forall a. a -> UnificationResult' a
    Unifies UnifyState
    s
                       else ListT TCM UnifyStep
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue (UnifyStrategy
    strategy UnifyState
    s)
      where
        tryUnifyStepsAndContinue
          :: ListT TCM UnifyStep -> UnifyLogT TCM (UnificationResult' UnifyState)
        tryUnifyStepsAndContinue :: ListT TCM UnifyStep
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue ListT TCM UnifyStep
    steps = do
          x <- (UnifyStep
     -> UnifyLogT TCM (UnificationResult' UnifyState)
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    -> ListT (WriterT UnifyLog' TCM) UnifyStep
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT UnifyStep
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStep UnifyLogT TCM (UnificationResult' UnifyState)
    forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
    failure ((forall a1. TCM a1 -> WriterT UnifyLog' TCM a1)
    -> ListT TCM UnifyStep -> ListT (WriterT UnifyLog' TCM) UnifyStep
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
    liftListT TCM a1 -> WriterT UnifyLog' TCM a1
    forall a1. TCM a1 -> WriterT UnifyLog' TCM a1
    forall (m :: * -> *) a. Monad m => m a -> WriterT UnifyLog' m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ListT TCM UnifyStep
    steps)
          case x of
            Unifies UnifyState
    s'     -> UnifyState
    -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
    unify UnifyState
    s' UnifyStrategy
    strategy
            NoUnify NegativeUnification
    err    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (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
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (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
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a b. (a -> b) -> a -> b
    $ [UnificationFailure] -> UnificationResult' UnifyState
    forall a. [UnificationFailure] -> UnificationResult' a
    UnifyStuck [UnificationFailure]
    err

        tryUnifyStep :: UnifyStep
                     -> UnifyLogT TCM (UnificationResult' UnifyState)
                     -> UnifyLogT TCM (UnificationResult' UnifyState)
        tryUnifyStep :: UnifyStep
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStep UnifyStep
    step UnifyLogT TCM (UnificationResult' UnifyState)
    fallback = do
          Telescope -> WriterT UnifyLog' TCM () -> WriterT UnifyLog' TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    s) (WriterT UnifyLog' TCM () -> WriterT UnifyLog' TCM ())
    -> WriterT UnifyLog' TCM () -> WriterT UnifyLog' TCM ()
    forall a b. (a -> b) -> a -> b
    $
            String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
    -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    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
    forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    prettyTCM UnifyStep
    step
          (x, output) <- TCM (UnificationResult' UnifyState, UnifyOutput)
    -> WriterT
         UnifyLog' TCM (UnificationResult' UnifyState, UnifyOutput)
    forall (m :: * -> *) a. Monad m => m a -> WriterT UnifyLog' m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (UnificationResult' UnifyState, UnifyOutput)
     -> WriterT
          UnifyLog' TCM (UnificationResult' UnifyState, UnifyOutput))
    -> TCM (UnificationResult' UnifyState, UnifyOutput)
    -> WriterT
         UnifyLog' TCM (UnificationResult' UnifyState, UnifyOutput)
    forall a b. (a -> b) -> a -> b
    $ UnifyStepT TCM (UnificationResult' UnifyState)
    -> TCM (UnificationResult' UnifyState, UnifyOutput)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (UnifyStepT TCM (UnificationResult' UnifyState)
     -> TCM (UnificationResult' UnifyState, UnifyOutput))
    -> UnifyStepT TCM (UnificationResult' UnifyState)
    -> TCM (UnificationResult' UnifyState, UnifyOutput)
    forall a b. (a -> b) -> a -> b
    $ UnifyState
    -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
    unifyStep UnifyState
    s UnifyStep
    step
          case x of
            Unifies UnifyState
    s'   -> do
              String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
    -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "unifyStep successful."
              String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify" Nat
    20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
    -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
    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
    forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
    prettyTCM UnifyState
    s'
              -- tell output
              (UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ()
    forall (m :: * -> *).
    MonadWriter UnifyLog' m =>
    (UnifyLogEntry, UnifyState) -> m ()
    writeUnifyLog ((UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ())
    -> (UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ()
    forall a b. (a -> b) -> a -> b
    $ (UnifyState -> UnifyStep -> UnifyOutput -> UnifyLogEntry
    UnificationStep UnifyState
    s UnifyStep
    step UnifyOutput
    output,UnifyState
    s')
              UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    x
            NoUnify{}       -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    x
            UnifyBlocked Blocker
    b1 -> do
              y <- UnifyLogT TCM (UnificationResult' UnifyState)
    fallback
              case y of
                UnifyStuck [UnificationFailure]
    _    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (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
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (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
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UnificationResult' UnifyState
    y
            UnifyStuck [UnificationFailure]
    err1 -> do
              y <- UnifyLogT TCM (UnificationResult' UnifyState)
    fallback
              case y of
                UnifyStuck [UnificationFailure]
    err2 -> UnificationResult' UnifyState
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UnificationResult' UnifyState
     -> UnifyLogT TCM (UnificationResult' UnifyState))
    -> UnificationResult' UnifyState
    -> UnifyLogT TCM (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
    -> UnifyLogT TCM (UnificationResult' UnifyState)
    forall a. a -> WriterT UnifyLog' TCM a
    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 a. a -> m 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}.
    (HasConstInfo (t (t m)), DeBruijn a,
     MonadWriter (IntMap Modality) (t (t m)),
     MonadState (IntMap Modality) (t (t m)), MonadTrans t, MonadTrans t,
     Monad (t m), MonadReduce m) =>
    Modality -> Term -> t (t m) (Pattern' a)
    go Modality
    unitModality 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 -> Nat -> m (Pattern' a)
    bind a
    md Nat
    i = do
          (IntMap a -> Maybe a) -> m (Maybe a)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (Nat -> IntMap a -> Maybe a
    forall a. Nat -> IntMap a -> Maybe a
    IntMap.lookup Nat
    i) m (Maybe a) -> (Maybe a -> m (Pattern' a)) -> m (Pattern' a)
    forall a b. m a -> (a -> m b) -> m b
    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
    $ Nat -> a -> IntMap a
    forall a. Nat -> a -> IntMap a
    IntMap.singleton Nat
    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
    $ Nat -> IntMap a -> IntMap a
    forall a. Nat -> IntMap a -> IntMap a
    IntMap.delete Nat
    i
              Pattern' a -> m (Pattern' a)
    forall a. a -> m 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 (Nat -> a
    forall a. DeBruijn a => Nat -> a
    deBruijnVar Nat
    i)
            Maybe a
    _ -> Pattern' a -> m (Pattern' a)
    forall a. a -> m 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 (Nat -> Elims -> Term
    Var Nat
    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 a. a -> t (t m) 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
          v' <- t m Term -> t (t m) Term
    forall (m :: * -> *) a. Monad m => m a -> t m a
    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 (m :: * -> *) a. Monad m => m a -> t m a
    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 v' of
            Var Nat
    i [] -> Modality -> Nat -> t (t m) (Pattern' a)
    forall {m :: * -> *} {a} {a}.
    (MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
     DeBruijn a) =>
    a -> Nat -> m (Pattern' a)
    bind Modality
    md Nat
    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
                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
    Forced    Arg Term
    v = NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
    forall a. a -> t (t m) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a)))
    -> NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
    forall a b. (a -> b) -> a -> b
    $ (Term -> Named NamedName (Pattern' a))
    -> Arg Term -> NamedArg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    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) -> NamedArg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    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) -> NamedArg (Pattern' a))
    -> t (t m) (Arg (Pattern' a)) -> t (t m) (NamedArg (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg 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
                (ps, bound) <- listen $ zipWithM goArg (fs ++ repeat NotForced) vs
                if IntMap.null bound
                  then return $ dotP v  -- bound nothing
                  else do
                    let cpi = (ConInfo -> ConPatternInfo
    toConPatternInfo ConInfo
    ci) { conPLazy   = True } -- Not setting conPType. Is this a problem?
                    return $ ConP c cpi $ map (setOrigin Inserted) ps
              | Bool
    otherwise -> Pattern' a -> t (t m) (Pattern' a)
    forall a. a -> t (t m) 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 Nat
    _ (Elim
    _:Elims
    _) -> Pattern' a -> t (t m) (Pattern' a)
    forall a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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 a. a -> t (t m) 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{}       -> Pattern' a -> t (t m) (Pattern' a)
    forall a. a -> t (t m) 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
              -- Andreas, 2023-08-20, issue #6767
              -- The last case is not __IMPOSSIBLE__ (regresssion in 2.6.2).
              -- It would be if we had reduced to `constructorForm`,
              -- however, turning a `LitNat` into constructors would only result in churn,
              -- since literals have no variables that could be bound.