    module Agda.TypeChecking.Telescope where

    import Prelude hiding (null)

    import Control.Monad

    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.Internal
    import Agda.Syntax.Internal.Pattern

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

    import Agda.Utils.CallStack ( withCallerCallStack )
    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] #-}

    -- | 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 []   []            = Tele (Dom Type)
    forall a. Tele a
    EmptyTel
    unflattenTel (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' = [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel [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 (Int -> Term -> [Term]
    forall a. Int -> a -> [a]
    replicate ([Dom Type] -> Int
    forall a. Sized a => a -> Int
    size [Dom Type]
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) ((CallStack -> Term) -> Term
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Term
    impossibleTerm))
    unflattenTel [] (Dom Type
    _ : [Dom Type]
    _) = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    unflattenTel (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 :: ArgName
    absName = ArgName
    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 = (Dom (ArgName, Type) -> Arg ArgName)
    -> [Dom (ArgName, Type)] -> [Arg ArgName]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom' Term ArgName -> Arg ArgName
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom' Term ArgName -> Arg ArgName)
    -> (Dom (ArgName, Type) -> Dom' Term ArgName)
    -> Dom (ArgName, Type)
    -> Arg ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((ArgName, Type) -> ArgName)
    -> Dom (ArgName, Type) -> Dom' Term ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, Type) -> ArgName
    forall a b. (a, b) -> a
    fst) ([Dom (ArgName, Type)] -> [Arg ArgName])
    -> (Tele (Dom Type) -> [Dom (ArgName, Type)])
    -> Tele (Dom Type)
    -> [Arg 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

    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' Term a)
    -> [Int] -> [Dom (ArgName, t)] -> [Dom' Term 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' 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) => Telescope -> [NamedArg a]
    teleNamedArgs :: forall a. DeBruijn a => Tele (Dom Type) -> [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 Type) -> [Dom' Term a])
    -> Tele (Dom Type)
    -> [NamedArg a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Dom' Term a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
    teleDoms

    -- | 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 (WithOrigin (Ranged ArgName)) a -> NamedArg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Maybe (WithOrigin (Ranged ArgName))
    -> a -> Named (WithOrigin (Ranged ArgName)) a
    forall name a. Maybe name -> a -> Named name a
    Named (WithOrigin (Ranged ArgName) -> Maybe (WithOrigin (Ranged ArgName))
    forall a. a -> Maybe a
    Just (WithOrigin (Ranged ArgName)
     -> Maybe (WithOrigin (Ranged ArgName)))
    -> WithOrigin (Ranged ArgName)
    -> Maybe (WithOrigin (Ranged ArgName))
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged ArgName -> WithOrigin (Ranged ArgName)
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged ArgName -> WithOrigin (Ranged ArgName))
    -> Ranged ArgName -> WithOrigin (Ranged ArgName)
    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

    -- | 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, Arg Term -> Lock
    forall a. LensLock a => a -> Lock
    getLock Arg Term
    a Lock -> Lock -> Bool
    forall a. Eq a => a -> a -> Bool
    == Lock
    IsLock]
            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 :: PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    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. DeBruijn a => Tele (Dom Type) -> [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')

    -- | 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)

    -- | @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

    -- | @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 (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
      Type
    t <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Pi Dom Type
    a Abs Type
    b | Dom Type -> Bool
    p Dom Type
    a -> 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
    <$> 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 (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
      where
        absV :: Dom a -> ArgName -> TelV a -> TelV a
    absV Dom a
    a ArgName
    x (TelV Tele (Dom a)
    tel a
    t) = Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom a
    a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Tele (Dom a)
    tel)) a
    t

    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)

    -- | @telViewUpToPath n t@ takes off $t$
    --   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
    telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
    telViewUpToPath :: forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
    telViewUpToPath Int
    0 Type
    t = TelView -> m TelView
    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
    telViewUpToPath Int
    n Type
    t = do
      Either (Dom Type, Abs Type) Type
    vt <- Type -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi (Type -> m (Either (Dom Type, Abs Type) Type))
    -> Type -> m (Either (Dom Type, Abs Type) Type)
    forall a b. (a -> b) -> a -> b
    $ Type
    t
      case Either (Dom Type, Abs Type) Type
    vt of
        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) -> 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)
        Right (El Sort' Term
    _ Term
    t) | Pi Dom Type
    a Abs Type
    b <- Term
    t
                       -> 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)
        Right Type
    t        -> TelView -> m TelView
    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
      where
        absV :: Dom a -> ArgName -> TelV a -> TelV a
    absV Dom a
    a ArgName
    x (TelV Tele (Dom a)
    tel a
    t) = Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom a
    a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Tele (Dom a)
    tel)) a
    t

    -- | [[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]
    type Boundary = Boundary' (Term,Term)
    type Boundary' a = [(Term,a)]

    -- | 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@.
    telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView,Boundary)
    telViewUpToPathBoundary' :: forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' Int
    0 Type
    t = (TelView, Boundary) -> m (TelView, Boundary)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TelView, Boundary) -> m (TelView, Boundary))
    -> (TelView, Boundary) -> m (TelView, Boundary)
    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,[])
    telViewUpToPathBoundary' Int
    n Type
    t = do
      Either ((Dom Type, Abs Type), (Term, Term)) Type
    vt <- 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 -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type))
    -> Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. (a -> b) -> a -> b
    $ Type
    t
      case Either ((Dom Type, Abs Type), (Term, Term)) Type
    vt of
        Left ((Dom Type
    a,Abs Type
    b),(Term, Term)
    xy) -> (Term, Term) -> (TelView, Boundary) -> (TelView, Boundary)
    forall {b} {a}.
    Subst b =>
    b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
    addEndPoints (Term, Term)
    xy ((TelView, Boundary) -> (TelView, Boundary))
    -> ((TelView, Boundary) -> (TelView, Boundary))
    -> (TelView, Boundary)
    -> (TelView, Boundary)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom Type -> ArgName -> (TelView, Boundary) -> (TelView, Boundary)
    forall {a} {b}. Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
    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
    <$> 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) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
        Right (El Sort' Term
    _ Term
    t) | Pi Dom Type
    a Abs Type
    b <- Term
    t
                       -> Dom Type -> ArgName -> (TelView, Boundary) -> (TelView, Boundary)
    forall {a} {b}. Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
    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
    <$> 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) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
        Right Type
    t        -> (TelView, Boundary) -> m (TelView, Boundary)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TelView, Boundary) -> m (TelView, Boundary))
    -> (TelView, Boundary) -> m (TelView, Boundary)
    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,[])
      where
        absV :: Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
    absV Dom a
    a ArgName
    x (TelV Tele (Dom a)
    tel a
    t, b
    cs) = (Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom a
    a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Tele (Dom a)
    tel)) a
    t, b
    cs)
        addEndPoints :: b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
    addEndPoints b
    xy (telv :: TelV a
    telv@(TelV Tele (Dom a)
    tel a
    _),[(Term, b)]
    cs) = (TelV a
    telv, (Int -> Term
    var (Int -> Term) -> Int -> Term
    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, b
    xyInTel)(Term, b) -> [(Term, b)] -> [(Term, b)]
    forall a. a -> [a] -> [a]
    :[(Term, b)]
    cs)
          where
           xyInTel :: b
    xyInTel = Int -> b -> b
    forall a. Subst a => Int -> a -> a
    raise (Tele (Dom a) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom a)
    tel) b
    xy

    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' Term]
    es = Tele (Dom Type) -> Boundary -> [Elim' Term]
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, 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 ((Term, (Term, Term)) -> (Term, (Term, Term)))
    -> Boundary -> Boundary
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (t :: Term
    t@(Var Int
    i []), (Term, Term)
    xy) -> (Term
    t, (Term, Term)
    xy (Term, Term) -> [Elim' Term] -> (Term, Term)
    forall t. Apply t => t -> [Elim' Term] -> t
    `applyE` (Int -> [Elim' Term] -> [Elim' Term]
    forall a. Int -> [a] -> [a]
    drop (Int
    l Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) [Elim' Term]
    es))) Boundary
    bs

    -- | @(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 :: TelView
    telv@(TelV Tele (Dom Type)
    tel Type
    b), Boundary
    bs) <- Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary' Int
    i Type
    a
       (TelView, Boundary) -> m (TelView, Boundary)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TelView, Boundary) -> m (TelView, Boundary))
    -> (TelView, Boundary) -> m (TelView, Boundary)
    forall a b. (a -> b) -> a -> b
    $ (TelView
    telv, Tele (Dom Type) -> Boundary -> Boundary
    fullBoundary Tele (Dom Type)
    tel Boundary
    bs)

    -- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundaryP 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 Γ.
    telViewUpToPathBoundaryP :: PureTCM m => Int -> Type -> m (TelView,Boundary)
    telViewUpToPathBoundaryP :: forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundaryP = Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundary'

    telViewPathBoundaryP :: PureTCM m => Type -> m (TelView,Boundary)
    telViewPathBoundaryP :: forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
    telViewPathBoundaryP = Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundaryP (-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' (a,a) -> [Elim' a]
    teleElims :: forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
    teleElims Tele (Dom Type)
    tel [] = (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 [(Term, (a, a))]
    boundary = [Arg a] -> [Elim' a]
    recurse (Tele (Dom Type) -> [Arg a]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel)
      where
        recurse :: [Arg a] -> [Elim' a]
    recurse = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Arg a -> Elim' a
    updateArg
        matchVar :: Int -> Maybe (a, a)
    matchVar Int
    x =
          (Term, (a, a)) -> (a, a)
    forall a b. (a, b) -> b
    snd ((Term, (a, a)) -> (a, a)) -> Maybe (Term, (a, a)) -> Maybe (a, a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Term, (a, a)) -> Bool)
    -> [(Term, (a, a))] -> Maybe (Term, (a, a))
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find (\case
            (Var Int
    i [],(a, a)
    _) -> Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    x
            (Term, (a, a))
    _            -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__) [(Term, (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

    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

    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 (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

    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
      Type -> PathView
    view <- m (Type -> PathView)
    forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
    pathView'
      Maybe Term
    minterval  <- ArgName -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getBuiltin' ArgName
    builtinInterval
      (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
     -> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type))
    -> (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall a b. (a -> b) -> a -> b
    $ \ Type
    t -> case Type -> PathView
    view Type
    t of
        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"
              i :: Type
    i = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Level' Term -> Sort' Term
    forall t. Level' t -> Sort' t
    SSet (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level' Term
    ClosedLevel Integer
    0) Term
    interval
          in
            ((Dom Type, Abs Type), (Term, Term))
    -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    forall a b. a -> Either a b
    Left (((Dom Type, Abs Type), (Term, Term))
     -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> ((Dom Type, Abs Type), (Term, Term))
    -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    forall a b. (a -> b) -> a -> b
    $ ((Type -> Dom Type
    forall a. a -> Dom a
    defaultDom (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Type
    i, 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))

        PathView
    _    -> 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
      Either ((Dom Type, Abs Type), (Term, Term)) Type
    t <- 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t
      case Either ((Dom Type, Abs Type), (Term, Term)) Type
    t of
        Left ((Dom Type, Abs Type)
    p,(Term, Term)
    _) -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Dom Type, Abs Type) Type
     -> m (Either (Dom Type, Abs Type) Type))
    -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall a b. (a -> b) -> a -> b
    $ (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)) -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Dom Type, Abs Type) Type
     -> m (Either (Dom Type, Abs Type) Type))
    -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall a b. (a -> b) -> a -> 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
    t -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Dom Type, Abs Type) Type
     -> m (Either (Dom Type, Abs Type) Type))
    -> Either (Dom Type, Abs Type) Type
    -> m (Either (Dom Type, Abs Type) Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Either (Dom Type, Abs Type) Type
    forall a b. b -> Either a b
    Right Type
    t

    telView'UpToPath :: Int -> Type -> TCM TelView
    telView'UpToPath :: Int -> Type -> TCM TelView
    telView'UpToPath Int
    0 Type
    t = TelView -> TCM TelView
    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'UpToPath Int
    n Type
    t = do
      Either ((Dom Type, Abs Type), (Term, Term)) Type
    vt <- TCMT IO (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 TCMT IO (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    -> TCMT IO Type
    -> TCMT IO (Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> TCMT IO Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t
      case Either ((Dom Type, Abs Type), (Term, Term)) Type
    vt of
        Left ((Dom Type
    a,Abs Type
    b),(Term, Term)
    _)     -> 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 (El Sort' Term
    _ Term
    t) | Pi Dom Type
    a Abs Type
    b <- Term
    t
                       -> 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
    t        -> TelView -> TCM TelView
    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
      where
        absV :: Dom a -> ArgName -> TelV a -> TelV a
    absV Dom a
    a ArgName
    x (TelV Tele (Dom a)
    tel a
    t) = Tele (Dom a) -> a -> TelV a
    forall a. Tele (Dom a) -> a -> TelV a
    TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom a
    a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Tele (Dom a)
    tel)) a
    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 = ((Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type))
    -> (Type -> Maybe (Dom Type, Abs Type))
    -> Either (Dom Type, Abs Type) Type
    -> Maybe (Dom Type, Abs Type)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type)
    forall a. a -> Maybe a
    Just (Maybe (Dom Type, Abs Type) -> Type -> Maybe (Dom Type, Abs Type)
    forall a b. a -> b -> a
    const Maybe (Dom Type, Abs Type)
    forall a. Maybe a
    Nothing) (Either (Dom Type, Abs Type) Type -> Maybe (Dom Type, Abs Type))
    -> m (Either (Dom Type, Abs Type) Type)
    -> m (Maybe (Dom Type, Abs Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi Type
    t

    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' forall a. DeBruijn a => Tele (Dom Type) -> [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 [] = 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
    boundary = [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    -> [NamedArg (Pattern' a)]
    recurse ([Arg (Named (WithOrigin (Ranged ArgName)) a)]
     -> [NamedArg (Pattern' a)])
    -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    f Tele (Dom Type)
    tel
      where
        recurse :: [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    -> [NamedArg (Pattern' a)]
    recurse = ((Arg (Named (WithOrigin (Ranged ArgName)) a)
     -> NamedArg (Pattern' a))
    -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    -> [NamedArg (Pattern' a)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Arg (Named (WithOrigin (Ranged ArgName)) a)
      -> NamedArg (Pattern' a))
     -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
     -> [NamedArg (Pattern' a)])
    -> ((a -> Pattern' a)
        -> Arg (Named (WithOrigin (Ranged ArgName)) a)
        -> NamedArg (Pattern' a))
    -> (a -> Pattern' a)
    -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
    -> [NamedArg (Pattern' a)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named (WithOrigin (Ranged ArgName)) a
     -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
    -> Arg (Named (WithOrigin (Ranged ArgName)) a)
    -> NamedArg (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named (WithOrigin (Ranged ArgName)) a
      -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
     -> Arg (Named (WithOrigin (Ranged ArgName)) a)
     -> NamedArg (Pattern' a))
    -> ((a -> Pattern' a)
        -> Named (WithOrigin (Ranged ArgName)) a
        -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
    -> (a -> Pattern' a)
    -> Arg (Named (WithOrigin (Ranged ArgName)) a)
    -> NamedArg (Pattern' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Pattern' a)
    -> Named (WithOrigin (Ranged ArgName)) a
    -> Named (WithOrigin (Ranged ArgName)) (Pattern' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) a -> Pattern' a
    updateVar
        matchVar :: Int -> Maybe (Term, Term)
    matchVar Int
    x =
          (Term, (Term, Term)) -> (Term, Term)
    forall a b. (a, b) -> b
    snd ((Term, (Term, Term)) -> (Term, Term))
    -> Maybe (Term, (Term, Term)) -> Maybe (Term, Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Term, (Term, Term)) -> Bool)
    -> Boundary -> Maybe (Term, (Term, Term))
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find (\case
            (Var Int
    i [],(Term, Term)
    _) -> Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    x
            (Term, (Term, Term))
    _            -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__) Boundary
    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 (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 = do
      Term
    t <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce 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
    _      -> Term -> m a
    no Term
    t

    -- | 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> tcm Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    t))

    -- | 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
    piApplyM' m Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    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 (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

    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
    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
    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 (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 (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
    piApplyM' m Empty
    err Type
    t a
    v)) (Type -> m Type
    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 Tele (Dom Type)
    tel Type
    _ <- Type -> TCM TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m TelView
    telView Type
    t
      Int -> TCM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel)

    ---------------------------------------------------------------------------
    -- * Instance definitions
    ---------------------------------------------------------------------------

    data OutputTypeName
      = OutputTypeName QName
      | OutputTypeVar
      | OutputTypeVisiblePi
      | OutputTypeNameNotYetKnown Blocker
      | NoOutputTypeName

    -- | Strips all hidden and instance Pi's and return the argument
    --   telescope and head definition name, if possible.
    getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
    getOutputTypeName :: Type -> TCM (Tele (Dom Type), OutputTypeName)
    getOutputTypeName Type
    t = do
      TelV Tele (Dom Type)
    tel Type
    t' <- Int -> (Dom Type -> Bool) -> Type -> TCM TelView
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> (Dom Type -> Bool) -> Type -> m TelView
    telViewUpTo' (-Int
    1) Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Type
    t
      Term
    -> (Blocker -> Term -> TCM (Tele (Dom Type), OutputTypeName))
    -> (NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t') (\ Blocker
    b Term
    _ -> (Tele (Dom Type), OutputTypeName)
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type)
    tel , Blocker -> OutputTypeName
    OutputTypeNameNotYetKnown Blocker
    b)) ((NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
     -> TCM (Tele (Dom Type), OutputTypeName))
    -> (NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    _ Term
    v ->
        case Term
    v of
          -- Possible base types:
          Def QName
    n [Elim' Term]
    _  -> (Tele (Dom Type), OutputTypeName)
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type)
    tel , QName -> OutputTypeName
    OutputTypeName QName
    n)
          Sort{}   -> (Tele (Dom Type), OutputTypeName)
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type)
    tel , OutputTypeName
    NoOutputTypeName)
          Var Int
    n [Elim' Term]
    _  -> (Tele (Dom Type), OutputTypeName)
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type)
    tel , OutputTypeName
    OutputTypeVar)
          Pi{}     -> (Tele (Dom Type), OutputTypeName)
    -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type)
    tel , OutputTypeName
    OutputTypeVisiblePi)
          -- Not base types:
          Con{}    -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lam{}    -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lit{}    -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level{}  -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaV{}  -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DontCare{} -> TCM (Tele (Dom Type), OutputTypeName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Dummy ArgName
    s [Elim' Term]
    _ -> ArgName -> TCM (Tele (Dom Type), OutputTypeName)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s

    -- | Register the definition with the given type as an instance
    addTypedInstance :: QName -> Type -> TCM ()
    addTypedInstance :: QName -> Type -> TCM ()
    addTypedInstance QName
    x Type
    t = do
      (Tele (Dom Type)
    tel , OutputTypeName
    n) <- Type -> TCM (Tele (Dom Type), OutputTypeName)
    getOutputTypeName Type
    t
      case OutputTypeName
    n of
        OutputTypeName QName
    n -> QName -> QName -> TCM ()
    addNamedInstance QName
    x QName
    n
        OutputTypeNameNotYetKnown{} -> QName -> TCM ()
    addUnknownInstance QName
    x
        OutputTypeName
    NoOutputTypeName -> Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning
    WrongInstanceDeclaration
        OutputTypeName
    OutputTypeVar -> Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning
    WrongInstanceDeclaration
        OutputTypeName
    OutputTypeVisiblePi -> Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    InstanceWithExplicitArg QName
    x

    resolveUnknownInstanceDefs :: TCM ()
    resolveUnknownInstanceDefs :: TCM ()
    resolveUnknownInstanceDefs = do
      Set QName
    anonInstanceDefs <- TCM (Set QName)
    getAnonInstanceDefs
      TCM ()
    clearAnonInstanceDefs
      Set QName -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ Set QName
    anonInstanceDefs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    n -> QName -> Type -> TCM ()
    addTypedInstance QName
    n (Type -> TCM ()) -> TCMT IO Type -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Type
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m Type
    typeOfConst QName
    n

    -- | Try to solve the instance definitions whose type is not yet known, report
    --   an error if it doesn't work and return the instance table otherwise.
    getInstanceDefs :: TCM InstanceTable
    getInstanceDefs :: TCM InstanceTable
    getInstanceDefs = do
      TCM ()
    resolveUnknownInstanceDefs
      TempInstanceTable
    insts <- TCM TempInstanceTable
    getAllInstanceDefs
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Set QName -> Bool
    forall a. Null a => a -> Bool
    null (Set QName -> Bool) -> Set QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ TempInstanceTable -> Set QName
    forall a b. (a, b) -> b
    snd TempInstanceTable
    insts) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> ArgName -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "There are instances whose type is still unsolved"
      InstanceTable -> TCM InstanceTable
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InstanceTable -> TCM InstanceTable)
    -> InstanceTable -> TCM InstanceTable
    forall a b. (a -> b) -> a -> b
    $ TempInstanceTable -> InstanceTable
    forall a b. (a, b) -> a
    fst TempInstanceTable
    insts