    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.IApplyConfluence where

    import Prelude hiding (null, (!!))  -- do not use partial functions like !!

    import Control.Monad.Except ( MonadError(..) )

    import Data.Bifunctor (first, second)
    import Data.DList (DList)
    import Data.Foldable (toList)
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern

    import Agda.Interaction.Options

    import Agda.TypeChecking.Primitive hiding (Nat)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Maybe
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Impossible
    import Agda.Utils.Functor

    checkIApplyConfluence_ :: QName -> TCM ()
    checkIApplyConfluence_ :: QName -> TCM ()
    checkIApplyConfluence_ QName
    f = TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      -- Andreas, 2019-03-27, iapply confluence should only be checked
      -- when --cubical or --erased-cubical is active. See
      -- test/Succeed/CheckIApplyConfluence.agda.
      -- We cannot reach the following crash point unless
      -- --cubical/--erased-cubical is active.
      VerboseKey -> Int -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadTCM m, MonadDebug m) =>
    VerboseKey -> Int -> m ()
    __CRASH_WHEN__ VerboseKey
    "tc.cover.iapply.confluence.crash" Int
    666
      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.cover.iapply" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text VerboseKey
    "Checking IApply confluence of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    f
      QName -> (Definition -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    f ((Definition -> TCM ()) -> TCM ())
    -> (Definition -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    d -> do
      case Definition -> Defn
    theDef Definition
    d of
        Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls', funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cls} -> do
          VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.cover.iapply" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text VerboseKey
    "length cls =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ([Clause] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Clause]
    cls)
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([Clause] -> Bool
    forall a. Null a => a -> Bool
    null [Clause]
    cls Bool -> Bool -> Bool
    && (Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Bool -> Bool
    not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Int] -> Bool
    forall a. Null a => a -> Bool
    null ([Int] -> Bool) -> (Clause -> [Int]) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NAPs -> [Int]
    forall p. IApplyVars p => p -> [Int]
    iApplyVars (NAPs -> [Int]) -> (Clause -> NAPs) -> Clause -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> NAPs
    namedClausePats) [Clause]
    cls') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (PragmaOptions -> Bool
    optKeepCoveringClauses (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    f ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef
              ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ ([Clause] -> [Clause]) -> Defn -> Defn
    updateCovering ([Clause] -> [Clause] -> [Clause]
    forall a b. a -> b -> a
    const [])

          Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [Clause] -> Bool -> Call
    CheckFunDefCall (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    f) QName
    f [] Bool
    False) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Clause] -> (Clause -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Clause]
    cls ((Clause -> TCM ()) -> TCM ()) -> (Clause -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Clause -> TCM ()
    checkIApplyConfluence QName
    f
        Defn
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | @checkIApplyConfluence f (Clause {namedClausePats = ps})@ checks that @f ps@
    -- reduces in a way that agrees with @IApply@ reductions.
    checkIApplyConfluence :: QName -> Clause -> TCM ()
    checkIApplyConfluence :: QName -> Clause -> TCM ()
    checkIApplyConfluence QName
    f Clause
    cl = case Clause
    cl of
          Clause {clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    Nothing} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Clause {clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Maybe (Arg Type)
    Nothing} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- Inserted clause, will respect boundaries whenever the
          -- user-written clauses do. Saves a ton of work!
          Clause {namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps} | NAPs -> Bool
    hasDefP NAPs
    ps -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
          cl :: Clause
    cl@Clause { clauseTel :: Clause -> Telescope
    clauseTel = Telescope
    clTel
                    , namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps
                    , clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Just Arg Type
    t
                    , clauseBody :: Clause -> Maybe Term
    clauseBody = Just Term
    body
                    } -> Range -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Clause -> Range
    clauseLHSRange Clause
    cl) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              let
                trhs :: Type
    trhs = Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    t
              oldCall <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe (Closure Call)
    envCall
              reportSDoc "tc.cover.iapply" 40 $ "tel =" <+> prettyTCM clTel
              reportSDoc "tc.cover.iapply" 40 $ "ps =" <+> pretty ps
              ps <- normaliseProjP ps
              forM_ (iApplyVars ps) $ \ Int
    i -> do
                unview <- TCMT IO (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
                let phi = IntervalView -> Term
    unview (IntervalView -> Term) -> IntervalView -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Arg Term -> IntervalView
    IMax (Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ IntervalView -> Term
    unview (Arg Term -> IntervalView
    INeg (Arg Term -> IntervalView) -> Arg Term -> IntervalView
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i)) (Arg Term -> IntervalView) -> Arg Term -> IntervalView
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i
                let es = NAPs -> [Elim]
    patternsToElims NAPs
    ps
                let lhs = QName -> [Elim] -> Term
    Def QName
    f [Elim]
    es

                reportSDoc "tc.cover.iapply" 40 $ text "clause:" <+> pretty ps <+> "->" <+> pretty body
                reportSDoc "tc.cover.iapply" 20 $ "body =" <+> prettyTCM body
                inTopContext $ reportSDoc "tc.cover.iapply" 20 $ "Γ =" <+> prettyTCM clTel

                let
                  k :: Substitution -> Comparison -> Type -> Term -> Term -> TCM ()
                  -- TODO (Amy, 2023-07-08): Simplifying the LHS of a
                  -- generated clause in its context is loopy, see #6722
                  k Substitution
    phi Comparison
    cmp Type
    ty Term
    u Term
    v | NAPs -> Bool
    hasDefP NAPs
    ps = Comparison -> Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Type -> Term -> Term -> m ()
    compareTerm Comparison
    cmp Type
    ty Term
    u Term
    v
                  k Substitution
    phi Comparison
    cmp Type
    ty Term
    u Term
    v = do
                    u_e   <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
    simplify Term
    u
                    -- Issue #6725: Print these terms in their own TC state.
                    -- If printing the values before entering the conversion
                    -- checker is too expensive then we could save the TC
                    -- state and print them when erroring instead, but that
                    -- might cause space leaks.
                    (u_p, v_p) <- (,) <$> prettyTCM u_e <*> (prettyTCM =<< simplify v)

                    let
                      -- Make note of the context (literally): we're
                      -- checking that this specific clause in f is
                      -- confluent with IApply reductions. That way if we
                      -- can tell the user what the endpoints are.
                      why = Range -> QName -> Term -> Term -> Term -> Type -> Call
    CheckIApplyConfluence
                        (Clause -> Range
    forall a. HasRange a => a -> Range
    getRange Clause
    cl) QName
    f
                        (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    phi Term
    lhs)
                        Term
    u_e Term
    v Type
    ty

                      -- But if the conversion checking failed really early, we drop the extra
                      -- information. In that case, it's just noise.
                      maybeDropCall e :: TCErr
    e@(TypeError CallStack
    loc TCState
    s Closure TypeError
    err)
                        | UnequalTerms Comparison
    _ Term
    u' Term
    v' CompareAs
    _ <- Closure TypeError -> TypeError
    forall a. Closure a -> a
    clValue Closure TypeError
    err =
                          -- Issue #6725: restore the TC state from the
                          -- error before dealing with the stored terms.
                          (TCState -> TCState) -> TCM () -> TCM ()
    forall a. (TCState -> TCState) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> m a -> m a
    withTCState (TCState -> TCState -> TCState
    forall a b. a -> b -> a
    const TCState
    s) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Closure TypeError -> (TypeError -> TCM ()) -> TCM ()
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeError
    err ((TypeError -> TCM ()) -> TCM ())
    -> (TypeError -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TypeError
    e' -> do
                            u' <- Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCMT IO Term
    forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
    simplify Term
    u'
                            v' <- prettyTCM =<< simplify v'

                            -- Specifically, we compare how the things are pretty-printed, to avoid
                            -- double-printing, rather than a more refined heuristic, since the
                            -- “failure case” here is *at worst* accidentally reminding the user of how
                            -- IApplyConfluence works.
                            if (u_p == u' && v_p == v')
                              then localTC (\TCEnv
    e -> TCEnv
    e { envCall = oldCall }) $ typeError e'
                              else throwError e
                      maybeDropCall TCErr
    x = TCErr -> TCM ()
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    x

                    -- Note: Any postponed constraint with this call *will* have the extra
                    -- information. This is a feature: if the constraint is woken up later,
                    -- then it's probably a good idea to remind the user of what's going on,
                    -- instead of presenting a mysterious error.
                    traceCall why (compareTerm cmp ty u v `catchError` maybeDropCall)

                addContext clTel $ compareTermOnFace' k CmpEq phi trhs lhs body

    -- | current context is of the form Γ.Δ
    unifyElims :: Args
                  -- ^ variables to keep   Γ ⊢ x_n .. x_0 : Γ
               -> Args
                  -- ^ variables to solve  Γ.Δ ⊢ ts : Γ
               -> (Substitution -> [(Term,Term)] -> TCM a)
                  -- Γ.Δ' ⊢ σ : Γ.Δ
                  -- Γ.Δ' new current context.
                  -- Γ.Δ' ⊢ [(x = u)]
                  -- Γ.Δ', [(x = u)] ⊢ id_g = ts[σ] : Γ
               -> TCM a
    unifyElims :: forall a.
    Args -> Args -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    unifyElims Args
    vs Args
    ts Substitution -> [(Term, Term)] -> TCM a
    k = do
      dom <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      let (binds' , eqs' ) = candidate (map unArg vs) (map unArg ts)
          (binds'', eqss') =
            unzip $
            map (\(Int
    j, DList Term
    tts) -> case DList Term -> [Term]
    forall a. DList a -> [a]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList DList Term
    tts of
                    Term
    t : [Term]
    ts -> ((Int
    j, Term
    t), (Term -> (Term, Term)) -> [Term] -> [(Term, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, Int -> Term
    var Int
    j) [Term]
    ts)
                    []     -> ((Int, Term), [(Term, Term)])
    forall a. HasCallStack => a
    __IMPOSSIBLE__) $
            IntMap.toList $ IntMap.fromListWith (<>) binds'
          cod'  = Substitution -> IntSet -> Context -> Context
    codomain Substitution
    s ([Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ ((Int, Term) -> Int) -> [(Int, Term)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Term) -> Int
    forall a b. (a, b) -> a
    fst [(Int, Term)]
    binds'')
          cod   = Context -> Context
    cod' Context
    dom
          svs   = Args -> Int
    forall a. Sized a => a -> Int
    size Args
    vs
          binds = [(Int, Term)] -> IntMap Term
    forall a. [(Int, a)] -> IntMap a
    IntMap.fromList ([(Int, Term)] -> IntMap Term) -> [(Int, Term)] -> IntMap Term
    forall a b. (a -> b) -> a -> b
    $
                  ((Int, Term) -> (Int, Term)) -> [(Int, Term)] -> [(Int, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Term) -> (Int, Term) -> (Int, Term)
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Context -> Int
    forall a. Sized a => a -> Int
    size Context
    cod Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    svs))) [(Int, Term)]
    binds''
          eqs   = ((Term, Term) -> (Term, Term)) -> [(Term, Term)] -> [(Term, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Term) -> (Term, Term) -> (Term, Term)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first  (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Context -> Int
    forall a. Sized a => a -> Int
    size Context
    dom Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    svs))) ([(Term, Term)] -> [(Term, Term)])
    -> [(Term, Term)] -> [(Term, Term)]
    forall a b. (a -> b) -> a -> b
    $
                  [(Term, Term)]
    eqs' [(Term, Term)] -> [(Term, Term)] -> [(Term, Term)]
    forall a. [a] -> [a] -> [a]
    ++ [[(Term, Term)]] -> [(Term, Term)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(Term, Term)]]
    eqss'
          s     = IntMap Term -> Substitution
    forall {a}. DeBruijn a => IntMap a -> Substitution' a
    bindS IntMap Term
    binds
      updateContext s cod' $ k s (s `applySubst` eqs)
      where
      candidate :: [Term] -> [Term] -> ([(Nat, DList Term)], [(Term, Term)])
      candidate :: [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
    candidate [Term]
    is [Term]
    ts = case ([Term]
    is, [Term]
    ts) of
        (Term
    i : [Term]
    is, Var Int
    j [] : [Term]
    ts) -> ([(Int, DList Term)] -> [(Int, DList Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first ((Int
    j, Term -> DList Term
    forall el coll. Singleton el coll => el -> coll
    singleton Term
    i) (Int, DList Term) -> [(Int, DList Term)] -> [(Int, DList Term)]
    forall a. a -> [a] -> [a]
    :) (([(Int, DList Term)], [(Term, Term)])
     -> ([(Int, DList Term)], [(Term, Term)]))
    -> ([(Int, DList Term)], [(Term, Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    forall a b. (a -> b) -> a -> b
    $
                                   [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
    candidate [Term]
    is [Term]
    ts
        (Term
    i : [Term]
    is, Term
    t : [Term]
    ts)        -> ([(Term, Term)] -> [(Term, Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second ((Term
    i, Term
    t) (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
    forall a. a -> [a] -> [a]
    :) (([(Int, DList Term)], [(Term, Term)])
     -> ([(Int, DList Term)], [(Term, Term)]))
    -> ([(Int, DList Term)], [(Term, Term)])
    -> ([(Int, DList Term)], [(Term, Term)])
    forall a b. (a -> b) -> a -> b
    $
                                   [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
    candidate [Term]
    is [Term]
    ts
        ([],     [])            -> ([], [])
        ([Term], [Term])
    _                       -> ([(Int, DList Term)], [(Term, Term)])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      bindS :: IntMap a -> Substitution' a
    bindS IntMap a
    binds = [a] -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([a] -> Substitution' a) -> [a] -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $
        case IntMap a -> Maybe (Int, a)
    forall a. IntMap a -> Maybe (Int, a)
    IntMap.lookupMax IntMap a
    binds of
          Maybe (Int, a)
    Nothing       -> []
          Just (Int
    max, a
    _) -> [Int] -> (Int -> a) -> [a]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Int
    0 .. Int
    max] ((Int -> a) -> [a]) -> (Int -> a) -> [a]
    forall a b. (a -> b) -> a -> b
    $ \Int
    i ->
            a -> Maybe a -> a
    forall a. a -> Maybe a -> a
    fromMaybe (Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar Int
    i) (Int -> IntMap a -> Maybe a
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    i IntMap a
    binds)

      codomain
        :: Substitution
        -> IntSet  -- Support.
        -> Context -> Context
      codomain :: Substitution -> IntSet -> Context -> Context
    codomain Substitution
    s IntSet
    vs =
        ((Int, ContextEntry) -> Maybe ContextEntry)
    -> [(Int, ContextEntry)] -> Context
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\(Int
    i, ContextEntry
    c) -> if Int
    i Int -> IntSet -> Bool
    `IntSet.member` IntSet
    vs
                             then Maybe ContextEntry
    forall a. Maybe a
    Nothing
                             else ContextEntry -> Maybe ContextEntry
    forall a. a -> Maybe a
    Just ContextEntry
    c) ([(Int, ContextEntry)] -> Context)
    -> (Context -> [(Int, ContextEntry)]) -> Context -> Context
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
        (Int -> ContextEntry -> (Int, ContextEntry))
    -> [Int] -> Context -> [(Int, ContextEntry)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Int
    i ContextEntry
    c -> (Int
    i, Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    dropS (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Substitution
    s Substitution' (SubstArg ContextEntry)
    -> ContextEntry -> ContextEntry
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` ContextEntry
    c)) [Int
    0..]

    -- | Like @unifyElims@ but @Γ@ is from the meta's @MetaInfo@ and
    -- the context extension @Δ@ is taken from the @Closure@.
    unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term,Term)] -> Constraint -> TCM a) -> TCM a
    unifyElimsMeta :: forall a.
    MetaId
    -> Args
    -> Closure Constraint
    -> ([(Term, Term)] -> Constraint -> TCM a)
    -> TCM a
    unifyElimsMeta MetaId
    m Args
    es_m Closure Constraint
    cl [(Term, Term)] -> Constraint -> TCM a
    k = TCMT IO Bool -> TCM a -> TCM a -> TCM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption) (Closure Constraint -> (Constraint -> TCM a) -> TCM a
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Constraint
    cl ((Constraint -> TCM a) -> TCM a) -> (Constraint -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ [(Term, Term)] -> Constraint -> TCM a
    k []) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
                      mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
                      enterClosure (getMetaInfo mv) $ \ Range
    _ -> do -- mTel ⊢
                      ty <- MetaId -> TCMT IO Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    m
                      mTel0 <- getContextTelescope
                      unless (size mTel0 == size es_m) $ reportSDoc "tc.iapply.ip.meta" 20 $ "funny number of elims" <+> text (show (size mTel0, size es_m))
                      unless (size mTel0 <= size es_m) $ __IMPOSSIBLE__ -- meta has at least enough arguments to fill its creation context.
                      reportSDoc "tc.iapply.ip.meta" 20 $ "ty: " <+> prettyTCM ty

                      -- if we have more arguments we extend the telescope accordingly.
                      TelV mTel1 _ <- telViewUpToPath (size es_m) ty
                      addContext (mTel1 `apply` teleArgs mTel0) $ do
                      mTel <- getContextTelescope
                      reportSDoc "tc.iapply.ip.meta" 20 $ "mTel: " <+> prettyTCM mTel

                      es_m <- return $ take (size mTel) es_m
                      -- invariant: size mTel == size es_m

                      (c,cxt) <- enterClosure cl $ \ Constraint
    c -> (Constraint
    c,) (Telescope -> (Constraint, Telescope))
    -> TCMT IO Telescope -> TCMT IO (Constraint, Telescope)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
                      reportSDoc "tc.iapply.ip.meta" 20 $ prettyTCM cxt

                      addContext cxt $ do

                      reportSDoc "tc.iapply.ip.meta" 20 $ "es_m" <+> prettyTCM es_m

                      reportSDoc "tc.iapply.ip.meta" 20 $ "trying unifyElims"

                      unifyElims (teleArgs mTel) es_m $ \ Substitution
    sigma [(Term, Term)]
    eqs -> do

                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip.meta" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "gotten a substitution"

                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip.meta" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "sigma:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
    prettyTCM Substitution
    sigma
                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip.meta" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "sigma:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    sigma

                      [(Term, Term)] -> Constraint -> TCM a
    k [(Term, Term)]
    eqs (Substitution
    Substitution' (SubstArg Constraint)
    sigma Substitution' (SubstArg Constraint) -> Constraint -> Constraint
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Constraint
    c)