    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Telescope where

    import Prelude hiding (null)

    import Control.Monad

    import Data.Bifunctor (first)
    import Data.Foldable (find)
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Maybe
    import Data.Monoid

    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty ( Pretty )
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern ( patternToTerm )

    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Free

    import Agda.Utils.CallStack ( withCallerCallStack )
    import Agda.Utils.Either
    import Agda.Utils.Empty
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Tuple
    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    -- | Flatten telescope: @(Γ : Tel) -> [Type Γ]@
    flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel :: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom a)
    EmptyTel          = []
    flattenTel (ExtendTel Dom a
    a Abs (Tele (Dom a))
    tel) = Int -> Dom a -> Dom a
    forall a. Subst a => Int -> a -> a
    raise (Abs (Tele (Dom a)) -> Int
    forall a. Sized a => a -> Int
    size Abs (Tele (Dom a))
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Dom a
    a Dom a -> [Dom a] -> [Dom a]
    forall a. a -> [a] -> [a]
    : Tele (Dom a) -> [Dom a]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Abs (Tele (Dom a)) -> Tele (Dom a)
    forall a. Subst a => Abs a -> a
    absBody Abs (Tele (Dom a))
    tel)

    {-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}

    -- | Turn a context into a flat telescope: all entries live in the whole context.
    -- @
    --    (Γ : Context) -> [Type Γ]
    -- @
    flattenContext :: Context -> [ContextEntry]
    flattenContext :: Context -> Context
    flattenContext = Int -> Context -> Context -> Context
    forall {a}. Subst a => Int -> [a] -> [a] -> [a]
    loop Int
    1 []
      where
        loop :: Int -> [a] -> [a] -> [a]
    loop Int
    n [a]
    tel []       = [a]
    tel
        loop Int
    n [a]
    tel (a
    ce:[a]
    ctx) = Int -> [a] -> [a] -> [a]
    loop (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Int -> a -> a
    forall a. Subst a => Int -> a -> a
    raise Int
    n a
    ce a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    tel) [a]
    ctx

    -- | Order a flattened telescope in the correct dependeny order: Γ ->
    --   Permutation (Γ -> Γ~)
    --
    --   Since @reorderTel tel@ uses free variable analysis of type in @tel@,
    --   the telescope should be 'normalise'd.
    reorderTel :: [Dom Type] -> Maybe Permutation
    reorderTel :: [Dom Type] -> Maybe Permutation
    reorderTel [Dom Type]
    tel = ((Int, Dom Type) -> (Int, Dom Type) -> Bool)
    -> [(Int, Dom Type)] -> Maybe Permutation
    forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
    topoSort (Int, Dom Type) -> (Int, Dom Type) -> Bool
    forall {a} {b} {a} {t} {t}.
    Free a =>
    (Int, b) -> (a, Dom' t (Type'' t a)) -> Bool
    comesBefore [(Int, Dom Type)]
    tel'
      where
        tel' :: [(Int, Dom Type)]
    tel' = [Int] -> [Dom Type] -> [(Int, Dom Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Dom Type] -> Int
    forall a. Sized a => a -> Int
    size [Dom Type]
    tel) [Dom Type]
    tel
        (Int
    i, b
    _) comesBefore :: (Int, b) -> (a, Dom' t (Type'' t a)) -> Bool
    `comesBefore` (a
    _, Dom' t (Type'' t a)
    a) = Int
    i Int -> a -> Bool
    forall a. Free a => Int -> a -> Bool
    `freeIn` Type'' t a -> a
    forall t a. Type'' t a -> a
    unEl (Dom' t (Type'' t a) -> Type'' t a
    forall t e. Dom' t e -> e
    unDom Dom' t (Type'' t a)
    a) -- a tiny bit unsafe

    reorderTel_ :: [Dom Type] -> Permutation
    reorderTel_ :: [Dom Type] -> Permutation
    reorderTel_ [Dom Type]
    tel = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Dom Type] -> Maybe Permutation
    reorderTel [Dom Type]
    tel)

    -- | Unflatten: turns a flattened telescope into a proper telescope. Must be
    --   properly ordered.
    unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
    unflattenTel :: [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel [ArgName]
    xs [Dom Type]
    tel = Int -> [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel' ([Dom Type] -> Int
    forall a. Sized a => a -> Int
    size [Dom Type]
    tel) [ArgName]
    xs [Dom Type]
    tel

    -- | A variant of 'unflattenTel' which takes the size of the last
    -- argument as an argument.
    unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Telescope
    unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel' !Int
    n [ArgName]
    xs [Dom Type]
    tel = case ([ArgName]
    xs, [Dom Type]
    tel) of
      ([],     [])      -> Tele (Dom Type)
    forall a. Tele a
    EmptyTel
      (ArgName
    x : [ArgName]
    xs, Dom Type
    a : [Dom Type]
    tel) -> Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a' (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Tele (Dom Type)
    tel')
        where
        tel' :: Tele (Dom Type)
    tel' = Int -> [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel' (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [ArgName]
    xs [Dom Type]
    tel
        a' :: Dom Type
    a'   = Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Dom Type))
    rho Dom Type
    a
        rho :: Substitution' Term
    rho  = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $
               Int -> Term -> [Term]
    forall a. Int -> a -> [a]
    replicate Int
    n ((CallStack -> Term) -> Term
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Term
    impossibleTerm)
      ([],    Dom Type
    _ : [Dom Type]
    _) -> Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      (ArgName
    _ : [ArgName]
    _, [])    -> Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Rename the variables in the telescope to the given names
    --   Precondition: @size xs == size tel@.
    renameTel :: [Maybe ArgName] -> Telescope -> Telescope
    renameTel :: [Maybe ArgName] -> Tele (Dom Type) -> Tele (Dom Type)
    renameTel []           Tele (Dom Type)
    EmptyTel           = Tele (Dom Type)
    forall a. Tele a
    EmptyTel
    renameTel (Maybe ArgName
    Nothing:[Maybe ArgName]
    xs) (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel') = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ [Maybe ArgName] -> Tele (Dom Type) -> Tele (Dom Type)
    renameTel [Maybe ArgName]
    xs (Tele (Dom Type) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Abs (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (Tele (Dom Type))
    tel'
    renameTel (Just ArgName
    x :[Maybe ArgName]
    xs) (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel') = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ [Maybe ArgName] -> Tele (Dom Type) -> Tele (Dom Type)
    renameTel [Maybe ArgName]
    xs (Tele (Dom Type) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Abs (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Abs (Tele (Dom Type))
    tel' { absName = x })
    renameTel []           (ExtendTel Dom Type
    _ Abs (Tele (Dom Type))
    _   ) = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    renameTel (Maybe ArgName
    _      :[Maybe ArgName]
    _ ) Tele (Dom Type)
    EmptyTel           = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Get the suggested names from a telescope
    teleNames :: Telescope -> [ArgName]
    teleNames :: Tele (Dom Type) -> [ArgName]
    teleNames = (Dom (ArgName, Type) -> ArgName)
    -> [Dom (ArgName, Type)] -> [ArgName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((ArgName, Type) -> ArgName
    forall a b. (a, b) -> a
    fst ((ArgName, Type) -> ArgName)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom (ArgName, Type)] -> [ArgName])
    -> (Tele (Dom Type) -> [Dom (ArgName, Type)])
    -> Tele (Dom Type)
    -> [ArgName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList

    teleArgNames :: Telescope -> [Arg ArgName]
    teleArgNames :: Tele (Dom Type) -> [Arg ArgName]
    teleArgNames = Tele (Dom Type) -> [Arg ArgName]
    forall a. TelToArgs a => a -> [Arg ArgName]
    telToArgs

    teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
    teleArgs :: forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs = (Dom' Term a -> Arg a) -> [Dom' Term a] -> [Arg a]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term a -> Arg a
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term a] -> [Arg a])
    -> (Tele (Dom t) -> [Dom' Term a]) -> Tele (Dom t) -> [Arg a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom t) -> [Dom' Term a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
    teleDoms

    teleDoms :: (DeBruijn a) => Tele (Dom t) -> [Dom a]
    teleDoms :: forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
    teleDoms Tele (Dom t)
    tel = (Int -> Dom (ArgName, t) -> Dom a)
    -> [Int] -> [Dom (ArgName, t)] -> [Dom a]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Int
    i Dom (ArgName, t)
    dom -> Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar Int
    i a -> Dom (ArgName, t) -> Dom a
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom (ArgName, t)
    dom) (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, t)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, t)]
    l) [Dom (ArgName, t)]
    l
      where l :: [Dom (ArgName, t)]
    l = Tele (Dom t) -> [Dom (ArgName, t)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom t)
    tel

    -- UNUSED
    -- withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
    -- xs `withNamedArgsFromTel` tel =
    --   [ Arg info (Named (Just $ Ranged empty $ argNameToString name) x)
    --   | (x, Dom {domInfo = info, unDom = (name,_)}) <- zip xs l ]
    --   where l = telToList tel

    teleNamedArgs :: (DeBruijn a) => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs :: forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs = (Dom' Term a -> NamedArg a) -> [Dom' Term a] -> [NamedArg a]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term a -> NamedArg a
    forall t a. Dom' t a -> NamedArg a
    namedArgFromDom ([Dom' Term a] -> [NamedArg a])
    -> (Tele (Dom t) -> [Dom' Term a]) -> Tele (Dom t) -> [NamedArg a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom t) -> [Dom' Term a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
    teleDoms

    {-# INLINABLE tele2NamedArgs #-}
    -- | A variant of `teleNamedArgs` which takes the argument names (and the argument info)
    --   from the first telescope and the variable names from the second telescope.
    --
    --   Precondition: the two telescopes have the same length.
    tele2NamedArgs :: (DeBruijn a) => Telescope -> Telescope -> [NamedArg a]
    tele2NamedArgs :: forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Tele (Dom Type) -> [NamedArg a]
    tele2NamedArgs Tele (Dom Type)
    tel0 Tele (Dom Type)
    tel =
      [ ArgInfo -> Named_ a -> NamedArg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Maybe NamedName -> a -> Named_ a
    forall name a. Maybe name -> a -> Named name a
    Named (NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged ArgName -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Ranged ArgName
    forall a. a -> Ranged a
    unranged (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
    forall a b. (a -> b) -> a -> b
    $ ArgName -> ArgName
    argNameToString ArgName
    argName) (ArgName -> Int -> a
    forall a. DeBruijn a => ArgName -> Int -> a
    deBruijnNamedVar ArgName
    varName Int
    i))
      | (Int
    i, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = (ArgName
    argName,Type
    _)}, Dom{unDom :: forall t e. Dom' t e -> e
    unDom = (ArgName
    varName,Type
    _)}) <- [Int]
    -> [Dom (ArgName, Type)]
    -> [Dom (ArgName, Type)]
    -> [(Int, Dom (ArgName, Type), Dom (ArgName, Type))]
    forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
    zip3 (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    l) [Dom (ArgName, Type)]
    l0 [Dom (ArgName, Type)]
    l ]
      where
      l :: [Dom (ArgName, Type)]
    l  = Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel
      l0 :: [Dom (ArgName, Type)]
    l0 = Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel0

    -- | Split the telescope at the specified position.
    splitTelescopeAt :: Int -> Telescope -> (Telescope,Telescope)
    splitTelescopeAt :: Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt Int
    n Tele (Dom Type)
    tel
      | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0    = (Tele (Dom Type)
    forall a. Tele a
    EmptyTel, Tele (Dom Type)
    tel)
      | Bool
    otherwise = Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt' Int
    n Tele (Dom Type)
    tel
        where
          splitTelescopeAt' :: Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt' Int
    _ Tele (Dom Type)
    EmptyTel          = (Tele (Dom Type)
    forall a. Tele a
    EmptyTel,Tele (Dom Type)
    forall a. Tele a
    EmptyTel)
          splitTelescopeAt' Int
    1 (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel) = (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs (Tele (Dom Type))
    tel Abs (Tele (Dom Type)) -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Tele (Dom Type)
    forall a. Tele a
    EmptyTel), Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. Subst a => Abs a -> a
    absBody Abs (Tele (Dom Type))
    tel)
          splitTelescopeAt' Int
    m (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel) = (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs (Tele (Dom Type))
    tel Abs (Tele (Dom Type)) -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Tele (Dom Type)
    tel'), Tele (Dom Type)
    tel'')
            where
              (Tele (Dom Type)
    tel', Tele (Dom Type)
    tel'') = Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type)))
    -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. Subst a => Abs a -> a
    absBody Abs (Tele (Dom Type))
    tel

    -- | Permute telescope: permutes or drops the types in the telescope according
    --   to the given permutation. Assumes that the permutation preserves the
    --   dependencies in the telescope.
    --
    --   For example (Andreas, 2016-12-18, issue #2344):
    --   @
    --     tel                     = (A : Set) (X : _18 A) (i : Fin (_m_23 A X))
    --     tel (de Bruijn)         = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0)
    --     flattenTel tel          = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0) |- [ Set, _18 @2, Fin (_m_23 @2 @1) ]
    --     perm                    = 0,1,2 -> 0,1  (picks the first two)
    --     renaming _ perm         = [var 0, var 1, error]  -- THE WRONG RENAMING!
    --     renaming _ (flipP perm) = [error, var 1, var 0]  -- The correct renaming!
    --     apply to flattened tel  = ... |- [ Set, _18 @1, Fin (_m_23 @1 @0) ]
    --     permute perm it         = ... |- [ Set, _18 @1 ]
    --     unflatten (de Bruijn)   = 1:Set, 0: _18 @0
    --     unflatten               = (A : Set) (X : _18 A)
    --  @
    permuteTel :: Permutation -> Telescope -> Telescope
    permuteTel :: Permutation -> Tele (Dom Type) -> Tele (Dom Type)
    permuteTel Permutation
    perm Tele (Dom Type)
    tel =
      let names :: [ArgName]
    names = Permutation -> [ArgName] -> [ArgName]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm ([ArgName] -> [ArgName]) -> [ArgName] -> [ArgName]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [ArgName]
    teleNames Tele (Dom Type)
    tel
          types :: [Dom Type]
    types = Permutation -> [Dom Type] -> [Dom Type]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Permutation -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    flipP Permutation
    perm) ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
      in  [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel [ArgName]
    names [Dom Type]
    types

    -- | Like 'permuteTel', but start with a context.
    --
    permuteContext :: Permutation -> Context -> Telescope
    permuteContext :: Permutation -> Context -> Tele (Dom Type)
    permuteContext Permutation
    perm Context
    ctx = Permutation -> Tele (Dom Type) -> Tele (Dom Type)
    permuteTel Permutation
    perm (Tele (Dom Type) -> Tele (Dom Type))
    -> Tele (Dom Type) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Context -> Tele (Dom Type)
    contextToTel Context
    ctx

    -- | Recursively computes dependencies of a set of variables in a given
    --   telescope. Any dependencies outside of the telescope are ignored.
    varDependencies :: Telescope -> IntSet -> IntSet
    varDependencies :: Tele (Dom Type) -> IntSet -> IntSet
    varDependencies Tele (Dom Type)
    tel = IntSet -> IntSet
    addLocks (IntSet -> IntSet) -> (IntSet -> IntSet) -> IntSet -> IntSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntSet -> IntSet -> IntSet
    allDependencies IntSet
    IntSet.empty
      where
        addLocks :: IntSet -> IntSet
    addLocks IntSet
    s | IntSet -> Bool
    IntSet.null IntSet
    s = IntSet
    s
                   | Bool
    otherwise = IntSet -> IntSet -> IntSet
    IntSet.union IntSet
    s (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ [Int] -> IntSet
    IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (Int -> Bool) -> [Int] -> [Int]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    m) [Int]
    locks
          where
            locks :: [Int]
    locks = [Maybe Int] -> [Int]
    forall a. [Maybe a] -> [a]
    catMaybes [ Term -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) | (Arg Term
    a :: Arg Term) <- Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel, IsLock{} <- Lock -> [Lock]
    forall a. a -> [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Arg Term -> Lock
    forall a. LensLock a => a -> Lock
    getLock Arg Term
    a)]
            m :: Int
    m = IntSet -> Int
    IntSet.findMin IntSet
    s
        n :: Int
    n  = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
        ts :: [Dom Type]
    ts = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel

        directDependencies :: Int -> IntSet
        directDependencies :: Int -> IntSet
    directDependencies Int
    i = Dom Type -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars (Dom Type -> IntSet) -> Dom Type -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> [Dom Type] -> Int -> Dom Type
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Dom Type]
    ts (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    i)

        allDependencies :: IntSet -> IntSet -> IntSet
        allDependencies :: IntSet -> IntSet -> IntSet
    allDependencies =
          (Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
    forall b. (Int -> b -> b) -> b -> IntSet -> b
    IntSet.foldr ((Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet)
    -> (Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ \Int
    j IntSet
    soFar ->
            if Int
    j Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    n Bool -> Bool -> Bool
    || Int
    j Int -> IntSet -> Bool
    `IntSet.member` IntSet
    soFar
            then IntSet
    soFar
            else Int -> IntSet -> IntSet
    IntSet.insert Int
    j (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ IntSet -> IntSet -> IntSet
    allDependencies IntSet
    soFar (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int -> IntSet
    directDependencies Int
    j

    -- | Computes the set of variables in a telescope whose type depend on
    --   one of the variables in the given set (including recursive
    --   dependencies). Any dependencies outside of the telescope are
    --   ignored.
    varDependents :: Telescope -> IntSet -> IntSet
    varDependents :: Tele (Dom Type) -> IntSet -> IntSet
    varDependents Tele (Dom Type)
    tel = IntSet -> IntSet
    allDependents
      where
        n :: Int
    n  = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
        ts :: [Dom Type]
    ts = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel

        directDependents :: IntSet -> IntSet
        directDependents :: IntSet -> IntSet
    directDependents IntSet
    is = [Int] -> IntSet
    IntSet.fromList
          [ Int
    j | Int
    j <- Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n
              , let tj :: Dom Type
    tj = Dom Type -> [Dom Type] -> Int -> Dom Type
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Dom Type]
    ts (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    j)
              , Any -> Bool
    getAny (Any -> Bool) -> Any -> Bool
    forall a b. (a -> b) -> a -> b
    $ SingleVar Any -> IgnoreSorts -> Dom Type -> Any
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree (Bool -> Any
    Any (Bool -> Any) -> (Int -> Bool) -> SingleVar Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> IntSet -> Bool
    `IntSet.member` IntSet
    is)) IgnoreSorts
    IgnoreNot Dom Type
    tj
              ]

        allDependents :: IntSet -> IntSet
        allDependents :: IntSet -> IntSet
    allDependents IntSet
    is
         | IntSet -> Bool
    forall a. Null a => a -> Bool
    null IntSet
    new  = IntSet
    forall a. Null a => a
    empty
         | Bool
    otherwise = IntSet
    new IntSet -> IntSet -> IntSet
    `IntSet.union` IntSet -> IntSet
    allDependents IntSet
    new
          where new :: IntSet
    new = IntSet -> IntSet
    directDependents IntSet
    is

    -- | A telescope split in two.
    data SplitTel = SplitTel
      { SplitTel -> Tele (Dom Type)
    firstPart  :: Telescope
      , SplitTel -> Tele (Dom Type)
    secondPart :: Telescope
      , SplitTel -> Permutation
    splitPerm  :: Permutation
        -- ^ The permutation takes us from the original telescope to
        --   @firstPart ++ secondPart@.
      }

    -- | Split a telescope into the part that defines the given variables and the
    --   part that doesn't.
    --
    --   See 'Agda.TypeChecking.Tests.prop_splitTelescope'.
    splitTelescope
      :: VarSet     -- ^ A set of de Bruijn indices.
      -> Telescope  -- ^ Original telescope.
      -> SplitTel   -- ^ @firstPart@ mentions the given variables, @secondPart@ not.
    splitTelescope :: IntSet -> Tele (Dom Type) -> SplitTel
    splitTelescope IntSet
    fv Tele (Dom Type)
    tel = Tele (Dom Type) -> Tele (Dom Type) -> Permutation -> SplitTel
    SplitTel Tele (Dom Type)
    tel1 Tele (Dom Type)
    tel2 Permutation
    perm
      where
        names :: [ArgName]
    names = Tele (Dom Type) -> [ArgName]
    teleNames Tele (Dom Type)
    tel
        ts0 :: [Dom Type]
    ts0   = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
        n :: Int
    n     = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel

        is :: IntSet
    is    = Tele (Dom Type) -> IntSet -> IntSet
    varDependencies Tele (Dom Type)
    tel IntSet
    fv
        isC :: IntSet
    isC   = [Int] -> IntSet
    IntSet.fromList [Int
    0..(Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)] IntSet -> IntSet -> IntSet
    `IntSet.difference` IntSet
    is

        perm :: Permutation
    perm  = Int -> [Int] -> Permutation
    Perm Int
    n ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ IntSet -> [Int]
    VarSet.toDescList IntSet
    is [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ IntSet -> [Int]
    VarSet.toDescList IntSet
    isC

        ts1 :: [Dom Type]
    ts1   = Impossible -> Permutation -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    perm) (Permutation -> [Dom Type] -> [Dom Type]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [Dom Type]
    ts0)

        tel' :: Tele (Dom Type)
    tel'  = [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel (Permutation -> [ArgName] -> [ArgName]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [ArgName]
    names) [Dom Type]
    ts1

        m :: Int
    m     = IntSet -> Int
    forall a. Sized a => a -> Int
    size IntSet
    is
        (Tele (Dom Type)
    tel1, Tele (Dom Type)
    tel2) = [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList ([Dom (ArgName, Type)] -> Tele (Dom Type))
    -> ([Dom (ArgName, Type)] -> Tele (Dom Type))
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> (Tele (Dom Type), Tele (Dom Type))
    forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    -*- [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList (([Dom (ArgName, Type)], [Dom (ArgName, Type)])
     -> (Tele (Dom Type), Tele (Dom Type)))
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> (Tele (Dom Type), Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Int
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    m ([Dom (ArgName, Type)]
     -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel'

    -- | As splitTelescope, but fails if any additional variables or reordering
    --   would be needed to make the first part well-typed.
    splitTelescopeExact
      :: [Int]          -- ^ A list of de Bruijn indices
      -> Telescope      -- ^ The telescope to split
      -> Maybe SplitTel -- ^ @firstPart@ mentions the given variables in the given order,
                        --   @secondPart@ contains all other variables
    splitTelescopeExact :: [Int] -> Tele (Dom Type) -> Maybe SplitTel
    splitTelescopeExact [Int]
    is Tele (Dom Type)
    tel = Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    ok Maybe () -> SplitTel -> Maybe SplitTel
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Tele (Dom Type) -> Tele (Dom Type) -> Permutation -> SplitTel
    SplitTel Tele (Dom Type)
    tel1 Tele (Dom Type)
    tel2 Permutation
    perm
      where
        names :: [ArgName]
    names = Tele (Dom Type) -> [ArgName]
    teleNames Tele (Dom Type)
    tel
        ts0 :: [Dom Type]
    ts0   = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
        n :: Int
    n     = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel

        checkDependencies :: IntSet -> [Int] -> Bool
        checkDependencies :: IntSet -> [Int] -> Bool
    checkDependencies IntSet
    soFar []     = Bool
    True
        checkDependencies IntSet
    soFar (Int
    j:[Int]
    js) = Bool
    ok Bool -> Bool -> Bool
    && IntSet -> [Int] -> Bool
    checkDependencies (Int -> IntSet -> IntSet
    IntSet.insert Int
    j IntSet
    soFar) [Int]
    js
          where
            t :: Dom Type
    t   = Dom Type -> [Dom Type] -> Int -> Dom Type
    forall a. a -> [a] -> Int -> a
    indexWithDefault Dom Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Dom Type]
    ts0 (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    j)  -- ts0[n-1-j]
            -- Skip the construction of intermediate @IntSet@s in the check @ok@.
            -- ok  = (allFreeVars t `IntSet.intersection` IntSet.fromAscList [ 0 .. n-1 ])
            --       `IntSet.isSubsetOf` soFar
            good :: Int -> All
    good Int
    i = Bool -> All
    All (Bool -> All) -> Bool -> All
    forall a b. (a -> b) -> a -> b
    $ (Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n) Bool -> Bool -> Bool
    `implies` (Int
    i Int -> IntSet -> Bool
    `IntSet.member` IntSet
    soFar) where implies :: Bool -> Bool -> Bool
    implies = Bool -> Bool -> Bool
    forall a. Ord a => a -> a -> Bool
    (<=)
            ok :: Bool
    ok = All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Int -> All) -> IgnoreSorts -> Dom Type -> All
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree Int -> All
    good IgnoreSorts
    IgnoreNot Dom Type
    t

        ok :: Bool
    ok    = (Int -> Bool) -> [Int] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n) [Int]
    is Bool -> Bool -> Bool
    && IntSet -> [Int] -> Bool
    checkDependencies IntSet
    IntSet.empty [Int]
    is

        isC :: [Int]
    isC   = Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n [Int] -> [Int] -> [Int]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ [Int]
    is

        perm :: Permutation
    perm  = Int -> [Int] -> Permutation
    Perm Int
    n ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Int]
    is [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Int]
    isC

        ts1 :: [Dom Type]
    ts1   = Impossible -> Permutation -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    perm) (Permutation -> [Dom Type] -> [Dom Type]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [Dom Type]
    ts0)

        tel' :: Tele (Dom Type)
    tel'  = [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel (Permutation -> [ArgName] -> [ArgName]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [ArgName]
    names) [Dom Type]
    ts1

        m :: Int
    m     = [Int] -> Int
    forall a. Sized a => a -> Int
    size [Int]
    is
        (Tele (Dom Type)
    tel1, Tele (Dom Type)
    tel2) = [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList ([Dom (ArgName, Type)] -> Tele (Dom Type))
    -> ([Dom (ArgName, Type)] -> Tele (Dom Type))
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> (Tele (Dom Type), Tele (Dom Type))
    forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    -*- [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList (([Dom (ArgName, Type)], [Dom (ArgName, Type)])
     -> (Tele (Dom Type), Tele (Dom Type)))
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> (Tele (Dom Type), Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Int
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    m ([Dom (ArgName, Type)]
     -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel'

    -- | Try to instantiate one variable in the telescope (given by its de Bruijn
    --   level) with the given value, returning the new telescope and a
    --   substitution to the old one. Returns Nothing if the given value depends
    --   (directly or indirectly) on the variable.
    instantiateTelescope
      :: Telescope -- ^ ⊢ Γ
      -> Int       -- ^ Γ ⊢ var k : A   de Bruijn _level_
      -> DeBruijnPattern -- ^ Γ ⊢ u : A
      -> Maybe (Telescope,           -- ⊢ Γ'
                PatternSubstitution, -- Γ' ⊢ σ : Γ
                Permutation)         -- Γ  ⊢ flipP ρ : Γ'
    instantiateTelescope :: Tele (Dom Type)
    -> Int
    -> Pattern' DBPatVar
    -> Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
    instantiateTelescope Tele (Dom Type)
    tel Int
    k Pattern' DBPatVar
    p = Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    ok Maybe ()
    -> (Tele (Dom Type), PatternSubstitution, Permutation)
    -> Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> (Tele (Dom Type)
    tel', PatternSubstitution
    sigma, Permutation
    rho)
      where
        names :: [ArgName]
    names = Tele (Dom Type) -> [ArgName]
    teleNames Tele (Dom Type)
    tel
        ts0 :: [Dom Type]
    ts0   = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
        n :: Int
    n     = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
        j :: Int
    j     = Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    k
        u :: Term
    u     = Pattern' DBPatVar -> Term
    patternToTerm Pattern' DBPatVar
    p

        -- Jesper, 2019-12-31: Previous implementation that does some
        -- unneccessary reordering but is otherwise correct (keep!)
        -- -- is0 is the part of Γ that is needed to type u
        -- is0   = varDependencies tel $ allFreeVars u
        -- -- is1 is the rest of Γ (minus the variable we are instantiating)
        -- is1   = IntSet.delete j $
        --           IntSet.fromAscList [ 0 .. n-1 ] `IntSet.difference` is0
        -- -- we work on de Bruijn indices, so later parts come first
        -- is    = IntSet.toAscList is1 ++ IntSet.toAscList is0

        -- -- if u depends on var j, we cannot instantiate
        -- ok    = not $ j `IntSet.member` is0

        -- is0 is the part of Γ that is needed to type u
        is0 :: IntSet
    is0   = Tele (Dom Type) -> IntSet -> IntSet
    varDependencies Tele (Dom Type)
    tel (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Term -> IntSet
    forall t. Free t => t -> IntSet
    allFreeVars Term
    u
        -- is1 is the part of Γ that depends on variable j
        is1 :: IntSet
    is1   = Tele (Dom Type) -> IntSet -> IntSet
    varDependents Tele (Dom Type)
    tel (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ Int -> IntSet
    forall el coll. Singleton el coll => el -> coll
    singleton Int
    j
        -- lasti is the last (rightmost) variable of is0
        lasti :: Int
    lasti = if IntSet -> Bool
    forall a. Null a => a -> Bool
    null IntSet
    is0 then Int
    n else IntSet -> Int
    IntSet.findMin IntSet
    is0
        -- we move each variable in is1 to the right until it comes after
        -- all variables in is0 (i.e. after lasti)
        ([Int]
    as,[Int]
    bs) = (Int -> Bool) -> [Int] -> ([Int], [Int])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (Int -> IntSet -> Bool
    `IntSet.member` IntSet
    is1) [ Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1 , Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    2 .. Int
    lasti ]
        is :: [Int]
    is    = [Int] -> [Int]
    forall a. [a] -> [a]
    reverse ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int] -> [Int]
    forall a. Eq a => a -> [a] -> [a]
    List.delete Int
    j ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [Int]
    bs [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Int]
    as [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    lasti

        -- if u depends on var j, we cannot instantiate
        ok :: Bool
    ok    = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Int
    j Int -> IntSet -> Bool
    `IntSet.member` IntSet
    is0

        perm :: Permutation
    perm  = Int -> [Int] -> Permutation
    Perm Int
    n ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [Int]
    is    -- works on de Bruijn indices
        rho :: Permutation
    rho   = Permutation -> Permutation
    reverseP Permutation
    perm  -- works on de Bruijn levels

        p1 :: Pattern' DBPatVar
    p1    = Impossible -> Permutation -> Pattern' DBPatVar -> Pattern' DBPatVar
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible Permutation
    perm Pattern' DBPatVar
    p -- Γ' ⊢ p1 : A'
        us :: [Pattern' DBPatVar]
    us    = (Int -> Pattern' DBPatVar) -> [Int] -> [Pattern' DBPatVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int
    i -> Pattern' DBPatVar
    -> (Int -> Pattern' DBPatVar) -> Maybe Int -> Pattern' DBPatVar
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Pattern' DBPatVar
    p1 Int -> Pattern' DBPatVar
    forall a. DeBruijn a => Int -> a
    deBruijnVar (Int -> [Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex Int
    i [Int]
    is)) [ Int
    0 .. Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1 ]
        sigma :: PatternSubstitution
    sigma = [Pattern' DBPatVar]
    us [Pattern' DBPatVar] -> PatternSubstitution -> PatternSubstitution
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Int -> PatternSubstitution
    forall a. Int -> Substitution' a
    raiseS (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)

        ts1 :: [Dom Type]
    ts1   = Permutation -> [Dom Type] -> [Dom Type]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    rho ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ PatternSubstitution -> [Dom Type] -> [Dom Type]
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    sigma [Dom Type]
    ts0
        tel' :: Tele (Dom Type)
    tel'  = [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel (Permutation -> [ArgName] -> [ArgName]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    rho [ArgName]
    names) [Dom Type]
    ts1

    -- | Try to eta-expand one variable in the telescope (given by its de Bruijn
    --   level)
    expandTelescopeVar
      :: Telescope  -- Γ = Γ₁(x : D pars)Γ₂
      -> Int        -- k = size Γ₁
      -> Telescope  -- Γ₁ ⊢ Δ
      -> ConHead    -- Γ₁ ⊢ c : Δ → D pars
      -> ( Telescope            -- Γ' = Γ₁ΔΓ₂[x ↦ c Δ]
         , PatternSubstitution) -- Γ' ⊢ ρ : Γ
    expandTelescopeVar :: Tele (Dom Type)
    -> Int
    -> Tele (Dom Type)
    -> ConHead
    -> (Tele (Dom Type), PatternSubstitution)
    expandTelescopeVar Tele (Dom Type)
    gamma Int
    k Tele (Dom Type)
    delta ConHead
    c = (Tele (Dom Type)
    tel', PatternSubstitution
    rho)
      where
        ([Dom (ArgName, Type)]
    ts1,Dom (ArgName, Type)
    xa:[Dom (ArgName, Type)]
    ts2) = ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. a -> Maybe a -> a
    fromMaybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
     -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
    -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a b. (a -> b) -> a -> b
    $
                        Int
    -> [Dom (ArgName, Type)]
    -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt Int
    k ([Dom (ArgName, Type)]
     -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
    -> [Dom (ArgName, Type)]
    -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    gamma
        a :: Dom Type
    a = Int -> Dom Type -> Dom Type
    forall a. Subst a => Int -> a -> a
    raise (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) ((ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom (ArgName, Type)
    xa) -- Γ₁Δ ⊢ D pars

        cpi :: ConPatternInfo
    cpi         = ConPatternInfo
          { conPInfo :: PatternInfo
    conPInfo   = PatternInfo
    defaultPatternInfo
          , conPRecord :: Bool
    conPRecord = Bool
    True
          , conPFallThrough :: Bool
    conPFallThrough
                       = Bool
    False
          , conPType :: Maybe (Arg Type)
    conPType   = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a
          , conPLazy :: Bool
    conPLazy   = Bool
    True
          }
        cargs :: [NamedArg (Pattern' DBPatVar)]
    cargs       = (NamedArg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar))
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Origin
    -> NamedArg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted) ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
    forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    delta
        cdelta :: Pattern' DBPatVar
    cdelta      = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    cpi [NamedArg (Pattern' DBPatVar)]
    cargs                    -- Γ₁Δ ⊢ c Δ : D pars
        rho0 :: PatternSubstitution
    rho0        = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Pattern' DBPatVar
    cdelta (PatternSubstitution -> PatternSubstitution)
    -> PatternSubstitution -> PatternSubstitution
    forall a b. (a -> b) -> a -> b
    $ Int -> PatternSubstitution
    forall a. Int -> Substitution' a
    raiseS (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta)  -- Γ₁Δ ⊢ ρ₀ : Γ₁(x : D pars)
        rho :: PatternSubstitution
    rho         = Int -> PatternSubstitution -> PatternSubstitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS ([Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    ts2) PatternSubstitution
    rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂

        gamma1 :: Tele (Dom Type)
    gamma1      = [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList [Dom (ArgName, Type)]
    ts1
        gamma2' :: Tele (Dom Type)
    gamma2'     = PatternSubstitution -> Tele (Dom Type) -> Tele (Dom Type)
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    rho0 (Tele (Dom Type) -> Tele (Dom Type))
    -> Tele (Dom Type) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> Tele (Dom Type)
    telFromList [Dom (ArgName, Type)]
    ts2

        tel' :: Tele (Dom Type)
    tel'        = Tele (Dom Type)
    gamma1 Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    `abstract` (Tele (Dom Type)
    delta Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    `abstract` Tele (Dom Type)
    gamma2')

    {-# INLINE telView #-}
    -- | Gather leading Πs of a type in a telescope.
    telView :: (MonadReduce m, MonadAddContext m) => Type -> m TelView
    telView :: forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m TelView
    telView = Int -> Type -> m TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m TelView
    telViewUpTo (-Int
    1)

    {-# INLINE telViewUpTo #-}
    -- | @telViewUpTo n t@ takes off the first @n@ function types of @t@.
    -- Takes off all if @n < 0@.
    telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
    telViewUpTo :: forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m TelView
    telViewUpTo Int
    n Type
    t = Int -> (Dom Type -> Bool) -> Type -> m TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m TelView
    telViewUpTo' Int
    n (Bool -> Dom Type -> Bool
    forall a b. a -> b -> a
    const Bool
    True) Type
    t

    {-# SPECIALIZE telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView #-}
    -- | @telViewUpTo' n p t@ takes off $t$
    --   the first @n@ (or arbitrary many if @n < 0@) function domains
    --   as long as they satify @p@.
    telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
    telViewUpTo' :: forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m TelView
    telViewUpTo' Int
    0 Dom Type -> Bool
    p Type
    t = TelView -> m TelView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TelView -> m TelView) -> TelView -> m TelView
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t
    telViewUpTo' Int
    n Dom Type -> Bool
    p Type
    t = do
      t <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
      case unEl t of
        Pi Dom Type
    a Abs Type
    b | Dom Type -> Bool
    p Dom Type
    a ->
              -- Force the name to avoid retaining the rest of b.
          let !bn :: ArgName
    bn = Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b in
          Dom Type -> ArgName -> TelView -> TelView
    forall a. Dom a -> ArgName -> TelV a -> TelV a
    absV Dom Type
    a ArgName
    bn (TelView -> TelView) -> m TelView -> m TelView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            Dom Type -> Abs Type -> (Type -> m TelView) -> m TelView
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom Type
    a Abs Type
    b ((Type -> m TelView) -> m TelView)
    -> (Type -> m TelView) -> m TelView
    forall a b. (a -> b) -> a -> b
    $ \Type
    b -> Int -> (Dom Type -> Bool) -> Type -> m TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m TelView
    telViewUpTo' (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Dom Type -> Bool
    p Type
    b
        Term
    _ -> TelView -> m TelView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TelView -> m TelView) -> TelView -> m TelView
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t

    {-# INLINE telViewPath #-}
    telViewPath :: PureTCM m => Type -> m TelView
    telViewPath :: forall (m :: * -> *). PureTCM m => Type -> m TelView
    telViewPath = Int -> Type -> m TelView
    forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
    telViewUpToPath (-Int
    1)

    {-# SPECIALIZE telViewUpToPath :: Int -> Type -> TCM TelView #-}
    -- | @telViewUpToPath n t@ takes off @t@
    --   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
    --
    -- @telViewUpToPath n t = fst <$> telViewUpToPathBoundary' n t@
    telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
    telViewUpToPath :: forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
    telViewUpToPath Int
    n Type
    t = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then Type -> m TelView
    forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
    done Type
    t else do
      Type -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi Type
    t m (Either (Dom Type, Abs Type) Type)
    -> (Either (Dom Type, Abs Type) Type -> m TelView) -> m TelView
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left  (Dom Type
    a, Abs Type
    b)          -> Dom Type -> Abs Type -> m TelView
    recurse Dom Type
    a Abs Type
    b
        Right (El Sort' Term
    _ (Pi Dom Type
    a Abs Type
    b)) -> Dom Type -> Abs Type -> m TelView
    recurse Dom Type
    a Abs Type
    b
        Right Type
    t               -> Type -> m TelView
    forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
    done Type
    t
      where
        done :: a -> m (TelV a)
    done a
    t      = TelV a -> m (TelV a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TelV a -> m (TelV a)) -> TelV a -> m (TelV a)
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom a)
    forall a. Tele a
    EmptyTel a
    t
        recurse :: Dom Type -> Abs Type -> m TelView
    recurse Dom Type
    a Abs Type
    b = Dom Type -> ArgName -> TelView -> TelView
    forall a. Dom a -> ArgName -> TelV a -> TelV a
    absV Dom Type
    a (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b) (TelView -> TelView) -> m TelView -> m TelView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Type -> m TelView
    forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
    telViewUpToPath (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)

    -- | Boundary conditions @[[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]@.
    -- For instance, if @p : Path A a b@, then @p i@ has boundary condition @(i,(a,b))@.
    -- We call @i@ the /dimension/ and @(x,y)@ its /boundary/.
    newtype Boundary' x a = Boundary { forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary :: [(x,(a,a))] }
      deriving (Int -> Boundary' x a -> ArgName -> ArgName
    [Boundary' x a] -> ArgName -> ArgName
    Boundary' x a -> ArgName
    (Int -> Boundary' x a -> ArgName -> ArgName)
    -> (Boundary' x a -> ArgName)
    -> ([Boundary' x a] -> ArgName -> ArgName)
    -> Show (Boundary' x a)
    forall a.
    (Int -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    forall x a.
    (Show x, Show a) =>
    Int -> Boundary' x a -> ArgName -> ArgName
    forall x a.
    (Show x, Show a) =>
    [Boundary' x a] -> ArgName -> ArgName
    forall x a. (Show x, Show a) => Boundary' x a -> ArgName
    $cshowsPrec :: forall x a.
    (Show x, Show a) =>
    Int -> Boundary' x a -> ArgName -> ArgName
    showsPrec :: Int -> Boundary' x a -> ArgName -> ArgName
    $cshow :: forall x a. (Show x, Show a) => Boundary' x a -> ArgName
    show :: Boundary' x a -> ArgName
    $cshowList :: forall x a.
    (Show x, Show a) =>
    [Boundary' x a] -> ArgName -> ArgName
    showList :: [Boundary' x a] -> ArgName -> ArgName
    Show, Boundary' x a
    Boundary' x a -> Bool
    Boundary' x a -> (Boundary' x a -> Bool) -> Null (Boundary' x a)
    forall a. a -> (a -> Bool) -> Null a
    forall x a. Boundary' x a
    forall x a. Boundary' x a -> Bool
    $cempty :: forall x a. Boundary' x a
    empty :: Boundary' x a
    $cnull :: forall x a. Boundary' x a -> Bool
    null :: Boundary' x a -> Bool
    Null)

    -- | Usually, the dimensions of a boundary condition are interval /variables/,
    -- represented by a de Bruijn index @Int@.
    type Boundary = Boundary' Int Term

    -- | Substitution formally creates dimensions that are interval /expressions/,
    -- represented by a @Term@.
    -- However, in practice these terms should be of the form @'var' i@.
    type TmBoundary = Boundary' Term Term

    -- | Turn dimension variables @i@ into dimension expressions @'var' i@.
    tmBoundary :: Boundary' Int a -> Boundary' Term a
    tmBoundary :: forall a. Boundary' Int a -> Boundary' Term a
    tmBoundary = [(Term, (a, a))] -> Boundary' Term a
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary ([(Term, (a, a))] -> Boundary' Term a)
    -> (Boundary' Int a -> [(Term, (a, a))])
    -> Boundary' Int a
    -> Boundary' Term a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, (a, a)) -> (Term, (a, a)))
    -> [(Int, (a, a))] -> [(Term, (a, a))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> Term) -> (Int, (a, a)) -> (Term, (a, a))
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Int -> Term
    var) ([(Int, (a, a))] -> [(Term, (a, a))])
    -> (Boundary' Int a -> [(Int, (a, a))])
    -> Boundary' Int a
    -> [(Term, (a, a))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Boundary' Int a -> [(Int, (a, a))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary

    -- | Turn dimension expressions into dimension variables.
    -- Formally this is a partial operation, but should only be called when the precondition is met.
    --
    -- Precondition: the dimension terms in the boundary are all of the form @'var' i@.
    varBoundary :: Boundary' Term a -> Boundary' Int a
    varBoundary :: forall a. Boundary' Term a -> Boundary' Int a
    varBoundary = [(Int, (a, a))] -> Boundary' Int a
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary ([(Int, (a, a))] -> Boundary' Int a)
    -> (Boundary' Term a -> [(Int, (a, a))])
    -> Boundary' Term a
    -> Boundary' Int a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Term, (a, a)) -> (Int, (a, a)))
    -> [(Term, (a, a))] -> [(Int, (a, a))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> Int) -> (Term, (a, a)) -> (Int, (a, a))
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Term -> Int
    unVar) ([(Term, (a, a))] -> [(Int, (a, a))])
    -> (Boundary' Term a -> [(Term, (a, a))])
    -> Boundary' Term a
    -> [(Int, (a, a))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Boundary' Term a -> [(Term, (a, a))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary
      where
        unVar :: Term -> Int
    unVar (Var Int
    i []) = Int
    i
        unVar Term
    _ = Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Substitution into a 'Boundary' a priori creates a 'TmBoundary' which we convert back via 'varBoundary'.
    -- A priori, this is a partial operation.
    instance Subst Boundary where
      type SubstArg Boundary = Term
      applySubst :: Substitution' (SubstArg Boundary) -> Boundary -> Boundary
    applySubst Substitution' (SubstArg Boundary)
    sub = Boundary' Term Term -> Boundary
    forall a. Boundary' Term a -> Boundary' Int a
    varBoundary (Boundary' Term Term -> Boundary)
    -> (Boundary -> Boundary' Term Term) -> Boundary -> Boundary
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg (Boundary' Term Term))
    -> Boundary' Term Term -> Boundary' Term Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Boundary)
    Substitution' (SubstArg (Boundary' Term Term))
    sub (Boundary' Term Term -> Boundary' Term Term)
    -> (Boundary -> Boundary' Term Term)
    -> Boundary
    -> Boundary' Term Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Boundary -> Boundary' Term Term
    forall a. Boundary' Int a -> Boundary' Term a
    tmBoundary

    instance Subst TmBoundary where
      type SubstArg TmBoundary = Term
      applySubst :: Substitution' (SubstArg (Boundary' Term Term))
    -> Boundary' Term Term -> Boundary' Term Term
    applySubst Substitution' (SubstArg (Boundary' Term Term))
    sub = [(Term, (Term, Term))] -> Boundary' Term Term
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary ([(Term, (Term, Term))] -> Boundary' Term Term)
    -> (Boundary' Term Term -> [(Term, (Term, Term))])
    -> Boundary' Term Term
    -> Boundary' Term Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg [(Term, (Term, Term))])
    -> [(Term, (Term, Term))] -> [(Term, (Term, Term))]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [(Term, (Term, Term))])
    Substitution' (SubstArg (Boundary' Term Term))
    sub ([(Term, (Term, Term))] -> [(Term, (Term, Term))])
    -> (Boundary' Term Term -> [(Term, (Term, Term))])
    -> Boundary' Term Term
    -> [(Term, (Term, Term))]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Boundary' Term Term -> [(Term, (Term, Term))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary

    deriving instance (Pretty x, Pretty a) => Pretty (Boundary' x a)

    {-# SPECIALIZE telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView, Boundary) #-}
    -- | Like 'telViewUpToPath' but also returns the 'Boundary' expected by the Path types encountered.
    -- The boundary terms live in the telescope given by the 'TelView'.
    -- Each point of the boundary has the type of the codomain of the Path type it got taken from, see 'fullBoundary'.
    --
    -- @
    --  (TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary' n a
    --  Input:  Δ ⊢ a
    --  Output: Δ.Γ ⊢ b
    --          Δ.Γ ⊢ T is the codomain of the PathP at variable i
    --          Δ.Γ ⊢ i : I
    --          Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
    -- @
    --
    -- Useful to reconstruct IApplyP patterns after teleNamedArgs Γ.
    --
    telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' :: forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' Int
    n Type
    t = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then Type -> m (TelView, Boundary)
    forall {m :: * -> *} {b} {a}.
    (Monad m, Null b) =>
    a -> m (TelV a, b)
    done Type
    t else do
      Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi' Type
    t m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> (Either ((Dom Type, Abs Type), (Term, Term)) Type
        -> m (TelView, Boundary))
    -> m (TelView, Boundary)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left ((Dom Type
    a, Abs Type
    b), (Term, Term)
    xy)     -> (Term, Term) -> (TelView, Boundary) -> (TelView, Boundary)
    forall {a} {a}.
    Subst a =>
    (a, a) -> (TelV a, Boundary' Int a) -> (TelV a, Boundary' Int a)
    addEndPoints (Term, Term)
    xy ((TelView, Boundary) -> (TelView, Boundary))
    -> m (TelView, Boundary) -> m (TelView, Boundary)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> Abs Type -> m (TelView, Boundary)
    recurse Dom Type
    a Abs Type
    b
        Right (El Sort' Term
    _ (Pi Dom Type
    a Abs Type
    b)) -> Dom Type -> Abs Type -> m (TelView, Boundary)
    recurse Dom Type
    a Abs Type
    b
        Right Type
    t               -> Type -> m (TelView, Boundary)
    forall {m :: * -> *} {b} {a}.
    (Monad m, Null b) =>
    a -> m (TelV a, b)
    done Type
    t
      where
        done :: a -> m (TelV a, b)
    done a
    t      = (TelV a, b) -> m (TelV a, b)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom a)
    forall a. Tele a
    EmptyTel a
    t, b
    forall a. Null a => a
    empty)
        recurse :: Dom Type -> Abs Type -> m (TelView, Boundary)
    recurse Dom Type
    a Abs Type
    b = (TelView -> TelView) -> (TelView, Boundary) -> (TelView, Boundary)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (Dom Type -> ArgName -> TelView -> TelView
    forall a. Dom a -> ArgName -> TelV a -> TelV a
    absV Dom Type
    a (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b)) ((TelView, Boundary) -> (TelView, Boundary))
    -> m (TelView, Boundary) -> m (TelView, Boundary)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          Dom Type
    -> Abs Type
    -> (Type -> m (TelView, Boundary))
    -> m (TelView, Boundary)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom Type
    a Abs Type
    b ((Type -> m (TelView, Boundary)) -> m (TelView, Boundary))
    -> (Type -> m (TelView, Boundary)) -> m (TelView, Boundary)
    forall a b. (a -> b) -> a -> b
    $ \Type
    b -> Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Type
    b
        addEndPoints :: (a, a) -> (TelV a, Boundary' Int a) -> (TelV a, Boundary' Int a)
    addEndPoints (a, a)
    xy (telv :: TelV a
    telv@(TelV Tele (Dom a)
    tel a
    _), Boundary [(Int, (a, a))]
    cs) =
          (TelV a
    telv, [(Int, (a, a))] -> Boundary' Int a
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary ([(Int, (a, a))] -> Boundary' Int a)
    -> [(Int, (a, a))] -> Boundary' Int a
    forall a b. (a -> b) -> a -> b
    $ (Tele (Dom a) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom a)
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1, Int -> (a, a) -> (a, a)
    forall a. Subst a => Int -> a -> a
    raise (Tele (Dom a) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom a)
    tel) (a, a)
    xy) (Int, (a, a)) -> [(Int, (a, a))] -> [(Int, (a, a))]
    forall a. a -> [a] -> [a]
    : [(Int, (a, a))]
    cs)

    fullBoundary :: Telescope -> Boundary -> Boundary
    fullBoundary :: Tele (Dom Type) -> Boundary -> Boundary
    fullBoundary Tele (Dom Type)
    tel Boundary
    bs =
          -- tel = Γ
          -- ΔΓ ⊢ b
          -- Δ ⊢ a = PiPath Γ bs b
          -- Δ.Γ ⊢ T is the codomain of the PathP at variable i
          -- Δ.Γ ⊢ i : I
          -- Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
          -- Δ.Γ | PiPath Γ bs A ⊢ teleElims tel bs : b
       let es :: [Elim]
    es = Tele (Dom Type) -> Boundary -> [Elim]
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' Int a -> [Elim' a]
    teleElims Tele (Dom Type)
    tel Boundary
    bs
           l :: Int
    l  = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
       in [(Int, (Term, Term))] -> Boundary
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary ([(Int, (Term, Term))] -> Boundary)
    -> [(Int, (Term, Term))] -> Boundary
    forall a b. (a -> b) -> a -> b
    $ ((Int, (Term, Term)) -> (Int, (Term, Term)))
    -> [(Int, (Term, Term))] -> [(Int, (Term, Term))]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (Int
    i, (Term, Term)
    xy) -> (Int
    i, (Term, Term)
    xy (Term, Term) -> [Elim] -> (Term, Term)
    forall t. Apply t => t -> [Elim] -> t
    `applyE` (Int -> [Elim] -> [Elim]
    forall a. Int -> [a] -> [a]
    drop (Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) [Elim]
    es))) ([(Int, (Term, Term))] -> [(Int, (Term, Term))])
    -> [(Int, (Term, Term))] -> [(Int, (Term, Term))]
    forall a b. (a -> b) -> a -> b
    $ Boundary -> [(Int, (Term, Term))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary Boundary
    bs

    {-# SPECIALIZE telViewUpToPathBoundary :: Int -> Type -> TCM (TelView, Boundary) #-}
    -- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary n a@
    --  Input:  Δ ⊢ a
    --  Output: ΔΓ ⊢ b
    --          ΔΓ ⊢ i : I
    --          ΔΓ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : b
    telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary :: forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary Int
    i Type
    a = do
       (telv@(TelV tel b), bs) <- Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' Int
    i Type
    a
       return (telv, fullBoundary tel bs)

    {-# INLINE telViewPathBoundary #-}
    telViewPathBoundary :: PureTCM m => Type -> m (TelView, Boundary)
    telViewPathBoundary :: forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
    telViewPathBoundary = Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' (-Int
    1)

    -- | @teleElimsB args bs = es@
    --  Input:  Δ.Γ ⊢ args : Γ
    --          Δ.Γ ⊢ T is the codomain of the PathP at variable i
    --          Δ.Γ ⊢ i : I
    --          Δ.Γ ⊢ bs = [ (i=0) -> t_i; (i=1) -> u_i ] : T
    --  Output: Δ.Γ | PiPath Γ bs A ⊢ es : A
    teleElims :: DeBruijn a => Telescope -> Boundary' Int a -> [Elim' a]
    teleElims :: forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' Int a -> [Elim' a]
    teleElims Tele (Dom Type)
    tel (Boundary []) = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply ([Arg a] -> [Elim' a]) -> [Arg a] -> [Elim' a]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel
    teleElims Tele (Dom Type)
    tel (Boundary [(Int, (a, a))]
    boundary) = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg a -> Elim' a
    updateArg ([Arg a] -> [Elim' a]) -> [Arg a] -> [Elim' a]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel
      where
        matchVar :: Int -> Maybe (a, a)
    matchVar Int
    i = (Int, (a, a)) -> (a, a)
    forall a b. (a, b) -> b
    snd ((Int, (a, a)) -> (a, a)) -> Maybe (Int, (a, a)) -> Maybe (a, a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Int, (a, a)) -> Bool) -> [(Int, (a, a))] -> Maybe (Int, (a, a))
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find ((Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Int -> Bool) -> ((Int, (a, a)) -> Int) -> (Int, (a, a)) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int, (a, a)) -> Int
    forall a b. (a, b) -> a
    fst) [(Int, (a, a))]
    boundary
        updateArg :: Arg a -> Elim' a
    updateArg a :: Arg a
    a@(Arg ArgInfo
    info a
    p) =
          case a -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView a
    p of
            Just Int
    i | Just (a
    t,a
    u) <- Int -> Maybe (a, a)
    matchVar Int
    i -> a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply a
    t a
    u a
    p
            Maybe Int
    _                                 -> Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply Arg a
    a

    {-# SPECIALIZE pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type) #-}
    -- | Reduces 'Type'.
    pathViewAsPi
      :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi Type
    t = (((Dom Type, Abs Type), (Term, Term))
     -> Either (Dom Type, Abs Type) Type)
    -> (Type -> Either (Dom Type, Abs Type) Type)
    -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    -> Either (Dom Type, Abs Type) Type
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ((Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
    forall a b. a -> Either a b
    Left ((Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type)
    -> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
    -> ((Dom Type, Abs Type), (Term, Term))
    -> Either (Dom Type, Abs Type) Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
    forall a b. (a, b) -> a
    fst) Type -> Either (Dom Type, Abs Type) Type
    forall a b. b -> Either a b
    Right (Either ((Dom Type, Abs Type), (Term, Term)) Type
     -> Either (Dom Type, Abs Type) Type)
    -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m (Either (Dom Type, Abs Type) Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi' Type
    t

    {-# SPECIALIZE pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
    -- | Reduces 'Type'.
    pathViewAsPi'
      :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term,Term)) Type)
    pathViewAsPi' :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi' Type
    t = do
      m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t

    {-# SPECIALIZE pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
    pathViewAsPi'whnf
      :: (HasBuiltins m)
      => m (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type)
    pathViewAsPi'whnf :: forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf = do
      view <- m (Type -> PathView)
    forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
    pathView'
      minterval  <- getTerm' builtinInterval
      return $ \case
        (Type -> PathView
    view -> PathType Sort' Term
    s QName
    l Arg Term
    p Arg Term
    a Arg Term
    x Arg Term
    y) | Just Term
    interval <- Maybe Term
    minterval ->
          let name :: ArgName
    name | Lam ArgInfo
    _ (Abs ArgName
    n Term
    _) <- Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a = ArgName
    n
                   | Bool
    otherwise = ArgName
    "i"
          in
            ((Dom Type, Abs Type), (Term, Term))
    -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    forall a b. a -> Either a b
    Left ( ( Type -> Dom Type
    forall a. a -> Dom a
    defaultDom (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    intervalSort Term
    interval
                   , ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    name (Type -> Abs Type) -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort' Term -> Sort' Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Sort' Term
    s) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0]
                   )
                 , (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    x, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    y)
                 )

        Type
    t    -> Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    forall a b. b -> Either a b
    Right Type
    t

    -- | Returns @Left (a,b)@ in case the type is @Pi a b@ or @PathP b _ _@.
    --   Assumes the 'Type' is in whnf.
    piOrPath :: HasBuiltins m => Type -> m (Either (Dom Type, Abs Type) Type)
    piOrPath :: forall (m :: * -> *).
    HasBuiltins m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    piOrPath Type
    t = do
      (m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t) m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> (Either ((Dom Type, Abs Type), (Term, Term)) Type
        -> Either (Dom Type, Abs Type) Type)
    -> m (Either (Dom Type, Abs Type) Type)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        Left ((Dom Type, Abs Type)
    p, (Term, Term)
    _)           -> (Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
    forall a b. a -> Either a b
    Left (Dom Type, Abs Type)
    p
        Right (El Sort' Term
    _ (Pi Dom Type
    a Abs Type
    b)) -> (Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
    forall a b. a -> Either a b
    Left (Dom Type
    a,Abs Type
    b)
        Right Type
    _               -> Type -> Either (Dom Type, Abs Type) Type
    forall a b. b -> Either a b
    Right Type
    t

    -- | Assumes 'Type' is in whnf.
    telView'UpToPath :: Int -> Type -> TCM TelView
    telView'UpToPath :: Int -> Type -> TCM TelView
    telView'UpToPath Int
    n Type
    t = if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then TCM TelView
    done else do
      Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    piOrPath Type
    t TCMT IO (Either (Dom Type, Abs Type) Type)
    -> (Either (Dom Type, Abs Type) Type -> TCM TelView) -> TCM TelView
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Left (Dom Type
    a, Abs Type
    b) -> Dom Type -> ArgName -> TelView -> TelView
    forall a. Dom a -> ArgName -> TelV a -> TelV a
    absV Dom Type
    a (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b) (TelView -> TelView) -> TCM TelView -> TCM TelView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Type -> TCM TelView
    forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
    telViewUpToPath (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
        Right Type
    _     -> TCM TelView
    done
      where
        done :: TCM TelView
    done = TelView -> TCM TelView
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TelView -> TCM TelView) -> TelView -> TCM TelView
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t

    telView'Path :: Type -> TCM TelView
    telView'Path :: Type -> TCM TelView
    telView'Path = Int -> Type -> TCM TelView
    telView'UpToPath (-Int
    1)

    isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
    isPath :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (Dom Type, Abs Type))
    isPath Type
    t = Type
    -> (Dom Type -> Abs Type -> m (Maybe (Dom Type, Abs Type)))
    -> (Type -> m (Maybe (Dom Type, Abs Type)))
    -> m (Maybe (Dom Type, Abs Type))
    forall (m :: * -> *) a.
    PureTCM m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPath Type
    t (\Dom Type
    a Abs Type
    b -> Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type)))
    -> Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
    forall a b. (a -> b) -> a -> b
    $ (Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type)
    forall a. a -> Maybe a
    Just (Dom Type
    a,Abs Type
    b)) (m (Maybe (Dom Type, Abs Type))
    -> Type -> m (Maybe (Dom Type, Abs Type))
    forall a b. a -> b -> a
    const (m (Maybe (Dom Type, Abs Type))
     -> Type -> m (Maybe (Dom Type, Abs Type)))
    -> m (Maybe (Dom Type, Abs Type))
    -> Type
    -> m (Maybe (Dom Type, Abs Type))
    forall a b. (a -> b) -> a -> b
    $ Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Dom Type, Abs Type)
    forall a. Maybe a
    Nothing)

    ifPath :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPath :: forall (m :: * -> *) a.
    PureTCM m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPath Type
    t Dom Type -> Abs Type -> m a
    yes Type -> m a
    no = Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPathB Type
    t Dom Type -> Abs Type -> m a
    yes ((Blocked Type -> m a) -> m a) -> (Blocked Type -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ Type -> m a
    no (Type -> m a) -> (Blocked Type -> Type) -> Blocked Type -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocked Type -> Type
    forall t a. Blocked' t a -> a
    ignoreBlocking

    {-# SPECIALIZE ifPathB :: Type -> (Dom Type -> Abs Type -> TCM a) -> (Blocked Type -> TCM a) -> TCM a #-}
    ifPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPathB :: forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPathB Type
    t Dom Type -> Abs Type -> m a
    yes Blocked Type -> m a
    no = Type
    -> (Blocker -> Type -> m a) -> (NotBlocked -> Type -> m a) -> m a
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Type
    t
      (\Blocker
    b Type
    t -> Blocked Type -> m a
    no (Blocked Type -> m a) -> Blocked Type -> m a
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Type -> Blocked Type
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b Type
    t)
      (\NotBlocked
    nb Type
    t -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> (((Dom Type, Abs Type), (Term, Term)) -> m a)
    -> (Type -> m a)
    -> m a
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t)
        ((Dom Type -> Abs Type -> m a) -> (Dom Type, Abs Type) -> m a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> m a
    yes ((Dom Type, Abs Type) -> m a)
    -> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
    -> ((Dom Type, Abs Type), (Term, Term))
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
    forall a b. (a, b) -> a
    fst)
        (Blocked Type -> m a
    no (Blocked Type -> m a) -> (Type -> Blocked Type) -> Type -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NotBlocked -> Type -> Blocked Type
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked
    nb))

    ifNotPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPathB :: forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPathB = ((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
    -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
     -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
    -> (Type
        -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
    -> Type
    -> (Blocked Type -> m a)
    -> (Dom Type -> Abs Type -> m a)
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPathB

    ifPiOrPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiOrPathB :: forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiOrPathB Type
    t Dom Type -> Abs Type -> m a
    yes Blocked Type -> m a
    no = Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiTypeB Type
    t
      (\Dom Type
    a Abs Type
    b -> Dom Type -> Abs Type -> m a
    yes Dom Type
    a Abs Type
    b)
      (\Blocked Type
    bt -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> (((Dom Type, Abs Type), (Term, Term)) -> m a)
    -> (Type -> m a)
    -> m a
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Blocked Type -> Type
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Type
    bt))
        ((Dom Type -> Abs Type -> m a) -> (Dom Type, Abs Type) -> m a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> m a
    yes ((Dom Type, Abs Type) -> m a)
    -> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
    -> ((Dom Type, Abs Type), (Term, Term))
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
    forall a b. (a, b) -> a
    fst)
        (Blocked Type -> m a
    no (Blocked Type -> m a) -> (Type -> Blocked Type) -> Type -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Blocked Type
    bt Blocked Type -> Type -> Blocked Type
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>)))

    ifNotPiOrPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiOrPathB :: forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiOrPathB = ((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
    -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
     -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
    -> (Type
        -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
    -> Type
    -> (Blocked Type -> m a)
    -> (Dom Type -> Abs Type -> m a)
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiOrPathB

    telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns :: forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns = (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
    -> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
    forall a.
    DeBruijn a =>
    (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
    -> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns' Tele (Dom Type) -> [NamedArg a]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs

    telePatterns' :: DeBruijn a =>
                    (forall a. (DeBruijn a) => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns' :: forall a.
    DeBruijn a =>
    (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
    -> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns' forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    f Tele (Dom Type)
    tel (Boundary []) = Tele (Dom Type) -> [NamedArg (Pattern' a)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    f Tele (Dom Type)
    tel
    telePatterns' forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    f Tele (Dom Type)
    tel (Boundary [(Int, (Term, Term))]
    boundary) = [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
    recurse ([Arg (Named NamedName a)] -> [NamedArg (Pattern' a)])
    -> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg (Named NamedName a)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    f Tele (Dom Type)
    tel
      where
        recurse :: [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
    recurse = ((Arg (Named NamedName a) -> NamedArg (Pattern' a))
    -> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Arg (Named NamedName a) -> NamedArg (Pattern' a))
     -> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)])
    -> ((a -> Pattern' a)
        -> Arg (Named NamedName a) -> NamedArg (Pattern' a))
    -> (a -> Pattern' a)
    -> [Arg (Named NamedName a)]
    -> [NamedArg (Pattern' a)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName a -> Named NamedName (Pattern' a))
    -> Arg (Named NamedName a) -> NamedArg (Pattern' a)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName a -> Named NamedName (Pattern' a))
     -> Arg (Named NamedName a) -> NamedArg (Pattern' a))
    -> ((a -> Pattern' a)
        -> Named NamedName a -> Named NamedName (Pattern' a))
    -> (a -> Pattern' a)
    -> Arg (Named NamedName a)
    -> NamedArg (Pattern' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Pattern' a)
    -> Named NamedName a -> Named NamedName (Pattern' a)
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) a -> Pattern' a
    updateVar
        matchVar :: Int -> Maybe (Term, Term)
    matchVar Int
    i = (Int, (Term, Term)) -> (Term, Term)
    forall a b. (a, b) -> b
    snd ((Int, (Term, Term)) -> (Term, Term))
    -> Maybe (Int, (Term, Term)) -> Maybe (Term, Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Int, (Term, Term)) -> Bool)
    -> [(Int, (Term, Term))] -> Maybe (Int, (Term, Term))
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find ((Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Int -> Bool)
    -> ((Int, (Term, Term)) -> Int) -> (Int, (Term, Term)) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int, (Term, Term)) -> Int
    forall a b. (a, b) -> a
    fst) [(Int, (Term, Term))]
    boundary
        updateVar :: a -> Pattern' a
    updateVar a
    x =
          case a -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView a
    x of
            Just Int
    i | Just (Term
    t,Term
    u) <- Int -> Maybe (Term, Term)
    matchVar Int
    i -> PatternInfo -> Term -> Term -> a -> Pattern' a
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    defaultPatternInfo Term
    t Term
    u a
    x
            Maybe Int
    _                                 -> PatternInfo -> a -> Pattern' a
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    defaultPatternInfo a
    x

    -- | Decomposing a function type.

    mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type)
    mustBePi :: forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t = Type
    -> (Type -> m (Dom Type, Abs Type))
    -> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    t Type -> m (Dom Type, Abs Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((Dom Type -> Abs Type -> m (Dom Type, Abs Type))
     -> m (Dom Type, Abs Type))
    -> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
    -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ ((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    -- | If the given type is a @Pi@, pass its parts to the first continuation.
    --   If not (or blocked), pass the reduced type to the second continuation.
    ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    ifPi :: forall (m :: * -> *) a.
    MonadReduce m =>
    Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    ifPi Term
    t Dom Type -> Abs Type -> m a
    yes Term -> m a
    no = Term
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Term
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    ifPiB Term
    t Dom Type -> Abs Type -> m a
    yes (Term -> m a
    no (Term -> m a) -> (Blocked Term -> Term) -> Blocked Term -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking)

    ifPiB :: (MonadReduce m) => Term -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    ifPiB :: forall (m :: * -> *) a.
    MonadReduce m =>
    Term
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    ifPiB Term
    t Dom Type -> Abs Type -> m a
    yes Blocked Term -> m a
    no = Term
    -> (Blocker -> Term -> m a) -> (NotBlocked -> Term -> m a) -> m a
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    t
      (\Blocker
    b Term
    t -> Blocked Term -> m a
    no (Blocked Term -> m a) -> Blocked Term -> m a
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Term -> Blocked Term
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b Term
    t) -- Pi type is never blocked
      (\NotBlocked
    nb Term
    t -> case Term
    t of
        Pi Dom Type
    a Abs Type
    b -> Dom Type -> Abs Type -> m a
    yes Dom Type
    a Abs Type
    b
        Term
    _      -> Blocked Term -> m a
    no (Blocked Term -> m a) -> Blocked Term -> m a
    forall a b. (a -> b) -> a -> b
    $ NotBlocked -> Term -> Blocked Term
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked
    nb Term
    t)

    ifPiTypeB :: (MonadReduce m) => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiTypeB :: forall (m :: * -> *) a.
    MonadReduce m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiTypeB (El Sort' Term
    s Term
    t) Dom Type -> Abs Type -> m a
    yes Blocked Type -> m a
    no = Term
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Term
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
    ifPiB Term
    t Dom Type -> Abs Type -> m a
    yes (\Blocked Term
    bt -> Blocked Type -> m a
    no (Blocked Type -> m a) -> Blocked Type -> m a
    forall a b. (a -> b) -> a -> b
    $ Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s (Term -> Type) -> Blocked Term -> Blocked Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Blocked Term
    bt)

    -- | If the given type is a @Pi@, pass its parts to the first continuation.
    --   If not (or blocked), pass the reduced type to the second continuation.
    ifPiType :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPiType :: forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPiType (El Sort' Term
    s Term
    t) Dom Type -> Abs Type -> m a
    yes Type -> m a
    no = Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    ifPi Term
    t Dom Type -> Abs Type -> m a
    yes (Type -> m a
    no (Type -> m a) -> (Term -> Type) -> Term -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    s)

    -- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
    --   If it is a @Pi@, pass its parts to the second continuation.
    ifNotPi :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPi :: forall (m :: * -> *) a.
    MonadReduce m =>
    Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPi = ((Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
    -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
     -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
    -> (Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
    -> Term
    -> (Term -> m a)
    -> (Dom Type -> Abs Type -> m a)
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
    ifPi

    -- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
    --   If it is a @Pi@, pass its parts to the second continuation.
    ifNotPiType :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiType :: forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    ifNotPiType = ((Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
    -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
     -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
    -> (Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
    -> Type
    -> (Type -> m a)
    -> (Dom Type -> Abs Type -> m a)
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPiType

    ifNotPiOrPathType :: (MonadReduce tcm, HasBuiltins tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
    ifNotPiOrPathType :: forall (tcm :: * -> *) a.
    (MonadReduce tcm, HasBuiltins tcm) =>
    Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
    ifNotPiOrPathType Type
    t Type -> tcm a
    no Dom Type -> Abs Type -> tcm a
    yes = do
      Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPiType Type
    t Dom Type -> Abs Type -> tcm a
    yes (\ Type
    t -> (((Dom Type, Abs Type), (Term, Term)) -> tcm a)
    -> (Type -> tcm a)
    -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    -> tcm a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ((Dom Type -> Abs Type -> tcm a) -> (Dom Type, Abs Type) -> tcm a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> tcm a
    yes ((Dom Type, Abs Type) -> tcm a)
    -> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
    -> ((Dom Type, Abs Type), (Term, Term))
    -> tcm a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
    forall a b. (a, b) -> a
    fst) (tcm a -> Type -> tcm a
    forall a b. a -> b -> a
    const (tcm a -> Type -> tcm a) -> tcm a -> Type -> tcm a
    forall a b. (a -> b) -> a -> b
    $ Type -> tcm a
    no Type
    t) (Either ((Dom Type, Abs Type), (Term, Term)) Type -> tcm a)
    -> tcm (Either ((Dom Type, Abs Type), (Term, Term)) Type) -> tcm a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (tcm (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf tcm (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> tcm Type
    -> tcm (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. tcm (a -> b) -> tcm a -> tcm b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> tcm Type
    forall a. a -> tcm a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t))

    shouldBePath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
    shouldBePath :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePath Type
    t = Type
    -> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
    -> (Blocked Type -> m (Dom Type, Abs Type))
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPathB Type
    t
      (((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)
      (Blocked Type -> m Type
    forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
    fromBlocked (Blocked Type -> m Type)
    -> (Type -> m (Dom Type, Abs Type))
    -> Blocked Type
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> \case
        El Sort' Term
    _ Dummy{} -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__, ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "x" Type
    HasCallStack => Type
    __DUMMY_TYPE__)
        Type
    t -> TypeError -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Dom Type, Abs Type))
    -> TypeError -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBePath Type
    t)

    shouldBePi :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
    shouldBePi :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePi Type
    t = Type
    -> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
    -> (Blocked Type -> m (Dom Type, Abs Type))
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiTypeB Type
    t
      (((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)
      (Blocked Type -> m Type
    forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
    fromBlocked (Blocked Type -> m Type)
    -> (Type -> m (Dom Type, Abs Type))
    -> Blocked Type
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> \case
        El Sort' Term
    _ Dummy{} -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__, ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "x" Type
    HasCallStack => Type
    __DUMMY_TYPE__)
        Type
    t -> TypeError -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Dom Type, Abs Type))
    -> TypeError -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBePi Type
    t)

    shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
    shouldBePiOrPath :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    Type -> m (Dom Type, Abs Type)
    shouldBePiOrPath Type
    t = Type
    -> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
    -> (Blocked Type -> m (Dom Type, Abs Type))
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    PureTCM m =>
    Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
    ifPiOrPathB Type
    t
      (((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
    -> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)
      (Blocked Type -> m Type
    forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
    fromBlocked (Blocked Type -> m Type)
    -> (Type -> m (Dom Type, Abs Type))
    -> Blocked Type
    -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> \case
        El Sort' Term
    _ Dummy{} -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__, ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "x" Type
    HasCallStack => Type
    __DUMMY_TYPE__)
        Type
    t -> TypeError -> m (Dom Type, Abs Type)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m (Dom Type, Abs Type))
    -> TypeError -> m (Dom Type, Abs Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBePi Type
    t) -- TODO: separate error

    -- | A safe variant of 'piApply'.

    class PiApplyM a where
      piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type

      piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type
      piApplyM = m Empty -> Type -> a -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    piApplyM' m Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      {-# INLINE piApplyM #-}

    instance PiApplyM Term where
      piApplyM' :: forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Term -> m Type
    piApplyM' m Empty
    err Type
    t Term
    v = Type
    -> (Type -> m Type) -> (Dom Type -> Abs Type -> m Type) -> m Type
    forall (tcm :: * -> *) a.
    (MonadReduce tcm, HasBuiltins tcm) =>
    Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
    ifNotPiOrPathType Type
    t (\Type
    _ -> Empty -> Type
    forall a. Empty -> a
    absurd (Empty -> Type) -> m Empty -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Empty
    err) {-else-} ((Dom Type -> Abs Type -> m Type) -> m Type)
    -> (Dom Type -> Abs Type -> m Type) -> m Type
    forall a b. (a -> b) -> a -> b
    $ \ Dom Type
    _ Abs Type
    b -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b Term
    SubstArg Type
    v
      {-# INLINABLE piApplyM' #-}

    {-# SPECIALIZE piApplyM' :: TCM Empty -> Type -> Term -> TCM Type #-}

    instance PiApplyM a => PiApplyM (Arg a) where
      piApplyM' :: forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Arg a -> m Type
    piApplyM' m Empty
    err Type
    t = m Empty -> Type -> a -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    piApplyM' m Empty
    err Type
    t (a -> m Type) -> (Arg a -> a) -> Arg a -> m Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg a -> a
    forall e. Arg e -> e
    unArg

    instance PiApplyM a => PiApplyM (Named n a) where
      piApplyM' :: forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Named n a -> m Type
    piApplyM' m Empty
    err Type
    t = m Empty -> Type -> a -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    piApplyM' m Empty
    err Type
    t (a -> m Type) -> (Named n a -> a) -> Named n a -> m Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named n a -> a
    forall name a. Named name a -> a
    namedThing

    instance PiApplyM a => PiApplyM [a] where
      piApplyM' :: forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> [a] -> m Type
    piApplyM' m Empty
    err Type
    t = (m Type -> a -> m Type) -> m Type -> [a] -> m Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\ m Type
    mt a
    v -> m Type
    mt m Type -> (Type -> m Type) -> m Type
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Type
    t -> (m Empty -> Type -> a -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    piApplyM' m Empty
    err Type
    t a
    v)) (Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t)

    -- | Compute type arity

    typeArity :: Type -> TCM Nat
    typeArity :: Type -> TCM Int
    typeArity Type
    t = do
      TelV tel _ <- Type -> TCM TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m TelView
    telView Type
    t
      return (size tel)

    -- | Fold a telescope into a monadic computation, adding variables to the
    -- context at each step.

    foldrTelescopeM
      :: MonadAddContext m
      => (Dom (ArgName, Type) -> m b -> m b)
      -> m b
      -> Telescope
      -> m b
    foldrTelescopeM :: forall (m :: * -> *) b.
    MonadAddContext m =>
    (Dom (ArgName, Type) -> m b -> m b)
    -> m b -> Tele (Dom Type) -> m b
    foldrTelescopeM Dom (ArgName, Type) -> m b -> m b
    f m b
    b = Tele (Dom Type) -> m b
    go
      where
        go :: Tele (Dom Type) -> m b
    go Tele (Dom Type)
    EmptyTel = m b
    b
        go (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel) =
          Dom (ArgName, Type) -> m b -> m b
    f ((Abs (Tele (Dom Type)) -> ArgName
    forall a. Abs a -> ArgName
    absName Abs (Tele (Dom Type))
    tel,) (Type -> (ArgName, Type)) -> Dom Type -> Dom (ArgName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    a) (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ Dom Type
    -> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> m b) -> m b
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    a Abs (Tele (Dom Type))
    tel Tele (Dom Type) -> m b
    go