    {-# LANGUAGE NondecreasingIndentation #-}
    module Agda.TypeChecking.IApplyConfluence where

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

    import Control.Monad
    import Control.Arrow (first,second)

    import qualified Data.List as List
    import qualified Data.Map as Map

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Internal.Generic
    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 qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Maybe
    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)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical (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
    $ 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 (t :: * -> *) a. Foldable t => t a -> Int
    length [Clause]
    cls)
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Clause] -> Bool
    forall a. Null a => a -> Bool
    null [Clause]
    cls Bool -> Bool -> Bool
    && Bool -> Bool
    not ([Int] -> Bool
    forall a. Null a => a -> Bool
    null ([Int] -> Bool) -> [Int] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Clause -> [Int]) -> [Clause] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (NAPs -> [Int]
    forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [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__
          (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 (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 (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | @addClause 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 (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__
          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 (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    f) (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
              VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.cover.iapply" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    clTel
              VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.cover.iapply" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NAPs -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty NAPs
    ps
              NAPs
    ps <- NAPs -> TCMT IO NAPs
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP NAPs
    ps
              [Int] -> (Int -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (NAPs -> [Int]
    forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars NAPs
    ps) ((Int -> TCM ()) -> TCM ()) -> (Int -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i -> do
                IntervalView -> Term
    unview <- TCMT IO (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
                let phi :: Term
    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 :: [Elim]
    es = NAPs -> [Elim]
    patternsToElims NAPs
    ps
                let lhs :: Term
    lhs = QName -> [Elim] -> Term
    Def QName
    f [Elim]
    es

                VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply" Int
    40 (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
    "clause:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NAPs -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty NAPs
    ps 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    body
                VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "body =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    body

                Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    clTel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Term -> Type -> Term -> Term -> m ()
    equalTermOnFace Term
    phi Type
    trhs Term
    lhs Term
    body

                case Term
    body of
                  MetaV MetaId
    m [Elim]
    es_m' | Just [Arg Term]
    es_m <- [Elim] -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    es_m' ->
                    TCMT IO (Maybe InteractionId)
    -> TCM () -> (InteractionId -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (MetaId -> TCMT IO (Maybe InteractionId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    m) (() -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((InteractionId -> TCM ()) -> TCM ())
    -> (InteractionId -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ InteractionId
    ii -> do
                    [Closure (IPBoundary' Term)]
    cs' <- do
                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "clTel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    clTel
                      MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
                      Closure Range
    -> (Range -> TCMT IO [Closure (IPBoundary' Term)])
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure (MetaVariable -> Closure Range
    getMetaInfo MetaVariable
    mv) ((Range -> TCMT IO [Closure (IPBoundary' Term)])
     -> TCMT IO [Closure (IPBoundary' Term)])
    -> (Range -> TCMT IO [Closure (IPBoundary' Term)])
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> do -- mTel ⊢
                      Type
    ty <- MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    m
                      Telescope
    mTel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "size mTel =" 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 (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel)
                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "size es_m =" 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 ([Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m)

                      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "funny number of elims" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text ((Int, Int) -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel, [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m))
                      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                      let over :: Overapplied
    over = if Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m then Overapplied
    NotOverapplied else Overapplied
    Overapplied

                      -- extend telescope to handle extra elims
                      TelV Telescope
    mTel1 Type
    _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
    telViewUpToPath ([Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) Type
    ty
                      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "mTel1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    mTel1

                      Telescope
    -> TCMT IO [Closure (IPBoundary' Term)]
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    mTel1 Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    mTel) (TCMT IO [Closure (IPBoundary' Term)]
     -> TCMT IO [Closure (IPBoundary' Term)])
    -> TCMT IO [Closure (IPBoundary' Term)]
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall a b. (a -> b) -> a -> b
    $ do
                      Telescope
    mTel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope

                      Telescope
    -> TCMT IO [Closure (IPBoundary' Term)]
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    clTel (TCMT IO [Closure (IPBoundary' Term)]
     -> TCMT IO [Closure (IPBoundary' Term)])
    -> TCMT IO [Closure (IPBoundary' Term)]
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall a b. (a -> b) -> a -> b
    $ do -- mTel.clTel ⊢
                        () <- VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "mTel.clTel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
                        Term
    -> (Map Int Bool
        -> Blocker -> Term -> TCMT IO (Closure (IPBoundary' Term)))
    -> (Substitution -> TCMT IO (Closure (IPBoundary' Term)))
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall (m :: * -> *) a.
    MonadConversion m =>
    Term
    -> (Map Int Bool -> Blocker -> Term -> m a)
    -> (Substitution -> m a)
    -> m [a]
    forallFaceMaps Term
    phi Map Int Bool
    -> Blocker -> Term -> TCMT IO (Closure (IPBoundary' Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((Substitution -> TCMT IO (Closure (IPBoundary' Term)))
     -> TCMT IO [Closure (IPBoundary' Term)])
    -> (Substitution -> TCMT IO (Closure (IPBoundary' Term)))
    -> TCMT IO [Closure (IPBoundary' Term)]
    forall a b. (a -> b) -> a -> b
    $ \ Substitution
    alpha -> do
                        -- mTel.clTel' ⊢
                        -- mTel.clTel  ⊢ alpha : mTel.clTel'
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "mTel.clTel' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)

                        -- TelV tel _ <- telViewUpTo (size es) ty
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "i0S =" 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
    alpha
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    fsep [TCMT IO Doc
    "es :", [Elim] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Elim]
    es]
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    fsep [TCMT IO Doc
    "es_alpha :", [Elim] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Substitution
    Substitution' (SubstArg [Elim])
    alpha Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [Elim]
    es) ]

                        -- reducing path applications on endpoints in lhs
                        let
                           loop :: Term -> ReduceM Term
    loop t :: Term
    t@(Def QName
    _ [Elim]
    es) = Term -> [Elim] -> ReduceM Term
    loop' Term
    t [Elim]
    es
                           loop t :: Term
    t@(Var Int
    _ [Elim]
    es) = Term -> [Elim] -> ReduceM Term
    loop' Term
    t [Elim]
    es
                           loop t :: Term
    t@(Con ConHead
    _ ConInfo
    _ [Elim]
    es) = Term -> [Elim] -> ReduceM Term
    loop' Term
    t [Elim]
    es
                           loop t :: Term
    t@(MetaV MetaId
    _ [Elim]
    es) = Term -> [Elim] -> ReduceM Term
    loop' Term
    t [Elim]
    es
                           loop Term
    t = Term -> ReduceM Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t
                           loop' :: Term -> [Elim] -> ReduceM Term
    loop' Term
    t [Elim]
    es = Blocked' Term Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking (Blocked' Term Term -> Term)
    -> ReduceM (Blocked' Term Term) -> ReduceM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Term -> ReduceM (Blocked' Term Term))
    -> ReduceM (Blocked' Term Term)
    -> [Elim]
    -> ReduceM (Blocked' Term Term)
    reduceIApply' (Blocked' Term Term -> ReduceM (Blocked' Term Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Blocked' Term Term -> ReduceM (Blocked' Term Term))
    -> (Term -> Blocked' Term Term)
    -> Term
    -> ReduceM (Blocked' Term Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Blocked' Term Term
    forall a t. a -> Blocked' t a
    notBlocked) (Blocked' Term Term -> ReduceM (Blocked' Term Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Blocked' Term Term -> ReduceM (Blocked' Term Term))
    -> (Term -> Blocked' Term Term)
    -> Term
    -> ReduceM (Blocked' Term Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Blocked' Term Term
    forall a t. a -> Blocked' t a
    notBlocked (Term -> ReduceM (Blocked' Term Term))
    -> Term -> ReduceM (Blocked' Term Term)
    forall a b. (a -> b) -> a -> b
    $ Term
    t) [Elim]
    es)
                        Term
    lhs <- ReduceM Term -> TCMT IO Term
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM Term -> TCMT IO Term) -> ReduceM Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> ReduceM Term
    loop (QName -> [Elim] -> Term
    Def QName
    f (Substitution
    Substitution' (SubstArg [Elim])
    alpha Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [Elim]
    es))

                        let
                            idG :: [Elim]
    idG = Int -> [Elim] -> [Elim]
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    clTel) ([Elim] -> [Elim]) -> [Elim] -> [Elim]
    forall a b. (a -> b) -> a -> b
    $ (Telescope -> Boundary' (Term, Term) -> [Elim]
    forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
    teleElims Telescope
    mTel [])

                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    fsep [TCMT IO Doc
    "lhs :", Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    lhs]
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "cxt1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Constraint -> TCMT IO Doc) -> Constraint -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Substitution
    Substitution' (SubstArg Constraint)
    alpha Substitution' (SubstArg Constraint) -> Constraint -> Constraint
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Comparison -> Term -> Type -> Term -> Term -> Constraint
    ValueCmpOnFace Comparison
    CmpEq Term
    phi Type
    trhs Term
    lhs (MetaId -> [Elim] -> Term
    MetaV MetaId
    m [Elim]
    idG)

                        [Arg Term]
    -> [Arg Term]
    -> (Substitution
        -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
    -> TCMT IO (Closure (IPBoundary' Term))
    forall a.
    [Arg Term]
    -> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    unifyElims (Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    mTel) (Substitution
    Substitution' (SubstArg [Arg Term])
    alpha Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [Arg Term]
    es_m) ((Substitution
      -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
     -> TCMT IO (Closure (IPBoundary' Term)))
    -> (Substitution
        -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
    -> TCMT IO (Closure (IPBoundary' Term))
    forall a b. (a -> b) -> a -> b
    $ \ Substitution
    sigma [(Term, Term)]
    eqs -> do
                        -- mTel.clTel'' ⊢
                        -- mTel ⊢ clTel' ≃ clTel''.[eqs]
                        -- mTel.clTel'' ⊢ sigma : mTel.clTel'
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "cxt2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    40 (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
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.iapply.ip" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "eqs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(Term, Term)] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [(Term, Term)]
    eqs

                        IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term))
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure (IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term)))
    -> IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term))
    forall a b. (a -> b) -> a -> b
    $ IPBoundary :: forall t. [(t, t)] -> t -> t -> Overapplied -> IPBoundary' t
    IPBoundary
                           { ipbEquations :: [(Term, Term)]
    ipbEquations = [(Term, Term)]
    eqs
                           , ipbValue :: Term
    ipbValue     = Substitution
    Substitution' (SubstArg Term)
    sigma Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    lhs
                           , ipbMetaApp :: Term
    ipbMetaApp   = Substitution
    Substitution' (SubstArg Term)
    alpha Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` MetaId -> [Elim] -> Term
    MetaV MetaId
    m [Elim]
    es_m'
                           , ipbOverapplied :: Overapplied
    ipbOverapplied = Overapplied
    over
                           }

                        -- WAS:
                        -- fmap (over,) $ buildClosure $ (eqs
                        --                , sigma `applySubst`
                        --                    (ValueCmp CmpEq (AsTermsOf (alpha `applySubst` trhs)) lhs (alpha `applySubst` MetaV m es_m)))

                    let f :: InteractionPoint -> InteractionPoint
    f InteractionPoint
    ip = InteractionPoint
    ip { ipClause :: IPClause
    ipClause = case InteractionPoint -> IPClause
    ipClause InteractionPoint
    ip of
                                                 ipc :: IPClause
    ipc@IPClause{ipcBoundary :: IPClause -> [Closure (IPBoundary' Term)]
    ipcBoundary = [Closure (IPBoundary' Term)]
    b}
                                                   -> IPClause
    ipc {ipcBoundary :: [Closure (IPBoundary' Term)]
    ipcBoundary = [Closure (IPBoundary' Term)]
    b [Closure (IPBoundary' Term)]
    -> [Closure (IPBoundary' Term)] -> [Closure (IPBoundary' Term)]
    forall a. [a] -> [a] -> [a]
    ++ [Closure (IPBoundary' Term)]
    cs'}
                                                 ipc :: IPClause
    ipc@IPNoClause{} -> IPClause
    ipc}
                    (InteractionPoints -> InteractionPoints) -> TCM ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints ((InteractionPoint -> InteractionPoint)
    -> InteractionId -> InteractionPoints -> InteractionPoints
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> v) -> k -> BiMap k v -> BiMap k v
    BiMap.adjust InteractionPoint -> InteractionPoint
    f InteractionId
    ii)
                  Term
    _ -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | 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.
    [Arg Term]
    -> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    unifyElims [Arg Term]
    vs [Arg Term]
    ts Substitution -> [(Term, Term)] -> TCM a
    k = do
                          Context
    dom <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
                          let ([(Int, Term)]
    binds' , [(Term, Term)]
    eqs' ) = [Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
    candidate ((Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg [Arg Term]
    vs) ((Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg [Arg Term]
    ts)
                              ([(Int, Term)]
    binds'', [[(Term, Term)]]
    eqss') =
                                [((Int, Term), [(Term, Term)])]
    -> ([(Int, Term)], [[(Term, Term)]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([((Int, Term), [(Term, Term)])]
     -> ([(Int, Term)], [[(Term, Term)]]))
    -> [((Int, Term), [(Term, Term)])]
    -> ([(Int, Term)], [[(Term, Term)]])
    forall a b. (a -> b) -> a -> b
    $ ((Int, [Term]) -> ((Int, Term), [(Term, Term)]))
    -> [(Int, [Term])] -> [((Int, Term), [(Term, Term)])]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (Int
    j,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])] -> [((Int, Term), [(Term, Term)])])
    -> [(Int, [Term])] -> [((Int, Term), [(Term, Term)])]
    forall a b. (a -> b) -> a -> b
    $ Map Int [Term] -> [(Int, [Term])]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map Int [Term] -> [(Int, [Term])])
    -> Map Int [Term] -> [(Int, [Term])]
    forall a b. (a -> b) -> a -> b
    $ ([Term] -> [Term] -> [Term]) -> [(Int, [Term])] -> Map Int [Term]
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    (++) (((Int, Term) -> (Int, [Term])) -> [(Int, Term)] -> [(Int, [Term])]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> [Term]) -> (Int, Term) -> (Int, [Term])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[])) [(Int, Term)]
    binds')
                              cod :: Context
    cod   = Substitution -> [Int] -> Context -> Context
    codomain Substitution
    s (((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) Context
    dom
                              binds :: [(Int, Term)]
    binds = ((Int, Term) -> (Int, Term)) -> [(Int, Term)] -> [(Int, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Term) -> (Int, Term) -> (Int, Term)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, 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
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    vs))) [(Int, Term)]
    binds''
                              eqs :: [(Term, Term)]
    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 d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first  (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int -> Term -> Term) -> Int -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Context -> Int
    forall a. Sized a => a -> Int
    size Context
    dom Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    vs)) ([(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 :: Substitution
    s     = [(Int, Term)] -> Substitution
    forall {a}. DeBruijn a => [(Int, a)] -> Substitution' a
    bindS [(Int, Term)]
    binds
                          Substitution -> (Context -> Context) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Substitution -> (Context -> Context) -> m a -> m a
    updateContext Substitution
    s (Substitution -> [Int] -> Context -> Context
    codomain Substitution
    s (((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)) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
                          Substitution -> [(Term, Term)] -> TCM a
    k Substitution
    s (Substitution
    Substitution' (SubstArg [(Term, Term)])
    s Substitution' (SubstArg [(Term, Term)])
    -> [(Term, Term)] -> [(Term, Term)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [(Term, Term)]
    eqs)
      where
        candidate :: [Term] -> [Term] -> ([(Nat,Term)],[(Term,Term)])
        candidate :: [Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
    candidate (Term
    i:[Term]
    is) (Var Int
    j []:[Term]
    ts) = ([(Int, Term)] -> [(Int, Term)])
    -> ([(Int, Term)], [(Term, Term)])
    -> ([(Int, Term)], [(Term, Term)])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Int
    j,Term
    i)(Int, Term) -> [(Int, Term)] -> [(Int, Term)]
    forall a. a -> [a] -> [a]
    :) ([Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
    candidate [Term]
    is [Term]
    ts)
        candidate (Term
    i:[Term]
    is) (Term
    t:[Term]
    ts)        = ([(Term, Term)] -> [(Term, Term)])
    -> ([(Int, Term)], [(Term, Term)])
    -> ([(Int, Term)], [(Term, Term)])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Term
    i,Term
    t)(Term, Term) -> [(Term, Term)] -> [(Term, Term)]
    forall a. a -> [a] -> [a]
    :) ([Term] -> [Term] -> ([(Int, Term)], [(Term, Term)])
    candidate [Term]
    is [Term]
    ts)
        candidate [] [] = ([],[])
        candidate [Term]
    _ [Term]
    _ = ([(Int, Term)], [(Term, Term)])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        bindS :: [(Int, a)] -> Substitution' a
    bindS [(Int, a)]
    binds = [a] -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Int] -> (Int -> a) -> [a]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Int
    0..[Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (-Int
    1Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :((Int, a) -> Int) -> [(Int, a)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, a) -> Int
    forall a b. (a, b) -> a
    fst [(Int, a)]
    binds)] ((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 -> [(Int, a)] -> Maybe a
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    List.lookup Int
    i [(Int, a)]
    binds)))

        codomain :: Substitution
                 -> [Nat]  -- support
                 -> Context -> Context
        codomain :: Substitution -> [Int] -> Context -> Context
    codomain Substitution
    s [Int]
    vs Context
    cxt = ((Int, ContextEntry) -> ContextEntry)
    -> [(Int, ContextEntry)] -> Context
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, ContextEntry) -> ContextEntry
    forall a b. (a, b) -> b
    snd ([(Int, ContextEntry)] -> Context)
    -> [(Int, ContextEntry)] -> Context
    forall a b. (a -> b) -> a -> b
    $ ((Int, ContextEntry) -> Bool)
    -> [(Int, ContextEntry)] -> [(Int, ContextEntry)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Int
    i,ContextEntry
    c) -> Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `List.notElem` [Int]
    vs) ([(Int, ContextEntry)] -> [(Int, ContextEntry)])
    -> [(Int, ContextEntry)] -> [(Int, ContextEntry)]
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Context -> [(Int, ContextEntry)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] Context
    cxt'
         where
          cxt' :: Context
    cxt' = (Int -> ContextEntry -> ContextEntry)
    -> [Int] -> Context -> Context
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Int
    n ContextEntry
    d -> Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    dropS Int
    n Substitution
    s Substitution' (SubstArg ContextEntry)
    -> ContextEntry -> ContextEntry
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` ContextEntry
    d) [Int
    1..] Context
    cxt

    -- | Like @unifyElims@ but @Γ@ is from the 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
    -> [Arg Term]
    -> Closure Constraint
    -> ([(Term, Term)] -> Constraint -> TCM a)
    -> TCM a
    unifyElimsMeta MetaId
    m [Arg Term]
    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)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical (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) (Closure Constraint -> (Constraint -> TCM a) -> TCM a
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    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
                      MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
                      Closure Range -> (Range -> TCM a) -> TCM a
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure (MetaVariable -> Closure Range
    getMetaInfo MetaVariable
    mv) ((Range -> TCM a) -> TCM a) -> (Range -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ Range
    _ -> do -- mTel ⊢
                      Type
    ty <- MetaId -> TCMT IO Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    m
                      Telescope
    mTel0 <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel0 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    "funny number of elims" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text ((Int, Int) -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel0, [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m))
                      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- meta has at least enough arguments to fill its creation context.
                      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
    "ty: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ty

                      -- if we have more arguments we extend the telescope accordingly.
                      TelV Telescope
    mTel1 Type
    _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
    telViewUpToPath ([Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    es_m) Type
    ty
                      Telescope -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    mTel1 Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    mTel0) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
                      Telescope
    mTel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                      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
    "mTel: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    mTel

                      [Arg Term]
    es_m <- [Arg Term] -> TCMT IO [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg Term] -> TCMT IO [Arg Term])
    -> [Arg Term] -> TCMT IO [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    take (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    mTel) [Arg Term]
    es_m
                      -- invariant: size mTel == size es_m

                      (Constraint
    c,Telescope
    cxt) <- Closure Constraint
    -> (Constraint -> TCMT IO (Constraint, Telescope))
    -> TCMT IO (Constraint, Telescope)
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Constraint
    cl ((Constraint -> TCMT IO (Constraint, Telescope))
     -> TCMT IO (Constraint, Telescope))
    -> (Constraint -> TCMT IO (Constraint, Telescope))
    -> TCMT IO (Constraint, Telescope)
    forall a b. (a -> b) -> a -> b
    $ \ 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 :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
                      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
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    cxt

                      Telescope -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    cxt (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ 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
    "es_m" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    es_m

                      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
    "trying unifyElims"

                      [Arg Term]
    -> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    forall a.
    [Arg Term]
    -> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    unifyElims (Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    mTel) [Arg Term]
    es_m ((Substitution -> [(Term, Term)] -> TCM a) -> TCM a)
    -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ 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
    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)