content: {-# 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 ( All(..) )
  import qualified Data.List as List
  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.Size
  import Agda.Utils.Singleton
  import qualified Agda.Utils.VarSet as VarSet
  
  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 @
    , TCM (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 (Show, Functor, Foldable, 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 linv tel flex a us vs =
      fmap (\(a,b,c,_) -> (a,b,c)) <$> unifyIndices' linv tel flex a us 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' linv tel flex a us vs = Bench.billTo [Bench.UnifyIndices] $ case (us, vs) of
    ([], []) -> pure $ Unifies (tel, idS, [], pure $ Right (idS, raiseS 1))
    _        -> do
      reportSDoc "tc.lhs.unify" 10 $
        sep [ "unifyIndices"
            , ("tel  =" <+>) $ nest 2 $ prettyTCM tel
            , ("flex =" <+>) $ nest 2 $ addContext tel $ text $ show $ map flexVar flex
            , ("a    =" <+>) $ nest 2 $ addContext tel $ parens (prettyTCM a)
            , ("us   =" <+>) $ nest 2 $ addContext tel $ prettyList $ map prettyTCM us
            , ("vs   =" <+>) $ nest 2 $ addContext tel $ prettyList $ map prettyTCM vs
            ]
      initialState    <- initUnifyState tel flex a us vs
      reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState
      (result,log) <- runUnifyLogT $ unify initialState rightToLeftStrategy
      forM result $ \ s -> do -- Unifies case
          let output = mconcat [output | (UnificationStep _ _ output,_) <- log ]
          let ps = applySubst (unifyProof output) $ teleNamedArgs (eqTel initialState)
          let getTauInv = do
                strict     <- asksTC envSplitOnStrict
                cubicalCompatible <- cubicalCompatibleOption
                withoutK <- withoutKOption
                case linv of
                  Just reason -> pure (Left reason)
                  Nothing
                    | strict            -> pure (Left SplitOnStrict)
                    | cubicalCompatible -> buildLeftInverse initialState log
                    | withoutK          -> pure (Left NoCubical)
                    | otherwise         -> pure (Left WithKEnabled)
          reportSDoc "tc.lhs.unify" 20 $ "ps:" <+> pretty ps
          return (varTel s, unifySubst output, ps, getTauInv)
  
  
  
  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 s =
      msum (for (downFrom n) $ \k -> completeStrategyAt k s)
    where n = size $ eqTel s
  
  completeStrategyAt :: Int -> UnifyStrategy
  completeStrategyAt k s = msum $ map (\strat -> strat k s) $
  -- ASR (2021-02-07). The below eta-expansions are required by GHC >=
  -- 9.0.1 (see Issue #4955).
      [ (\n -> skipIrrelevantStrategy n)
      , (\n -> basicUnifyStrategy n)
      , (\n -> literalStrategy n)
      , (\n -> dataStrategy n)
      , (\n -> etaExpandVarStrategy  n)
      , (\n -> etaExpandEquationStrategy n)
      , (\n -> injectiveTypeConStrategy n)
      , (\n -> injectivePragmaStrategy n)
      , (\n -> simplifySizesStrategy n)
      , (\n -> checkEqualityStrategy 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 n x = do
    guard $ getAll $ runFree (All . (>= n)) IgnoreNot x
    return $ raise (-n) x
  
  findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
  findFlexible i flex = List.find ((i ==) . flexVar) flex
  
  basicUnifyStrategy :: Int -> UnifyStrategy
  basicUnifyStrategy k s = do
    Equal dom@Dom{unDom = a} u v <- eqUnLevel (getEquality k 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 i, Just j)
       | i == j -> mzero -- Taken care of by checkEqualityStrategy
      (Just i, Just j)
       | Just fi <- findFlexible i flex
       , Just fj <- findFlexible j flex -> do
         let choice = chooseFlex fi fj
             firstTryLeft  = msum [ return (Solution k dom{unDom = ha} fi v left)
                                  , return (Solution k dom{unDom = ha} fj u right)]
             firstTryRight = msum [ return (Solution k dom{unDom = ha} fj u right)
                                  , return (Solution k dom{unDom = ha} fi v left)]
         reportSDoc "tc.lhs.unify" 40 $ "fi = " <+> text (show fi)
         reportSDoc "tc.lhs.unify" 40 $ "fj = " <+> text (show fj)
         reportSDoc "tc.lhs.unify" 40 $ "chooseFlex: " <+> text (show choice)
         case choice of
           ChooseLeft   -> firstTryLeft
           ChooseRight  -> firstTryRight
           ExpandBoth   -> mzero -- This should be taken care of by etaExpandEquationStrategy
           ChooseEither -> firstTryRight
      (Just i, _)
       | Just fi <- findFlexible i flex -> return $ Solution k dom{unDom = ha} fi v left
      (_, Just j)
       | Just fj <- findFlexible j flex -> return $ Solution k dom{unDom = ha} fj u right
      _ -> mzero
    where
      flex = flexVars s
      n = eqCount s
      left = Left (); right = Right ()
  
  dataStrategy :: Int -> UnifyStrategy
  dataStrategy k s = do
    Equal Dom{unDom = a} u v <- eqConstructorForm =<< eqUnLevel =<< getReducedEqualityUnraised k s
    sortOk <- reduce (getSort a) <&> \case
      Type{} -> True
      Inf{}  -> True
      SSet{} -> True
      _      -> False
    case unEl a of
      Def d es | sortOk -> do
        npars <- catMaybesMP $ getNumberOfParameters 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 c _ _   , Con c' _ _  ) | c == c' -> return $ Injectivity k a d pars ixs c
          (Con c _ _   , Con c' _ _  ) -> return $ Conflict k a d pars u v
          (Var i []  , v         ) -> ifOccursStronglyRigid i v $ return $ Cycle k a d pars i v
          (u         , Var j []  ) -> ifOccursStronglyRigid j u $ return $ Cycle k a d pars j u
          _ -> mzero
      _ -> mzero
    where
      ifOccursStronglyRigid i u ret = do
          -- Call forceNotFree to reduce u as far as possible
          -- around any occurrences of i
          (_ , u) <- forceNotFree (singleton i) u
          case flexRigOccurrenceIn i u of
            Just StronglyRigid -> ret
            _ -> mzero
  
  checkEqualityStrategy :: Int -> UnifyStrategy
  checkEqualityStrategy k s = do
    let Equal Dom{unDom = a} u v = getEquality k s
        n = eqCount s
    ha <- fromMaybeMP $ isHom n a
    return $ Deletion k ha u v
  
  literalStrategy :: Int -> UnifyStrategy
  literalStrategy k s = do
    let n = eqCount s
    Equal Dom{unDom = a} u v <- eqUnLevel $ getEquality k s
    ha <- fromMaybeMP $ isHom n a
    (u, v) <- reduce (u, v)
    case (u , v) of
      (Lit l1 , Lit l2)
       | l1 == l2  -> return $ Deletion k ha u v
       | otherwise -> return $ LitConflict k ha l1 l2
      _ -> mzero
  
  etaExpandVarStrategy :: Int -> UnifyStrategy
  etaExpandVarStrategy k s = do
    Equal Dom{unDom = a} u v <- eqUnLevel =<< getReducedEquality k 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 (Var i es) v a s = do
        fi       <- fromMaybeMP $ findFlexible i (flexVars 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  = varCount s - 1 - i -- position of var i in telescope
            b0 = unDom $ getVarTypeUnraised k 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 _ _ _ _ = mzero
  
      isRecCon (Con c _ _) = isJust <$> isRecordConstructor (conName c)
      isRecCon _           = return False
  
  etaExpandEquationStrategy :: Int -> UnifyStrategy
  etaExpandEquationStrategy k s = do
    -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
    Equal Dom{unDom = a} u v <- getReducedEqualityUnraised k 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 = \case
        Def f es   -> usesCopatterns f
        Con c _ _  -> isJust <$> isRecordConstructor (conName c)
  
        Var _ _    -> return False
        Lam _ _    -> __IMPOSSIBLE__
        Lit _      -> __IMPOSSIBLE__
        Pi _ _     -> __IMPOSSIBLE__
        Sort _     -> __IMPOSSIBLE__
        Level _    -> __IMPOSSIBLE__
        MetaV _ _  -> return False
        DontCare _ -> return False
        Dummy s _  -> __IMPOSSIBLE_VERBOSE__ s
  
      tel = varTel s `abstract` telFromList (take k $ telToList $ eqTel s)
  
  simplifySizesStrategy :: Int -> UnifyStrategy
  simplifySizesStrategy k s = do
    isSizeName <- isSizeNameTest
    Equal Dom{unDom = a} u v <- getReducedEquality k s
    case unEl a of
      Def d _ -> do
        guard $ isSizeName d
        su <- sizeView u
        sv <- sizeView v
        case (su, sv) of
          (SizeSuc u, SizeSuc v) -> return $ StripSizeSuc k u v
          (SizeSuc u, SizeInf  ) -> return $ StripSizeSuc k u v
          (SizeInf  , SizeSuc v) -> return $ StripSizeSuc k u v
          _ -> mzero
      _ -> mzero
  
  injectiveTypeConStrategy :: Int -> UnifyStrategy
  injectiveTypeConStrategy k s = do
    injTyCon <- optInjectiveTypeConstructors <$> pragmaOptions
    guard injTyCon
    eq <- eqUnLevel =<< getReducedEquality k s
    case eq of
      Equal a u@(Def d es) v@(Def d' es') | d == d' -> do
        -- d must be a data, record or axiom
        def <- getConstInfo d
        guard $ case theDef def of
                  Datatype{} -> True
                  Record{}   -> True
                  Axiom{}    -> True
                  DataOrRecSig{} -> True
                  AbstractDefn{} -> False -- True triggers issue #2250
                  Function{}   -> False
                  Primitive{}  -> False
                  PrimitiveSort{} -> __IMPOSSIBLE__
                  GeneralizableVar{} -> __IMPOSSIBLE__
                  Constructor{} -> __IMPOSSIBLE__  -- Never a type!
        let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
            vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
        return $ TypeConInjectivity k d us vs
      _ -> mzero
  
  injectivePragmaStrategy :: Int -> UnifyStrategy
  injectivePragmaStrategy k s = do
    eq <- eqUnLevel =<< getReducedEquality k s
    case eq of
      Equal a u@(Def d es) v@(Def d' es') | d == d' -> do
        -- d must have an injective pragma
        def <- getConstInfo d
        guard $ defInjective def
        let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
            vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
        return $ TypeConInjectivity k d us vs
      _ -> mzero
  
  skipIrrelevantStrategy :: Int -> UnifyStrategy
  skipIrrelevantStrategy k s = do
    let Equal a _ _ = getEquality k s                                 -- reduce not necessary
    addContext (varTel s `abstract` eqTel s) $
      guard . (== Right True) =<< runBlocked (isIrrelevantOrPropM a)  -- reduction takes place here
    -- TODO: do something in case the above is blocked (i.e. `Left b`)
    return $ SkipIrrelevantEquation k
  
  
  ----------------------------------------------------
  -- Actually doing the unification
  ----------------------------------------------------
  
  unifyStep
    :: UnifyState -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
  unifyStep s Deletion{ deleteAt = k , deleteType = a , deleteLeft = u , deleteRight = v } = do
      -- Check definitional equality of u and v
      isReflexive <- addContext (varTel s) $ pureEqualTermB a u v
      withoutK <- withoutKOption
      splitOnStrict <- asksTC envSplitOnStrict
      case isReflexive of
        Left block   -> return $ UnifyBlocked block
        Right False  -> return $ UnifyStuck []
        Right True | withoutK && not splitOnStrict
                     -> return $ UnifyStuck [UnifyReflexiveEq (varTel s) a u]
        Right True   -> do
          let (s', sigma) = solveEq k u s
          tellUnifyProof sigma
          Unifies <$> lensEqTel reduce s'
  
  unifyStep s step@Solution{} = solutionStep RetryNormalised s step
  
  unifyStep s (Injectivity k a d pars ixs c) = do
    ifM (consOfHIT $ conName c) (return $ UnifyStuck []) $ do
    withoutK <- 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  = defType cdef `piApply` 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 unEl ctarget of
                 Def d' es | d == d' ->
                   let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
                   in  drop (length pars) args
                 _ -> __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 = eqTel1 `abstract` ctel
        notforced = replicate (size hduTel) 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 _ -> __IMPOSSIBLE__
  
      -- Higher-dimensional unification is blocked: propagate
      UnifyBlocked block -> return $ UnifyBlocked 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 _ | not withoutK -> do
        -- using the same variable names as in the case where hdu succeeds.
        let eqTel1' = eqTel1 `abstract` ctel
            rho1    = raiseS (size ctel)
            ceq     = ConP c noConPatternInfo $ teleNamedArgs ctel
            rho3    = consS ceq rho1
            eqTel2' = applyPatSubst rho3 eqTel2
            eqTel'  = eqTel1' `abstract` eqTel2'
            rho     = liftS (size eqTel2) rho3
  
        tellUnifyProof rho
  
        eqTel' <- addContext (varTel s) $ reduce eqTel'
  
        -- Compute new lhs and rhs by matching the old ones against rho
        (lhs', rhs') <- addContext (varTel s) $ do
          let ps = applySubst rho $ teleNamedArgs $ eqTel s
          (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
          (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
          case (lhsMatch, rhsMatch) of
            (Match.Yes _ lhs', Match.Yes _ rhs') -> return
              (reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs',
               reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs')
            _ -> __IMPOSSIBLE__
  
        return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }
  
  
      UnifyStuck _ -> let n           = eqCount s
                          Equal Dom{unDom = a} u v = getEquality k s
                      in return $ UnifyStuck [UnifyIndicesNotVars
                           (varTel s `abstract` eqTel s) a
                           (raise n u) (raise n v) (raise (n-k) ixs)]
  
      Unifies (eqTel1', rho0, _, _) -> do
        -- Split ps0 into parts for eqTel1 and ctel
        let (rho1, rho2) = splitS (size ctel) rho0
  
        -- Compute new equation telescope context and substitution
        let ceq     = ConP c noConPatternInfo $ applySubst rho2 $ teleNamedArgs ctel
            rho3    = consS ceq rho1
            eqTel2' = applyPatSubst rho3 eqTel2
            eqTel'  = eqTel1' `abstract` eqTel2'
            rho     = liftS (size eqTel2) rho3
  
        tellUnifyProof rho
  
        eqTel' <- addContext (varTel s) $ reduce eqTel'
  
        -- Compute new lhs and rhs by matching the old ones against rho
        (lhs', rhs') <- addContext (varTel s) $ do
          let ps = applySubst rho $ teleNamedArgs $ eqTel s
          (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
          (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
          case (lhsMatch, rhsMatch) of
            (Match.Yes _ lhs', Match.Yes _ rhs') -> return
              (reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs',
               reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs')
            _ -> __IMPOSSIBLE__
  
        return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }
  
  unifyStep s Conflict
    { conflictLeft  = u
    , conflictRight = v
    } =
    case u of
      Con h _ _ -> do
        ifM (consOfHIT $ conName h) (return $ UnifyStuck []) $ do
          return $ NoUnify $ UnifyConflict (varTel s) u v
      _ -> __IMPOSSIBLE__
  unifyStep s Cycle
    { cycleVar        = i
    , cycleOccursIn   = u
    } =
    case u of
      Con h _ _ -> do
        ifM (consOfHIT $ conName h) (return $ UnifyStuck []) $ do
          return $ NoUnify $ UnifyCycle (varTel s) i u
      _ -> __IMPOSSIBLE__
  
  unifyStep s EtaExpandVar{ expandVar = fi, expandVarRecordType = d , expandVarParameters = pars } = do
    recd <- fromMaybe __IMPOSSIBLE__ <$> isRecord d
    let delta = _recTel recd `apply` pars
        c     = _recConHead recd
    let nfields         = size delta
        (varTel', rho)  = expandTelescopeVar (varTel s) (m-1-i) delta c
        projectFlexible = [ FlexibleVar (getArgInfo fi) (flexForced fi) (projFlexKind j) (flexPos fi) (i + j) | j <- [0 .. nfields - 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 = flexVar fi
      m = varCount s
  
      projFlexKind :: Int -> FlexibleVarKind
      projFlexKind j = case flexKind fi of
        RecordFlex ks -> indexWithDefault ImplicitFlex ks j
        ImplicitFlex  -> ImplicitFlex
        DotFlex       -> DotFlex
        OtherFlex     -> OtherFlex
  
      liftFlexible :: Int -> Int -> Maybe Int
      liftFlexible n j = if j == i then Nothing else Just (if j > i then j + (n-1) else j)
  
      liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
      liftFlexibles n fs = mapMaybe (traverse $ liftFlexible n) fs
  
  unifyStep s EtaExpandEquation{ expandAt = k, expandRecordType = d, expandParameters = pars } = do
    recd  <- fromMaybe __IMPOSSIBLE__ <$> isRecord d
    let delta = _recTel recd `apply` pars
        c     = _recConHead 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 us = do
        let (us1,v:us2) = fromMaybe __IMPOSSIBLE__ $ splitExactlyAt k us
        vs <- snd <$> etaExpandRecord d pars (unArg v)
        vs <- reduce vs
        return $ us1 ++ vs ++ us2
  
  unifyStep s LitConflict
    { litType          = a
    , litConflictLeft  = l
    , litConflictRight = l'
    } = return $ NoUnify $ UnifyConflict (varTel s) (Lit l) (Lit l')
  
  unifyStep s (StripSizeSuc k u v) = do
    sizeTy <- sizeType
    sizeSu <- sizeSuc 1 (var 0)
    let n          = eqCount s
        sub        = liftS (n-k-1) $ consS sizeSu $ raiseS 1
        eqFlatTel  = flattenTel $ eqTel s
        eqFlatTel' = applySubst sub $ updateAt k (fmap $ const sizeTy) $ eqFlatTel
        eqTel'     = unflattenTel (teleNames $ eqTel s) 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 s (SkipIrrelevantEquation k) = do
    let lhs = eqLHS s
        (s', sigma) = solveEq k (DontCare $ unArg $ indexWithDefault __IMPOSSIBLE__ lhs k) s
    tellUnifyProof sigma
    return $ Unifies s'
  
  unifyStep s (TypeConInjectivity k d us vs) = do
    dtype <- defType <$> getConstInfo d
    TelV dtel _ <- telView dtype
    let deq = Def d $ map Apply $ teleArgs 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 (Eq, Show)
  
  solutionStep
    :: (PureTCM m, MonadWriter UnifyOutput m)
    => RetryNormalised
    -> UnifyState
    -> UnifyStep
    -> m (UnificationResult' UnifyState)
  solutionStep retry s
    step@Solution{ solutionAt   = k
                 , solutionType = dom@Dom{ unDom = a }
                 , solutionVar  = fi@FlexibleVar{ flexVar = i }
                 , solutionTerm = u } = do
    let m = varCount 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 <- viewTC eMakeCase
    let forcedVars | inMakeCase = IntMap.empty
                   | otherwise  = IntMap.fromList [ (flexVar fi, getModality fi) | fi <- flexVars s,
                                                                                   flexForced fi == 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 = foldr composeS idS [ inplaceS i (dotP (Var i [])) | i <- IntMap.keys 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 md vars tel
          | IntMap.null vars = tel
          | otherwise        = telFromList $ zipWith upd (downFrom $ size tel) (telToList tel)
          where
            upd i a | Just md' <- IntMap.lookup i vars = setModality (composeModality md md') a
                    | otherwise                        = 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  = getRelevance dom
        eqmod  = getModality dom
        varmod = getModality dom'
        mod    = applyUnless (shapeIrrelevant `moreRelevant` eqrel) (setRelevance eqrel)
               $ applyUnless (usableQuantity envmod) (setQuantity zeroQuantity)
               $ 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) $ \ usable -> do
  
    reportSDoc "tc.lhs.unify" 45 $ "Modality ok: " <+> prettyTCM usable
    unless usable $ reportSDoc "tc.lhs.unify" 65 $ "Rejected solution: " <+> prettyTCM 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 not (getCohesion eqmod `moreCohesion` getCohesion varmod) then return $ UnifyStuck [] else do
  
    case equalTypes of
      Left block  -> return $ UnifyBlocked block
      Right False -> return $ UnifyStuck []
      Right True | usable ->
        case solveVar (m - 1 - i) p s of
          Nothing | retry == RetryNormalised -> do
            u <- normalise u
            s <- lensVarTel normalise s
            solutionStep DontRetryNormalised s step{ solutionTerm = u }
          Nothing ->
            return $ UnifyStuck [UnifyRecursiveEq (varTel s) a i u]
          Just (s', sub) -> do
            let rho = sub `composeS` dotSub
            tellUnifySubst rho
            let (s'', sigma) = solveEq k (applyPatSubst rho u) s'
            tellUnifyProof sigma
            return $ Unifies s''
            -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
            -- Unifies <$> liftTCM (reduce s'')
      Right True -> return $ UnifyStuck [UnifyUnusableModality (varTel s) a i u mod]
  solutionStep _ _ _ = __IMPOSSIBLE__
  
  unify :: UnifyState -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
  unify s strategy = if isUnifyStateSolved s
                     then return $ Unifies s
                     else tryUnifyStepsAndContinue (strategy s)
    where
      tryUnifyStepsAndContinue
        :: ListT TCM UnifyStep -> UnifyLogT TCM (UnificationResult' UnifyState)
      tryUnifyStepsAndContinue steps = do
        x <- foldListT tryUnifyStep failure (liftListT lift steps)
        case x of
          Unifies s'     -> unify s' strategy
          NoUnify err    -> return $ NoUnify err
          UnifyBlocked b -> return $ UnifyBlocked b
          UnifyStuck err -> return $ UnifyStuck err
  
      tryUnifyStep :: UnifyStep
                   -> UnifyLogT TCM (UnificationResult' UnifyState)
                   -> UnifyLogT TCM (UnificationResult' UnifyState)
      tryUnifyStep step fallback = do
        addContext (varTel s) $
          reportSDoc "tc.lhs.unify" 20 $ "trying unifyStep" <+> prettyTCM step
        (x, output) <- lift $ runWriterT $ unifyStep s step
        case x of
          Unifies s'   -> do
            reportSDoc "tc.lhs.unify" 20 $ "unifyStep successful."
            reportSDoc "tc.lhs.unify" 20 $ "new unifyState:" <+> prettyTCM s'
            -- tell output
            writeUnifyLog $ (UnificationStep s step output,s')
            return x
          NoUnify{}       -> return x
          UnifyBlocked b1 -> do
            y <- fallback
            case y of
              UnifyStuck _    -> return $ UnifyBlocked b1
              UnifyBlocked b2 -> return $ UnifyBlocked $ unblockOnEither b1 b2
              _               -> return y
          UnifyStuck err1 -> do
            y <- fallback
            case y of
              UnifyStuck err2 -> return $ UnifyStuck $ err1 ++ err2
              _               -> return y
  
      failure :: Monad m => m (UnificationResult' a)
      failure = return $ 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 forced v = do
    let v' = precomputeFreeVars_ v
    runWriterT (evalStateT (go unitModality v') forced)
    where
      noForced v = gets $ VarSet.disjoint (precomputedFreeVars v) . VarSet.fromList . IntMap.keys
  
      bind md i = do
        gets (IntMap.lookup i) >>= \case
          Just md' | related md POLE 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
            tell   $ IntMap.singleton i md
            modify $ IntMap.delete i
            return $ varP (deBruijnVar i)
          _ -> return $ dotP (Var i [])
  
      go md v = ifM (noForced v) (return $ dotP v) $ do
        v' <- lift $ lift $ reduce v
        case v' of
          Var i [] -> bind md i  -- we know i is forced
          Con c ci es
            | Just vs <- allApplyElims es -> do
              fs <- defForced <$> getConstInfo (conName c)
              let goArg Forced    v = return $ fmap (unnamed . dotP) v
                  goArg NotForced v = fmap unnamed <$> traverse (go $ composeModality md $ getModality v) v
              (ps, bound) <- listen $ zipWithM goArg (fs ++ repeat NotForced) vs
              if IntMap.null bound
                then return $ dotP v  -- bound nothing
                else do
                  let cpi = (toConPatternInfo ci) { conPLazy   = True } -- Not setting conPType. Is this a problem?
                  return $ ConP c cpi $ map (setOrigin Inserted) ps
            | otherwise -> return $ dotP v   -- Higher constructor (es has IApply)
  
          -- Non-pattern positions
          Var _ (_:_) -> return $ dotP v
          Lam{}       -> return $ dotP v
          Pi{}        -> return $ dotP v
          Def{}       -> return $ dotP v
          MetaV{}     -> return $ dotP v
          Sort{}      -> return $ dotP v
          Level{}     -> return $ dotP v
          DontCare{}  -> return $ dotP v
          Dummy{}     -> return $ dotP v
          Lit{}       -> return $ dotP 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.
  