    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Rules.LHS.Unify.LeftInverse where

    import Prelude hiding ((!!), null)

    import Control.Monad
    import Control.Monad.State
    import Control.Monad.Except

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

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

    import Agda.TypeChecking.Rules.LHS.Problem
    import Agda.TypeChecking.Rules.LHS.Unify.Types

    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    instance PrettyTCM NoLeftInv where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => NoLeftInv -> m Doc
    prettyTCM (UnsupportedYet UnifyStep
    s) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "It relies on" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [UnifyStep -> m Doc
    forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    explainStep UnifyStep
    s m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ","] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "which is not yet supported"
      prettyTCM NoLeftInv
    UnsupportedCxt     = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "it relies on higher-dimensional unification, which is not yet supported"
      prettyTCM (Illegal UnifyStep
    s)        = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "It relies on" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [UnifyStep -> m Doc
    forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    explainStep UnifyStep
    s m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ","] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [m Doc]
    forall (m :: * -> *). Applicative m => String -> [m Doc]
    pwords String
    "which is incompatible with" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    "Cubical Agda"]
      prettyTCM NoLeftInv
    NoCubical          = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "Cubical Agda is disabled"
      prettyTCM NoLeftInv
    WithKEnabled       = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "The K rule is enabled"
      prettyTCM NoLeftInv
    SplitOnStrict      = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "It splits on a type in SSet"
      prettyTCM NoLeftInv
    SplitOnFlat        = String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    fwords String
    "It splits on a @♭ argument"

    data NoLeftInv
      = UnsupportedYet {NoLeftInv -> UnifyStep
    badStep :: UnifyStep}
      | Illegal        {badStep :: UnifyStep}
      | NoCubical
      | WithKEnabled
      | SplitOnStrict  -- ^ splitting on a Strict Set.
      | SplitOnFlat    -- ^ splitting on a @♭ argument
      | UnsupportedCxt
      deriving Int -> NoLeftInv -> ShowS
    [NoLeftInv] -> ShowS
    NoLeftInv -> String
    (Int -> NoLeftInv -> ShowS)
    -> (NoLeftInv -> String)
    -> ([NoLeftInv] -> ShowS)
    -> Show NoLeftInv
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NoLeftInv -> ShowS
    showsPrec :: Int -> NoLeftInv -> ShowS
    $cshow :: NoLeftInv -> String
    show :: NoLeftInv -> String
    $cshowList :: [NoLeftInv] -> ShowS
    showList :: [NoLeftInv] -> ShowS
    Show

    buildLeftInverse :: (PureTCM tcm, MonadError TCErr tcm) => UnifyState -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
    buildLeftInverse :: forall (tcm :: * -> *).
    (PureTCM tcm, MonadError TCErr tcm) =>
    UnifyState
    -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
    buildLeftInverse UnifyState
    s0 UnifyLog
    log = do
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv.badstep" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ do
        cubical <- TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
        "cubical:" <+> text (show cubical)
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv.badstep" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ do
        pathp <- BuiltinId -> TCMT IO (Maybe Term)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm' BuiltinId
    builtinPathP
        "pathp:" <+> text (show $ isJust pathp)
      let cond :: tcm Bool
    cond = [tcm Bool] -> tcm Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM
           -- TODO: handle open contexts: they happen during "higher dimensional" unification,
           --       in injectivity cases.
           [
             Context -> Bool
    forall a. Null a => a -> Bool
    null (Context -> Bool) -> tcm Context -> tcm Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> tcm Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
           ]
      tcm Bool
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM tcm Bool
    cond (Either NoLeftInv (Substitution, Substitution)
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either NoLeftInv (Substitution, Substitution)
     -> tcm (Either NoLeftInv (Substitution, Substitution)))
    -> Either NoLeftInv (Substitution, Substitution)
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    forall a b. (a -> b) -> a -> b
    $ NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    UnsupportedCxt) (tcm (Either NoLeftInv (Substitution, Substitution))
     -> tcm (Either NoLeftInv (Substitution, Substitution)))
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    forall a b. (a -> b) -> a -> b
    $ do
      equivs <- UnifyLog
    -> ((UnifyLogEntry, UnifyState)
        -> tcm (Either NoLeftInv (Retract, Term)))
    -> tcm [Either NoLeftInv (Retract, Term)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM UnifyLog
    log (((UnifyLogEntry, UnifyState)
      -> tcm (Either NoLeftInv (Retract, Term)))
     -> tcm [Either NoLeftInv (Retract, Term)])
    -> ((UnifyLogEntry, UnifyState)
        -> tcm (Either NoLeftInv (Retract, Term)))
    -> tcm [Either NoLeftInv (Retract, Term)]
    forall a b. (a -> b) -> a -> b
    $ (UnifyLogEntry
     -> UnifyState -> tcm (Either NoLeftInv (Retract, Term)))
    -> (UnifyLogEntry, UnifyState)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry UnifyLogEntry
    -> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
    forall (tcm :: * -> *).
    (PureTCM tcm, MonadError TCErr tcm) =>
    UnifyLogEntry
    -> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
    buildEquiv
      case sequence equivs of
        Left NoLeftInv
    no -> do
          String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv.badstep" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "No Left Inverse:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> UnifyStep -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    prettyTCM (NoLeftInv -> UnifyStep
    badStep NoLeftInv
    no)
          Either NoLeftInv (Substitution, Substitution)
    -> tcm (Either NoLeftInv (Substitution, Substitution))
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
    forall a b. a -> Either a b
    Left NoLeftInv
    no)
        Right [(Retract, Term)]
    xs -> do
        -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
        -- Γ,φ,us =_Δ vs, i : I ⊢ leftInv0 : Γ,φ,us =_Δ vs
        -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,φ,refls][τ0] = IdS : Γ,φ,us =_Δ vs
        (tau0,leftInv0) <- case [(Retract, Term)]
    xs of
          [] -> (Substitution, Substitution) -> tcm (Substitution, Substitution)
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Substitution
    forall a. Substitution' a
    idS,Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1)
          [(Retract, Term)]
    xs -> do
            let
                loop :: [(Retract, Term)] -> m Retract
    loop [] = m Retract
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                loop [(Retract, Term)
    x] = Retract -> m Retract
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Retract -> m Retract) -> Retract -> m Retract
    forall a b. (a -> b) -> a -> b
    $ (Retract, Term) -> Retract
    forall a b. (a, b) -> a
    fst (Retract, Term)
    x
                loop ((Retract, Term)
    x:[(Retract, Term)]
    xs) = do
                  r <- [(Retract, Term)] -> m Retract
    loop [(Retract, Term)]
    xs
                  uncurry composeRetract x r
            (_,_,tau,leftInv) <- [(Retract, Term)] -> tcm Retract
    forall {m :: * -> *}.
    (PureTCM m, MonadError TCErr m) =>
    [(Retract, Term)] -> m Retract
    loop [(Retract, Term)]
    xs
            return (tau,leftInv)
        -- Γ,φ,us =_Δ vs ⊢ τ0 : Γ', φ
        -- leftInv0 : [wkS |φ,us =_Δ vs| ρ,1,refls][τ] = idS : Γ,φ,us =_Δ vs
        let tau = Substitution
    tau0 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1
        unview <- intervalUnview'
        let replaceAt Int
    n a
    x [a]
    xs = [a]
    xs0 [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    xs1
                    where ([a]
    xs0,a
    _:[a]
    xs1) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [a]
    xs
        let max Term
    r Term
    s = 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
    r) (Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    s)
            neg Term
    r = IntervalView -> Term
    unview (IntervalView -> Term) -> IntervalView -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> IntervalView
    INeg (Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    r)
        let phieq = Term -> Term
    neg (Int -> Term
    var Int
    0) Term -> Term -> Term
    `max` Int -> Term
    var (Telescope -> Int
    forall a. Sized a => a -> Int
    size (UnifyState -> Telescope
    eqTel UnifyState
    s0) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                           -- I + us =_Δ vs -- inplaceS
        let leftInv = Impossible -> [Term] -> Substitution
    forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
    termsS Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> [Term] -> [Term]
    forall {a}. Int -> a -> [a] -> [a]
    replaceAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size (UnifyState -> Telescope
    varTel UnifyState
    s0)) Term
    phieq ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution -> Int -> Term
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution
    leftInv0) ([Int] -> [Term]) -> [Int] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Telescope -> Int
    forall a. Sized a => a -> Int
    size (UnifyState -> Telescope
    varTel UnifyState
    s0) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Telescope -> Int
    forall a. Sized a => a -> Int
    size (UnifyState -> Telescope
    eqTel UnifyState
    s0))
        let working_tel = Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract (UnifyState -> Telescope
    varTel UnifyState
    s0) (Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__ (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs String
    "phi0" (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ (UnifyState -> Telescope
    eqTel UnifyState
    s0))
        reportSDoc "tc.lhs.unify.inv" 20 $ "=== before mod"
        do
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "tau0    :" <+> prettyTCM tau0
            addContext working_tel $ addContext ("r" :: String, __DUMMY_DOM__)
                                   $ reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv0:  " <+> prettyTCM leftInv0

        reportSDoc "tc.lhs.unify.inv" 20 $ "=== after mod"
        do
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "tau    :" <+> prettyTCM tau
            addContext working_tel $ addContext ("r" :: String, __DUMMY_DOM__)
                                   $ reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv:   " <+> prettyTCM leftInv

        return $ Right (tau,leftInv)

    type Retract = (Telescope, Substitution, Substitution, Substitution)
         -- Γ (the problem, including equalities),
         -- Δ ⊢ ρ : Γ
         -- Γ ⊢ τ : Δ
         -- Γ, i : I ⊢ leftInv : Γ, such that (λi. leftInv) : ρ[τ] = id_Γ

    --- Γ ⊢ us : Δ   Γ ⊢ termsS e us : Δ
    termsS ::  DeBruijn a => Impossible -> [a] -> Substitution' a
    termsS :: forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
    termsS Impossible
    e [a]
    xs = [a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    xs [a] -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Impossible -> Substitution' a
    forall a. Impossible -> Substitution' a
    EmptyS Impossible
    e

    composeRetract :: (PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm,HasBuiltins tcm, MonadAddContext tcm) => Retract -> Term -> Retract -> tcm Retract
    composeRetract :: forall (tcm :: * -> *).
    (PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm,
     HasBuiltins tcm, MonadAddContext tcm) =>
    Retract -> Term -> Retract -> tcm Retract
    composeRetract (Telescope
    prob0,Substitution
    rho0,Substitution
    tau0,Substitution
    leftInv0) Term
    phi0 (Telescope
    prob1,Substitution
    rho1,Substitution
    tau1,Substitution
    leftInv1) = do
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "=== composing"
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Γ0   :" 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
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    prob0
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tau0  :" 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
    tau0
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Γ1   :" 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
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    prob1
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob1 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tau1  :" 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
    tau1

      {-
      Γ0 = prob0
      S0 ⊢ ρ0 : Γ0
      Γ0 ⊢ τ0 : S0
      Γ0 ⊢ leftInv0 : ρ0[τ0] = idΓ0
      Γ0 ⊢ φ0
      Γ0,φ0 ⊢ leftInv0 = refl

      Γ1 = prob1
      S1 ⊢ ρ1 : Γ1
      Γ1 ⊢ τ1 : S1
      Γ1 ⊢ leftInv1 : ρ1[τ1] = idΓ1
      Γ1 ⊢ φ1 = φ0[τ0] (**)
      Γ1,φ1 ⊢ leftInv1 = refl
      S0 = Γ1

      (**) implies?
      Γ0,φ0 ⊢ leftInv1[τ0] = refl  (*)

      S1 ⊢ ρ := ρ0[ρ1] : Γ0
      Γ0 ⊢ τ := τ1[τ0] : S1
      -}

      let prob :: Telescope
    prob = Telescope
    prob0
      let rho :: Substitution
    rho = Substitution
    rho1 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    rho0
      let tau :: Substitution
    tau = Substitution
    tau0 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    tau1

      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tau  :" 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
    tau

      {-
      Γ0 ⊢ leftInv : ρ[τ] = idΓ0
      Γ0 ⊢ leftInv : ρ0[ρ1[τ1]][τ0] = idΓ0
      Γ0 ⊢ step0 := ρ0[leftInv1[τ0]] : ρ0[ρ1[τ1]][τ0] = ρ0[τ0]

      Γ0,φ0 ⊢ step0 = refl     by (*)

      Γ0 ⊢ leftInv := step0 · leftInv0 : ρ0[ρ1[τ1]][τ0] = idΓ0

      Γ0 ⊢ leftInv := tr (\ i → ρ0[ρ1[τ1]][τ0] = leftInv0[i]) φ0 step0
      Γ0,φ0 ⊢ leftInv = refl  -- because it will become step0, which is refl when φ0

      Γ0, i : I ⊢ hcomp {Γ0} (\ j → \ { (i = 0) -> ρ0[ρ1[τ1]][τ0]
                                      ; (i = 1) -> leftInv0[j]
                                      ; (φ0 = 1) -> γ0
                                      })
                             (step0[i])

      -}
      let step0 :: Substitution
    step0 = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    1 Substitution
    tau0 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    leftInv1 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    rho0

      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ (String, Dom Type) -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    "r" :: String, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "leftInv0  :" 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
    leftInv0
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob1 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "rho0  :" 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
    rho0
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tau0  :" 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
    tau0
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "rhos0[tau0]  :" 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
    tau0 Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    rho0)

      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob1 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ (String, Dom Type) -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    "r" :: String, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "leftInv1  :" 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
    leftInv1
      Telescope -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    prob0 (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ (String, Dom Type) -> tcm () -> tcm ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    "r" :: String, Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__) (tcm () -> tcm ()) -> tcm () -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "step0  :" 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
    step0

      interval <- tcm Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
      max <- primIMax
      neg <- primINeg
      result <- sequenceA <$> do
        addContext prob0 $ runNamesT (teleNames prob0) $ do
                 phi <- open phi0
                 g0 <- open $ raise (size prob0) prob0
                 step0 <- open $ Abs "i" $ step0 `applySubst` teleArgs prob0
                 leftInv0 <- open $ Abs "i" $ map unArg $ leftInv0 `applySubst` teleArgs prob0
                 bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT tcm b
    i -> (String, Dom Type)
    -> NamesT tcm (Either (Closure (Abs Type)) [Term])
    -> NamesT tcm (Either (Closure (Abs Type)) [Term])
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (String, Dom Type) -> m a -> m a
    addContext (String
    "i" :: String, Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    interval) (NamesT tcm (Either (Closure (Abs Type)) [Term])
     -> NamesT tcm (Either (Closure (Abs Type)) [Term]))
    -> NamesT tcm (Either (Closure (Abs Type)) [Term])
    -> NamesT tcm (Either (Closure (Abs Type)) [Term])
    forall a b. (a -> b) -> a -> b
    $ do
                  tel <- String
    -> ((forall b. (Subst b, DeBruijn b) => NamesT tcm b)
        -> NamesT tcm Telescope)
    -> NamesT tcm (Abs Telescope)
    forall (m :: * -> *) a.
    Monad m =>
    String
    -> ((forall b. (Subst b, DeBruijn b) => NamesT m b) -> NamesT m a)
    -> NamesT m (Abs a)
    bind String
    "_" (((forall b. (Subst b, DeBruijn b) => NamesT tcm b)
      -> NamesT tcm Telescope)
     -> NamesT tcm (Abs Telescope))
    -> ((forall b. (Subst b, DeBruijn b) => NamesT tcm b)
        -> NamesT tcm Telescope)
    -> NamesT tcm (Abs Telescope)
    forall a b. (a -> b) -> a -> b
    $ \ (NamesT tcm Term
    _ :: NamesT tcm Term) -> NamesT tcm Telescope
    g0
                  step0i <- lazyAbsApp <$> step0 <*> i
                  face <- pure max <@> (pure neg <@> i) <@> phi
                  leftInv0 <- leftInv0
                  i <- i
                  -- this composition could be optimized further whenever step0i is actually constant in i.
                  lift $ runExceptT (map unArg <$> transpSysTel' True tel [(i, leftInv0)] face step0i)
      leftInv <- case result of
        Right Abs [Term]
    x  -> Abs [Term] -> tcm (Abs [Term])
    forall a. a -> tcm a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Abs [Term]
    x
        Left Closure (Abs Type)
    cl -> do
          String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "impossible" Int
    10 (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
    vcat
            [ TCMT IO Doc
    "transpSysTel' errored with term"
            , Closure (Abs Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Closure (Abs Type) -> m Doc
    prettyTCM Closure (Abs Type)
    cl
            ]
          tcm (Abs [Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      let sigma = Impossible -> [Term] -> Substitution
    forall a. DeBruijn a => Impossible -> [a] -> Substitution' a
    termsS Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Abs [Term] -> [Term]
    forall a. Subst a => Abs a -> a
    absBody Abs [Term]
    leftInv
      verboseS "tc.lhs.unify.inv" 20 do
        addContext prob0 $ addContext ("r" :: String, __DUMMY_DOM__) do
          reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv    :" <+> prettyTCM (absBody leftInv)
          reportSDoc "tc.lhs.unify.inv" 40 $ "leftInv    :" <+> pretty (absBody leftInv)
          reportSDoc "tc.lhs.unify.inv" 40 $ "leftInvSub :" <+> pretty sigma
      return (prob, rho, tau, sigma)

    buildEquiv :: forall tcm. (PureTCM tcm, MonadError TCErr tcm) => UnifyLogEntry -> UnifyState -> tcm (Either NoLeftInv (Retract,Term))
    buildEquiv :: forall (tcm :: * -> *).
    (PureTCM tcm, MonadError TCErr tcm) =>
    UnifyLogEntry
    -> UnifyState -> tcm (Either NoLeftInv (Retract, Term))
    buildEquiv (UnificationStep UnifyState
    st step :: UnifyStep
    step@(Solution Int
    k Dom Type
    ty FlexibleVar Int
    fx Term
    tm Either () ()
    side) UnifyOutput
    output) UnifyState
    next = ExceptT NoLeftInv tcm (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT NoLeftInv tcm (Retract, Term)
     -> tcm (Either NoLeftInv (Retract, Term)))
    -> ExceptT NoLeftInv tcm (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a b. (a -> b) -> a -> b
    $ do
            let
              errorToUnsupported :: ExceptT a tcm b -> ExceptT NoLeftInv tcm b
              errorToUnsupported :: forall a b. ExceptT a tcm b -> ExceptT NoLeftInv tcm b
    errorToUnsupported ExceptT a tcm b
    m = (a -> NoLeftInv) -> ExceptT a tcm b -> ExceptT NoLeftInv tcm b
    forall (m :: * -> *) e e' a.
    Functor m =>
    (e -> e') -> ExceptT e m a -> ExceptT e' m a
    withExceptT (\ a
    _ -> UnifyStep -> NoLeftInv
    UnsupportedYet UnifyStep
    step) ExceptT a tcm b
    m
            String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
    -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "step unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> UnifyState -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
    prettyTCM UnifyState
    st
            String -> Int -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> ExceptT NoLeftInv tcm ())
    -> TCMT IO Doc -> ExceptT NoLeftInv tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "step step:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (UnifyState -> Telescope
    varTel UnifyState
    st) (UnifyStep -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    prettyTCM UnifyStep
    step)
            unview <- ExceptT NoLeftInv tcm (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
            cxt <- getContextTelescope
            reportSDoc "tc.lhs.unify.inv" 20 $ "context:" <+> prettyTCM cxt
            let
              -- k counds in eqs from the left
              m = UnifyState -> Int
    varCount UnifyState
    st
              gamma = UnifyState -> Telescope
    varTel UnifyState
    st
              eqs = UnifyState -> Telescope
    eqTel UnifyState
    st
              u = UnifyState -> [Arg Term]
    eqLHS UnifyState
    st [Arg Term] -> Int -> Arg Term
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    k
              v = UnifyState -> [Arg Term]
    eqRHS UnifyState
    st [Arg Term] -> Int -> Arg Term
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    k
              x = FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Int
    fx
              neqs = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqs
              phis = Int
    1 -- neqs
            interval <- lift $ primIntervalType
             -- Γ, φs : I^phis
            let gamma_phis = Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gamma (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $
                  (Int -> Dom (String, Type)) -> [Int] -> ListTel
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom ((String, Type) -> Dom (String, Type))
    -> (Int -> (String, Type)) -> Int -> Dom (String, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,Type
    interval) (String -> (String, Type))
    -> (Int -> String) -> Int -> (String, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    "phi" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS -> (Int -> String) -> Int -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> String
    forall a. Show a => a -> String
    show) [Int
    0 .. Int
    phis Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
            working_tel <- abstract gamma_phis <$>
              errorToUnsupported (pathTelescope' (raise phis $ eqTel st) (raise phis $ eqLHS st) (raise phis $ eqRHS st))
            reportSDoc "tc.lhs.unify.inv" 20 $ vcat
              [ "working tel:" <+> prettyTCM (working_tel :: Telescope)
              , addContext working_tel $ "working tel args:" <+> prettyTCM (teleArgs working_tel :: [Arg Term])
              ]
            (tau,leftInv,phi) <- addContext working_tel $ runNamesT [] $ do
              let raiseFrom Telescope
    tel Term
    x = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    working_tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Term
    x
              u <- open . raiseFrom gamma . unArg $ u
              v <- open . raiseFrom gamma . unArg $ v
              -- φ
              let phi = Telescope -> Term -> Term
    raiseFrom Telescope
    gamma_phis (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0
              -- working_tel ⊢ γ₁,x,γ₂,φ,eqs
              let all_args = Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    working_tel
              -- Γ₁,x : A,Γ₂
    --          gamma <- open $ raiseFrom EmptyTel gamma
              -- -- γ₁,x,γ₂,φ,eqs : W
              -- working_tel <- open $ raiseFrom EmptyTel working_tel

              -- eq_tel <- open $ raiseFrom gamma (eqTel st)

              -- [lhs,rhs] <- mapM (open . raiseFrom gamma) [eqLHS st,eqRHS st]
              let bindSplit (Telescope
    tel1,a
    tel2) = (Telescope
    tel1,Names -> a -> AbsN a
    forall a. Names -> a -> AbsN a
    AbsN (Telescope -> Names
    teleNames Telescope
    tel1) a
    tel2)
              -- . ⊢ Γ₁  ,  γ₁. (x : A),Γ₂,φ : I,[lhs ≡ rhs]
              let (gamma1, xxi) = bindSplit $ splitTelescopeAt (size gamma - x - 1) working_tel
              let (gamma1_args,xxi_args) = splitAt (size gamma1) all_args
                  (_x_arg:xi_args) = xxi_args
                  (x_arg:xi0,k_arg:xi1) = splitAt ((size gamma - size gamma1) + phis + k) xxi_args
                  -- W ⊢ (x : A),Γ₂,φ : I,[lhs ≡ rhs]
              let
                xxi_here :: Telescope
                xxi_here = AbsN Telescope -> [SubstArg Telescope] -> Telescope
    forall a. Subst a => AbsN a -> [SubstArg a] -> a
    absAppN AbsN Telescope
    xxi ([SubstArg Telescope] -> Telescope)
    -> [SubstArg Telescope] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (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]
    gamma1_args
              --                                                      x:A,Γ₂                φ
              let (xpre,krest) = bindSplit $ splitTelescopeAt ((size gamma - size gamma1) + phis + k) xxi_here
              k_arg <- open $ unArg k_arg
              xpre <- open xpre
              krest <- open krest
              delta <- bindN ["x","eq"] $ \ [NamesT (ExceptT NoLeftInv tcm) Term
    x,NamesT (ExceptT NoLeftInv tcm) Term
    eq] -> do
                         let pre :: NamesT (ExceptT NoLeftInv tcm) Telescope
    pre = Telescope -> Term -> Telescope
    forall t. Apply t => t -> Term -> t
    apply1 (Telescope -> Term -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) Telescope
    xpre NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    x
                         NamesT (ExceptT NoLeftInv tcm) Telescope
    -> (Vars (ExceptT NoLeftInv tcm)
        -> NamesT (ExceptT NoLeftInv tcm) Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall (m :: * -> *) a.
    (Monad m, Abstract a) =>
    NamesT m Telescope -> (Vars m -> NamesT m a) -> NamesT m a
    abstractN NamesT (ExceptT NoLeftInv tcm) Telescope
    pre ((Vars (ExceptT NoLeftInv tcm)
      -> NamesT (ExceptT NoLeftInv tcm) Telescope)
     -> NamesT (ExceptT NoLeftInv tcm) Telescope)
    -> (Vars (ExceptT NoLeftInv tcm)
        -> NamesT (ExceptT NoLeftInv tcm) Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall a b. (a -> b) -> a -> b
    $ \ Vars (ExceptT NoLeftInv tcm)
    args ->
                           Telescope -> Term -> Telescope
    forall t. Apply t => t -> Term -> t
    apply1 (Telescope -> Term -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
    -> [NamesT (ExceptT NoLeftInv tcm) (SubstArg Telescope)]
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
    applyN NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
    krest (NamesT (ExceptT NoLeftInv tcm) Term
    xNamesT (ExceptT NoLeftInv tcm) Term
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    forall a. a -> [a] -> [a]
    :[NamesT (ExceptT NoLeftInv tcm) Term]
    Vars (ExceptT NoLeftInv tcm)
    args) NamesT (ExceptT NoLeftInv tcm) (Term -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    eq
    --          let delta_zero = absAppN delta $ map unArg [x_arg,k_arg]
              let d_zero_args = [Arg Term]
    xi0 [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    xi1
              reportSDoc "tc.lhs.unify.inv" 20 $ "size delta:" <+> text (show $ size $ unAbsN delta)
              reportSDoc "tc.lhs.unify.inv" 20 $ "size d0args:" <+> text (show $ size d_zero_args)
              let appSide = case Either () ()
    side of
                              Left{} -> Term -> Term
    forall a. a -> a
    id
                              Right{} -> IntervalView -> Term
    unview (IntervalView -> Term) -> (Term -> IntervalView) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> IntervalView
    INeg (Arg Term -> IntervalView)
    -> (Term -> Arg Term) -> Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall e. e -> Arg e
    argN
              let
                      -- csingl :: NamesT tcm Term -> NamesT tcm [Arg Term]
                      csingl NamesT (ExceptT NoLeftInv tcm) Term
    i = (NamesT (ExceptT NoLeftInv tcm) Term
     -> NamesT (ExceptT NoLeftInv tcm) (Arg Term))
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((Term -> Arg Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) (Arg Term)
    forall a b.
    (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Arg Term
    forall e. e -> Arg e
    defaultArg) ([NamesT (ExceptT NoLeftInv tcm) Term]
     -> NamesT (ExceptT NoLeftInv tcm) [Arg Term])
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ NamesT (ExceptT NoLeftInv tcm) Term
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    csingl' NamesT (ExceptT NoLeftInv tcm) Term
    i
                      -- csingl' :: NamesT tcm Term -> [NamesT tcm Term]
                      csingl' NamesT (ExceptT NoLeftInv tcm) Term
    i = [ NamesT (ExceptT NoLeftInv tcm) Term
    k_arg NamesT (ExceptT NoLeftInv tcm) Term
    -> (NamesT (ExceptT NoLeftInv tcm) Term,
        NamesT (ExceptT NoLeftInv tcm) Term,
        NamesT (ExceptT NoLeftInv tcm) Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (m :: * -> *).
    Applicative m =>
    m Term -> (m Term, m Term, m Term) -> m Term
    <@@> (NamesT (ExceptT NoLeftInv tcm) Term
    u, NamesT (ExceptT NoLeftInv tcm) Term
    v, Term -> Term
    appSide (Term -> Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) Term
    i)
                                  , String
    -> (NamesT (ExceptT NoLeftInv tcm) Term
        -> NamesT (ExceptT NoLeftInv tcm) Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "j" ((NamesT (ExceptT NoLeftInv tcm) Term
      -> NamesT (ExceptT NoLeftInv tcm) Term)
     -> NamesT (ExceptT NoLeftInv tcm) Term)
    -> (NamesT (ExceptT NoLeftInv tcm) Term
        -> NamesT (ExceptT NoLeftInv tcm) Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (ExceptT NoLeftInv tcm) Term
    j ->
                                      let r :: Term -> Term -> Term
    r Term
    i Term
    j = case Either () ()
    side of
                                                Left{} -> IntervalView -> Term
    unview (Arg Term -> Arg Term -> IntervalView
    IMax (Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    j) (Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    i))
                                                Right{} -> IntervalView -> Term
    unview (Arg Term -> Arg Term -> IntervalView
    IMin (Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    j) (Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term)
    -> (IntervalView -> Term) -> IntervalView -> Arg Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntervalView -> Term
    unview (IntervalView -> Arg Term) -> IntervalView -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ 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
    i))
                                      in NamesT (ExceptT NoLeftInv tcm) Term
    k_arg NamesT (ExceptT NoLeftInv tcm) Term
    -> (NamesT (ExceptT NoLeftInv tcm) Term,
        NamesT (ExceptT NoLeftInv tcm) Term,
        NamesT (ExceptT NoLeftInv tcm) Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (m :: * -> *).
    Applicative m =>
    m Term -> (m Term, m Term, m Term) -> m Term
    <@@> (NamesT (ExceptT NoLeftInv tcm) Term
    u, NamesT (ExceptT NoLeftInv tcm) Term
    v, Term -> Term -> Term
    r (Term -> Term -> Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) Term
    i NamesT (ExceptT NoLeftInv tcm) (Term -> Term)
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    j)
                                  ]
              let replaceAt Int
    n a
    x [a]
    xs = [a]
    xs0 [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    xs1
                    where ([a]
    xs0,a
    _:[a]
    xs1) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [a]
    xs
                  dropAt Int
    n [a]
    xs = [a]
    xs0 [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a]
    xs1
                    where ([a]
    xs0,a
    _:[a]
    xs1) = Int -> [a] -> ([a], [a])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [a]
    xs
              delta <- open delta
              d <- bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i -> NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
    -> [NamesT (ExceptT NoLeftInv tcm) (SubstArg Telescope)]
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    NamesT m (AbsN a) -> [NamesT m (SubstArg a)] -> NamesT m a
    applyN NamesT (ExceptT NoLeftInv tcm) (AbsN Telescope)
    delta (NamesT (ExceptT NoLeftInv tcm) Term
    -> [NamesT (ExceptT NoLeftInv tcm) Term]
    csingl' NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i)

              -- Andrea 06/06/2018
              -- We do not actually add a transp/fill if the family is
              -- constant (TODO: postpone for metas) This is so variables
              -- whose types do not depend on "x" are left alone, in
              -- particular those the solution "t" depends on.
              --
              -- We might want to instead use the info discovered by the
              -- solver when checking if "t" depends on "x" to decide what
              -- to transp and what not to.
              let flag = Bool
    True
                     {-   φ -}
              tau <- {-dropAt (size gamma - 1 + k) .-} (gamma1_args ++) <$>
                                                       lift (errorToUnsupported (transpTel' flag d phi d_zero_args))
              reportSDoc "tc.lhs.unify.inv" 20 $ "tau    :" <+> prettyTCM (map (setHiding NotHidden) tau)
              leftInv <- do
                gamma1_args <- open gamma1_args
                phi <- open phi
                -- xxi_here <- open xxi_here
                -- (xi_here_f :: Abs Telescope) <- bind "i" $ \ i -> apply <$> xxi_here <*> (take 1 `fmap` csingl i)
                -- xi_here_f <- open xi_here_f
                -- xi_args <- open xi_args
                -- xif <- bind "i" $ \ i -> do
                --                      m <- (runExceptT <$> (trFillTel' flag <$> xi_here_f <*> phi <*> xi_args <*> i))
                --                      either __IMPOSSIBLE__ id <$> lift m
                -- xif <- open xif

                xi0 <- open xi0
                xi1 <- open xi1
                delta0 <- bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i -> Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    apply (Telescope -> [Arg Term] -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    -> NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) Telescope
    xpre NamesT (ExceptT NoLeftInv tcm) ([Arg Term] -> Telescope)
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) Telescope
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    take Int
    1 ([Arg Term] -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    csingl NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i)
                delta0 <- open delta0
                xi0f <- bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i -> do
                                     m <- Bool
    -> Abs Telescope
    -> Term
    -> [Arg Term]
    -> Term
    -> ExceptT (Closure (Abs Type)) tcm [Arg Term]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Bool
    -> Abs Telescope
    -> Term
    -> [Arg Term]
    -> Term
    -> ExceptT (Closure (Abs Type)) m [Arg Term]
    trFillTel' Bool
    flag (Abs Telescope
     -> Term
     -> [Arg Term]
     -> Term
     -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (Term
          -> [Arg Term]
          -> Term
          -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
    delta0 NamesT
      (ExceptT NoLeftInv tcm)
      (Term
       -> [Arg Term]
       -> Term
       -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT
         (ExceptT NoLeftInv tcm)
         ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    phi NamesT
      (ExceptT NoLeftInv tcm)
      ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    xi0 NamesT
      (ExceptT NoLeftInv tcm)
      (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i
                                     lift (errorToUnsupported m)
                xi0f <- open xi0f

                delta1 <- bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i -> do

                       args <- (Arg Term
     -> NamesT
          (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
    -> [Arg Term]
    -> NamesT
         (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Term
    -> NamesT
         (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
    forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term
     -> NamesT
          (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term))
    -> (Arg Term -> Term)
    -> Arg Term
    -> NamesT
         (ExceptT NoLeftInv tcm) (NamesT (ExceptT NoLeftInv tcm) Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) ([Arg Term]
     -> NamesT
          (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT
         (ExceptT NoLeftInv tcm) [NamesT (ExceptT NoLeftInv tcm) Term]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Abs [Arg Term] -> Term -> [Arg Term]
    Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    xi0f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i)
                       apply <$> applyN krest (take 1 (csingl' i) ++ args) <*> (drop 1 `fmap` csingl i)
                delta1 <- open delta1
                xi1f <- bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i -> do
                                     m <- Bool
    -> Abs Telescope
    -> Term
    -> [Arg Term]
    -> Term
    -> ExceptT (Closure (Abs Type)) tcm [Arg Term]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Bool
    -> Abs Telescope
    -> Term
    -> [Arg Term]
    -> Term
    -> ExceptT (Closure (Abs Type)) m [Arg Term]
    trFillTel' Bool
    flag (Abs Telescope
     -> Term
     -> [Arg Term]
     -> Term
     -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (Term
          -> [Arg Term]
          -> Term
          -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (Abs Telescope)
    delta1 NamesT
      (ExceptT NoLeftInv tcm)
      (Term
       -> [Arg Term]
       -> Term
       -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT
         (ExceptT NoLeftInv tcm)
         ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    phi NamesT
      (ExceptT NoLeftInv tcm)
      ([Arg Term] -> Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    xi1 NamesT
      (ExceptT NoLeftInv tcm)
      (Term -> ExceptT (Closure (Abs Type)) tcm [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT
         (ExceptT NoLeftInv tcm)
         (ExceptT (Closure (Abs Type)) tcm [Arg Term])
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i
                                     lift (errorToUnsupported m)
                xi1f <- open xi1f
                fmap absBody $ bind "i" $ \ forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i' -> do
                  let +++ :: m [a] -> m [a] -> m [a]
    (+++) m [a]
    m = ([a] -> [a] -> [a]) -> m [a] -> m [a] -> m [a]
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    (++) m [a]
    m
                      i :: NamesT (ExceptT NoLeftInv tcm) Term
    i = ExceptT NoLeftInv tcm Term -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl (tcm Term -> ExceptT NoLeftInv tcm Term
    forall (m :: * -> *) a. Monad m => m a -> ExceptT NoLeftInv m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift tcm Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primINeg) NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (ExceptT NoLeftInv tcm) Term
    forall b. (Subst b, DeBruijn b) => NamesT (ExceptT NoLeftInv tcm) b
    i'
    --              replaceAt (size gamma + k) <$> (fmap defaultArg $ cl primIMax <@> phi <@> i) <*> do
                  do
                    NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    gamma1_args NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
    +++ (Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    take Int
    1 ([Arg Term] -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    csingl NamesT (ExceptT NoLeftInv tcm) Term
    i NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
    +++ ((Abs [Arg Term] -> Term -> [Arg Term]
    Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    xi0f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    i) NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
    +++ (Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([Arg Term] -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    csingl NamesT (ExceptT NoLeftInv tcm) Term
    i NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall {m :: * -> *} {a}. Monad m => m [a] -> m [a] -> m [a]
    +++ (Abs [Arg Term] -> Term -> [Arg Term]
    Abs [Arg Term] -> SubstArg [Arg Term] -> [Arg Term]
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs [Arg Term] -> Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (ExceptT NoLeftInv tcm) (Abs [Arg Term])
    xi1f NamesT (ExceptT NoLeftInv tcm) (Term -> [Arg Term])
    -> NamesT (ExceptT NoLeftInv tcm) Term
    -> NamesT (ExceptT NoLeftInv tcm) [Arg Term]
    forall a b.
    NamesT (ExceptT NoLeftInv tcm) (a -> b)
    -> NamesT (ExceptT NoLeftInv tcm) a
    -> NamesT (ExceptT NoLeftInv tcm) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT (ExceptT NoLeftInv tcm) Term
    i))))
              return (tau,leftInv,phi)
            iz <- lift $ primIZero
            io <- lift $ primIOne
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "tau    :" <+> prettyTCM (map (setHiding NotHidden) tau)
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "tauS   :" <+> prettyTCM (termsS __IMPOSSIBLE__ $ map unArg tau)
            addContext working_tel $ addContext ("r" :: String, defaultDom interval)
                                   $ reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv:   " <+> prettyTCM (map (setHiding NotHidden) leftInv)
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv[0]:" <+> (prettyTCM =<< reduce (subst 0 iz $ map (setHiding NotHidden) leftInv))
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "leftInv[1]:" <+> (prettyTCM =<< reduce  (subst 0 io $ map (setHiding NotHidden) leftInv))
            addContext working_tel $ reportSDoc "tc.lhs.unify.inv" 20 $ "[rho]tau :" <+>
                                                                                      -- k   φ
              prettyTCM (applySubst (termsS __IMPOSSIBLE__ $ map unArg tau) $ fromPatternSubstitution
                                                                          $ raise (size (eqTel st) - 1{-k-} + phis {-neqs{-φs-} - 1{-φ0-}-})
                                                                          $ unifySubst output)
            reportSDoc "tc.lhs.unify.inv" 20 $ "."
            let rho0 = PatternSubstitution -> Substitution
    fromPatternSubstitution (PatternSubstitution -> Substitution)
    -> PatternSubstitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ UnifyOutput -> PatternSubstitution
    unifySubst UnifyOutput
    output
            addContext (varTel next) $ addContext (eqTel next) $ reportSDoc "tc.lhs.unify.inv" 20 $
              "prf :" <+> prettyTCM (fromPatternSubstitution $ unifyProof output)
            let c0 = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    Abs String
    "i" (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> Int -> Term
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS (PatternSubstitution -> Substitution
    fromPatternSubstitution (PatternSubstitution -> Substitution)
    -> PatternSubstitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ UnifyOutput -> PatternSubstitution
    unifyProof UnifyOutput
    output) (Int
    neqs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
            let c = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> Telescope -> Int
    forall a b. (a -> b) -> a -> b
    $ UnifyState -> Telescope
    eqTel UnifyState
    next) (Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1) Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    c0
            addContext (varTel next) $ addContext ("φ" :: String, __DUMMY_DOM__) $ addContext (raise 1 $ eqTel next) $
              reportSDoc "tc.lhs.unify.inv" 20 $ "c :" <+> prettyTCM c
    --        let rho = liftS (neqs - k - 1) $ consS (raise (1 + k) c) $ liftS (1 + k) rho0
            let rho = Int -> Term -> Substitution
    forall a. DeBruijn a => Int -> a -> Substitution' a
    singletonS (Int
    neqs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    k Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    c  Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    neqs) Substitution
    rho0
            reportSDoc "tc.lhs.unify.inv" 20 $ text "old_sizes: " <+> pretty (size $ varTel st, size $ eqTel st)
            reportSDoc "tc.lhs.unify.inv" 20 $ text "new_sizes: " <+> pretty (size $ varTel next, size $ eqTel next)
    --        addContext (abstract (varTel next) $ ExtendTel __DUMMY_DOM__ (Abs "φ" $ raise 1 $ eqTel next)) $
            addContext (varTel next) $ addContext ("φ" :: String, __DUMMY_DOM__) $ addContext (raise 1 $ eqTel next) $
              reportSDoc "tc.lhs.unify.inv" 20 $ "rho   :" <+> prettyTCM rho
            return $ ((working_tel
                     , rho
                     , termsS __IMPOSSIBLE__ $ map unArg tau
                     , termsS __IMPOSSIBLE__ $ map unArg leftInv)
                     , phi)
    buildEquiv (UnificationStep UnifyState
    st step :: UnifyStep
    step@(EtaExpandVar FlexibleVar Int
    fv QName
    _d [Arg Term]
    _args) UnifyOutput
    output) UnifyState
    next = ((Retract, Term) -> Either NoLeftInv (Retract, Term))
    -> tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term))
    forall a b. (a -> b) -> tcm a -> tcm b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Retract, Term) -> Either NoLeftInv (Retract, Term)
    forall a b. b -> Either a b
    Right (tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term)))
    -> tcm (Retract, Term) -> tcm (Either NoLeftInv (Retract, Term))
    forall a b. (a -> b) -> a -> b
    $ do
            String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 TCMT IO Doc
    "buildEquiv EtaExpandVar"
            let
              gamma :: Telescope
    gamma = UnifyState -> Telescope
    varTel UnifyState
    st
              eqs :: Telescope
    eqs = UnifyState -> Telescope
    eqTel UnifyState
    st
              x :: Int
    x = FlexibleVar Int -> Int
    forall a. FlexibleVar a -> a
    flexVar FlexibleVar Int
    fv
              neqs :: Int
    neqs = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    eqs
              phis :: Int
    phis = Int
    1
            interval <- tcm Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
             -- Γ, φs : I^phis
            let gamma_phis = Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gamma (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $
                  (Int -> Dom (String, Type)) -> [Int] -> ListTel
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> Dom (String, Type)
    forall a. a -> Dom a
    defaultDom ((String, Type) -> Dom (String, Type))
    -> (Int -> (String, Type)) -> Int -> Dom (String, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,Type
    interval) (String -> (String, Type))
    -> (Int -> String) -> Int -> (String, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    "phi" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++) ShowS -> (Int -> String) -> Int -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> String
    forall a. Show a => a -> String
    show) [Int
    0 .. Int
    phis Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
            working_tel <- abstract gamma_phis <$>
              pathTelescope (raise phis $ eqTel st) (raise phis $ eqLHS st) (raise phis $ eqRHS st)
            let raiseFrom Telescope
    tel Int
    x = (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    working_tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    x
            let phi = Int -> Term
    var (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int -> Int
    raiseFrom Telescope
    gamma_phis Int
    0

            caseMaybeM (expandRecordVar (raiseFrom gamma x) working_tel) __IMPOSSIBLE__ $ \ (Telescope
    _,Substitution
    tau,Substitution
    rho,Telescope
    _) -> do
              String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    working_tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tau    :" 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
    tau
              (Retract, Term) -> tcm (Retract, Term)
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Retract, Term) -> tcm (Retract, Term))
    -> (Retract, Term) -> tcm (Retract, Term)
    forall a b. (a -> b) -> a -> b
    $ ((Telescope
    working_tel,Substitution
    rho,Substitution
    tau,Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1),Term
    phi)

    buildEquiv (UnificationStep UnifyState
    st UnifyStep
    step UnifyOutput
    output) UnifyState
    _ = do
      String -> Int -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "tc.lhs.unify.inv" Int
    20 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "steps"
      let illegal :: tcm (Either NoLeftInv (Retract, Term))
    illegal     = Either NoLeftInv (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either NoLeftInv (Retract, Term)
     -> tcm (Either NoLeftInv (Retract, Term)))
    -> Either NoLeftInv (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a b. (a -> b) -> a -> b
    $ NoLeftInv -> Either NoLeftInv (Retract, Term)
    forall a b. a -> Either a b
    Left (NoLeftInv -> Either NoLeftInv (Retract, Term))
    -> NoLeftInv -> Either NoLeftInv (Retract, Term)
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> NoLeftInv
    Illegal UnifyStep
    step
          unsupported :: tcm (Either NoLeftInv (Retract, Term))
    unsupported = Either NoLeftInv (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either NoLeftInv (Retract, Term)
     -> tcm (Either NoLeftInv (Retract, Term)))
    -> Either NoLeftInv (Retract, Term)
    -> tcm (Either NoLeftInv (Retract, Term))
    forall a b. (a -> b) -> a -> b
    $ NoLeftInv -> Either NoLeftInv (Retract, Term)
    forall a b. a -> Either a b
    Left (NoLeftInv -> Either NoLeftInv (Retract, Term))
    -> NoLeftInv -> Either NoLeftInv (Retract, Term)
    forall a b. (a -> b) -> a -> b
    $ UnifyStep -> NoLeftInv
    UnsupportedYet UnifyStep
    step
      case UnifyStep
    step of
        Deletion{}           -> tcm (Either NoLeftInv (Retract, Term))
    illegal
        TypeConInjectivity{} -> tcm (Either NoLeftInv (Retract, Term))
    illegal
        -- These should end up in a NoUnify
        Conflict{}    -> tcm (Either NoLeftInv (Retract, Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        LitConflict{} -> tcm (Either NoLeftInv (Retract, Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Cycle{}       -> tcm (Either NoLeftInv (Retract, Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        UnifyStep
    _ -> tcm (Either NoLeftInv (Retract, Term))
    unsupported

    {-# SPECIALIZE explainStep :: UnifyStep -> TCM Doc #-}
    explainStep :: MonadPretty m => UnifyStep -> m Doc
    explainStep :: forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
    explainStep Injectivity{injectConstructor :: UnifyStep -> ConHead
    injectConstructor = ConHead
    ch} =
      m Doc
    "injectivity of the data constructor" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (ConHead -> QName
    conName ConHead
    ch)
    explainStep TypeConInjectivity{} = m Doc
    "injectivity of type constructors"
    explainStep Deletion{}           = m Doc
    "the K rule"
    explainStep Solution{}           = m Doc
    "substitution in Setω"
    -- Note: this is the actual reason that a Solution step can fail, rather
    -- than the explanation for the actual step
    explainStep Conflict{}          = m Doc
    "the disjointness of data constructors"
    explainStep LitConflict{}       = m Doc
    "the disjointness of literal values"
    explainStep Cycle{}             = m Doc
    "the impossibility of cyclic values"
    explainStep EtaExpandVar{}      = m Doc
    "eta-expansion of variables"
    explainStep EtaExpandEquation{} = m Doc
    "eta-expansion of equations"
    explainStep StripSizeSuc{}      = m Doc
    "the injectivity of size successors"
    explainStep SkipIrrelevantEquation{} = m Doc
    "ignoring irrelevant equations"