    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE TypeApplications    #-}

    {-# OPTIONS_GHC -fno-warn-orphans #-}

    {-# OPTIONS_GHC -ddump-simpl -dsuppress-all -ddump-to-file #-}

    -- | This module contains the definition of hereditary substitution
    -- and application operating on internal syntax which is in β-normal
    -- form (β including projection reductions).
    --
    -- Further, it contains auxiliary functions which rely on substitution
    -- but not on reduction.

    module Agda.TypeChecking.Substitute
      ( module Agda.TypeChecking.Substitute
      , module Agda.TypeChecking.Substitute.Class
      , module Agda.TypeChecking.Substitute.DeBruijn
      , Substitution'(..), Substitution
      ) where

    import Control.Arrow (first, second)

    import Data.Coerce
    import Data.Function (on)
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map.Strict as MapS
    import Data.Maybe
    import Data.HashMap.Strict (HashMap)

    import Debug.Trace (trace)

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import qualified Agda.Syntax.Abstract as A

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Free as Free
    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Positivity.Occurrence as Occ

    import Agda.TypeChecking.Substitute.Class
    import Agda.TypeChecking.Substitute.DeBruijn

    import Agda.Utils.Either
    import Agda.Utils.Empty
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | Apply @Elims@ while using the given function to report ill-typed
    --   redexes.
    --   Recursive calls for @applyE@ and @applySubst@ happen at type @t@ to
    --   propagate the same strategy to subtrees.
    {-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-}
    {-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-}
    applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t)
               => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
    applyTermE :: forall t.
    (Coercible Term t, Apply t, EndoSubst t) =>
    (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
    applyTermE Empty -> Term -> Elims -> Term
    err' t
    m [] = t
    m
    applyTermE Empty -> Term -> Elims -> Term
    err' t
    m Elims
    es = Term -> t
    forall a b. Coercible a b => a -> b
    coerce (Term -> t) -> Term -> t
    forall a b. (a -> b) -> a -> b
    $
        case t -> Term
    forall a b. Coercible a b => a -> b
    coerce t
    m of
          Var Int
    i Elims
    es'   -> Int -> Elims -> Term
    Var Int
    i (Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es)
          Def QName
    f Elims
    es'   -> QName -> Elims -> Elims -> Term
    defApp QName
    f Elims
    es' Elims
    es  -- remove projection redexes
          Con ConHead
    c ConInfo
    ci Elims
    args -> forall t.
    (Coercible t Term, Apply t) =>
    (Empty -> Term -> Elims -> Term)
    -> ConHead -> ConInfo -> Elims -> Elims -> Term
    conApp @t Empty -> Term -> Elims -> Term
    err' ConHead
    c ConInfo
    ci Elims
    args Elims
    es
          Lam ArgInfo
    _ Abs Term
    b     ->
            case Elims
    es of
              Apply Arg Term
    a : Elims
    es0      -> Abs t -> SubstArg t -> t
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs Term -> Abs t
    forall a b. Coercible a b => a -> b
    coerce Abs Term
    b :: Abs t) (Term -> SubstArg t
    forall a b. Coercible a b => a -> b
    coerce (Term -> SubstArg t) -> Term -> SubstArg t
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) t -> Elims -> Term
    forall a. Coercible t a => a -> Elims -> Term
    `app` Elims
    es0
              IApply Term
    _ Term
    _ Term
    a : Elims
    es0 -> Abs t -> SubstArg t -> t
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp (Abs Term -> Abs t
    forall a b. Coercible a b => a -> b
    coerce Abs Term
    b :: Abs t) (Term -> t
    forall a b. Coercible a b => a -> b
    coerce Term
    a)         t -> Elims -> Term
    forall a. Coercible t a => a -> Elims -> Term
    `app` Elims
    es0
              Elims
    _                  -> Empty -> Term
    err Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaV MetaId
    x Elims
    es' -> MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es)
          Lit{}       -> Empty -> Term
    err Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Level{}     -> Empty -> Term
    err Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Pi Dom Type
    _ Abs Type
    _      -> Empty -> Term
    err Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Sort Sort
    s      -> Sort -> Term
    Sort (Sort -> Term) -> Sort -> Term
    forall a b. (a -> b) -> a -> b
    $ Sort
    s Sort -> Elims -> Sort
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es
          Dummy [Char]
    s Elims
    es' -> [Char] -> Elims -> Term
    Dummy [Char]
    s (Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es)
          DontCare Term
    mv -> Term -> Term
    dontCare (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Term
    mv Term -> Elims -> Term
    forall a. Coercible t a => a -> Elims -> Term
    `app` Elims
    es  -- Andreas, 2011-10-02
            -- need to go under DontCare, since "with" might resurrect irrelevant term
       where
         app :: Coercible t a => a -> Elims -> Term
         app :: forall a. Coercible t a => a -> Elims -> Term
    app a
    u Elims
    es = t -> Term
    forall a b. Coercible a b => a -> b
    coerce (t -> Term) -> t -> Term
    forall a b. (a -> b) -> a -> b
    $ (a -> t
    forall a b. Coercible a b => a -> b
    coerce a
    u :: t) t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es
         err :: Empty -> Term
    err Empty
    e = Empty -> Term -> Elims -> Term
    err' Empty
    e (t -> Term
    forall a b. Coercible a b => a -> b
    coerce t
    m) Elims
    es

    instance Apply Term where
      applyE :: Term -> Elims -> Term
    applyE = (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term
    forall t.
    (Coercible Term t, Apply t, EndoSubst t) =>
    (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
    applyTermE Empty -> Term -> Elims -> Term
    forall a. Empty -> a
    absurd

    instance Apply BraveTerm where
      applyE :: BraveTerm -> Elims -> BraveTerm
    applyE = (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm
    forall t.
    (Coercible Term t, Apply t, EndoSubst t) =>
    (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
    applyTermE (\ Empty
    _ Term
    t Elims
    es ->  [Char] -> Elims -> Term
    Dummy [Char]
    "applyE" (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    t) Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    es))

    -- | If @v@ is a record or constructed value, @canProject f v@
    --   returns its field @f@.
    canProject :: QName -> Term -> Maybe (Arg Term)
    canProject :: QName -> Term -> Maybe (Arg Term)
    canProject QName
    f Term
    v =
      case Term
    v of
        -- Andreas, 2022-06-10, issue #5922: also unfold data projections
        -- (not just record projections).
        (Con (ConHead QName
    _ DataOrRecord
    _ Induction
    _ [Arg QName]
    fs) ConInfo
    _ Elims
    vs) -> do
          (fld, i) <- (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
    forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
    findWithIndex ((QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg QName -> QName
    forall e. Arg e -> e
    unArg) [Arg QName]
    fs
          -- Jesper, 2019-10-17: dont unfold irrelevant projections
          guard $ not $ isIrrelevant fld
          -- Andreas, 2018-06-12, issue #2170
          -- The ArgInfo from the ConHead is more accurate (relevance subtyping!).
          setArgInfo (getArgInfo fld) <.> isApplyElim =<< listToMaybe (drop i vs)
        Term
    _ -> Maybe (Arg Term)
    forall a. Maybe a
    Nothing

    -- | Eliminate a constructed term.
    conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
    conApp :: forall t.
    (Coercible t Term, Apply t) =>
    (Empty -> Term -> Elims -> Term)
    -> ConHead -> ConInfo -> Elims -> Elims -> Term
    conApp Empty -> Term -> Elims -> Term
    fallback ConHead
    ch                    ConInfo
    ci Elims
    args []                  = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    ch ConInfo
    ci Elims
    args
    conApp Empty -> Term -> Elims -> Term
    fallback ConHead
    ch                    ConInfo
    ci Elims
    args    (a :: Elim' Term
    a@Apply{} : Elims
    es) = forall t.
    (Coercible t Term, Apply t) =>
    (Empty -> Term -> Elims -> Term)
    -> ConHead -> ConInfo -> Elims -> Elims -> Term
    conApp @t Empty -> Term -> Elims -> Term
    fallback ConHead
    ch ConInfo
    ci (Elims
    args Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term
    a]) Elims
    es
    conApp Empty -> Term -> Elims -> Term
    fallback ConHead
    ch                    ConInfo
    ci Elims
    args   (a :: Elim' Term
    a@IApply{} : Elims
    es) = forall t.
    (Coercible t Term, Apply t) =>
    (Empty -> Term -> Elims -> Term)
    -> ConHead -> ConInfo -> Elims -> Elims -> Term
    conApp @t Empty -> Term -> Elims -> Term
    fallback ConHead
    ch ConInfo
    ci (Elims
    args Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term
    a]) Elims
    es
    conApp Empty -> Term -> Elims -> Term
    fallback ch :: ConHead
    ch@(ConHead QName
    c DataOrRecord
    _ Induction
    _ [Arg QName]
    fs) ConInfo
    ci Elims
    args ees :: Elims
    ees@(Proj ProjOrigin
    o QName
    f : Elims
    es) =
      let failure :: forall a. a -> a
          failure :: forall a. a -> a
    failure a
    err = ([Char] -> a -> a) -> a -> [Char] -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [Char] -> a -> a
    forall a. [Char] -> a -> a
    trace a
    err ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
            [ [Char]
    "conApp: constructor ", QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    c
            , [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    " with fields" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : (Arg QName -> [Char]) -> [Arg QName] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> [Char]) -> (Arg QName -> [Char]) -> Arg QName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow) [Arg QName]
    fs
            , [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    " and args"    [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : (Elim' Term -> [Char]) -> Elims -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> [Char])
    -> (Elim' Term -> [Char]) -> Elim' Term -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' Term -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow) Elims
    args
            , [Char]
    " projected by ", QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f
            ]
          isApply :: Elim' a -> Arg a
    isApply Elim' a
    e = Arg a -> Maybe (Arg a) -> Arg a
    forall a. a -> Maybe a -> a
    fromMaybe (Arg a -> Arg a
    forall a. a -> a
    failure Arg a
    forall a. HasCallStack => a
    __IMPOSSIBLE__) (Maybe (Arg a) -> Arg a) -> Maybe (Arg a) -> Arg a
    forall a b. (a -> b) -> a -> b
    $ Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elim' a
    e
          stuck :: Empty -> Term
    stuck Empty
    err = Empty -> Term -> Elims -> Term
    fallback Empty
    err (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    ch ConInfo
    ci Elims
    args) [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f]
          -- Recurse using the instance for 't', see @applyTermE@
          app :: Term -> Elims -> Term
          app :: Term -> Elims -> Term
    app Term
    v Elims
    es = t -> Term
    forall a b. Coercible a b => a -> b
    coerce (t -> Term) -> t -> Term
    forall a b. (a -> b) -> a -> b
    $ t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    applyE (Term -> t
    forall a b. Coercible a b => a -> b
    coerce Term
    v :: t) Elims
    es
      in
       case (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
    forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
    findWithIndex ((QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg QName -> QName
    forall e. Arg e -> e
    unArg) [Arg QName]
    fs of
         Maybe (Arg QName, Int)
    Nothing -> Term -> Term
    forall a. a -> a
    failure (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Empty -> Term
    stuck Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Term -> Elims -> Term
    `app` Elims
    es
         Just (Arg QName
    fld, Int
    i) -> let
          -- Andreas, 2018-06-12, issue #2170
          -- We safe-guard the projected value by DontCare using the ArgInfo stored at the record constructor,
          -- since the ArgInfo in the constructor application might be inaccurate because of subtyping.
          v :: Term
    v = Term -> (Elim' Term -> Term) -> Maybe (Elim' Term) -> Term
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Term -> Term
    forall a. a -> a
    failure (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Empty -> Term
    stuck Empty
    forall a. HasCallStack => a
    __IMPOSSIBLE__) (Arg QName -> Term -> Term
    forall a. LensRelevance a => a -> Term -> Term
    relToDontCare Arg QName
    fld (Term -> Term) -> (Elim' Term -> Term) -> Elim' Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    argToDontCare (Arg Term -> Term)
    -> (Elim' Term -> Arg Term) -> Elim' Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' Term -> Arg Term
    forall {a}. Elim' a -> Arg a
    isApply) (Maybe (Elim' Term) -> Term) -> Maybe (Elim' Term) -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe (Elim' Term)
    forall a. [a] -> Maybe a
    listToMaybe (Elims -> Maybe (Elim' Term)) -> Elims -> Maybe (Elim' Term)
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    drop Int
    i Elims
    args
          in Term
    v Term -> Elims -> Term
    `app` Elims
    es

      -- -- Andreas, 2016-07-20 futile attempt to magically fix ProjOrigin
      --     fallback = v
      -- in  if not $ null es then applyE v es else
      --     -- If we have no more eliminations, we can return v
      --     if o == ProjSystem then fallback else
      --       -- If the result is a projected term with ProjSystem,
      --       -- we can can restore it to ProjOrigin o.
      --       -- Otherwise, we get unpleasant printing with eta-expanded record metas.
      --     caseMaybe (hasElims v) fallback $ \ (hd, es0) ->
      --       caseMaybe (initLast es0) fallback $ \ (es1, e2) ->
      --         case e2 of
      --           -- We want to replace this ProjSystem by o.
      --           Proj ProjSystem q -> hd (es1 ++ [Proj o q])
      --             -- Andreas, 2016-07-21 for the whole testsuite
      --             -- this case was never triggered!
      --           _ -> fallback

    {-
          i = maybe failure id    $ elemIndex f $ map unArg fs
          v = maybe failure unArg $ listToMaybe $ drop i args
          -- Andreas, 2013-10-20 see Issue543a:
          -- protect result of irrelevant projection.
          r = maybe __IMPOSSIBLE__ getRelevance $ listToMaybe $ drop i fs
          u | Irrelevant <- r = DontCare v
            | otherwise       = v
      in  applyE v es
    -}

    -- | @defApp f us vs@ applies @Def f us@ to further arguments @vs@,
    --   eliminating top projection redexes.
    --   If @us@ is not empty, we cannot have a projection redex, since
    --   the record argument is the first one.
    defApp :: QName -> Elims -> Elims -> Term
    defApp :: QName -> Elims -> Elims -> Term
    defApp QName
    f [] (Apply Arg Term
    a : Elims
    es) | Just Arg Term
    v <- QName -> Term -> Maybe (Arg Term)
    canProject QName
    f (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a)
      = Arg Term -> Term
    argToDontCare Arg Term
    v Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es
    defApp QName
    f Elims
    es0 Elims
    es = QName -> Elims -> Term
    Def QName
    f (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims
    es0 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es

    -- protect irrelevant fields (see issue 610)
    argToDontCare :: Arg Term -> Term
    argToDontCare :: Arg Term -> Term
    argToDontCare (Arg ArgInfo
    ai Term
    v) = ArgInfo -> Term -> Term
    forall a. LensRelevance a => a -> Term -> Term
    relToDontCare ArgInfo
    ai Term
    v

    relToDontCare :: LensRelevance a => a -> Term -> Term
    relToDontCare :: forall a. LensRelevance a => a -> Term -> Term
    relToDontCare a
    ai = Bool -> (Term -> Term) -> Term -> Term
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (a -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant a
    ai) Term -> Term
    dontCare

    -- Andreas, 2016-01-19: In connection with debugging issue #1783,
    -- I consider the Apply instance for Type harmful, as piApply is not
    -- safe if the type is not sufficiently reduced.
    -- (piApply is not in the monad and hence cannot unfold type synonyms).
    --
    -- Without apply for types, one has to at least use piApply and be
    -- aware of doing something which has a precondition
    -- (type sufficiently reduced).
    --
    -- By grepping for piApply, one can quickly get an overview over
    -- potentially harmful uses.
    --
    -- In general, piApplyM is preferable over piApply since it is more robust
    -- and fails earlier than piApply, which may only fail at serialization time,
    -- when all thunks are forced.

    -- REMOVED:
    -- instance Apply Type where
    --   apply = piApply
    --   -- Maybe an @applyE@ instance would be useful here as well.
    --   -- A record type could be applied to a projection name
    --   -- to yield the field type.
    --   -- However, this works only in the monad where we can
    --   -- look up the fields of a record type.

    instance Apply Sort where
      applyE :: Sort -> Elims -> Sort
    applyE Sort
    s [] = Sort
    s
      applyE Sort
    s Elims
    es = case Sort
    s of
        MetaS MetaId
    x Elims
    es' -> MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x (Elims -> Sort) -> Elims -> Sort
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es
        DefS  QName
    d Elims
    es' -> QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS  QName
    d (Elims -> Sort) -> Elims -> Sort
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es
        Sort
    _ -> Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- @applyE@ does not make sense for telecopes, definitions, clauses etc.

    instance TermSubst a => Apply (Tele a) where
      apply :: Tele a -> Args -> Tele a
    apply Tele a
    tel               []       = Tele a
    tel
      apply Tele a
    EmptyTel          Args
    _        = Tele a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      apply (ExtendTel a
    _ Abs (Tele a)
    tel) (Arg Term
    t : Args
    ts) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp Abs (Tele a)
    tel (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t) Tele a -> Args -> Tele a
    forall t. Apply t => t -> Args -> t
    `apply` Args
    ts

      applyE :: Tele a -> Elims -> Tele a
    applyE Tele a
    t Elims
    es = Tele a -> Args -> Tele a
    forall t. Apply t => t -> Args -> t
    apply Tele a
    t (Args -> Tele a) -> Args -> Tele a
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply Definition where
      apply :: Definition -> Args -> Definition
    apply (Defn ArgInfo
    info QName
    x Type
    t [Polarity]
    pol [Occurrence]
    occ [Maybe Name]
    gpars [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe InstanceInfo
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang Defn
    d) Args
    args =
        ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe InstanceInfo
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn ArgInfo
    info QName
    x (Type -> Args -> Type
    piApply Type
    t Args
    args) ([Polarity] -> Args -> [Polarity]
    forall t. Apply t => t -> Args -> t
    apply [Polarity]
    pol Args
    args) ([Occurrence] -> Args -> [Occurrence]
    forall t. Apply t => t -> Args -> t
    apply [Occurrence]
    occ Args
    args) (Int -> [Maybe Name] -> [Maybe Name]
    forall a. Int -> [a] -> [a]
    drop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [Maybe Name]
    gpars) [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe InstanceInfo
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang (Defn -> Args -> Defn
    forall t. Apply t => t -> Args -> t
    apply Defn
    d Args
    args)

      applyE :: Definition -> Elims -> Definition
    applyE Definition
    t Elims
    es = Definition -> Args -> Definition
    forall t. Apply t => t -> Args -> t
    apply Definition
    t (Args -> Definition) -> Args -> Definition
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply RewriteRule where
      apply :: RewriteRule -> Args -> RewriteRule
    apply RewriteRule
    r Args
    args =
        let newContext :: Telescope
    newContext = Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    apply (RewriteRule -> Telescope
    rewContext RewriteRule
    r) Args
    args
            sub :: Substitution' NLPat
    sub        = Int -> Substitution' NLPat -> Substitution' NLPat
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    newContext) (Substitution' NLPat -> Substitution' NLPat)
    -> Substitution' NLPat -> Substitution' NLPat
    forall a b. (a -> b) -> a -> b
    $ [NLPat] -> Substitution' NLPat
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([NLPat] -> Substitution' NLPat) -> [NLPat] -> Substitution' NLPat
    forall a b. (a -> b) -> a -> b
    $
                           [NLPat] -> [NLPat]
    forall a. [a] -> [a]
    reverse ([NLPat] -> [NLPat]) -> [NLPat] -> [NLPat]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> NLPat) -> Args -> [NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> NLPat
    PTerm (Term -> NLPat) -> (Arg Term -> Term) -> Arg Term -> NLPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) Args
    args
        in RewriteRule
           { rewName :: QName
    rewName    = RewriteRule -> QName
    rewName RewriteRule
    r
           , rewContext :: Telescope
    rewContext = Telescope
    newContext
           , rewHead :: QName
    rewHead    = RewriteRule -> QName
    rewHead RewriteRule
    r
           , rewPats :: PElims
    rewPats    = Substitution' (SubstArg PElims) -> PElims -> PElims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg PElims)
    Substitution' NLPat
    sub (RewriteRule -> PElims
    rewPats RewriteRule
    r)
           , rewRHS :: Term
    rewRHS     = Substitution' NLPat -> Term -> Term
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' NLPat
    sub (RewriteRule -> Term
    rewRHS RewriteRule
    r)
           , rewType :: Type
    rewType    = Substitution' NLPat -> Type -> Type
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' NLPat
    sub (RewriteRule -> Type
    rewType RewriteRule
    r)
           , rewFromClause :: Bool
    rewFromClause = RewriteRule -> Bool
    rewFromClause RewriteRule
    r
           , rewTopModule :: TopLevelModuleName
    rewTopModule  = RewriteRule -> TopLevelModuleName
    rewTopModule RewriteRule
    r
           }

      applyE :: RewriteRule -> Elims -> RewriteRule
    applyE RewriteRule
    t Elims
    es = RewriteRule -> Args -> RewriteRule
    forall t. Apply t => t -> Args -> t
    apply RewriteRule
    t (Args -> RewriteRule) -> Args -> RewriteRule
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
      apply :: [Occurrence] -> Args -> [Occurrence]
    apply [Occurrence]
    occ Args
    args = Int -> [Occurrence] -> [Occurrence]
    forall a. Int -> [a] -> [a]
    List.drop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [Occurrence]
    occ
      applyE :: [Occurrence] -> Elims -> [Occurrence]
    applyE [Occurrence]
    t Elims
    es = [Occurrence] -> Args -> [Occurrence]
    forall t. Apply t => t -> Args -> t
    apply [Occurrence]
    t (Args -> [Occurrence]) -> Args -> [Occurrence]
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance {-# OVERLAPPING #-} Apply [Polarity] where
      apply :: [Polarity] -> Args -> [Polarity]
    apply [Polarity]
    pol Args
    args = Int -> [Polarity] -> [Polarity]
    forall a. Int -> [a] -> [a]
    List.drop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [Polarity]
    pol
      applyE :: [Polarity] -> Elims -> [Polarity]
    applyE [Polarity]
    t Elims
    es = [Polarity] -> Args -> [Polarity]
    forall t. Apply t => t -> Args -> t
    apply [Polarity]
    t (Args -> [Polarity]) -> Args -> [Polarity]
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply NumGeneralizableArgs where
      apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs
    apply NumGeneralizableArgs
    NoGeneralizableArgs       Args
    args = NumGeneralizableArgs
    NoGeneralizableArgs
      apply (SomeGeneralizableArgs Int
    n) Args
    args = Int -> NumGeneralizableArgs
    SomeGeneralizableArgs (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args)
      applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs
    applyE NumGeneralizableArgs
    t Elims
    es = NumGeneralizableArgs -> Args -> NumGeneralizableArgs
    forall t. Apply t => t -> Args -> t
    apply NumGeneralizableArgs
    t (Args -> NumGeneralizableArgs) -> Args -> NumGeneralizableArgs
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    -- | Make sure we only drop variable patterns.
    instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
      apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
    apply [NamedArg (Pattern' a)]
    ps Args
    args = Int -> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
    forall {t} {x}.
    (Eq t, Num t) =>
    t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    loop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [NamedArg (Pattern' a)]
    ps
        where
        loop :: t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    loop t
    0 [NamedArg (Pattern' x)]
    ps = [NamedArg (Pattern' x)]
    ps
        loop t
    n [] = [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        loop t
    n (NamedArg (Pattern' x)
    p : [NamedArg (Pattern' x)]
    ps) =
          let recurse :: [NamedArg (Pattern' x)]
    recurse = t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    loop (t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1) [NamedArg (Pattern' x)]
    ps
          in  case NamedArg (Pattern' x) -> Pattern' x
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' x)
    p of
                VarP{}  -> [NamedArg (Pattern' x)]
    recurse
                DotP{}  -> [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                LitP{}  -> [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ConP{}  -> [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                DefP{}  -> [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ProjP{} -> [NamedArg (Pattern' x)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                IApplyP{} -> [NamedArg (Pattern' x)]
    recurse

      applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]
    applyE [NamedArg (Pattern' a)]
    t Elims
    es = [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
    forall t. Apply t => t -> Args -> t
    apply [NamedArg (Pattern' a)]
    t (Args -> [NamedArg (Pattern' a)])
    -> Args -> [NamedArg (Pattern' a)]
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply Projection where
      apply :: Projection -> Args -> Projection
    apply Projection
    p Args
    args = Projection
    p
        { projIndex = projIndex p - size args
        , projLams  = projLams p `apply` args
        }
      applyE :: Projection -> Elims -> Projection
    applyE Projection
    t Elims
    es = Projection -> Args -> Projection
    forall t. Apply t => t -> Args -> t
    apply Projection
    t (Args -> Projection) -> Args -> Projection
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply ProjLams where
      apply :: ProjLams -> Args -> ProjLams
    apply (ProjLams [Arg [Char]]
    lams) Args
    args = [Arg [Char]] -> ProjLams
    ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg [Char]] -> [Arg [Char]]
    forall a. Int -> [a] -> [a]
    List.drop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [Arg [Char]]
    lams
      applyE :: ProjLams -> Elims -> ProjLams
    applyE ProjLams
    t Elims
    es = ProjLams -> Args -> ProjLams
    forall t. Apply t => t -> Args -> t
    apply ProjLams
    t (Args -> ProjLams) -> Args -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply Defn where
      apply :: Defn -> Args -> Defn
    apply Defn
    d [] = Defn
    d
      apply Defn
    d args :: Args
    args@(Arg Term
    arg1:Args
    args1) = case Defn
    d of
        Axiom{} -> Defn
    d
        DataOrRecSig Int
    n -> Int -> Defn
    DataOrRecSig (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args)
        GeneralizableVar NumGeneralizableArgs
    gv -> NumGeneralizableArgs -> Defn
    GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
    forall a b. (a -> b) -> a -> b
    $ NumGeneralizableArgs -> Args -> NumGeneralizableArgs
    forall t. Apply t => t -> Args -> t
    apply NumGeneralizableArgs
    gv Args
    args
        AbstractDefn Defn
    d -> Defn -> Defn
    AbstractDefn (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $ Defn -> Args -> Defn
    forall t. Apply t => t -> Args -> t
    apply Defn
    d Args
    args
        Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc, funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cov, funInv :: Defn -> FunctionInverse
    funInv = FunctionInverse
    inv
                , funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    extLam
                , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    _ } ->
          Defn
    d { funClauses    = apply cs args
            , funCompiled   = apply cc args
            , funCovering   = apply cov args
            , funInv        = apply inv args
            , funExtLam     = modifySystem (`apply` args) <$> extLam
            }

        Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc, funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cov, funInv :: Defn -> FunctionInverse
    funInv = FunctionInverse
    inv
                , funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    extLam
                , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    p0 } ->
          case Projection
    p0 Projection -> Args -> Projection
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args of
            p :: Projection
    p@Projection{ projIndex :: Projection -> Int
    projIndex = Int
    n }
              | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0     -> Defn
    d { funProjection = __IMPOSSIBLE__ } -- TODO (#3123): we actually get here!
              -- case: applied only to parameters
              | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0     -> Defn
    d { funProjection = Right p }
              -- case: applied also to record value (n == 0)
              | Bool
    otherwise ->
                  Defn
    d { funClauses        = apply cs args'
                    , funCompiled       = apply cc args'
                    , funCovering       = apply cov args'
                    , funInv            = apply inv args'
                    , funProjection     = if isVar0 then Right p{ projIndex = 0 } else Left MaybeProjection
                    , funExtLam         = modifySystem (\ System
    _ -> System
    forall a. HasCallStack => a
    __IMPOSSIBLE__) <$> extLam
                    }
                  where
                    larg :: Arg Term
    larg  = Arg Term -> Args -> Arg Term
    forall a. a -> [a] -> a
    last1 Arg Term
    arg1 Args
    args1 -- the record value
                    args' :: Args
    args' = [Arg Term
    larg]
                    isVar0 :: Bool
    isVar0 = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    larg of Var Int
    0 [] -> Bool
    True; Term
    _ -> Bool
    False

        Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl } ->
          Defn
    d { dataPars = np - size args
            , dataClause     = apply cl args
            }
        Record{ recPars :: Defn -> Int
    recPars = Int
    np, recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recTel :: Defn -> Telescope
    recTel = Telescope
    tel
              {-, recArgOccurrences = occ-} } ->
          Defn
    d { recPars = np - size args
            , recClause = apply cl args, recTel = apply tel args
    --        , recArgOccurrences = List.drop (length args) occ
            }
        Constructor{ conPars :: Defn -> Int
    conPars = Int
    np } ->
          Defn
    d { conPars = np - size args }
        Primitive{ primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cs } ->
          Defn
    d { primClauses = apply cs args }
        PrimitiveSort{} -> Defn
    d

      applyE :: Defn -> Elims -> Defn
    applyE Defn
    t Elims
    es = Defn -> Args -> Defn
    forall t. Apply t => t -> Args -> t
    apply Defn
    t (Args -> Defn) -> Args -> Defn
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply PrimFun where
      apply :: PrimFun -> Args -> PrimFun
    apply (PrimFun QName
    x Int
    ar [Occurrence]
    occs Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def) Args
    args =
        QName
    -> Int
    -> [Occurrence]
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    PrimFun QName
    x (Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) (Int -> [Occurrence] -> [Occurrence]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Occurrence]
    occs) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
     -> PrimFun)
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \ Args
    vs -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def (Args
    args Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    vs)
        where
        n :: Int
    n = Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args
      applyE :: PrimFun -> Elims -> PrimFun
    applyE PrimFun
    t Elims
    es = PrimFun -> Args -> PrimFun
    forall t. Apply t => t -> Args -> t
    apply PrimFun
    t (Args -> PrimFun) -> Args -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply Clause where
        -- This one is a little bit tricksy after the parameter refinement change.
        -- It is assumed that we only apply a clause to "parameters", i.e.
        -- arguments introduced by lambda lifting. The problem is that these aren't
        -- necessarily the first elements of the clause telescope.
        apply :: Clause -> Args -> Clause
    apply cls :: Clause
    cls@(Clause Range
    rl Range
    rf Telescope
    tel [NamedArg DeBruijnPattern]
    ps Maybe Term
    b Maybe (Arg Type)
    t Catchall
    catchall Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell Maybe ModuleName
    wm) Args
    args
          | Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > [NamedArg DeBruijnPattern] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg DeBruijnPattern]
    ps = Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          | Bool
    otherwise =
          Range
    -> Range
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause Range
    rl Range
    rf
                 Telescope
    tel'
                 (Substitution' (SubstArg [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst PatternSubstitution
    Substitution' (SubstArg [NamedArg DeBruijnPattern])
    rhoP ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    drop (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [NamedArg DeBruijnPattern]
    ps)
                 (Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Maybe Term))
    rho Maybe Term
    b)
                 (Substitution' (SubstArg (Maybe (Arg Type)))
    -> Maybe (Arg Type) -> Maybe (Arg Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Maybe (Arg Type)))
    rho Maybe (Arg Type)
    t)
                 Catchall
    catchall
                 Maybe Bool
    recursive
                 Maybe Bool
    unreachable
                 ExpandedEllipsis
    ell
                 Maybe ModuleName
    wm
          where
            -- We have
            --  Γ ⊢ args, for some outer context Γ
            --  Δ ⊢ ps,   where Δ is the clause telescope (tel)
            rargs :: [Term]
    rargs = (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (Args -> [Term]) -> Args -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Args -> Args
    forall a. [a] -> [a]
    reverse Args
    args
            rps :: [NamedArg DeBruijnPattern]
    rps   = [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a]
    reverse ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    take (Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [NamedArg DeBruijnPattern]
    ps
            n :: Int
    n     = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel

            -- This is the new telescope. Created by substituting the args into the
            -- appropriate places in the old telescope. We know where those are by
            -- looking at the deBruijn indices of the patterns.
            tel' :: Telescope
    tel' = Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel Int
    n Telescope
    tel [NamedArg DeBruijnPattern]
    rps [Term]
    rargs

            -- We then have to create a substitution from the old telescope to the
            -- new telescope that we can apply to dot patterns and the clause body.
            rhoP :: PatternSubstitution
            rhoP :: PatternSubstitution
    rhoP = (Term -> DeBruijnPattern)
    -> Int
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> PatternSubstitution
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> DeBruijnPattern
    forall a. Term -> Pattern' a
    dotP Int
    n [NamedArg DeBruijnPattern]
    rps [Term]
    rargs
            rho :: Substitution' Term
    rho  = (Term -> Term)
    -> Int
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Substitution' Term
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> Term
    forall a. a -> a
    id   Int
    n [NamedArg DeBruijnPattern]
    rps [Term]
    rargs

            substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
            substP :: Int
    -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    substP Int
    i Term
    v = Int
    -> SubstArg [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    i (Term -> DeBruijnPattern
    forall a. Term -> Pattern' a
    dotP Term
    v)

            -- Building the substitution from the old telescope to the new. The
            -- interesting case is when we have a variable pattern:
            --  We need Δ′ ⊢ ρ : Δ
            --  where Δ′ = newTel Δ (xⁱ : ps) (v : vs)
            --           = newTel Δ[xⁱ:=v] ps[xⁱ:=v'] vs
            --  Note that we need v' = raise (|Δ| - 1) v, to make Γ ⊢ v valid in
            --  ΓΔ[xⁱ:=v].
            --  A recursive call ρ′ = mkSub (substP i v' ps) vs gets us
            --    Δ′ ⊢ ρ′ : Δ[xⁱ:=v]
            --  so we just need Δ[xⁱ:=v] ⊢ σ : Δ and then ρ = ρ′ ∘ σ.
            --  That's achieved by σ = singletonS i v'.
            mkSub :: EndoSubst a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
            mkSub :: forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> a
    _ Int
    _ [] [] = Substitution' a
    forall a. Substitution' a
    idS
            mkSub Term -> a
    tm Int
    n (NamedArg DeBruijnPattern
    p : [NamedArg DeBruijnPattern]
    ps) (Term
    v : [Term]
    vs) =
              case NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NamedArg DeBruijnPattern
    p of
                VarP PatternInfo
    _ (DBPatVar [Char]
    _ Int
    i) -> (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> a
    tm (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int
    -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    substP Int
    i Term
    v' [NamedArg DeBruijnPattern]
    ps) [Term]
    vs Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> a -> Substitution' a
    forall a. DeBruijn a => Int -> a -> Substitution' a
    singletonS Int
    i (Term -> a
    tm Term
    v')
                  where v' :: Term
    v' = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    v
                DotP{}  -> (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> a
    tm Int
    n [NamedArg DeBruijnPattern]
    ps [Term]
    vs
                ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    ps' -> (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> a
    tm Int
    n ([NamedArg DeBruijnPattern]
    ps' [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    ps) (ConHead -> Term -> [Term]
    projections ConHead
    c Term
    v [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    vs)
                DefP{}  -> Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                LitP{}  -> Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ProjP{} -> Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                IApplyP PatternInfo
    _ Term
    _ Term
    _ (DBPatVar [Char]
    _ Int
    i) -> (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    forall a.
    EndoSubst a =>
    (Term -> a)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
    mkSub Term -> a
    tm (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int
    -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    substP Int
    i Term
    v' [NamedArg DeBruijnPattern]
    ps) [Term]
    vs Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> a -> Substitution' a
    forall a. DeBruijn a => Int -> a -> Substitution' a
    singletonS Int
    i (Term -> a
    tm Term
    v')
                  where v' :: Term
    v' = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    v
            mkSub Term -> a
    _ Int
    _ [NamedArg DeBruijnPattern]
    _ [Term]
    _ = Substitution' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- The parameter patterns 'ps' are all variables or dot patterns, or eta
            -- expanded record patterns (issue #2550). If they are variables they
            -- can appear anywhere in the clause telescope. This function
            -- constructs the new telescope with 'vs' substituted for 'ps'.
            -- Example:
            --    tel = (x : A) (y : B) (z : C) (w : D)
            --    ps  = y@3 w@0
            --    vs  = u v
            --    newTel tel ps vs = (x : A) (z : C[u/y])
            newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
            newTel :: Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel Int
    n Telescope
    tel [] [] = Telescope
    tel
            newTel Int
    n Telescope
    tel (NamedArg DeBruijnPattern
    p : [NamedArg DeBruijnPattern]
    ps) (Term
    v : [Term]
    vs) =
              case NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NamedArg DeBruijnPattern
    p of
                VarP PatternInfo
    _ (DBPatVar [Char]
    _ Int
    i) -> Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int -> SubstArg (Dom Type) -> Telescope -> Telescope
    forall {t} {a}.
    (Eq t, Num t, Subst a, Subst (SubstArg a)) =>
    t -> SubstArg a -> Tele a -> Tele a
    subTel (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) Term
    SubstArg (Dom Type)
    v Telescope
    tel) (Int
    -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    substP Int
    i (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    v) [NamedArg DeBruijnPattern]
    ps) [Term]
    vs
                DotP{}              -> Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel Int
    n Telescope
    tel [NamedArg DeBruijnPattern]
    ps [Term]
    vs
                ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    ps'        -> Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel Int
    n Telescope
    tel ([NamedArg DeBruijnPattern]
    ps' [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    ps) (ConHead -> Term -> [Term]
    projections ConHead
    c Term
    v [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    vs)
                DefP{}  -> Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                LitP{}  -> Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ProjP{} -> Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                IApplyP PatternInfo
    _ Term
    _ Term
    _ (DBPatVar [Char]
    _ Int
    i) -> Int
    -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
    newTel (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int -> SubstArg (Dom Type) -> Telescope -> Telescope
    forall {t} {a}.
    (Eq t, Num t, Subst a, Subst (SubstArg a)) =>
    t -> SubstArg a -> Tele a -> Tele a
    subTel (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i) Term
    SubstArg (Dom Type)
    v Telescope
    tel) (Int
    -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    substP Int
    i (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Term
    v) [NamedArg DeBruijnPattern]
    ps) [Term]
    vs
            newTel Int
    _ Telescope
    tel [NamedArg DeBruijnPattern]
    _ [Term]
    _ = Telescope
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            projections :: ConHead -> Term -> [Term]
            projections :: ConHead -> Term -> [Term]
    projections ConHead
    c Term
    v = [ ArgInfo -> Term -> Term
    forall a. LensRelevance a => a -> Term -> Term
    relToDontCare ArgInfo
    ai (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $
                                -- #4528: We might have bogus terms here when printing a clause that
                                --        cannot be taken. To mitigate the problem we use a Def instead
                                --        a Proj elim for data constructors, which at least stops conApp
                                --        from crashing. See #4989 for not printing bogus terms at all.
                                case ConHead -> DataOrRecord
    conDataRecord ConHead
    c of
                                  DataOrRecord
    IsData     -> QName -> Elims -> Elims -> Term
    defApp QName
    f [] [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    v)]
                                                  -- Andreas, 2022-06-10, issue #5922.
                                                  -- This was @Def f [Apply (Arg ai v)]@, but are we sure
                                                  -- that @v@ isn't a matching @Con@?  The testcase for
                                                  -- #5922 does not require this precaution,
                                                  -- but I sleep better this way...
                                  IsRecord{} -> Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE Term
    v [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
                              | Arg ArgInfo
    ai QName
    f <- ConHead -> [Arg QName]
    conFields ConHead
    c ]

            -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v]
            subTel :: t -> SubstArg a -> Tele a -> Tele a
    subTel t
    i SubstArg a
    v Tele a
    EmptyTel = Tele a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            subTel t
    0 SubstArg a
    v (ExtendTel a
    _ Abs (Tele a)
    tel) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs (Tele a)
    tel SubstArg a
    SubstArg (Tele a)
    v
            subTel t
    i SubstArg a
    v (ExtendTel a
    a Abs (Tele a)
    tel) = a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel a
    a (Abs (Tele a) -> Tele a) -> Abs (Tele a) -> Tele a
    forall a b. (a -> b) -> a -> b
    $ t -> SubstArg a -> Tele a -> Tele a
    subTel (t
    i t -> t -> t
    forall a. Num a => a -> a -> a
    - t
    1) (Int -> SubstArg a -> SubstArg a
    forall a. Subst a => Int -> a -> a
    raise Int
    1 SubstArg a
    v) (Tele a -> Tele a) -> Abs (Tele a) -> Abs (Tele a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (Tele a)
    tel

        applyE :: Clause -> Elims -> Clause
    applyE Clause
    t Elims
    es = Clause -> Args -> Clause
    forall t. Apply t => t -> Args -> t
    apply Clause
    t (Args -> Clause) -> Args -> Clause
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply CompiledClauses where
      apply :: CompiledClauses -> Args -> CompiledClauses
    apply CompiledClauses
    cc Args
    args = case CompiledClauses
    cc of
        Fail [Arg [Char]]
    hs -> [Arg [Char]] -> CompiledClauses
    forall a. [Arg [Char]] -> CompiledClauses' a
    Fail (Int -> [Arg [Char]] -> [Arg [Char]]
    forall a. Int -> [a] -> [a]
    drop Int
    len [Arg [Char]]
    hs)
        Done [Arg [Char]]
    hs Term
    t
          | [Arg [Char]] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    hs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    len ->
             let sub :: Substitution' Term
    sub = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    var [Int
    0..[Arg [Char]] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    hs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1] [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    args
             in  [Arg [Char]] -> Term -> CompiledClauses
    forall a. [Arg [Char]] -> a -> CompiledClauses' a
    Done (Int -> [Arg [Char]] -> [Arg [Char]]
    forall a. Int -> [a] -> [a]
    List.drop Int
    len [Arg [Char]]
    hs) (Term -> CompiledClauses) -> Term -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Term)
    sub Term
    t
          | Bool
    otherwise -> CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Case Arg Int
    n Case CompiledClauses
    bs
          | Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    len -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case (Arg Int
    n Arg Int -> (Int -> Int) -> Arg Int
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Int
    m -> Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    len) (Case CompiledClauses -> Args -> Case CompiledClauses
    forall t. Apply t => t -> Args -> t
    apply Case CompiledClauses
    bs Args
    args)
          | Bool
    otherwise -> CompiledClauses
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        where
          len :: Int
    len = Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args
      applyE :: CompiledClauses -> Elims -> CompiledClauses
    applyE CompiledClauses
    t Elims
    es = CompiledClauses -> Args -> CompiledClauses
    forall t. Apply t => t -> Args -> t
    apply CompiledClauses
    t (Args -> CompiledClauses) -> Args -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply ExtLamInfo where
      apply :: ExtLamInfo -> Args -> ExtLamInfo
    apply (ExtLamInfo ModuleName
    m Bool
    b Maybe System
    sys) Args
    args = ModuleName -> Bool -> Maybe System -> ExtLamInfo
    ExtLamInfo ModuleName
    m Bool
    b (Maybe System -> Args -> Maybe System
    forall t. Apply t => t -> Args -> t
    apply Maybe System
    sys Args
    args)
      applyE :: ExtLamInfo -> Elims -> ExtLamInfo
    applyE ExtLamInfo
    t Elims
    es = ExtLamInfo -> Args -> ExtLamInfo
    forall t. Apply t => t -> Args -> t
    apply ExtLamInfo
    t (Args -> ExtLamInfo) -> Args -> ExtLamInfo
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply System where
      -- We assume we apply a system only to arguments introduced by
      -- lambda lifting.
      apply :: System -> Args -> System
    apply (System Telescope
    tel [(Face, Term)]
    sys) Args
    args
          = if Int
    nargs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    ntel then System
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            else Telescope -> [(Face, Term)] -> System
    System Telescope
    newTel (((Face, Term) -> (Face, Term)) -> [(Face, Term)] -> [(Face, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Term, Bool) -> (Term, Bool)) -> Face -> Face
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> Term
    f (Term -> Term) -> (Bool -> Bool) -> (Term, Bool) -> (Term, Bool)
    forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    -*- Bool -> Bool
    forall a. a -> a
    id) (Face -> Face) -> (Term -> Term) -> (Face, Term) -> (Face, Term)
    forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
    -*- Term -> Term
    f) [(Face, Term)]
    sys)

        where
          f :: Term -> Term
    f = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Term)
    sigma
          nargs :: Int
    nargs = Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args
          ntel :: Int
    ntel = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
          newTel :: Telescope
    newTel = Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    apply Telescope
    tel Args
    args
          -- newTel ⊢ σ : tel
          sigma :: Substitution' Term
    sigma = Int -> Substitution' Term -> Substitution' Term
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Int
    ntel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    nargs) ([Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    args))

      applyE :: System -> Elims -> System
    applyE System
    t Elims
    es = System -> Args -> System
    forall t. Apply t => t -> Args -> t
    apply System
    t (Args -> System) -> Args -> System
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply a => Apply (WithArity a) where
      apply :: WithArity a -> Args -> WithArity a
    apply  (WithArity Int
    n a
    a) Args
    args = Int -> a -> WithArity a
    forall c. Int -> c -> WithArity c
    WithArity Int
    n (a -> WithArity a) -> a -> WithArity a
    forall a b. (a -> b) -> a -> b
    $ a -> Args -> a
    forall t. Apply t => t -> Args -> t
    apply  a
    a Args
    args
      applyE :: WithArity a -> Elims -> WithArity a
    applyE (WithArity Int
    n a
    a) Elims
    es   = Int -> a -> WithArity a
    forall c. Int -> c -> WithArity c
    WithArity Int
    n (a -> WithArity a) -> a -> WithArity a
    forall a b. (a -> b) -> a -> b
    $ a -> Elims -> a
    forall t. Apply t => t -> Elims -> t
    applyE a
    a Elims
    es

    instance Apply a => Apply (Case a) where
      apply :: Case a -> Args -> Case a
    apply (Branches Bool
    cop Map QName (WithArity a)
    cs Maybe (ConHead, WithArity a)
    eta Map Literal a
    ls Maybe a
    m Maybe Bool
    b Bool
    lz) Args
    args =
        Bool
    -> Map QName (WithArity a)
    -> Maybe (ConHead, WithArity a)
    -> Map Literal a
    -> Maybe a
    -> Maybe Bool
    -> Bool
    -> Case a
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    cop (Map QName (WithArity a) -> Args -> Map QName (WithArity a)
    forall t. Apply t => t -> Args -> t
    apply Map QName (WithArity a)
    cs Args
    args) ((WithArity a -> WithArity a)
    -> (ConHead, WithArity a) -> (ConHead, WithArity a)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (WithArity a -> Args -> WithArity a
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) ((ConHead, WithArity a) -> (ConHead, WithArity a))
    -> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ConHead, WithArity a)
    eta) (Map Literal a -> Args -> Map Literal a
    forall t. Apply t => t -> Args -> t
    apply Map Literal a
    ls Args
    args) (Maybe a -> Args -> Maybe a
    forall t. Apply t => t -> Args -> t
    apply Maybe a
    m Args
    args) Maybe Bool
    b Bool
    lz
      applyE :: Case a -> Elims -> Case a
    applyE (Branches Bool
    cop Map QName (WithArity a)
    cs Maybe (ConHead, WithArity a)
    eta Map Literal a
    ls Maybe a
    m Maybe Bool
    b Bool
    lz) Elims
    es =
        Bool
    -> Map QName (WithArity a)
    -> Maybe (ConHead, WithArity a)
    -> Map Literal a
    -> Maybe a
    -> Maybe Bool
    -> Bool
    -> Case a
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    cop (Map QName (WithArity a) -> Elims -> Map QName (WithArity a)
    forall t. Apply t => t -> Elims -> t
    applyE Map QName (WithArity a)
    cs Elims
    es) ((WithArity a -> WithArity a)
    -> (ConHead, WithArity a) -> (ConHead, WithArity a)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (WithArity a -> Elims -> WithArity a
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) ((ConHead, WithArity a) -> (ConHead, WithArity a))
    -> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ConHead, WithArity a)
    eta)(Map Literal a -> Elims -> Map Literal a
    forall t. Apply t => t -> Elims -> t
    applyE Map Literal a
    ls Elims
    es) (Maybe a -> Elims -> Maybe a
    forall t. Apply t => t -> Elims -> t
    applyE Maybe a
    m Elims
    es) Maybe Bool
    b Bool
    lz

    instance Apply FunctionInverse where
      apply :: FunctionInverse -> Args -> FunctionInverse
    apply FunctionInverse
    NotInjective  Args
    args = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
      apply (Inverse InversionMap Clause
    inv) Args
    args = InversionMap Clause -> FunctionInverse
    forall c. InversionMap c -> FunctionInverse' c
    Inverse (InversionMap Clause -> FunctionInverse)
    -> InversionMap Clause -> FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ InversionMap Clause -> Args -> InversionMap Clause
    forall t. Apply t => t -> Args -> t
    apply InversionMap Clause
    inv Args
    args

      applyE :: FunctionInverse -> Elims -> FunctionInverse
    applyE FunctionInverse
    t Elims
    es = FunctionInverse -> Args -> FunctionInverse
    forall t. Apply t => t -> Args -> t
    apply FunctionInverse
    t (Args -> FunctionInverse) -> Args -> FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Apply DisplayTerm where
      apply :: DisplayTerm -> Args -> DisplayTerm
    apply (DTerm' Term
    v Elims
    es)      Args
    args = Term -> Elims -> DisplayTerm
    DTerm' Term
    v       (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args
      apply (DDot' Term
    v Elims
    es)       Args
    args = Term -> Elims -> DisplayTerm
    DDot' Term
    v        (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args
      apply (DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    vs)     Args
    args = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci     ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ [Arg DisplayTerm]
    vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Arg DisplayTerm) -> Args -> [Arg DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Args
    args
      apply (DDef QName
    c [Elim' DisplayTerm]
    es)        Args
    args = QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    c        ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ [Elim' DisplayTerm]
    es [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg DisplayTerm -> Elim' DisplayTerm
    forall a. Arg a -> Elim' a
    Apply (Arg DisplayTerm -> Elim' DisplayTerm)
    -> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Args
    args
      apply (DWithApp DisplayTerm
    v List1 DisplayTerm
    ws Elims
    es) Args
    args = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp DisplayTerm
    v List1 DisplayTerm
    ws (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args

      applyE :: DisplayTerm -> Elims -> DisplayTerm
    applyE (DTerm' Term
    v Elims
    es')      Elims
    es = Term -> Elims -> DisplayTerm
    DTerm' Term
    v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es
      applyE (DDot' Term
    v Elims
    es')       Elims
    es = Term -> Elims -> DisplayTerm
    DDot' Term
    v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es
      applyE (DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    vs)      Elims
    es = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ [Arg DisplayTerm]
    vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Arg DisplayTerm) -> Args -> [Arg DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Args
    ws
        where ws :: Args
    ws = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
      applyE (DDef QName
    c [Elim' DisplayTerm]
    es')        Elims
    es = QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    c ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ [Elim' DisplayTerm]
    es' [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
    forall a b. (a -> b) -> Elim' a -> Elim' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Elims
    es
      applyE (DWithApp DisplayTerm
    v List1 DisplayTerm
    ws Elims
    es') Elims
    es = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp DisplayTerm
    v List1 DisplayTerm
    ws (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Elims
    es' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es

    instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where
      apply :: [t] -> Args -> [t]
    apply  [t]
    ts Args
    args = (t -> t) -> [t] -> [t]
    forall a b. (a -> b) -> [a] -> [b]
    map (t -> Args -> t
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) [t]
    ts
      applyE :: [t] -> Elims -> [t]
    applyE [t]
    ts Elims
    es   = (t -> t) -> [t] -> [t]
    forall a b. (a -> b) -> [a] -> [b]
    map (t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) [t]
    ts

    instance Apply t => Apply (Blocked t) where
      apply :: Blocked t -> Args -> Blocked t
    apply  Blocked t
    b Args
    args = (t -> t) -> Blocked t -> Blocked t
    forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Args -> t
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) Blocked t
    b
      applyE :: Blocked t -> Elims -> Blocked t
    applyE Blocked t
    b Elims
    es   = (t -> t) -> Blocked t -> Blocked t
    forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) Blocked t
    b

    instance Apply t => Apply (Maybe t) where
      apply :: Maybe t -> Args -> Maybe t
    apply  Maybe t
    x Args
    args = (t -> t) -> Maybe t -> Maybe t
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Args -> t
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) Maybe t
    x
      applyE :: Maybe t -> Elims -> Maybe t
    applyE Maybe t
    x Elims
    es   = (t -> t) -> Maybe t -> Maybe t
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) Maybe t
    x

    instance Apply t => Apply (Strict.Maybe t) where
      apply :: Maybe t -> Args -> Maybe t
    apply  Maybe t
    x Args
    args = (t -> t) -> Maybe t -> Maybe t
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Args -> t
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) Maybe t
    x
      applyE :: Maybe t -> Elims -> Maybe t
    applyE Maybe t
    x Elims
    es   = (t -> t) -> Maybe t -> Maybe t
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) Maybe t
    x

    instance Apply v => Apply (Map k v) where
      apply :: Map k v -> Args -> Map k v
    apply  Map k v
    x Args
    args = (v -> v) -> Map k v -> Map k v
    forall a b. (a -> b) -> Map k a -> Map k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (v -> Args -> v
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) Map k v
    x
      applyE :: Map k v -> Elims -> Map k v
    applyE Map k v
    x Elims
    es   = (v -> v) -> Map k v -> Map k v
    forall a b. (a -> b) -> Map k a -> Map k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (v -> Elims -> v
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) Map k v
    x

    instance Apply v => Apply (HashMap k v) where
      apply :: HashMap k v -> Args -> HashMap k v
    apply  HashMap k v
    x Args
    args = (v -> v) -> HashMap k v -> HashMap k v
    forall a b. (a -> b) -> HashMap k a -> HashMap k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (v -> Args -> v
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) HashMap k v
    x
      applyE :: HashMap k v -> Elims -> HashMap k v
    applyE HashMap k v
    x Elims
    es   = (v -> v) -> HashMap k v -> HashMap k v
    forall a b. (a -> b) -> HashMap k a -> HashMap k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (v -> Elims -> v
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es) HashMap k v
    x

    instance (Apply a, Apply b) => Apply (a,b) where
      apply :: (a, b) -> Args -> (a, b)
    apply  (a
    x,b
    y) Args
    args = (a -> Args -> a
    forall t. Apply t => t -> Args -> t
    apply  a
    x Args
    args, b -> Args -> b
    forall t. Apply t => t -> Args -> t
    apply  b
    y Args
    args)
      applyE :: (a, b) -> Elims -> (a, b)
    applyE (a
    x,b
    y) Elims
    es   = (a -> Elims -> a
    forall t. Apply t => t -> Elims -> t
    applyE a
    x Elims
    es  , b -> Elims -> b
    forall t. Apply t => t -> Elims -> t
    applyE b
    y Elims
    es  )

    instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
      apply :: (a, b, c) -> Args -> (a, b, c)
    apply  (a
    x,b
    y,c
    z) Args
    args = (a -> Args -> a
    forall t. Apply t => t -> Args -> t
    apply  a
    x Args
    args, b -> Args -> b
    forall t. Apply t => t -> Args -> t
    apply  b
    y Args
    args, c -> Args -> c
    forall t. Apply t => t -> Args -> t
    apply  c
    z Args
    args)
      applyE :: (a, b, c) -> Elims -> (a, b, c)
    applyE (a
    x,b
    y,c
    z) Elims
    es   = (a -> Elims -> a
    forall t. Apply t => t -> Elims -> t
    applyE a
    x Elims
    es  , b -> Elims -> b
    forall t. Apply t => t -> Elims -> t
    applyE b
    y Elims
    es  , c -> Elims -> c
    forall t. Apply t => t -> Elims -> t
    applyE c
    z Elims
    es  )

    instance DoDrop a => Apply (Drop a) where
      apply :: Drop a -> Args -> Drop a
    apply Drop a
    x Args
    args = Int -> Drop a -> Drop a
    forall a. DoDrop a => Int -> Drop a -> Drop a
    dropMore (Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args) Drop a
    x
      applyE :: Drop a -> Elims -> Drop a
    applyE Drop a
    t Elims
    es = Drop a -> Args -> Drop a
    forall t. Apply t => t -> Args -> t
    apply Drop a
    t (Args -> Drop a) -> Args -> Drop a
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance DoDrop a => Abstract (Drop a) where
      abstract :: Telescope -> Drop a -> Drop a
    abstract Telescope
    tel Drop a
    x = Int -> Drop a -> Drop a
    forall a. DoDrop a => Int -> Drop a -> Drop a
    unDrop (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Drop a
    x

    instance Apply Permutation where
      -- The permutation must start with [0..m - 1]
      -- NB: section (- m) not possible (unary minus), hence (flip (-) m)
      apply :: Permutation -> Args -> Permutation
    apply (Perm Int
    n [Int]
    xs) Args
    args = Int -> [Int] -> Permutation
    Perm (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    m) ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> Int -> Int) -> Int -> Int -> Int
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (-) Int
    m) ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    drop Int
    m [Int]
    xs
        where
          m :: Int
    m = Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args

      applyE :: Permutation -> Elims -> Permutation
    applyE Permutation
    t Elims
    es = Permutation -> Args -> Permutation
    forall t. Apply t => t -> Args -> t
    apply Permutation
    t (Args -> Permutation) -> Args -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es

    instance Abstract Permutation where
      abstract :: Telescope -> Permutation -> Permutation
    abstract Telescope
    tel (Perm Int
    n [Int]
    xs) = Int -> [Int] -> Permutation
    Perm (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    m) ([Int] -> Permutation) -> [Int] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [Int
    0..Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1] [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ (Int -> Int) -> [Int] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    m) [Int]
    xs
        where
          m :: Int
    m = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel

    -- | @(x:A)->B(x) `piApply` [u] = B(u)@
    --
    --   Precondition: The type must contain the right number of pis without
    --   having to perform any reduction.
    --
    --   @piApply@ is potentially unsafe, the monadic 'piApplyM' is preferable.
    piApply :: Type -> Args -> Type
    piApply :: Type -> Args -> Type
    piApply Type
    t []                      = Type
    t
    piApply (El Sort
    _ (Pi  Dom Type
    _ Abs Type
    b)) (Arg Term
    a:Args
    args) = Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    lazyAbsApp Abs Type
    b (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) Type -> Args -> Type
    `piApply` Args
    args
    piApply Type
    t Args
    args                    =
      [Char] -> Type -> Type
    forall a. [Char] -> a -> a
    trace ([Char]
    "piApply t = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n  args = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Args -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Args
    args) Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ---------------------------------------------------------------------------
    -- * Abstraction
    ---------------------------------------------------------------------------

    instance Abstract Term where
      abstract :: Telescope -> Term -> Term
    abstract = Telescope -> Term -> Term
    teleLam

    instance Abstract Type where
      abstract :: Telescope -> Type -> Type
    abstract = Telescope -> Type -> Type
    telePi_

    instance Abstract Sort where
      abstract :: Telescope -> Sort -> Sort
    abstract Telescope
    EmptyTel Sort
    s = Sort
    s
      abstract Telescope
    _        Sort
    s = Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Abstract Telescope where
      Telescope
    EmptyTel           abstract :: Telescope -> Telescope -> Telescope
    `abstract` Telescope
    tel = Telescope
    tel
      ExtendTel Dom Type
    arg Abs Telescope
    xtel `abstract` Telescope
    tel = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    arg (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Abs Telescope
    xtel Abs Telescope -> (Telescope -> Telescope) -> Abs Telescope
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    tel)

    instance Abstract Definition where
      abstract :: Telescope -> Definition -> Definition
    abstract Telescope
    tel (Defn ArgInfo
    info QName
    x Type
    t [Polarity]
    pol [Occurrence]
    occ [Maybe Name]
    gpars [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe InstanceInfo
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang Defn
    d) =
        ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe InstanceInfo
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn ArgInfo
    info QName
    x (Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Type
    t) (Telescope -> [Polarity] -> [Polarity]
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel [Polarity]
    pol) (Telescope -> [Occurrence] -> [Occurrence]
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel [Occurrence]
    occ)
          (Int -> Maybe Name -> [Maybe Name]
    forall a. Int -> a -> [a]
    replicate (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Maybe Name
    forall a. Maybe a
    Nothing [Maybe Name] -> [Maybe Name] -> [Maybe Name]
    forall a. [a] -> [a] -> [a]
    ++ [Maybe Name]
    gpars)
          [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe InstanceInfo
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang (Telescope -> Defn -> Defn
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Defn
    d)

    -- | @tel ⊢ (Γ ⊢ lhs ↦ rhs : t)@ becomes @tel, Γ ⊢ lhs ↦ rhs : t)@
    --   we do not need to change lhs, rhs, and t since they live in Γ.
    --   See 'Abstract Clause'.
    instance Abstract RewriteRule where
      abstract :: Telescope -> RewriteRule -> RewriteRule
    abstract Telescope
    tel (RewriteRule QName
    q Telescope
    gamma QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c TopLevelModuleName
    top) =
        QName
    -> Telescope
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> TopLevelModuleName
    -> RewriteRule
    RewriteRule QName
    q (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Telescope
    gamma) QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c TopLevelModuleName
    top

    instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
      abstract :: Telescope -> [Occurrence] -> [Occurrence]
    abstract Telescope
    tel []  = []
      abstract Telescope
    tel [Occurrence]
    occ = Int -> Occurrence -> [Occurrence]
    forall a. Int -> a -> [a]
    replicate (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Occurrence
    Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
    forall a. [a] -> [a] -> [a]
    ++ [Occurrence]
    occ -- TODO: check occurrence

    instance {-# OVERLAPPING #-} Abstract [Polarity] where
      abstract :: Telescope -> [Polarity] -> [Polarity]
    abstract Telescope
    tel []  = []
      abstract Telescope
    tel [Polarity]
    pol = Int -> Polarity -> [Polarity]
    forall a. Int -> a -> [a]
    replicate (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) Polarity
    Invariant [Polarity] -> [Polarity] -> [Polarity]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity]
    pol -- TODO: check polarity

    instance Abstract NumGeneralizableArgs where
      abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
    abstract Telescope
    tel NumGeneralizableArgs
    NoGeneralizableArgs       = NumGeneralizableArgs
    NoGeneralizableArgs
      abstract Telescope
    tel (SomeGeneralizableArgs Int
    n) = Int -> NumGeneralizableArgs
    SomeGeneralizableArgs (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)

    instance Abstract Projection where
      abstract :: Telescope -> Projection -> Projection
    abstract Telescope
    tel Projection
    p = Projection
    p
        { projIndex = size tel + projIndex p
        , projLams  = abstract tel $ projLams p
        }

    instance Abstract ProjLams where
      abstract :: Telescope -> ProjLams -> ProjLams
    abstract Telescope
    tel (ProjLams [Arg [Char]]
    lams) = [Arg [Char]] -> ProjLams
    ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
    forall a b. (a -> b) -> a -> b
    $
        (Dom' Term ([Char], Type) -> Arg [Char])
    -> [Dom' Term ([Char], Type)] -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ !Dom' Term ([Char], Type)
    dom -> Dom' Term [Char] -> Arg [Char]
    forall t a. Dom' t a -> Arg a
    argFromDom (([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char])
    -> Dom' Term ([Char], Type) -> Dom' Term [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term ([Char], Type)
    dom)) (Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel) [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
    forall a. [a] -> [a] -> [a]
    ++ [Arg [Char]]
    lams

    instance Abstract System where
      abstract :: Telescope -> System -> System
    abstract Telescope
    tel (System Telescope
    tel1 [(Face, Term)]
    sys) = Telescope -> [(Face, Term)] -> System
    System (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Telescope
    tel1) [(Face, Term)]
    sys

    instance Abstract Defn where
      abstract :: Telescope -> Defn -> Defn
    abstract Telescope
    tel Defn
    d = case Defn
    d of
        Axiom{} -> Defn
    d
        DataOrRecSig Int
    n -> Int -> Defn
    DataOrRecSig (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)
        GeneralizableVar NumGeneralizableArgs
    gv -> NumGeneralizableArgs -> Defn
    GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
    forall a b. (a -> b) -> a -> b
    $ Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel NumGeneralizableArgs
    gv
        AbstractDefn Defn
    d -> Defn -> Defn
    AbstractDefn (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Defn -> Defn
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Defn
    d
        Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc, funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cov, funInv :: Defn -> FunctionInverse
    funInv = FunctionInverse
    inv
                , funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    extLam
                , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    _  } ->
          Defn
    d { funClauses  = abstract tel cs
            , funCompiled = abstract tel cc
            , funCovering = abstract tel cov
            , funInv      = abstract tel inv
            , funExtLam   = modifySystem (abstract tel) <$> extLam
            }
        Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc, funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cov, funInv :: Defn -> FunctionInverse
    funInv = FunctionInverse
    inv
                , funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    extLam
                , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    p } ->
          -- Andreas, 2015-05-11 if projection was applied to Var 0
          -- then abstract over last element of tel (the others are params).
          if Projection -> Int
    projIndex Projection
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 then
            Defn
    d { funProjection = Right $ abstract tel p
              , funClauses    = map (abstractClause EmptyTel) cs
              }
          else
            Defn
    d { funProjection = Right $ abstract tel p
              , funClauses    = map (abstractClause tel1) cs
              , funCompiled   = abstract tel1 cc
              , funCovering   = abstract tel1 cov
              , funInv        = abstract tel1 inv
              , funExtLam     = modifySystem (\ System
    _ -> System
    forall a. HasCallStack => a
    __IMPOSSIBLE__) <$> extLam
              }
            where
              tel1 :: Telescope
    tel1 = [Dom' Term ([Char], Type)] -> Telescope
    telFromList ([Dom' Term ([Char], Type)] -> Telescope)
    -> [Dom' Term ([Char], Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
    forall a. Int -> [a] -> [a]
    drop (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
    -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel
              -- #5128: clause telescopes should be abstracted over the full telescope, regardless of
              --        projection shenanigans.
              abstractClause :: Telescope -> Clause -> Clause
    abstractClause Telescope
    tel1 Clause
    c = (Telescope -> Clause -> Clause
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel1 Clause
    c) { clauseTel = abstract tel $ clauseTel c }

        Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl } ->
          Defn
    d { dataPars       = np + size tel
            , dataClause     = abstract tel cl
            }
        Record{ recPars :: Defn -> Int
    recPars = Int
    np, recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recTel :: Defn -> Telescope
    recTel = Telescope
    tel' } ->
          Defn
    d { recPars    = np + size tel
            , recClause  = abstract tel cl
            , recTel     = abstract tel tel'
            }
        Constructor{ conPars :: Defn -> Int
    conPars = Int
    np } ->
          Defn
    d { conPars = np + size tel }
        Primitive{ primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cs } ->
          Defn
    d { primClauses = abstract tel cs }
        PrimitiveSort{} -> Defn
    d

    instance Abstract PrimFun where
        abstract :: Telescope -> PrimFun -> PrimFun
    abstract Telescope
    tel (PrimFun QName
    x Int
    ar [Occurrence]
    occs Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def) =
          QName
    -> Int
    -> [Occurrence]
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    PrimFun QName
    x (Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n) (Int -> Occurrence -> [Occurrence]
    forall a. Int -> a -> [a]
    replicate Int
    n Occurrence
    Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
    forall a. [a] -> [a] -> [a]
    ++ [Occurrence]
    occs) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
     -> PrimFun)
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    forall a b. (a -> b) -> a -> b
    $ \Args
    ts ->
            Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    drop Int
    n Args
    ts
            where n :: Int
    n = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel

    instance Abstract Clause where
      abstract :: Telescope -> Clause -> Clause
    abstract Telescope
    tel (Clause Range
    rl Range
    rf Telescope
    tel' [NamedArg DeBruijnPattern]
    ps Maybe Term
    b Maybe (Arg Type)
    t Catchall
    catchall Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell Maybe ModuleName
    wm) =
        Range
    -> Range
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Catchall
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Maybe ModuleName
    -> Clause
    Clause Range
    rl Range
    rf (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Telescope
    tel')
               (Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m Telescope
    tel [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    ps)
               Maybe Term
    b
               Maybe (Arg Type)
    t -- nothing to do for t, since it lives under the telescope
               Catchall
    catchall
               Maybe Bool
    recursive
               Maybe Bool
    unreachable
               ExpandedEllipsis
    ell
               Maybe ModuleName
    wm
          where m :: Int
    m = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel'

    instance Abstract CompiledClauses where
      abstract :: Telescope -> CompiledClauses -> CompiledClauses
    abstract Telescope
    tel CompiledClauses
    cc = case CompiledClauses
    cc of
          Fail [Arg [Char]]
    xs   -> [Arg [Char]] -> CompiledClauses
    forall a. [Arg [Char]] -> CompiledClauses' a
    Fail ([Arg [Char]]
    hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
    forall a. [a] -> [a] -> [a]
    ++ [Arg [Char]]
    xs)
          Done [Arg [Char]]
    xs Term
    t -> [Arg [Char]] -> Term -> CompiledClauses
    forall a. [Arg [Char]] -> a -> CompiledClauses' a
    Done ([Arg [Char]]
    hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
    forall a. [a] -> [a] -> [a]
    ++ [Arg [Char]]
    xs) Term
    t
          Case Arg Int
    n Case CompiledClauses
    bs -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case (Arg Int
    n Arg Int -> (Int -> Int) -> Arg Int
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Int
    i -> Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) (Telescope -> Case CompiledClauses -> Case CompiledClauses
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Case CompiledClauses
    bs)
        where
          hs :: [Arg [Char]]
    hs = (Dom' Term ([Char], Type) -> Arg [Char])
    -> [Dom' Term ([Char], Type)] -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom' Term [Char] -> Arg [Char]
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom' Term [Char] -> Arg [Char])
    -> (Dom' Term ([Char], Type) -> Dom' Term [Char])
    -> Dom' Term ([Char], Type)
    -> Arg [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], Type) -> [Char])
    -> Dom' Term ([Char], Type) -> Dom' Term [Char]
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst) ([Dom' Term ([Char], Type)] -> [Arg [Char]])
    -> [Dom' Term ([Char], Type)] -> [Arg [Char]]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel

    instance Abstract a => Abstract (WithArity a) where
      abstract :: Telescope -> WithArity a -> WithArity a
    abstract Telescope
    tel (WithArity Int
    n a
    a) = Int -> a -> WithArity a
    forall c. Int -> c -> WithArity c
    WithArity Int
    n (a -> WithArity a) -> a -> WithArity a
    forall a b. (a -> b) -> a -> b
    $ Telescope -> a -> a
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel a
    a

    instance Abstract a => Abstract (Case a) where
      abstract :: Telescope -> Case a -> Case a
    abstract Telescope
    tel (Branches Bool
    cop Map QName (WithArity a)
    cs Maybe (ConHead, WithArity a)
    eta Map Literal a
    ls Maybe a
    m Maybe Bool
    b Bool
    lz) =
        Bool
    -> Map QName (WithArity a)
    -> Maybe (ConHead, WithArity a)
    -> Map Literal a
    -> Maybe a
    -> Maybe Bool
    -> Bool
    -> Case a
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    cop (Telescope -> Map QName (WithArity a) -> Map QName (WithArity a)
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Map QName (WithArity a)
    cs) ((WithArity a -> WithArity a)
    -> (ConHead, WithArity a) -> (ConHead, WithArity a)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Telescope -> WithArity a -> WithArity a
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel) ((ConHead, WithArity a) -> (ConHead, WithArity a))
    -> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (ConHead, WithArity a)
    eta)
                     (Telescope -> Map Literal a -> Map Literal a
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Map Literal a
    ls) (Telescope -> Maybe a -> Maybe a
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel Maybe a
    m) Maybe Bool
    b Bool
    lz

    telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
    telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
    telVars Int
    m = (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing) ([NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
    -> (Telescope -> [NamedArg DeBruijnPattern])
    -> Telescope
    -> [Arg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m)

    namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m Telescope
    EmptyTel                     = []
    namedTelVars Int
    m (ExtendTel !Dom Type
    dom Abs Telescope
    tel) =
      ArgInfo
    -> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    dom) (Int -> [Char] -> Named NamedName DeBruijnPattern
    namedDBVarP (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) ([Char] -> Named NamedName DeBruijnPattern)
    -> [Char] -> Named NamedName DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Abs Telescope -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Telescope
    tel) NamedArg DeBruijnPattern
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. a -> [a] -> [a]
    :
      Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Abs Telescope -> Telescope
    forall a. Abs a -> a
    unAbs Abs Telescope
    tel)

    instance Abstract FunctionInverse where
      abstract :: Telescope -> FunctionInverse -> FunctionInverse
    abstract Telescope
    tel FunctionInverse
    NotInjective  = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
      abstract Telescope
    tel (Inverse InversionMap Clause
    inv) = InversionMap Clause -> FunctionInverse
    forall c. InversionMap c -> FunctionInverse' c
    Inverse (InversionMap Clause -> FunctionInverse)
    -> InversionMap Clause -> FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ Telescope -> InversionMap Clause -> InversionMap Clause
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel InversionMap Clause
    inv

    instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where
      abstract :: Telescope -> [t] -> [t]
    abstract Telescope
    tel = (t -> t) -> [t] -> [t]
    forall a b. (a -> b) -> [a] -> [b]
    map (Telescope -> t -> t
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel)

    instance Abstract t => Abstract (Maybe t) where
      abstract :: Telescope -> Maybe t -> Maybe t
    abstract Telescope
    tel Maybe t
    x = (t -> t) -> Maybe t -> Maybe t
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Telescope -> t -> t
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel) Maybe t
    x

    instance Abstract v => Abstract (Map k v) where
      abstract :: Telescope -> Map k v -> Map k v
    abstract Telescope
    tel Map k v
    m = (v -> v) -> Map k v -> Map k v
    forall a b. (a -> b) -> Map k a -> Map k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Telescope -> v -> v
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel) Map k v
    m

    instance Abstract v => Abstract (HashMap k v) where
      abstract :: Telescope -> HashMap k v -> HashMap k v
    abstract Telescope
    tel HashMap k v
    m = (v -> v) -> HashMap k v -> HashMap k v
    forall a b. (a -> b) -> HashMap k a -> HashMap k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Telescope -> v -> v
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel) HashMap k v
    m

    abstractArgs :: Abstract a => Args -> a -> a
    abstractArgs :: forall a. Abstract a => Args -> a -> a
    abstractArgs Args
    args a
    x = Telescope -> a -> a
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel a
    x
        where
            tel :: Telescope
    tel   = (Arg [Char] -> Telescope -> Telescope)
    -> Telescope -> [Arg [Char]] -> Telescope
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\arg :: Arg [Char]
    arg@(Arg ArgInfo
    info [Char]
    x) -> Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type
    HasCallStack => Type
    __DUMMY_TYPE__ Type -> Dom' Term [Char] -> Dom Type
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg [Char] -> Dom' Term [Char]
    forall a. Arg a -> Dom a
    domFromArg Arg [Char]
    arg) (Abs Telescope -> Telescope)
    -> (Telescope -> Abs Telescope) -> Telescope -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x)
                          Telescope
    forall a. Tele a
    EmptyTel
                  ([Arg [Char]] -> Telescope) -> [Arg [Char]] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Arg Term -> Arg [Char])
    -> [[Char]] -> Args -> [Arg [Char]]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith [Char] -> Arg Term -> Arg [Char]
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$) [[Char]]
    names Args
    args
            names :: [[Char]]
    names = [[Char]] -> [[Char]]
    forall a. HasCallStack => [a] -> [a]
    cycle ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ (Char -> [Char]) -> [Char] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> [Char]
    stringToArgName ([Char] -> [Char]) -> (Char -> [Char]) -> Char -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[])) [Char
    'a'..Char
    'z']

    ---------------------------------------------------------------------------
    -- * Substitution and shifting\/weakening\/strengthening
    ---------------------------------------------------------------------------

    -- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@
    renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a
    renaming :: forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    err Permutation
    p = Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    forall a.
    DeBruijn a =>
    Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS Impossible
    err [Maybe a]
    gamma (Substitution' a -> Substitution' a)
    -> Substitution' a -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Int -> Substitution' a
    forall a. Int -> Substitution' a
    raiseS (Int -> Substitution' a) -> Int -> Substitution' a
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Int
    forall a. Sized a => a -> Int
    size Permutation
    p
      where
        gamma :: [Maybe a]
        gamma :: [Maybe a]
    gamma = Permutation -> (Int -> a) -> [Maybe a]
    forall a b. InversePermute a b => Permutation -> a -> b
    inversePermute Permutation
    p (Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar :: Int -> a)
        -- gamma = safePermute (invertP (-1) p) $ map deBruijnVar [0..]

    -- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renamingR π) : Term Δ -> Term Γ@
    renamingR :: DeBruijn a => Permutation -> Substitution' a
    renamingR :: forall a. DeBruijn a => Permutation -> Substitution' a
    renamingR p :: Permutation
    p@(Perm Int
    n [Int]
    is) = [a]
    xs [a] -> Substitution' a -> Substitution' a
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Int -> Substitution' a
    forall a. Int -> Substitution' a
    raiseS Int
    n
      where
      xs :: [a]
    xs = (Int -> a) -> [Int] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int
    i -> Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i)) ([Int] -> [Int]
    forall a. [a] -> [a]
    reverse [Int]
    is)

      -- The list xs used to be defined in the following way:
      --
      --   permute (reverseP p) (map deBruijnVar [0..])
      --
      -- We have that
      --
      --     permute (reverseP p) (map deBruijnVar [0..])
      --   = permute (Perm n $ map ((n - 1) -) $ reverse is)
      --       (map deBruijnVar [0..])
      --   = map (map deBruijnVar [0..] !!)
      --       (map ((n - 1) -) $ reverse is)
      --   = map deBruijnVar (map ((n - 1) -) $ reverse is)
      --   = map (\i -> deBruijnVar (n - 1 - i)) (reverse is).
      --
      -- The latter code is linear in the length of is (if deBruijnVar
      -- takes constant time), while the time complexity of the former
      -- code depends on the value of the largest index in is.

    -- | The permutation should permute the corresponding context. (right-to-left list)
    renameP :: Subst a => Impossible -> Permutation -> a -> a
    renameP :: forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    err Permutation
    p = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> Permutation -> Substitution' (SubstArg a)
    forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    err Permutation
    p)

    instance EndoSubst a => Subst (Substitution' a) where
      type SubstArg (Substitution' a) = a
      applySubst :: Substitution' (SubstArg (Substitution' a))
    -> Substitution' a -> Substitution' a
    applySubst Substitution' (SubstArg (Substitution' a))
    rho Substitution' a
    sgm = Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' a
    Substitution' (SubstArg (Substitution' a))
    rho Substitution' a
    sgm

    {-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
    {-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
    applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
    applySubstTerm :: forall t.
    (Coercible t Term, EndoSubst t, Apply t) =>
    Substitution' t -> t -> t
    applySubstTerm Substitution' t
    IdS t
    t = t
    t
    applySubstTerm Substitution' t
    rho t
    t    = Term -> t
    forall a b. Coercible a b => a -> b
    coerce (Term -> t) -> Term -> t
    forall a b. (a -> b) -> a -> b
    $ case t -> Term
    forall a b. Coercible a b => a -> b
    coerce t
    t of
        Var Int
    i Elims
    es    -> t -> Term
    forall a b. Coercible a b => a -> b
    coerce (t -> Term) -> t -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' t -> Int -> t
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' t
    rho Int
    i  t -> Elims -> t
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims -> Elims
    subE Elims
    es
        Lam ArgInfo
    h Abs Term
    m     -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @(Abs t) Abs Term
    m
        Def QName
    f Elims
    es    -> QName -> Elims -> Elims -> Term
    defApp QName
    f [] (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    subE Elims
    es
        Con ConHead
    c ConInfo
    ci Elims
    vs -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    subE Elims
    vs
        MetaV MetaId
    x Elims
    es  -> MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    subE Elims
    es
        Lit Literal
    l       -> Literal -> Term
    Lit Literal
    l
        Level Level
    l     -> Level -> Term
    levelTm (Level -> Term) -> Level -> Term
    forall a b. (a -> b) -> a -> b
    $ forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @(Level' t) Level
    l
        Pi Dom Type
    a Abs Type
    b      -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> Term
    Pi ((Dom Type, Abs Type) -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b. (a -> b) -> a -> b
    $ (Dom Type, Abs Type) -> (Dom Type, Abs Type)
    subPi (Dom Type
    a,Abs Type
    b)
        Sort Sort
    s      -> Sort -> Term
    Sort (Sort -> Term) -> Sort -> Term
    forall a b. (a -> b) -> a -> b
    $ forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @(Sort' t) Sort
    s
        DontCare Term
    mv -> Term -> Term
    dontCare (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @t Term
    mv
        Dummy [Char]
    s Elims
    es  -> [Char] -> Elims -> Term
    Dummy [Char]
    s (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Elims
    subE Elims
    es
     where
       sub :: forall a b. (Coercible b a, SubstWith t a) => b -> b
       sub :: forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub b
    t = a -> b
    forall a b. Coercible a b => a -> b
    coerce (a -> b) -> a -> b
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' t
    Substitution' (SubstArg a)
    rho (b -> a
    forall a b. Coercible a b => a -> b
    coerce b
    t :: a)
       subE :: Elims -> Elims
       subE :: Elims -> Elims
    subE  = forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @[Elim' t]
       subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
       subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
    subPi = forall a b. (Coercible b a, SubstWith t a) => b -> b
    sub @(Dom' t (Type'' t t), Abs (Type'' t t))

    instance Subst Term where
      type SubstArg Term = Term
      applySubst :: Substitution' (SubstArg Term) -> Term -> Term
    applySubst = Substitution' Term -> Term -> Term
    Substitution' (SubstArg Term) -> Term -> Term
    forall t.
    (Coercible t Term, EndoSubst t, Apply t) =>
    Substitution' t -> t -> t
    applySubstTerm

    -- András 2023-09-25: we can only put this here, because at the original definition site there's no Subst Term instance.
    {-# SPECIALIZE lookupS :: Substitution' Term -> Nat -> Term #-}
    {-# SPECIALIZE isNoAbs :: Abs Term -> Maybe Term #-}

    instance Subst BraveTerm where
      type SubstArg BraveTerm = BraveTerm
      applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
    applySubst = Substitution' BraveTerm -> BraveTerm -> BraveTerm
    Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
    forall t.
    (Coercible t Term, EndoSubst t, Apply t) =>
    Substitution' t -> t -> t
    applySubstTerm

    instance (Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) where
      type SubstArg (Type'' a b) = SubstArg a
      applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b
    applySubst Substitution' (SubstArg (Type'' a b))
    rho (El Sort' a
    s b
    t) = Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Sort' a))
    Substitution' (SubstArg (Type'' a b))
    rho Sort' a
    s Sort' a -> b -> Type'' a b
    forall t a. Sort' t -> a -> Type'' t a
    `El` Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (Type'' a b))
    rho b
    t

    instance (Coercible a Term, Subst a) => Subst (Sort' a) where
      type SubstArg (Sort' a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
    applySubst Substitution' (SubstArg (Sort' a))
    rho = \case
        Univ Univ
    u Level' a
    n   -> Univ -> Level' a -> Sort' a
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level' a -> Sort' a) -> Level' a -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ Level' a -> Level' a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Level' a
    n
        Inf Univ
    u Integer
    n    -> Univ -> Integer -> Sort' a
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n
        Sort' a
    SizeUniv   -> Sort' a
    forall t. Sort' t
    SizeUniv
        Sort' a
    LockUniv   -> Sort' a
    forall t. Sort' t
    LockUniv
        Sort' a
    LevelUniv  -> Sort' a
    forall t. Sort' t
    LevelUniv
        Sort' a
    IntervalUniv -> Sort' a
    forall t. Sort' t
    IntervalUniv
        PiSort Dom' a a
    a Sort' a
    s1 Abs (Sort' a)
    s2 -> Sort -> Sort' a
    forall a b. Coercible a b => a -> b
    coerce (Sort -> Sort' a) -> Sort -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ Dom Term -> Sort -> Abs Sort -> Sort
    piSort (Dom' a a -> Dom Term
    forall a b. Coercible a b => a -> b
    coerce (Dom' a a -> Dom Term) -> Dom' a a -> Dom Term
    forall a b. (a -> b) -> a -> b
    $ Dom' a a -> Dom' a a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Dom' a a
    a) (Sort' a -> Sort
    forall a b. Coercible a b => a -> b
    coerce (Sort' a -> Sort) -> Sort' a -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort' a -> Sort' a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Sort' a
    s1) (Abs (Sort' a) -> Abs Sort
    forall a b. Coercible a b => a -> b
    coerce (Abs (Sort' a) -> Abs Sort) -> Abs (Sort' a) -> Abs Sort
    forall a b. (a -> b) -> a -> b
    $ Abs (Sort' a) -> Abs (Sort' a)
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Abs (Sort' a)
    s2)
        FunSort Sort' a
    s1 Sort' a
    s2 -> Sort -> Sort' a
    forall a b. Coercible a b => a -> b
    coerce (Sort -> Sort' a) -> Sort -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    funSort (Sort' a -> Sort
    forall a b. Coercible a b => a -> b
    coerce (Sort' a -> Sort) -> Sort' a -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort' a -> Sort' a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Sort' a
    s1) (Sort' a -> Sort
    forall a b. Coercible a b => a -> b
    coerce (Sort' a -> Sort) -> Sort' a -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort' a -> Sort' a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Sort' a
    s2)
        UnivSort Sort' a
    s -> Sort -> Sort' a
    forall a b. Coercible a b => a -> b
    coerce (Sort -> Sort' a) -> Sort -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort
    univSort (Sort -> Sort) -> Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort' a -> Sort
    forall a b. Coercible a b => a -> b
    coerce (Sort' a -> Sort) -> Sort' a -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort' a -> Sort' a
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub Sort' a
    s
        MetaS MetaId
    x [Elim' a]
    es -> MetaId -> [Elim' a] -> Sort' a
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ [Elim' a] -> [Elim' a]
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub [Elim' a]
    es
        DefS QName
    d [Elim' a]
    es  -> QName -> [Elim' a] -> Sort' a
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    d ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ [Elim' a] -> [Elim' a]
    forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub [Elim' a]
    es
        s :: Sort' a
    s@DummyS{} -> Sort' a
    s
        where
          sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
          sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
    sub b
    x = Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (Sort' a))
    rho b
    x

    instance Subst a => Subst (Level' a) where
      type SubstArg (Level' a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a
    applySubst Substitution' (SubstArg (Level' a))
    rho (Max Integer
    n [PlusLevel' a]
    as) = Integer -> [PlusLevel' a] -> Level' a
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' a] -> Level' a) -> [PlusLevel' a] -> Level' a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [PlusLevel' a])
    -> [PlusLevel' a] -> [PlusLevel' a]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [PlusLevel' a])
    Substitution' (SubstArg (Level' a))
    rho [PlusLevel' a]
    as

    instance Subst a => Subst (PlusLevel' a) where
      type SubstArg (PlusLevel' a) = SubstArg a
      applySubst :: Substitution' (SubstArg (PlusLevel' a))
    -> PlusLevel' a -> PlusLevel' a
    applySubst Substitution' (SubstArg (PlusLevel' a))
    rho (Plus Integer
    n a
    l) = Integer -> a -> PlusLevel' a
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (a -> PlusLevel' a) -> a -> PlusLevel' a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (PlusLevel' a))
    rho a
    l

    instance Subst Name where
      type SubstArg Name = Term
      applySubst :: Substitution' (SubstArg Name) -> Name -> Name
    applySubst Substitution' (SubstArg Name)
    rho = Name -> Name
    forall a. a -> a
    id

    instance Subst ConPatternInfo where
      type SubstArg ConPatternInfo = Term
      applySubst :: Substitution' (SubstArg ConPatternInfo)
    -> ConPatternInfo -> ConPatternInfo
    applySubst Substitution' (SubstArg ConPatternInfo)
    rho ConPatternInfo
    i = ConPatternInfo
    i{ conPType = applySubst rho $ conPType i }

    instance Subst Pattern where
      type SubstArg Pattern = Term
      applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern
    applySubst Substitution' (SubstArg Pattern)
    rho = \case
        ConP ConHead
    c ConPatternInfo
    mt [NamedArg Pattern]
    ps    -> ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c (Substitution' (SubstArg ConPatternInfo)
    -> ConPatternInfo -> ConPatternInfo
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg ConPatternInfo)
    Substitution' (SubstArg Pattern)
    rho ConPatternInfo
    mt) ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg Pattern])
    -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [NamedArg Pattern])
    Substitution' (SubstArg Pattern)
    rho [NamedArg Pattern]
    ps
        DefP PatternInfo
    o QName
    q [NamedArg Pattern]
    ps     -> PatternInfo -> QName -> [NamedArg Pattern] -> Pattern
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    o QName
    q ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg Pattern])
    -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [NamedArg Pattern])
    Substitution' (SubstArg Pattern)
    rho [NamedArg Pattern]
    ps
        DotP PatternInfo
    o Term
    t        -> PatternInfo -> Term -> Pattern
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    o (Term -> Pattern) -> Term -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Pattern)
    Substitution' (SubstArg Term)
    rho Term
    t
        p :: Pattern
    p@(VarP PatternInfo
    _o [Char]
    _x)  -> Pattern
    p
        p :: Pattern
    p@(LitP PatternInfo
    _o Literal
    _l)  -> Pattern
    p
        p :: Pattern
    p@(ProjP ProjOrigin
    _o QName
    _x) -> Pattern
    p
        IApplyP PatternInfo
    o Term
    t Term
    u [Char]
    x -> PatternInfo -> Term -> Term -> [Char] -> Pattern
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    o (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Pattern)
    Substitution' (SubstArg Term)
    rho Term
    t) (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Pattern)
    Substitution' (SubstArg Term)
    rho Term
    u) [Char]
    x

    instance Subst A.ProblemEq where
      type SubstArg A.ProblemEq = Term
      applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq
    applySubst Substitution' (SubstArg ProblemEq)
    rho (A.ProblemEq Pattern
    p Term
    v Dom Type
    a) =
        (Term -> Dom Type -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Pattern -> Term -> Dom Type -> ProblemEq
    A.ProblemEq Pattern
    p) ((Term, Dom Type) -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Term, Dom Type))
    -> (Term, Dom Type) -> (Term, Dom Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Term, Dom Type))
    Substitution' (SubstArg ProblemEq)
    rho (Term
    v,Dom Type
    a)

    instance DeBruijn BraveTerm where
      deBruijnVar :: Int -> BraveTerm
    deBruijnVar = Term -> BraveTerm
    BraveTerm (Term -> BraveTerm) -> (Int -> Term) -> Int -> BraveTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Term
    forall a. DeBruijn a => Int -> a
    deBruijnVar
      deBruijnView :: BraveTerm -> Maybe Int
    deBruijnView = Term -> Maybe Int
    forall a. DeBruijn a => a -> Maybe Int
    deBruijnView (Term -> Maybe Int)
    -> (BraveTerm -> Term) -> BraveTerm -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BraveTerm -> Term
    unBrave

    instance DeBruijn NLPat where
      deBruijnVar :: Int -> NLPat
    deBruijnVar Int
    i = Int -> [Arg Int] -> NLPat
    PVar Int
    i []
      deBruijnView :: NLPat -> Maybe Int
    deBruijnView = \case
        PVar Int
    i []   -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i
        PVar{}      -> Maybe Int
    forall a. Maybe a
    Nothing
        PDef{}      -> Maybe Int
    forall a. Maybe a
    Nothing
        PLam{}      -> Maybe Int
    forall a. Maybe a
    Nothing
        PPi{}       -> Maybe Int
    forall a. Maybe a
    Nothing
        PSort{}     -> Maybe Int
    forall a. Maybe a
    Nothing
        PBoundVar{} -> Maybe Int
    forall a. Maybe a
    Nothing -- or... ?
        PTerm{}     -> Maybe Int
    forall a. Maybe a
    Nothing -- or... ?

    applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst :: forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst = Substitution' Term -> a -> a
    Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution' Term -> a -> a)
    -> (Substitution' NLPat -> Substitution' Term)
    -> Substitution' NLPat
    -> a
    -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NLPat -> Term) -> Substitution' NLPat -> Substitution' Term
    forall a b. (a -> b) -> Substitution' a -> Substitution' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NLPat -> Term
    nlPatToTerm
      where
        nlPatToTerm :: NLPat -> Term
        nlPatToTerm :: NLPat -> Term
    nlPatToTerm = \case
          PVar Int
    i [Arg Int]
    xs      -> Int -> Elims -> Term
    Var Int
    i (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Int -> Elim' Term) -> [Arg Int] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term)
    -> (Arg Int -> Arg Term) -> Arg Int -> Elim' Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Term) -> Arg Int -> Arg Term
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Term
    var) [Arg Int]
    xs
          PTerm Term
    u        -> Term
    u
          PDef QName
    f PElims
    es      -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PLam ArgInfo
    i Abs NLPat
    u       -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PPi Dom NLPType
    a Abs NLPType
    b        -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PSort NLPSort
    s        -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          PBoundVar Int
    i PElims
    es -> Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
    applyNLSubstToDom :: forall a.
    SubstWith NLPat a =>
    Substitution' NLPat -> Dom a -> Dom a
    applyNLSubstToDom Substitution' NLPat
    rho Dom a
    dom = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' NLPat
    rho (a -> a) -> Dom a -> Dom a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom a
    dom{ domTactic = applyNLPatSubst rho $ domTactic dom }

    instance Subst NLPat where
      type SubstArg NLPat = NLPat
      applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat
    applySubst Substitution' (SubstArg NLPat)
    rho = \case
        PVar Int
    i [Arg Int]
    bvs     -> Substitution' NLPat -> Int -> NLPat
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution' (SubstArg NLPat)
    Substitution' NLPat
    rho Int
    i NLPat -> [Arg Int] -> NLPat
    `applyBV` [Arg Int]
    bvs
        PDef QName
    f PElims
    es      -> QName -> PElims -> NLPat
    PDef QName
    f (PElims -> NLPat) -> PElims -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg PElims) -> PElims -> PElims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg PElims)
    Substitution' (SubstArg NLPat)
    rho PElims
    es
        PLam ArgInfo
    i Abs NLPat
    u       -> ArgInfo -> Abs NLPat -> NLPat
    PLam ArgInfo
    i (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Abs NLPat)) -> Abs NLPat -> Abs NLPat
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Abs NLPat))
    Substitution' (SubstArg NLPat)
    rho Abs NLPat
    u
        PPi Dom NLPType
    a Abs NLPType
    b        -> Dom NLPType -> Abs NLPType -> NLPat
    PPi (Substitution' NLPat -> Dom NLPType -> Dom NLPType
    forall a.
    SubstWith NLPat a =>
    Substitution' NLPat -> Dom a -> Dom a
    applyNLSubstToDom Substitution' (SubstArg NLPat)
    Substitution' NLPat
    rho Dom NLPType
    a) (Substitution' (SubstArg (Abs NLPType))
    -> Abs NLPType -> Abs NLPType
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Abs NLPType))
    Substitution' (SubstArg NLPat)
    rho Abs NLPType
    b)
        PSort NLPSort
    s        -> NLPSort -> NLPat
    PSort (NLPSort -> NLPat) -> NLPSort -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg NLPSort)
    Substitution' (SubstArg NLPat)
    rho NLPSort
    s
        PBoundVar Int
    i PElims
    es -> Int -> PElims -> NLPat
    PBoundVar Int
    i (PElims -> NLPat) -> PElims -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg PElims) -> PElims -> PElims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg PElims)
    Substitution' (SubstArg NLPat)
    rho PElims
    es
        PTerm Term
    u        -> Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Substitution' NLPat -> Term -> Term
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' (SubstArg NLPat)
    Substitution' NLPat
    rho Term
    u

        where
          applyBV :: NLPat -> [Arg Int] -> NLPat
          applyBV :: NLPat -> [Arg Int] -> NLPat
    applyBV NLPat
    p [Arg Int]
    ys = case NLPat
    p of
            PVar Int
    i [Arg Int]
    xs      -> Int -> [Arg Int] -> NLPat
    PVar Int
    i ([Arg Int]
    xs [Arg Int] -> [Arg Int] -> [Arg Int]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Int]
    ys)
            PTerm Term
    u        -> Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Term
    u Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` (Arg Int -> Arg Term) -> [Arg Int] -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> Term) -> Arg Int -> Arg Term
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Term
    var) [Arg Int]
    ys
            PDef QName
    f PElims
    es      -> NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            PLam ArgInfo
    i Abs NLPat
    u       -> NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            PPi Dom NLPType
    a Abs NLPType
    b        -> NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            PSort NLPSort
    s        -> NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            PBoundVar Int
    i PElims
    es -> NLPat
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Subst NLPType where
      type SubstArg NLPType = NLPat
      applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType
    applySubst Substitution' (SubstArg NLPType)
    rho (NLPType NLPSort
    s NLPat
    a) = NLPSort -> NLPat -> NLPType
    NLPType (Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg NLPSort)
    Substitution' (SubstArg NLPType)
    rho NLPSort
    s) (Substitution' (SubstArg NLPat) -> NLPat -> NLPat
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg NLPType)
    Substitution' (SubstArg NLPat)
    rho NLPat
    a)

    instance Subst NLPSort where
      type SubstArg NLPSort = NLPat
      applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
    applySubst Substitution' (SubstArg NLPSort)
    rho = \case
        PUniv Univ
    u NLPat
    l -> Univ -> NLPat -> NLPSort
    PUniv Univ
    u (NLPat -> NLPSort) -> NLPat -> NLPSort
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg NLPat) -> NLPat -> NLPat
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg NLPSort)
    Substitution' (SubstArg NLPat)
    rho NLPat
    l
        PInf Univ
    f Integer
    n  -> Univ -> Integer -> NLPSort
    PInf Univ
    f Integer
    n
        NLPSort
    PSizeUniv -> NLPSort
    PSizeUniv
        NLPSort
    PLockUniv -> NLPSort
    PLockUniv
        NLPSort
    PLevelUniv -> NLPSort
    PLevelUniv
        NLPSort
    PIntervalUniv -> NLPSort
    PIntervalUniv

    instance Subst RewriteRule where
      type SubstArg RewriteRule = NLPat
      applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule
    applySubst Substitution' (SubstArg RewriteRule)
    rho (RewriteRule QName
    q Telescope
    gamma QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c TopLevelModuleName
    top) =
        QName
    -> Telescope
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> TopLevelModuleName
    -> RewriteRule
    RewriteRule QName
    q (Substitution' NLPat -> Telescope -> Telescope
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' (SubstArg RewriteRule)
    Substitution' NLPat
    rho Telescope
    gamma)
                    QName
    f (Substitution' (SubstArg PElims) -> PElims -> PElims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' NLPat -> Substitution' NLPat
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution' (SubstArg RewriteRule)
    Substitution' NLPat
    rho) PElims
    ps)
                      (Substitution' NLPat -> Term -> Term
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution' (SubstArg RewriteRule)
    Substitution' NLPat
    rho) Term
    rhs)
                      (Substitution' NLPat -> Type -> Type
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution' (SubstArg RewriteRule)
    Substitution' NLPat
    rho) Type
    t)
                      Bool
    c TopLevelModuleName
    top
        where n :: Int
    n = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma

    instance Subst a => Subst (Blocked a) where
      type SubstArg (Blocked a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a
    applySubst Substitution' (SubstArg (Blocked a))
    rho Blocked a
    b = (a -> a) -> Blocked a -> Blocked a
    forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Blocked a))
    rho) Blocked a
    b

    instance Subst DisplayForm where
      type SubstArg DisplayForm = Term
      applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm
    applySubst Substitution' (SubstArg DisplayForm)
    rho (Display Int
    n Elims
    ps DisplayTerm
    v) =
        Int -> Elims -> DisplayTerm -> DisplayForm
    Display Int
    n (Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' Term -> Substitution' Term
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution' Term
    Substitution' (SubstArg DisplayForm)
    rho) Elims
    ps)
                  (Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' Term -> Substitution' Term
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution' Term
    Substitution' (SubstArg DisplayForm)
    rho) DisplayTerm
    v)

    instance Subst DisplayTerm where
      type SubstArg DisplayTerm = Term
      applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
    applySubst Substitution' (SubstArg DisplayTerm)
    rho (DTerm' Term
    v Elims
    es)      = Term -> Elims -> DisplayTerm
    DTerm' (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg DisplayTerm)
    rho Term
    v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Elims)
    Substitution' (SubstArg DisplayTerm)
    rho Elims
    es
      applySubst Substitution' (SubstArg DisplayTerm)
    rho (DDot' Term
    v Elims
    es)       = Term -> Elims -> DisplayTerm
    DDot'  (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg DisplayTerm)
    rho Term
    v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Elims)
    Substitution' (SubstArg DisplayTerm)
    rho Elims
    es
      applySubst Substitution' (SubstArg DisplayTerm)
    rho (DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    vs)     = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [Arg DisplayTerm])
    -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [Arg DisplayTerm])
    Substitution' (SubstArg DisplayTerm)
    rho [Arg DisplayTerm]
    vs
      applySubst Substitution' (SubstArg DisplayTerm)
    rho (DDef QName
    c [Elim' DisplayTerm]
    es)        = QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    c ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [Elim' DisplayTerm])
    -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [Elim' DisplayTerm])
    Substitution' (SubstArg DisplayTerm)
    rho [Elim' DisplayTerm]
    es
      applySubst Substitution' (SubstArg DisplayTerm)
    rho (DWithApp DisplayTerm
    v List1 DisplayTerm
    vs Elims
    es) = (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)
    -> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
    forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
    uncurry3 DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp ((DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm)
    -> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
    -> (DisplayTerm, List1 DisplayTerm, Elims)
    -> (DisplayTerm, List1 DisplayTerm, Elims)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
    Substitution' (SubstArg DisplayTerm)
    rho (DisplayTerm
    v, List1 DisplayTerm
    vs, Elims
    es)

    instance Subst a => Subst (Tele a) where
      type SubstArg (Tele a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a
    applySubst Substitution' (SubstArg (Tele a))
    rho  Tele a
    EmptyTel         = Tele a
    forall a. Tele a
    EmptyTel
      applySubst Substitution' (SubstArg (Tele a))
    rho (ExtendTel a
    t Abs (Tele a)
    tel) = (a -> Abs (Tele a) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel ((a, Abs (Tele a)) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (a, Abs (Tele a)))
    -> (a, Abs (Tele a)) -> (a, Abs (Tele a))
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (a, Abs (Tele a)))
    Substitution' (SubstArg (Tele a))
    rho (a
    t, Abs (Tele a)
    tel)

    instance Subst Constraint where
      type SubstArg Constraint = Term

      applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint
    applySubst Substitution' (SubstArg Constraint)
    rho = \case
        ValueCmp Comparison
    cmp CompareAs
    a Term
    u Term
    v       -> Comparison -> CompareAs -> Term -> Term -> Constraint
    ValueCmp Comparison
    cmp (CompareAs -> CompareAs
    forall a. TermSubst a => a -> a
    rf CompareAs
    a) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    u) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    v)
        ValueCmpOnFace Comparison
    cmp Term
    p Type
    t Term
    u Term
    v -> Comparison -> Term -> Type -> Term -> Term -> Constraint
    ValueCmpOnFace Comparison
    cmp (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    p) (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    t) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    u) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    v)
        ElimCmp [Polarity]
    ps [IsForced]
    fs Type
    a Term
    v Elims
    e1 Elims
    e2  -> [Polarity]
    -> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
    ElimCmp [Polarity]
    ps [IsForced]
    fs (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    a) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    v) (Elims -> Elims
    forall a. TermSubst a => a -> a
    rf Elims
    e1) (Elims -> Elims
    forall a. TermSubst a => a -> a
    rf Elims
    e2)
        SortCmp Comparison
    cmp Sort
    s1 Sort
    s2        -> Comparison -> Sort -> Sort -> Constraint
    SortCmp Comparison
    cmp (Sort -> Sort
    forall a. TermSubst a => a -> a
    rf Sort
    s1) (Sort -> Sort
    forall a. TermSubst a => a -> a
    rf Sort
    s2)
        LevelCmp Comparison
    cmp Level
    l1 Level
    l2       -> Comparison -> Level -> Level -> Constraint
    LevelCmp Comparison
    cmp (Level -> Level
    forall a. TermSubst a => a -> a
    rf Level
    l1) (Level -> Level
    forall a. TermSubst a => a -> a
    rf Level
    l2)
        IsEmpty Range
    r Type
    a              -> Range -> Type -> Constraint
    IsEmpty Range
    r (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    a)
        CheckSizeLtSat Term
    t         -> Term -> Constraint
    CheckSizeLtSat (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    t)
        FindInstance Range
    r MetaId
    m Maybe [Candidate]
    cands   -> Range -> MetaId -> Maybe [Candidate] -> Constraint
    FindInstance Range
    r MetaId
    m (Maybe [Candidate] -> Maybe [Candidate]
    forall a. TermSubst a => a -> a
    rf Maybe [Candidate]
    cands)
        ResolveInstanceHead QName
    q    -> QName -> Constraint
    ResolveInstanceHead (QName -> QName
    forall a. TermSubst a => a -> a
    rf QName
    q)
        c :: Constraint
    c@UnBlock{}              -> Constraint
    c
        c :: Constraint
    c@CheckFunDef{}          -> Constraint
    c
        HasBiggerSort Sort
    s          -> Sort -> Constraint
    HasBiggerSort (Sort -> Sort
    forall a. TermSubst a => a -> a
    rf Sort
    s)
        HasPTSRule Dom Type
    a Abs Sort
    s           -> Dom Type -> Abs Sort -> Constraint
    HasPTSRule (Dom Type -> Dom Type
    forall a. TermSubst a => a -> a
    rf Dom Type
    a) (Abs Sort -> Abs Sort
    forall a. TermSubst a => a -> a
    rf Abs Sort
    s)
        CheckLockedVars Term
    a Type
    b Arg Term
    c Type
    d  -> Term -> Type -> Arg Term -> Type -> Constraint
    CheckLockedVars (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    a) (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    b) (Arg Term -> Arg Term
    forall a. TermSubst a => a -> a
    rf Arg Term
    c) (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    d)
        UnquoteTactic Term
    t Term
    h Type
    g      -> Term -> Term -> Type -> Constraint
    UnquoteTactic (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    t) (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    h) (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    g)
        CheckDataSort QName
    q Sort
    s        -> QName -> Sort -> Constraint
    CheckDataSort QName
    q (Sort -> Sort
    forall a. TermSubst a => a -> a
    rf Sort
    s)
        CheckMetaInst MetaId
    m          -> MetaId -> Constraint
    CheckMetaInst MetaId
    m
        CheckType Type
    t              -> Type -> Constraint
    CheckType (Type -> Type
    forall a. TermSubst a => a -> a
    rf Type
    t)
        UsableAtModality WhyCheckModality
    cc Maybe Sort
    ms Modality
    mod Term
    m -> WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
    UsableAtModality WhyCheckModality
    cc (Maybe Sort -> Maybe Sort
    forall a. TermSubst a => a -> a
    rf Maybe Sort
    ms) Modality
    mod (Term -> Term
    forall a. TermSubst a => a -> a
    rf Term
    m)
        where
          rf :: forall a. TermSubst a => a -> a
          rf :: forall a. TermSubst a => a -> a
    rf a
    x = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg Constraint)
    rho a
    x

    instance Subst CompareAs where
      type SubstArg CompareAs = Term
      applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs
    applySubst Substitution' (SubstArg CompareAs)
    rho (AsTermsOf Type
    a) = Type -> CompareAs
    AsTermsOf (Type -> CompareAs) -> Type -> CompareAs
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Type)
    Substitution' (SubstArg CompareAs)
    rho Type
    a
      applySubst Substitution' (SubstArg CompareAs)
    rho CompareAs
    AsSizes       = CompareAs
    AsSizes
      applySubst Substitution' (SubstArg CompareAs)
    rho CompareAs
    AsTypes       = CompareAs
    AsTypes

    instance Subst a => Subst (Elim' a) where
      type SubstArg (Elim' a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a
    applySubst Substitution' (SubstArg (Elim' a))
    rho = \case
        Apply Arg a
    v      -> 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
    $ Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Arg a))
    Substitution' (SubstArg (Elim' a))
    rho Arg a
    v
        IApply a
    x a
    y a
    r -> a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Elim' a))
    rho a
    x) (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Elim' a))
    rho a
    y) (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Elim' a))
    rho a
    r)
        e :: Elim' a
    e@Proj{}     -> Elim' a
    e

    instance Subst a => Subst (Abs a) where
      type SubstArg (Abs a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a
    applySubst Substitution' (SubstArg (Abs a))
    rho (Abs [Char]
    x a
    a)   = [Char] -> a -> Abs a
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x (a -> Abs a) -> a -> Abs a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    1 Substitution' (SubstArg a)
    Substitution' (SubstArg (Abs a))
    rho) a
    a
      applySubst Substitution' (SubstArg (Abs a))
    rho (NoAbs [Char]
    x a
    a) = [Char] -> a -> Abs a
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    x (a -> Abs a) -> a -> Abs a
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Abs a))
    rho a
    a

    instance Subst a => Subst (Arg a) where
      type SubstArg (Arg a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
    applySubst Substitution' (SubstArg (Arg a))
    IdS Arg a
    arg = Arg a
    arg
      applySubst Substitution' (SubstArg (Arg a))
    rho Arg a
    arg = FreeVariables -> Arg a -> Arg a
    forall a. LensFreeVariables a => FreeVariables -> a -> a
    setFreeVariables FreeVariables
    unknownFreeVariables (Arg a -> Arg a) -> Arg a -> Arg a
    forall a b. (a -> b) -> a -> b
    $ (a -> a) -> Arg a -> Arg a
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Arg a))
    rho) Arg a
    arg

    instance Subst a => Subst (Named name a) where
      type SubstArg (Named name a) = SubstArg a
      applySubst :: Substitution' (SubstArg (Named name a))
    -> Named name a -> Named name a
    applySubst Substitution' (SubstArg (Named name a))
    rho = (a -> a) -> Named name a -> Named name a
    forall a b. (a -> b) -> Named name a -> Named name b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (Named name a))
    rho)

    instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) where
      type SubstArg (Dom' a b) = SubstArg a

      applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b
    applySubst Substitution' (SubstArg (Dom' a b))
    IdS Dom' a b
    dom = Dom' a b
    dom
      applySubst Substitution' (SubstArg (Dom' a b))
    rho Dom' a b
    dom = FreeVariables -> Dom' a b -> Dom' a b
    forall a. LensFreeVariables a => FreeVariables -> a -> a
    setFreeVariables FreeVariables
    unknownFreeVariables (Dom' a b -> Dom' a b) -> Dom' a b -> Dom' a b
    forall a b. (a -> b) -> a -> b
    $
        (b -> b) -> Dom' a b -> Dom' a b
    forall a b. (a -> b) -> Dom' a a -> Dom' a b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (Dom' a b))
    rho) Dom' a b
    dom{ domTactic = applySubst rho (domTactic dom) }
      {-# INLINABLE applySubst #-}

    instance Subst LetBinding where
      type SubstArg LetBinding = Term
      applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding
    applySubst Substitution' (SubstArg LetBinding)
    rho (LetBinding Origin
    o Term
    v Dom Type
    t) = Origin -> Term -> Dom Type -> LetBinding
    LetBinding Origin
    o (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg LetBinding)
    rho Term
    v) (Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Dom Type))
    Substitution' (SubstArg LetBinding)
    rho Dom Type
    t)

    instance Subst ContextEntry where
      type SubstArg ContextEntry = Term
      applySubst :: Substitution' (SubstArg ContextEntry)
    -> ContextEntry -> ContextEntry
    applySubst Substitution' (SubstArg ContextEntry)
    rho (CtxVar Name
    x Dom Type
    a)   = Name -> Dom Type -> ContextEntry
    CtxVar Name
    x (Dom Type -> ContextEntry) -> Dom Type -> ContextEntry
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Dom Type))
    Substitution' (SubstArg ContextEntry)
    rho Dom Type
    a

    instance Subst a => Subst (Maybe a) where
      type SubstArg (Maybe a) = SubstArg a

    instance Subst a => Subst [a] where
      type SubstArg [a] = SubstArg a

    instance Subst a => Subst (List1 a) where
      type SubstArg (List1 a) = SubstArg a

    instance (Ord k, Subst a) => Subst (Map k a) where
      type SubstArg (Map k a) = SubstArg a

    instance Subst a => Subst (Ranged a) where
      type SubstArg (Ranged a) = SubstArg a

    instance Subst a => Subst (WithHiding a) where
      type SubstArg (WithHiding a) = SubstArg a

    instance Subst () where
      type SubstArg () = Term
      applySubst :: Substitution' (SubstArg ()) -> () -> ()
    applySubst Substitution' (SubstArg ())
    _ ()
    _ = ()

    instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) where
      type SubstArg (a, b) = SubstArg a
      applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b)
    applySubst Substitution' (SubstArg (a, b))
    rho (a
    x,b
    y) = (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (a, b))
    rho a
    x, Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (a, b))
    rho b
    y)

    instance (Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) where
      type SubstArg (a, b, c) = SubstArg a
      applySubst :: Substitution' (SubstArg (a, b, c)) -> (a, b, c) -> (a, b, c)
    applySubst Substitution' (SubstArg (a, b, c))
    rho (a
    x,b
    y,c
    z) = (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (a, b, c))
    rho a
    x, Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (a, b, c))
    rho b
    y, Substitution' (SubstArg c) -> c -> c
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg c)
    Substitution' (SubstArg (a, b, c))
    rho c
    z)

    instance
      ( Subst a, Subst b, Subst c, Subst d
      , SubstArg a ~ SubstArg b
      , SubstArg b ~ SubstArg c
      , SubstArg c ~ SubstArg d
      ) => Subst (a, b, c, d) where
      type SubstArg (a, b, c, d) = SubstArg a
      applySubst :: Substitution' (SubstArg (a, b, c, d))
    -> (a, b, c, d) -> (a, b, c, d)
    applySubst Substitution' (SubstArg (a, b, c, d))
    rho (a
    x,b
    y,c
    z,d
    u) = (Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg a)
    Substitution' (SubstArg (a, b, c, d))
    rho a
    x, Substitution' (SubstArg b) -> b -> b
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg b)
    Substitution' (SubstArg (a, b, c, d))
    rho b
    y, Substitution' (SubstArg c) -> c -> c
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg c)
    Substitution' (SubstArg (a, b, c, d))
    rho c
    z, Substitution' (SubstArg d) -> d -> d
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg d)
    Substitution' (SubstArg (a, b, c, d))
    rho d
    u)

    instance Subst Candidate where
      type SubstArg Candidate = Term
      applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate
    applySubst Substitution' (SubstArg Candidate)
    rho (Candidate CandidateKind
    q Term
    u Type
    t OverlapMode
    ov) = CandidateKind -> Term -> Type -> OverlapMode -> Candidate
    Candidate CandidateKind
    q (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg Candidate)
    rho Term
    u) (Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Type)
    Substitution' (SubstArg Candidate)
    rho Type
    t) OverlapMode
    ov

    instance Subst EqualityView where
      type SubstArg EqualityView = Term
      applySubst :: Substitution' (SubstArg EqualityView)
    -> EqualityView -> EqualityView
    applySubst Substitution' (SubstArg EqualityView)
    rho = \case
        OtherType Type
    t          -> Type -> EqualityView
    OtherType (Type -> EqualityView) -> Type -> EqualityView
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityView)
    Substitution' (SubstArg Type)
    rho Type
    t
        IdiomType Type
    t          -> Type -> EqualityView
    IdiomType (Type -> EqualityView) -> Type -> EqualityView
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityView)
    Substitution' (SubstArg Type)
    rho Type
    t
        EqualityViewType EqualityTypeData
    eqt -> EqualityTypeData -> EqualityView
    EqualityViewType (EqualityTypeData -> EqualityView)
    -> EqualityTypeData -> EqualityView
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg EqualityTypeData)
    -> EqualityTypeData -> EqualityTypeData
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityTypeData)
    Substitution' (SubstArg EqualityView)
    rho EqualityTypeData
    eqt

    instance Subst EqualityTypeData where
      type SubstArg EqualityTypeData = Term
      applySubst :: Substitution' (SubstArg EqualityTypeData)
    -> EqualityTypeData -> EqualityTypeData
    applySubst Substitution' (SubstArg EqualityTypeData)
    rho (EqualityTypeData Range
    r Sort
    s QName
    eq Args
    l Arg Term
    t Arg Term
    a Arg Term
    b) = Range
    -> Sort
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityTypeData
    EqualityTypeData Range
    r
        (Substitution' (SubstArg Sort) -> Sort -> Sort
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityTypeData)
    Substitution' (SubstArg Sort)
    rho Sort
    s)
        QName
    eq
        ((Arg Term -> Arg Term) -> Args -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Arg Term))
    Substitution' (SubstArg EqualityTypeData)
    rho) Args
    l)
        (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Arg Term))
    Substitution' (SubstArg EqualityTypeData)
    rho Arg Term
    t)
        (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Arg Term))
    Substitution' (SubstArg EqualityTypeData)
    rho Arg Term
    a)
        (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Arg Term))
    Substitution' (SubstArg EqualityTypeData)
    rho Arg Term
    b)

    instance DeBruijn a => DeBruijn (Pattern' a) where
      deBruijnNamedVar :: [Char] -> Int -> Pattern' a
    deBruijnNamedVar [Char]
    n Int
    i             = a -> Pattern' a
    forall a. a -> Pattern' a
    varP (a -> Pattern' a) -> a -> Pattern' a
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> a
    forall a. DeBruijn a => [Char] -> Int -> a
    deBruijnNamedVar [Char]
    n Int
    i
      -- deBruijnView returns Nothing, to prevent consS and the like
      -- from dropping the names and origins when building a substitution.
      deBruijnView :: Pattern' a -> Maybe Int
    deBruijnView Pattern' a
    _                   = Maybe Int
    forall a. Maybe a
    Nothing

    fromPatternSubstitution :: PatternSubstitution -> Substitution
    fromPatternSubstitution :: PatternSubstitution -> Substitution' Term
    fromPatternSubstitution = (DeBruijnPattern -> Term)
    -> PatternSubstitution -> Substitution' Term
    forall a b. (a -> b) -> Substitution' a -> Substitution' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DeBruijnPattern -> Term
    patternToTerm

    applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst :: forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst = Substitution' Term -> a -> a
    Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution' Term -> a -> a)
    -> (PatternSubstitution -> Substitution' Term)
    -> PatternSubstitution
    -> a
    -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatternSubstitution -> Substitution' Term
    fromPatternSubstitution

    usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
    usePatOrigin :: forall a. PatOrigin -> Pattern' a -> Pattern' a
    usePatOrigin PatOrigin
    o Pattern' a
    p = case Pattern' a -> Maybe PatternInfo
    forall x. Pattern' x -> Maybe PatternInfo
    patternInfo Pattern' a
    p of
      Maybe PatternInfo
    Nothing -> Pattern' a
    p
      Just PatternInfo
    i  -> PatternInfo -> Pattern' a -> Pattern' a
    forall a. PatternInfo -> Pattern' a -> Pattern' a
    usePatternInfo (PatternInfo
    i { patOrigin = o }) Pattern' a
    p

    usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
    usePatternInfo :: forall a. PatternInfo -> Pattern' a -> Pattern' a
    usePatternInfo PatternInfo
    i Pattern' a
    p = case Pattern' a -> Maybe PatOrigin
    forall x. Pattern' x -> Maybe PatOrigin
    patternOrigin Pattern' a
    p of
      Maybe PatOrigin
    Nothing         -> Pattern' a
    p
      Just PatOrigin
    PatOSplit  -> Pattern' a
    p
      Just PatOrigin
    PatOAbsurd -> Pattern' a
    p
      Just PatOrigin
    _          -> case Pattern' a
    p of
        (VarP PatternInfo
    _ a
    x) -> PatternInfo -> a -> Pattern' a
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    i a
    x
        (DotP PatternInfo
    _ Term
    u) -> PatternInfo -> Term -> Pattern' a
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    i Term
    u
        (ConP ConHead
    c (ConPatternInfo PatternInfo
    _ Bool
    r Bool
    ft Maybe (Arg Type)
    b Bool
    l) [NamedArg (Pattern' a)]
    ps)
          -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c (PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    i Bool
    r Bool
    ft Maybe (Arg Type)
    b Bool
    l) [NamedArg (Pattern' a)]
    ps
        DefP PatternInfo
    _ QName
    q [NamedArg (Pattern' a)]
    ps -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    i QName
    q [NamedArg (Pattern' a)]
    ps
        (LitP PatternInfo
    _ Literal
    l) -> PatternInfo -> Literal -> Pattern' a
    forall x. PatternInfo -> Literal -> Pattern' x
    LitP PatternInfo
    i Literal
    l
        ProjP{} -> Pattern' a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (IApplyP PatternInfo
    _ Term
    t Term
    u a
    x) -> PatternInfo -> Term -> Term -> a -> Pattern' a
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    i Term
    t Term
    u a
    x

    instance Subst DeBruijnPattern where
      type SubstArg DeBruijnPattern = DeBruijnPattern
      applySubst :: Substitution' (SubstArg DeBruijnPattern)
    -> DeBruijnPattern -> DeBruijnPattern
    applySubst Substitution' (SubstArg DeBruijnPattern)
    IdS = DeBruijnPattern -> DeBruijnPattern
    forall a. a -> a
    id
      applySubst Substitution' (SubstArg DeBruijnPattern)
    rho = \case
        VarP PatternInfo
    i DBPatVar
    x     ->
          PatternInfo -> DeBruijnPattern -> DeBruijnPattern
    forall a. PatternInfo -> Pattern' a -> Pattern' a
    usePatternInfo PatternInfo
    i (DeBruijnPattern -> DeBruijnPattern)
    -> DeBruijnPattern -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> DeBruijnPattern -> DeBruijnPattern
    useName (DBPatVar -> [Char]
    dbPatVarName DBPatVar
    x) (DeBruijnPattern -> DeBruijnPattern)
    -> DeBruijnPattern -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $
          PatternSubstitution -> Int -> DeBruijnPattern
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x
        DotP PatternInfo
    i Term
    u     -> PatternInfo -> Term -> DeBruijnPattern
    forall x. PatternInfo -> Term -> Pattern' x
    DotP PatternInfo
    i (Term -> DeBruijnPattern) -> Term -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho Term
    u
        ConP ConHead
    c ConPatternInfo
    ci [NamedArg DeBruijnPattern]
    ps -> ConHead
    -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    ci {conPType = applyPatSubst rho (conPType ci)} ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
    Substitution' (SubstArg DeBruijnPattern)
    rho [NamedArg DeBruijnPattern]
    ps
        DefP PatternInfo
    i QName
    q [NamedArg DeBruijnPattern]
    ps  -> PatternInfo
    -> QName -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    i QName
    q ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
    Substitution' (SubstArg DeBruijnPattern)
    rho [NamedArg DeBruijnPattern]
    ps
        p :: DeBruijnPattern
    p@(LitP PatternInfo
    _ Literal
    _) -> DeBruijnPattern
    p
        p :: DeBruijnPattern
    p@ProjP{}    -> DeBruijnPattern
    p
        IApplyP PatternInfo
    i Term
    t Term
    u DBPatVar
    x ->
          case [Char] -> DeBruijnPattern -> DeBruijnPattern
    useName (DBPatVar -> [Char]
    dbPatVarName DBPatVar
    x) (DeBruijnPattern -> DeBruijnPattern)
    -> DeBruijnPattern -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ PatternSubstitution -> Int -> DeBruijnPattern
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x of
            IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    i (PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho Term
    t) (PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho Term
    u) DBPatVar
    y
            VarP  PatternInfo
    _ DBPatVar
    y       -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
    IApplyP PatternInfo
    i (PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho Term
    t) (PatternSubstitution -> Term -> Term
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho Term
    u) DBPatVar
    y
            DeBruijnPattern
    _ -> DeBruijnPattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        where
          useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
          useName :: [Char] -> DeBruijnPattern -> DeBruijnPattern
    useName [Char]
    n (VarP PatternInfo
    o DBPatVar
    x)
            | [Char] -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore (DBPatVar -> [Char]
    dbPatVarName DBPatVar
    x)
            = PatternInfo -> DBPatVar -> DeBruijnPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP PatternInfo
    o (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DBPatVar
    x { dbPatVarName = n }
          useName [Char]
    _ DeBruijnPattern
    x = DeBruijnPattern
    x

    instance Subst Range where
      type SubstArg Range = Term
      applySubst :: Substitution' (SubstArg Range) -> Range -> Range
    applySubst Substitution' (SubstArg Range)
    _ = Range -> Range
    forall a. a -> a
    id

    ---------------------------------------------------------------------------
    -- * Projections
    ---------------------------------------------------------------------------

    -- | @projDropParsApply proj o args = 'projDropPars' proj o `'apply'` args@
    --
    --   This function is an optimization, saving us from construction lambdas we
    --   immediately remove through application.
    projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
    projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
    projDropParsApply (Projection Maybe QName
    prop QName
    d Arg QName
    r Int
    _ ProjLams
    lams) ProjOrigin
    o Relevance
    rel Args
    args =
      case [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
    forall a. [a] -> Maybe ([a], a)
    initLast ([Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char]))
    -> [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
    forall a b. (a -> b) -> a -> b
    $ ProjLams -> [Arg [Char]]
    getProjLams ProjLams
    lams of
        -- If we have no more abstractions, we must be a record field
        -- (projection applied already to record value).
        Maybe ([Arg [Char]], Arg [Char])
    Nothing -> if Bool
    proper then QName -> Elims -> Term
    Def QName
    d (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args else Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Just ([Arg [Char]]
    pars, Arg ArgInfo
    i [Char]
    y) ->
          let irr :: Bool
    irr = Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    rel
              core :: Term
    core
                | Bool
    proper Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    irr = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    y (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    d]
                | Bool
    otherwise         = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    y (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 [] Term -> Arg QName -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg QName
    r]
                -- Issue2226: get ArgInfo for principal argument from projFromType
          -- Now drop pars many args
              ([Arg [Char]]
    pars', Args
    args') = [Arg [Char]] -> Args -> ([Arg [Char]], Args)
    forall a b. [a] -> [b] -> ([a], [b])
    dropCommon [Arg [Char]]
    pars Args
    args
          -- We only have to abstract over the parameters that exceed the arguments.
          -- We only have to apply to the arguments that exceed the parameters.
          in (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    List.foldr (\ (Arg ArgInfo
    ai [Char]
    x) -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    x) (Term
    core Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args') [Arg [Char]]
    pars'
      where proper :: Bool
    proper = Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe QName
    prop

    ---------------------------------------------------------------------------
    -- * Telescopes
    ---------------------------------------------------------------------------

    -- ** Telescope view of a type

    type TelView = TelV Type
    data TelV a  = TelV { forall a. TelV a -> Tele (Dom a)
    theTel :: Tele (Dom a), forall a. TelV a -> a
    theCore :: a }
      deriving (Int -> TelV a -> [Char] -> [Char]
    [TelV a] -> [Char] -> [Char]
    TelV a -> [Char]
    (Int -> TelV a -> [Char] -> [Char])
    -> (TelV a -> [Char])
    -> ([TelV a] -> [Char] -> [Char])
    -> Show (TelV a)
    forall a. Show a => Int -> TelV a -> [Char] -> [Char]
    forall a. Show a => [TelV a] -> [Char] -> [Char]
    forall a. Show a => TelV a -> [Char]
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> TelV a -> [Char] -> [Char]
    showsPrec :: Int -> TelV a -> [Char] -> [Char]
    $cshow :: forall a. Show a => TelV a -> [Char]
    show :: TelV a -> [Char]
    $cshowList :: forall a. Show a => [TelV a] -> [Char] -> [Char]
    showList :: [TelV a] -> [Char] -> [Char]
    Show, (forall a b. (a -> b) -> TelV a -> TelV b)
    -> (forall a b. a -> TelV b -> TelV a) -> Functor TelV
    forall a b. a -> TelV b -> TelV a
    forall a b. (a -> b) -> TelV a -> TelV b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
    fmap :: forall a b. (a -> b) -> TelV a -> TelV b
    $c<$ :: forall a b. a -> TelV b -> TelV a
    <$ :: forall a b. a -> TelV b -> TelV a
    Functor)

    deriving instance (TermSubst a, Eq  a) => Eq  (TelV a)
    deriving instance (TermSubst a, Ord a) => Ord (TelV a)

    -- | Takes off all exposed function domains from the given type.
    --   This means that it does not reduce to expose @Pi@-types.
    telView' :: Type -> TelView
    telView' :: Type -> TelView
    telView' = Int -> Type -> TelView
    telView'UpTo (-Int
    1)

    -- | @telView'UpTo n t@ takes off the first @n@ exposed function types of @t@.
    -- Takes off all (exposed ones) if @n < 0@.
    telView'UpTo :: Int -> Type -> TelView
    telView'UpTo :: Int -> Type -> TelView
    telView'UpTo Int
    0 Type
    t = Telescope -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Telescope
    forall a. Tele a
    EmptyTel Type
    t
    telView'UpTo Int
    n 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 -> [Char] -> TelView -> TelView
    forall a. Dom a -> [Char] -> TelV a -> TelV a
    absV Dom Type
    a (Abs Type -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Type
    b) (TelView -> TelView) -> TelView -> TelView
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> TelView
    telView'UpTo (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)
      Term
    _       -> Telescope -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Telescope
    forall a. Tele a
    EmptyTel Type
    t

    -- | Add given binding to the front of the telescope.
    absV :: Dom a -> ArgName -> TelV a -> TelV a
    absV :: forall a. Dom a -> [Char] -> TelV a -> TelV a
    absV Dom a
    a [Char]
    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 ([Char] -> Tele (Dom a) -> Abs (Tele (Dom a))
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x Tele (Dom a)
    tel)) a
    t

    -- ** Creating telescopes from lists of types

    -- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
    bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' :: forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' Name -> a
    f []     Dom Type
    t = []
    bindsToTel' Name -> a
    f (Name
    x:[Name]
    xs) Dom Type
    t = (Type -> (a, Type)) -> Dom Type -> Dom (a, Type)
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name -> a
    f Name
    x,) Dom Type
    t Dom (a, Type) -> [Dom (a, Type)] -> [Dom (a, Type)]
    forall a. a -> [a] -> [a]
    : (Name -> a) -> [Name] -> Dom Type -> [Dom (a, Type)]
    forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' Name -> a
    f [Name]
    xs (Int -> Dom Type -> Dom Type
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Dom Type
    t)

    bindsToTel :: [Name] -> Dom Type -> ListTel
    bindsToTel :: [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
    bindsToTel = (Name -> [Char])
    -> [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
    forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' Name -> [Char]
    nameToArgName

    bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
    bindsToTel'1 :: forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
    bindsToTel'1 Name -> a
    f = (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
    bindsToTel' Name -> a
    f ([Name] -> Dom Type -> ListTel' a)
    -> (List1 Name -> [Name]) -> List1 Name -> Dom Type -> ListTel' a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Name -> [Item (List1 Name)]
    List1 Name -> [Name]
    forall l. IsList l => l -> [Item l]
    List1.toList

    bindsToTel1 :: List1 Name -> Dom Type -> ListTel
    bindsToTel1 :: List1 Name -> Dom Type -> [Dom' Term ([Char], Type)]
    bindsToTel1 = [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
    bindsToTel ([Name] -> Dom Type -> [Dom' Term ([Char], Type)])
    -> (List1 Name -> [Name])
    -> List1 Name
    -> Dom Type
    -> [Dom' Term ([Char], Type)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Name -> [Item (List1 Name)]
    List1 Name -> [Name]
    forall l. IsList l => l -> [Item l]
    List1.toList

    -- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
    namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
    namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
    namedBindsToTel []       Type
    t = Telescope
    forall a. Tele a
    EmptyTel
    namedBindsToTel (NamedArg Name
    x : [NamedArg Name]
    xs) Type
    t =
      Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type
    t Type -> Dom' Term () -> Dom Type
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NamedArg Name -> Dom' Term ()
    domFromNamedArgName NamedArg Name
    x) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs (Name -> [Char]
    nameToArgName (Name -> [Char]) -> Name -> [Char]
    forall a b. (a -> b) -> a -> b
    $ NamedArg Name -> Name
    forall a. NamedArg a -> a
    namedArg NamedArg Name
    x) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Name] -> Type -> Telescope
    namedBindsToTel [NamedArg Name]
    xs (Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Type
    t)

    namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
    namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
    namedBindsToTel1 = [NamedArg Name] -> Type -> Telescope
    namedBindsToTel ([NamedArg Name] -> Type -> Telescope)
    -> (List1 (NamedArg Name) -> [NamedArg Name])
    -> List1 (NamedArg Name)
    -> Type
    -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (NamedArg Name) -> [Item (List1 (NamedArg Name))]
    List1 (NamedArg Name) -> [NamedArg Name]
    forall l. IsList l => l -> [Item l]
    List1.toList

    domFromNamedArgName :: NamedArg Name -> Dom ()
    domFromNamedArgName :: NamedArg Name -> Dom' Term ()
    domFromNamedArgName NamedArg Name
    x = () () -> Dom' Term Name -> Dom' Term ()
    forall a b. a -> Dom' Term b -> Dom' Term a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NamedArg Name -> Dom' Term Name
    forall a. NamedArg a -> Dom a
    domFromNamedArg ((Named NamedName Name -> Named NamedName Name)
    -> NamedArg Name -> NamedArg Name
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName Name -> Named NamedName Name
    forceName NamedArg Name
    x)
      where
        -- If no explicit name is given we use the bound name for the label.
        forceName :: Named NamedName Name -> Named NamedName Name
    forceName (Named Maybe NamedName
    Nothing Name
    x) = Maybe NamedName -> Name -> Named NamedName Name
    forall name a. Maybe name -> a -> Named name a
    Named (NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged [Char] -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged [Char] -> NamedName) -> Ranged [Char] -> NamedName
    forall a b. (a -> b) -> a -> b
    $ Range -> [Char] -> Ranged [Char]
    forall a. Range -> a -> Ranged a
    Ranged (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) ([Char] -> Ranged [Char]) -> [Char] -> Ranged [Char]
    forall a b. (a -> b) -> a -> b
    $ Name -> [Char]
    nameToArgName Name
    x) Name
    x
        forceName Named NamedName Name
    x = Named NamedName Name
    x

    -- ** Abstracting in terms and types

    mkPiSort :: Dom Type -> Abs Type -> Sort
    mkPiSort :: Dom Type -> Abs Type -> Sort
    mkPiSort Dom Type
    a Abs Type
    b = Dom Term -> Sort -> Abs Sort -> Sort
    piSort (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Dom Type -> Dom Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    a) (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Type -> Sort) -> Type -> Sort
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Type -> Sort) -> Abs Type -> Abs Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    b)

    -- | @mkPi dom t = telePi (telFromList [dom]) t@
    mkPi :: Dom (ArgName, Type) -> Type -> Type
    mkPi :: Dom' Term ([Char], Type) -> Type -> Type
    mkPi !Dom' Term ([Char], Type)
    dom Type
    b = Term -> Type
    el (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi Dom Type
    a ([Char] -> Type -> Abs Type
    forall a. (Subst a, Free a) => [Char] -> a -> Abs a
    mkAbs [Char]
    x Type
    b)
      where
        x :: [Char]
    x = ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Dom' Term ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom Dom' Term ([Char], Type)
    dom
        a :: Dom Type
    a = ([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd (([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term ([Char], Type)
    dom
        el :: Term -> Type
    el = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Term -> Type) -> Sort -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Sort
    mkPiSort Dom Type
    a ([Char] -> Type -> Abs Type
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x Type
    b)

    mkLam :: Arg ArgName -> Term -> Term
    mkLam :: Arg [Char] -> Term -> Term
    mkLam Arg [Char]
    a Term
    v = ArgInfo -> Abs Term -> Term
    Lam (Arg [Char] -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg [Char]
    a) ([Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs (Arg [Char] -> [Char]
    forall e. Arg e -> e
    unArg Arg [Char]
    a) Term
    v)

    lamView :: Term -> ([Arg ArgName], Term)
    lamView :: Term -> ([Arg [Char]], Term)
    lamView (Lam ArgInfo
    h (Abs   [Char]
    x Term
    b)) = ([Arg [Char]] -> [Arg [Char]])
    -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (ArgInfo -> [Char] -> Arg [Char]
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    h [Char]
    x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
    forall a. a -> [a] -> [a]
    :) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
    -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Arg [Char]], Term)
    lamView Term
    b
    lamView (Lam ArgInfo
    h (NoAbs [Char]
    x Term
    b)) = ([Arg [Char]] -> [Arg [Char]])
    -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (ArgInfo -> [Char] -> Arg [Char]
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    h [Char]
    x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
    forall a. a -> [a] -> [a]
    :) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
    -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Arg [Char]], Term)
    lamView (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Term
    b)
    lamView Term
    t                   = ([], Term
    t)

    unlamView :: [Arg ArgName] -> Term -> Term
    unlamView :: [Arg [Char]] -> Term -> Term
    unlamView [Arg [Char]]
    xs Term
    b = (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Arg [Char] -> Term -> Term
    mkLam Term
    b [Arg [Char]]
    xs

    telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
    telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
    telePi' Abs Type -> Abs Type
    reAbs = Telescope -> Type -> Type
    telePi where
      telePi :: Telescope -> Type -> Type
    telePi Telescope
    EmptyTel          Type
    t = Type
    t
      telePi (ExtendTel Dom Type
    u Abs Telescope
    tel) Type
    t = Term -> Type
    el (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi Dom Type
    u (Abs Type -> Term) -> Abs Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> Abs Type
    reAbs Abs Type
    b
        where
          b :: Abs Type
    b  = (Telescope -> Type -> Type
    `telePi` Type
    t) (Telescope -> Type) -> Abs Telescope -> Abs Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Telescope
    tel
          el :: Term -> Type
    el = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Term -> Type) -> Sort -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Sort
    mkPiSort Dom Type
    u Abs Type
    b

    -- | Uses free variable analysis to introduce 'NoAbs' bindings.
    telePi :: Telescope -> Type -> Type
    telePi :: Telescope -> Type -> Type
    telePi = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
    telePi' Abs Type -> Abs Type
    forall a. (Subst a, Free a) => Abs a -> Abs a
    reAbs

    -- | Everything will be an 'Abs'.
    telePi_ :: Telescope -> Type -> Type
    telePi_ :: Telescope -> Type -> Type
    telePi_ = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
    telePi' Abs Type -> Abs Type
    forall a. a -> a
    id

    -- | Only abstract the visible components of the telescope,
    --   and all that bind variables.  Everything will be an 'Abs'!
    -- Caution: quadratic time!

    telePiVisible :: Telescope -> Type -> Type
    telePiVisible :: Telescope -> Type -> Type
    telePiVisible Telescope
    EmptyTel Type
    t = Type
    t
    telePiVisible (ExtendTel Dom Type
    u Abs Telescope
    tel) Type
    t
        -- If u is not declared visible and b can be strengthened, skip quantification of u.
        | Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible Dom Type
    u, NoAbs [Char]
    x Type
    t' <- Abs Type
    b' = Type
    t'
        -- Otherwise, include quantification over u.
        | Bool
    otherwise = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Dom Type -> Abs Type -> Sort
    mkPiSort Dom Type
    u Abs Type
    b) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Type -> Term
    Pi Dom Type
    u Abs Type
    b
      where
        b :: Abs Type
    b  = Abs Telescope
    tel Abs Telescope -> (Telescope -> Type) -> Abs Type
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Telescope -> Type -> Type
    `telePiVisible` Type
    t)
        b' :: Abs Type
    b' = Abs Type -> Abs Type
    forall a. (Subst a, Free a) => Abs a -> Abs a
    reAbs Abs Type
    b

    -- | Abstract over a telescope in a term, producing lambdas.
    --   Dumb abstraction: Always produces 'Abs', never 'NoAbs'.
    --
    --   The implementation is sound because 'Telescope' does not use 'NoAbs'.
    teleLam :: Telescope -> Term -> Term
    teleLam :: Telescope -> Term -> Term
    teleLam  Telescope
    EmptyTel         Term
    t = Term
    t
    teleLam (ExtendTel Dom Type
    u Abs Telescope
    tel) Term
    t = ArgInfo -> Abs Term -> Term
    Lam (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    u) (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ (Telescope -> Term -> Term) -> Term -> Telescope -> Term
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Telescope -> Term -> Term
    teleLam Term
    t (Telescope -> Term) -> Abs Telescope -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Telescope
    tel

    -- | Performs void ('noAbs') abstraction over telescope.
    class TeleNoAbs a where
      teleNoAbs :: a -> Term -> Term

    instance TeleNoAbs ListTel where
      teleNoAbs :: [Dom' Term ([Char], Type)] -> Term -> Term
    teleNoAbs [Dom' Term ([Char], Type)]
    tel Term
    t = (Dom' Term ([Char], Type) -> Term -> Term)
    -> Term -> [Dom' Term ([Char], Type)] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai, unDom :: forall t e. Dom' t e -> e
    unDom = ([Char]
    x, Type
    _)} -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    x) Term
    t [Dom' Term ([Char], Type)]
    tel

    instance TeleNoAbs Telescope where
      teleNoAbs :: Telescope -> Term -> Term
    teleNoAbs Telescope
    tel = [Dom' Term ([Char], Type)] -> Term -> Term
    forall a. TeleNoAbs a => a -> Term -> Term
    teleNoAbs ([Dom' Term ([Char], Type)] -> Term -> Term)
    -> [Dom' Term ([Char], Type)] -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel

    -- ** Telescope typing

    -- | Given arguments @vs : tel@ (vector typing), extract their individual types.
    --   Returns @Nothing@ is @tel@ is not long enough.

    typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
    typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
    typeArgsWithTel Telescope
    _ []                         = [Dom Type] -> Maybe [Dom Type]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    typeArgsWithTel (ExtendTel Dom Type
    dom Abs Telescope
    tel) (Term
    v : [Term]
    vs) = (Dom Type
    dom Dom Type -> [Dom Type] -> [Dom Type]
    forall a. a -> [a] -> [a]
    :) ([Dom Type] -> [Dom Type]) -> Maybe [Dom Type] -> Maybe [Dom Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> [Term] -> Maybe [Dom Type]
    typeArgsWithTel (Abs Telescope -> SubstArg Telescope -> Telescope
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Telescope
    tel Term
    SubstArg Telescope
    v) [Term]
    vs
    typeArgsWithTel EmptyTel{} (Term
    _:[Term]
    _)             = Maybe [Dom Type]
    forall a. Maybe a
    Nothing

    ---------------------------------------------------------------------------
    -- * Clauses
    ---------------------------------------------------------------------------

    -- | In compiled clauses, the variables in the clause body are relative to the
    --   pattern variables (including dot patterns) instead of the clause telescope.
    compiledClauseBody :: Clause -> Maybe Term
    compiledClauseBody :: Clause -> Maybe Term
    compiledClauseBody Clause
    cl = Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Permutation -> Substitution' Term
    forall a. DeBruijn a => Permutation -> Substitution' a
    renamingR Permutation
    perm) (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    cl
      where perm :: Permutation
    perm = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Permutation
    clausePerm Clause
    cl

    ---------------------------------------------------------------------------
    -- * Syntactic equality and order
    --
    -- Needs weakening.
    ---------------------------------------------------------------------------

    deriving instance Eq Substitution
    deriving instance Ord Substitution

    deriving instance Eq Sort
    deriving instance Ord Sort
    deriving instance Eq Level
    deriving instance Ord Level
    deriving instance Eq PlusLevel
    deriving instance Eq NotBlocked
    deriving instance Eq t => Eq (Blocked t)
    deriving instance Eq CandidateKind
    deriving instance Eq Candidate
    deriving instance Ord CandidateKind
    deriving instance Ord Candidate

    deriving instance (Subst a, Eq a)  => Eq  (Tele a)
    deriving instance (Subst a, Ord a) => Ord (Tele a)

    -- Andreas, 2019-11-16, issue #4201: to avoid potential unintended
    -- performance loss, the Eq instance for Constraint is disabled:
    --
    -- -- deriving instance Eq Constraint
    --
    -- I am tempted to write
    --
    --   instance Eq Constraint where (==) = undefined
    --
    -- but this does not give a compilation error anymore when trying
    -- to use equality on constraints.
    -- Therefore, I hope this comment is sufficient to prevent a resurrection
    -- of the Eq instance for Constraint.

    deriving instance Eq Section

    instance Ord PlusLevel where
      -- Compare on the atom first. Makes most sense for levelMax.
      compare :: PlusLevel' Term -> PlusLevel' Term -> Ordering
    compare (Plus Integer
    n Term
    a) (Plus Integer
    m Term
    b) = (Term, Integer) -> (Term, Integer) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Term
    a,Integer
    n) (Term
    b,Integer
    m)

    -- | Syntactic 'Type' equality, ignores sort annotations.
    instance Eq a => Eq (Type' a) where
      == :: Type' a -> Type' a -> Bool
    (==) = a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (a -> a -> Bool) -> (Type' a -> a) -> Type' a -> Type' a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Type' a -> a
    forall t a. Type'' t a -> a
    unEl

    instance Ord a => Ord (Type' a) where
      compare :: Type' a -> Type' a -> Ordering
    compare = a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (a -> a -> Ordering)
    -> (Type' a -> a) -> Type' a -> Type' a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Type' a -> a
    forall t a. Type'' t a -> a
    unEl

    -- | Syntactic 'Term' equality, ignores stuff below @DontCare@ and sharing.
    instance Eq Term where
      Var Int
    x Elims
    vs   == :: Term -> Term -> Bool
    == Var Int
    x' Elims
    vs'   = Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    x' Bool -> Bool -> Bool
    && Elims
    vs Elims -> Elims -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elims
    vs'
      Lam ArgInfo
    h Abs Term
    v    == Lam ArgInfo
    h' Abs Term
    v'    = ArgInfo
    h ArgInfo -> ArgInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgInfo
    h' Bool -> Bool -> Bool
    && Abs Term
    v  Abs Term -> Abs Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Abs Term
    v'
      Lit Literal
    l      == Lit Literal
    l'       = Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'
      Def QName
    x Elims
    vs   == Def QName
    x' Elims
    vs'   = QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    x' Bool -> Bool -> Bool
    && Elims
    vs Elims -> Elims -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elims
    vs'
      Con ConHead
    x ConInfo
    _ Elims
    vs == Con ConHead
    x' ConInfo
    _ Elims
    vs' = ConHead
    x ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    x' Bool -> Bool -> Bool
    && Elims
    vs Elims -> Elims -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elims
    vs'
      Pi Dom Type
    a Abs Type
    b     == Pi Dom Type
    a' Abs Type
    b'     = Dom Type
    a Dom Type -> Dom Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Dom Type
    a' Bool -> Bool -> Bool
    && Abs Type
    b Abs Type -> Abs Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Abs Type
    b'
      Sort Sort
    s     == Sort Sort
    s'      = Sort
    s Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    s'
      Level Level
    l    == Level Level
    l'     = Level
    l Level -> Level -> Bool
    forall a. Eq a => a -> a -> Bool
    == Level
    l'
      MetaV MetaId
    m Elims
    vs == MetaV MetaId
    m' Elims
    vs' = MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m' Bool -> Bool -> Bool
    && Elims
    vs Elims -> Elims -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elims
    vs'
      DontCare Term
    _ == DontCare Term
    _   = Bool
    True
      Dummy{}    == Dummy{}      = Bool
    True
      Term
    _          == Term
    _            = Bool
    False

    instance Eq a => Eq (Pattern' a) where
      VarP PatternInfo
    _ a
    x        == :: Pattern' a -> Pattern' a -> Bool
    == VarP PatternInfo
    _ a
    y          = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y
      DotP PatternInfo
    _ Term
    u        == DotP PatternInfo
    _ Term
    v          = Term
    u Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    v
      ConP ConHead
    c ConPatternInfo
    _ [NamedArg (Pattern' a)]
    ps     == ConP ConHead
    c' ConPatternInfo
    _ [NamedArg (Pattern' a)]
    qs      = ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    c Bool -> Bool -> Bool
    && [NamedArg (Pattern' a)]
    ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [NamedArg (Pattern' a)]
    qs
      LitP PatternInfo
    _ Literal
    l        == LitP PatternInfo
    _ Literal
    l'         = Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l'
      ProjP ProjOrigin
    _ QName
    f       == ProjP ProjOrigin
    _ QName
    g         = QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    g
      IApplyP PatternInfo
    _ Term
    u Term
    v a
    x == IApplyP PatternInfo
    _ Term
    u' Term
    v' a
    y = Term
    u Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    u' Bool -> Bool -> Bool
    && Term
    v Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    v' Bool -> Bool -> Bool
    && a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y
      DefP PatternInfo
    _ QName
    f [NamedArg (Pattern' a)]
    ps     == DefP PatternInfo
    _ QName
    g [NamedArg (Pattern' a)]
    qs       = QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    g Bool -> Bool -> Bool
    && [NamedArg (Pattern' a)]
    ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [NamedArg (Pattern' a)]
    qs
      Pattern' a
    _               == Pattern' a
    _                 = Bool
    False

    instance Ord Term where
      Var Int
    a Elims
    b    compare :: Term -> Term -> Ordering
    `compare` Var Int
    x Elims
    y    = (Int, Elims) -> (Int, Elims) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int
    x, Elims
    b) (Int
    a, Elims
    y)
                                        -- sort de Bruijn indices down (#2765)
      Var{}      `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Var{}      = Ordering
    GT
      Def QName
    a Elims
    b    `compare` Def QName
    x Elims
    y    = (QName, Elims) -> (QName, Elims) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (QName
    a, Elims
    b) (QName
    x, Elims
    y)
      Def{}      `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Def{}      = Ordering
    GT
      Con ConHead
    a ConInfo
    _ Elims
    b  `compare` Con ConHead
    x ConInfo
    _ Elims
    y  = (ConHead, Elims) -> (ConHead, Elims) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (ConHead
    a, Elims
    b) (ConHead
    x, Elims
    y)
      Con{}      `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Con{}      = Ordering
    GT
      Lit Literal
    a      `compare` Lit Literal
    x      = Literal -> Literal -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Literal
    a Literal
    x
      Lit{}      `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Lit{}      = Ordering
    GT
      Lam ArgInfo
    a Abs Term
    b    `compare` Lam ArgInfo
    x Abs Term
    y    = (ArgInfo, Abs Term) -> (ArgInfo, Abs Term) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (ArgInfo
    a, Abs Term
    b) (ArgInfo
    x, Abs Term
    y)
      Lam{}      `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Lam{}      = Ordering
    GT
      Pi Dom Type
    a Abs Type
    b     `compare` Pi Dom Type
    x Abs Type
    y     = (Dom Type, Abs Type) -> (Dom Type, Abs Type) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Dom Type
    a, Abs Type
    b) (Dom Type
    x, Abs Type
    y)
      Pi{}       `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Pi{}       = Ordering
    GT
      Sort Sort
    a     `compare` Sort Sort
    x     = Sort -> Sort -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Sort
    a Sort
    x
      Sort{}     `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Sort{}     = Ordering
    GT
      Level Level
    a    `compare` Level Level
    x    = Level -> Level -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Level
    a Level
    x
      Level{}    `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` Level{}    = Ordering
    GT
      MetaV MetaId
    a Elims
    b  `compare` MetaV MetaId
    x Elims
    y  = (MetaId, Elims) -> (MetaId, Elims) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (MetaId
    a, Elims
    b) (MetaId
    x, Elims
    y)
      MetaV{}    `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` MetaV{}    = Ordering
    GT
      DontCare{} `compare` DontCare{} = Ordering
    EQ
      DontCare{} `compare` Term
    _          = Ordering
    LT
      Term
    _          `compare` DontCare{} = Ordering
    GT
      Dummy{}    `compare` Dummy{}    = Ordering
    EQ

    -- Andreas, 2017-10-04, issue #2775, ignore irrelevant arguments during with-abstraction.
    --
    -- For reasons beyond my comprehension, the following Eq instances are not employed
    -- by with-abstraction in TypeChecking.Abstract.isPrefixOf.
    -- Instead, I modified the general Eq instance for Arg to ignore the argument
    -- if irrelevant.

    -- -- | Ignore irrelevant arguments in equality check.
    -- --   Also ignore origin.
    -- instance {-# OVERLAPPING #-} Eq (Arg Term) where
    --   a@(Arg (ArgInfo h r _o) t) == a'@(Arg (ArgInfo h' r' _o') t') = trace ("Eq (Arg Term) on " ++ show a ++ " and " ++ show a') $
    --     h == h' && ((r == Irrelevant) || (r' == Irrelevant) || (t == t'))
    --     -- Andreas, 2017-10-04: According to Syntax.Common, equality on Arg ignores Relevance and Origin.

    -- instance {-# OVERLAPPING #-} Eq Args where
    --   us == vs = length us == length vs && and (zipWith (==) us vs)

    -- instance {-# OVERLAPPING #-} Eq Elims where
    --   us == vs = length us == length vs && and (zipWith (==) us vs)

    -- | Equality of binders relies on weakening
    --   which is a special case of renaming
    --   which is a special case of substitution.
    instance (Subst a, Eq a) => Eq (Abs a) where
      NoAbs [Char]
    _ a
    a == :: Abs a -> Abs a -> Bool
    == NoAbs [Char]
    _ a
    b = a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    b  -- no need to raise if both are NoAbs
      Abs a
    a         == Abs a
    b         = Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    b

    instance (Subst a, Ord a) => Ord (Abs a) where
      NoAbs [Char]
    _ a
    a compare :: Abs a -> Abs a -> Ordering
    `compare` NoAbs [Char]
    _ a
    b = a
    a a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` a
    b  -- no need to raise if both are NoAbs
      Abs a
    a         `compare` Abs a
    b         = Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    a a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Abs a -> a
    forall a. Subst a => Abs a -> a
    absBody Abs a
    b

    deriving instance Ord a => Ord (Dom a)

    instance (Subst a, Eq a)  => Eq  (Elim' a) where
      Apply  Arg a
    a == :: Elim' a -> Elim' a -> Bool
    == Apply  Arg a
    b = Arg a
    a Arg a -> Arg a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Arg a
    b
      Proj ProjOrigin
    _ QName
    x == Proj ProjOrigin
    _ QName
    y = QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    y
      IApply a
    x a
    y a
    r == IApply a
    x' a
    y' a
    r' = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    x' Bool -> Bool -> Bool
    && a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y' Bool -> Bool -> Bool
    && a
    r a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    r'
      Elim' a
    _ == Elim' a
    _ = Bool
    False

    instance (Subst a, Ord a) => Ord (Elim' a) where
      Apply  Arg a
    a compare :: Elim' a -> Elim' a -> Ordering
    `compare` Apply  Arg a
    b = Arg a
    a Arg a -> Arg a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Arg a
    b
      Proj ProjOrigin
    _ QName
    x `compare` Proj ProjOrigin
    _ QName
    y = QName
    x QName -> QName -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` QName
    y
      IApply a
    x a
    y a
    r `compare` IApply a
    x' a
    y' a
    r' = a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    x' Ordering -> Ordering -> Ordering
    forall a. Monoid a => a -> a -> a
    `mappend` a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    y a
    y' Ordering -> Ordering -> Ordering
    forall a. Monoid a => a -> a -> a
    `mappend` a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    r a
    r'
      Apply{}  `compare` Elim' a
    _        = Ordering
    LT
      Elim' a
    _        `compare` Apply{}  = Ordering
    GT
      Proj{}   `compare` Elim' a
    _        = Ordering
    LT
      Elim' a
    _        `compare` Proj{}   = Ordering
    GT

    ---------------------------------------------------------------------------
    -- * Sort stuff
    ---------------------------------------------------------------------------

    -- | @univSort' univInf s@ gets the next higher sort of @s@, if it is
    --   known (i.e. it is not just @UnivSort s@).
    --
    --   Precondition: @s@ is reduced
    univSort' :: Sort -> Either Blocker Sort
    univSort' :: Sort -> Either Blocker Sort
    univSort' (Univ Univ
    u Level
    l)   = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ (Univ -> Univ
    univUniv Univ
    u) (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Level
    levelSuc Level
    l
    univSort' (Inf Univ
    u Integer
    n)    = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ
    univUniv Univ
    u) (Integer -> Sort) -> Integer -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n
    univSort' Sort
    SizeUniv     = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    UType Integer
    0
    univSort' Sort
    LockUniv     = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    1
    univSort' Sort
    LevelUniv    = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    1
    univSort' Sort
    IntervalUniv = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    1
    univSort' (MetaS MetaId
    m Elims
    _)  = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
    univSort' FunSort{}    = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
    univSort' PiSort{}     = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
    univSort' UnivSort{}   = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
    univSort' DefS{}       = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
    univSort' DummyS{}     = Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock

    univSort :: Sort -> Sort
    univSort :: Sort -> Sort
    univSort Sort
    s = (Blocker -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> Either a b -> b
    fromRight (Sort -> Blocker -> Sort
    forall a b. a -> b -> a
    const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort Sort
    s) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Either Blocker Sort
    univSort' Sort
    s

    sort :: Sort -> Type
    sort :: Sort -> Type
    sort Sort
    s = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Sort
    univSort Sort
    s) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term
    Sort Sort
    s

    ssort :: Level -> Type
    ssort :: Level -> Type
    ssort Level
    l = Sort -> Type
    sort (Level -> Sort
    forall t. Level' t -> Sort' t
    SSet Level
    l)

    -- | A sort can either be small (Set l, Prop l, Size, ...)  or large
    --   (Setω n).
    data SizeOfSort = SizeOfSort
      { SizeOfSort -> Univ
    szSortUniv :: Univ
      , SizeOfSort -> Integer
    szSortSize :: Integer
      }

    pattern SmallSort :: Univ -> SizeOfSort
    pattern $mSmallSort :: forall {r}. SizeOfSort -> (Univ -> r) -> ((# #) -> r) -> r
    $bSmallSort :: Univ -> SizeOfSort
    SmallSort u = SizeOfSort u (-1)

    pattern LargeSort :: Univ -> Integer -> SizeOfSort
    -- What I want to write here is:
    -- @
    --   pattern LargeSort u n = SizeOfSort u n | n >= 0
    -- @
    -- But I have to write:
    pattern $mLargeSort :: forall {r}.
    SizeOfSort -> (Univ -> Integer -> r) -> ((# #) -> r) -> r
    $bLargeSort :: Univ -> Integer -> SizeOfSort
    LargeSort u n <- ((\ x :: SizeOfSort
    x@(SizeOfSort Univ
    u Integer
    n) -> Bool -> Maybe ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard (Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0) Maybe () -> SizeOfSort -> Maybe SizeOfSort
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> SizeOfSort
    x) -> Just (SizeOfSort u n))
    -- DON'T WORK:
    -- pattern LargeSort u n <- (n >= 0 -> True)
    -- pattern LargeSort u n <- (n >= 0 -> SizeOfSort u n)
    -- pattern LargeSort u n <- ((>= 0) . szSortSize -> SizeOfSort u n)
      where LargeSort Univ
    u Integer
    n = Univ -> Integer -> SizeOfSort
    SizeOfSort Univ
    u Integer
    n

    {-# COMPLETE SmallSort, LargeSort #-}

    -- | Returns @Left blocker@ for unknown (blocked) sorts, and otherwise
    --   returns @Right s@ where @s@ indicates the size and fibrancy.
    sizeOfSort :: Sort -> Either Blocker SizeOfSort
    sizeOfSort :: Sort -> Either Blocker SizeOfSort
    sizeOfSort = \case
      Univ Univ
    u Level
    _     -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> SizeOfSort
    SmallSort Univ
    u
      Sort
    SizeUniv     -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> SizeOfSort
    SmallSort Univ
    UType
      Sort
    LockUniv     -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> SizeOfSort
    SmallSort Univ
    UType
      Sort
    LevelUniv    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> SizeOfSort
    SmallSort Univ
    UType
      Sort
    IntervalUniv -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> SizeOfSort
    SmallSort Univ
    USSet
      Inf Univ
    u Integer
    n      -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. b -> Either a b
    Right (SizeOfSort -> Either Blocker SizeOfSort)
    -> SizeOfSort -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> SizeOfSort
    LargeSort Univ
    u Integer
    n
      MetaS MetaId
    m Elims
    _    -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left (Blocker -> Either Blocker SizeOfSort)
    -> Blocker -> Either Blocker SizeOfSort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
      FunSort{}    -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      PiSort{}     -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      UnivSort{}   -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      DefS{}       -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      DummyS{}     -> Blocker -> Either Blocker SizeOfSort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock

    isSmallSort :: Sort -> Bool
    isSmallSort :: Sort -> Bool
    isSmallSort Sort
    s = case Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    s of
      Right SmallSort{} -> Bool
    True
      Either Blocker SizeOfSort
    _                 -> Bool
    False

    -- | Compute the sort of a function type from the sorts of its domain and codomain.
    --
    --   This function should only be called on reduced sorts,
    --   since the @LevelUniv@ rules should only apply when the sort does not reduce to @Set@.
    funSort' :: Sort -> Sort -> Either Blocker Sort
    -- Andreas, 2023-05-12, AIM XXXVI, pri #6623:
    -- On GHC 8.6 and 8.8 this pattern matching triggers warning
    -- "Pattern match checker exceeded (2000000) iterations in a case alternative."
    -- No clue how to turn off this warning, so we have to turn off -Werror for GHC < 8.10.
    funSort' :: Sort -> Sort -> Either Blocker Sort
    funSort' = ((Sort, Sort) -> Either Blocker Sort)
    -> Sort -> Sort -> Either Blocker Sort
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry \case
      (Univ Univ
    u Level
    a      , Univ Univ
    u' Level
    b    ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ (Univ -> Univ -> Univ
    funUniv Univ
    u Univ
    u') (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Level -> Level
    levelLub Level
    a Level
    b
      (Inf Univ
    ua Integer
    m      , Sort
    b            ) -> Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    b Either Blocker SizeOfSort
    -> (SizeOfSort -> Sort) -> Either Blocker Sort
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ (SizeOfSort Univ
    ub Integer
    n) -> Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    ua Univ
    ub) (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n)
      (Sort
    a             , Inf Univ
    ub Integer
    n     ) -> Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    a Either Blocker SizeOfSort
    -> (SizeOfSort -> Sort) -> Either Blocker Sort
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ (SizeOfSort Univ
    ua Integer
    m) -> Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    ua Univ
    ub) (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n)
      (Sort
    LockUniv      , Sort
    LevelUniv    ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    LockUniv      , Sort
    b            ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right Sort
    b
      -- No functions into lock types
      (Sort
    a             , Sort
    LockUniv     ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      -- @IntervalUniv@ behaves like @SSet@, but functions into @Type@ land in @Type@
      (Sort
    IntervalUniv  , Sort
    IntervalUniv ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    0
      (Sort
    IntervalUniv  , Univ Univ
    u Level
    b     ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u Level
    b
      (Sort
    IntervalUniv  , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Univ Univ
    u Level
    a      , Sort
    IntervalUniv ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Level
    a
      (Sort
    _             , Sort
    IntervalUniv ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    SizeUniv      , Sort
    b            ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right Sort
    b
      (Sort
    a             , Sort
    SizeUniv     ) -> Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    a Either Blocker SizeOfSort
    -> (SizeOfSort -> Either Blocker Sort) -> Either Blocker Sort
    forall a b.
    Either Blocker a -> (a -> Either Blocker b) -> Either Blocker b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        SmallSort{} -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right Sort
    forall t. Sort' t
    SizeUniv
        LargeSort{} -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      -- No need to handle @LevelUniv@ in a special way here when --level-universe isn't on,
      -- since this function is currently always called after reduction.
      -- It would be safer to take it into account here, but would imply passing the option along as an argument.
      (Sort
    LevelUniv     , Sort
    LevelUniv    ) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right Sort
    forall t. Sort' t
    LevelUniv
      (Sort
    _             , Sort
    LevelUniv    ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    LevelUniv     , Sort
    b            ) -> Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    b Either Blocker SizeOfSort
    -> (SizeOfSort -> Sort) -> Either Blocker Sort
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        SmallSort Univ
    ub -> Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    ub Integer
    0
        LargeSort{}  -> Sort
    b
      (MetaS MetaId
    m Elims
    _     , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
      (Sort
    _             , MetaS MetaId
    m Elims
    _    ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
      (FunSort{}     , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    _             , FunSort{}    ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (PiSort{}      , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    _             , PiSort{}     ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (UnivSort{}    , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    _             , UnivSort{}   ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (DefS{}        , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    _             , DefS{}       ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (DummyS{}      , Sort
    _            ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock
      (Sort
    _             , DummyS{}     ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    neverUnblock

    funSort :: Sort -> Sort -> Sort
    funSort :: Sort -> Sort -> Sort
    funSort Sort
    a Sort
    b = (Blocker -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> Either a b -> b
    fromRight (Sort -> Blocker -> Sort
    forall a b. a -> b -> a
    const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    a Sort
    b) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Either Blocker Sort
    funSort' Sort
    a Sort
    b

    -- | Compute the sort of a pi type from the sorts of its domain
    --   and codomain.
    -- This function should only be called on reduced sorts, since the @LevelUniv@ rules should only apply when the sort doesn't reduce to @Set@
    piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
    piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
    piSort' Dom Term
    a Sort
    s1       (NoAbs [Char]
    _ Sort
    s2) = Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    s1 Sort
    s2
    piSort' Dom Term
    a Sort
    s1 s2Abs :: Abs Sort
    s2Abs@(Abs   [Char]
    _ Sort
    s2) = case Int -> Sort -> Maybe FlexRig
    forall a. Free a => Int -> a -> Maybe FlexRig
    flexRigOccurrenceIn Int
    0 Sort
    s2 of
      Maybe FlexRig
    Nothing -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    s1 (Sort -> Sort) -> Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Abs Sort -> Sort
    forall a. Subst a => Impossible -> Abs a -> a
    noabsApp Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Abs Sort
    s2Abs
      Just FlexRig
    o  -> case (Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    s1 , Sort -> Either Blocker SizeOfSort
    sizeOfSort Sort
    s2) of
        (Right (SmallSort Univ
    u1) , Right (SmallSort Univ
    u2)) -> case FlexRig
    o of
          FlexRig
    StronglyRigid -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    u1 Univ
    u2) Integer
    0
          FlexRig
    Unguarded     -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    u1 Univ
    u2) Integer
    0
          FlexRig
    WeaklyRigid   -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    u1 Univ
    u2) Integer
    0
          Flexible MetaSet
    ms   -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ MetaSet -> Blocker
    metaSetToBlocker MetaSet
    ms
        (Right (LargeSort Univ
    u1 Integer
    n) , Right (SmallSort Univ
    u2)) -> Sort -> Either Blocker Sort
    forall a b. b -> Either a b
    Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf (Univ -> Univ -> Univ
    funUniv Univ
    u1 Univ
    u2) Integer
    n
        (Either Blocker SizeOfSort
    _                     , Right LargeSort{}    ) ->
           -- large sorts cannot depend on variables
           Either Blocker Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
           -- (`trace` __IMPOSSIBLE__) $ unlines
           --   [ "piSort': unexpected dependency in large codomain s2"
           --   , "- a  = " ++ prettyShow a
           --   , "- s1 = " ++ prettyShow s1
           --   , "- s2 = " ++ prettyShow s2
           --   , "- s2 (raw) = " ++ show s2
           --   ]
        (Left Blocker
    blocker          , Right SizeOfSort
    _              ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    blocker
        (Right SizeOfSort
    _               , Left Blocker
    blocker         ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left Blocker
    blocker
        (Left Blocker
    blocker1         , Left Blocker
    blocker2        ) -> Blocker -> Either Blocker Sort
    forall a b. a -> Either a b
    Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Blocker -> Blocker
    unblockOnBoth Blocker
    blocker1 Blocker
    blocker2

    -- Andreas, 2019-06-20
    -- KEEP the following commented out code for the sake of the discussion on irrelevance.
    -- piSort' a bAbs@(Abs   _ b) = case occurrence 0 b of
    --     -- Andreas, Jesper, AIM XXIX, 2019-03-18, issue #3631
    --     -- Remember the NoAbs here!
    --     NoOccurrence  -> Just $ funSort a $ noabsApp __IMPOSSIBLE__ bAbs
    --     -- Andreas, 2017-01-18, issue #2408:
    --     -- The sort of @.(a : A) → Set (f a)@ in context @f : .A → Level@
    --     -- is @dLub Set λ a → Set (lsuc (f a))@, but @DLub@s are not serialized.
    --     -- Alternatives:
    --     -- 1. -- Irrelevantly -> sLub s1 (absApp b $ DontCare $ Sort Prop)
    --     --    We cheat here by simplifying the sort to @Set (lsuc (f *))@
    --     --    where * is a dummy value.  The rationale is that @f * = f a@ (irrelevance!)
    --     --    and that if we already have a neutral level @f a@
    --     --    it should not hurt to have @f *@ even if type @A@ is empty.
    --     --    However: sorts are printed in error messages when sorts do not match.
    --     --    Also, sorts with a dummy like Prop would be ill-typed.
    --     -- 2. We keep the DLub, and serialize it.
    --     --    That's clean and principled, even though DLubs make level solving harder.
    --     -- Jesper, 2018-04-20: another alternative:
    --     -- 3. Return @Inf@ as in the relevant case. This is conservative and might result
    --     --    in more occurrences of @Setω@ than desired, but at least it doesn't pollute
    --     --    the sort system with new 'exotic' sorts.
    --     Irrelevantly  -> Just Inf
    --     StronglyRigid -> Just Inf
    --     Unguarded     -> Just Inf
    --     WeaklyRigid   -> Just Inf
    --     Flexible _    -> Nothing

    piSort :: Dom Term -> Sort -> Abs Sort -> Sort
    piSort :: Dom Term -> Sort -> Abs Sort -> Sort
    piSort Dom Term
    a Sort
    s1 Abs Sort
    s2 = (Blocker -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> Either a b -> b
    fromRight (Sort -> Blocker -> Sort
    forall a b. a -> b -> a
    const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
    forall a b. (a -> b) -> a -> b
    $ Dom Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Dom Term
    a Sort
    s1 Abs Sort
    s2) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
    piSort' Dom Term
    a Sort
    s1 Abs Sort
    s2

    ---------------------------------------------------------------------------
    -- * Level stuff
    ---------------------------------------------------------------------------

    -- ^ Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form.
    levelMax :: Integer -> [PlusLevel] -> Level
    levelMax :: Integer -> [PlusLevel' Term] -> Level
    levelMax !Integer
    n0 [PlusLevel' Term]
    as0 = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n [PlusLevel' Term]
    as
      where
        -- step 1: flatten nested @Level@ expressions in @PlusLevel@s
        Max Integer
    n1 [PlusLevel' Term]
    as1 = Level -> Level
    expandLevel (Level -> Level) -> Level -> Level
    forall a b. (a -> b) -> a -> b
    $ Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n0 [PlusLevel' Term]
    as0
        -- step 2: remove subsumed @PlusLevel@s and sort what remains
        as :: [PlusLevel' Term]
    as        = [PlusLevel' Term] -> [PlusLevel' Term]
    removeSubsumed [PlusLevel' Term]
    as1
        -- step 3: set constant to 0 if it is subsumed by one of the @PlusLevel@s
        greatestB :: Integer
    greatestB = [Integer] -> Integer
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    Prelude.maximum ([Integer] -> Integer) -> [Integer] -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    0 Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [ Integer
    n | Plus Integer
    n Term
    _ <- [PlusLevel' Term]
    as ]
        n :: Integer
    n | Integer
    n1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    greatestB = Integer
    n1
          | Bool
    otherwise      = Integer
    0

        lmax :: Integer -> [PlusLevel] -> [Level] -> Level
        lmax :: Integer -> [PlusLevel' Term] -> [Level] -> Level
    lmax Integer
    m [PlusLevel' Term]
    as []              = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    m [PlusLevel' Term]
    as
        lmax Integer
    m [PlusLevel' Term]
    as (Max Integer
    n [PlusLevel' Term]
    bs : [Level]
    ls) = Integer -> [PlusLevel' Term] -> [Level] -> Level
    lmax (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n) ([PlusLevel' Term]
    bs [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. [a] -> [a] -> [a]
    ++ [PlusLevel' Term]
    as) [Level]
    ls

        expandLevel :: Level -> Level
        expandLevel :: Level -> Level
    expandLevel (Max Integer
    m [PlusLevel' Term]
    as) = Integer -> [PlusLevel' Term] -> [Level] -> Level
    lmax Integer
    m [] ([Level] -> Level) -> [Level] -> Level
    forall a b. (a -> b) -> a -> b
    $ (PlusLevel' Term -> Level) -> [PlusLevel' Term] -> [Level]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' Term -> Level
    expandPlus [PlusLevel' Term]
    as

        expandPlus :: PlusLevel -> Level
        expandPlus :: PlusLevel' Term -> Level
    expandPlus (Plus Integer
    m Term
    l) = Integer -> Level -> Level
    levelPlus Integer
    m (Term -> Level
    expandTm Term
    l)

        expandTm :: Term -> Level
    expandTm (Level Level
    l)       = Level -> Level
    expandLevel Level
    l
        expandTm Term
    l               = Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    l

        removeSubsumed :: [PlusLevel' Term] -> [PlusLevel' Term]
    removeSubsumed =
          ((Term, Integer) -> PlusLevel' Term)
    -> [(Term, Integer)] -> [PlusLevel' Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Term
    a, Integer
    n) -> Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n Term
    a) ([(Term, Integer)] -> [PlusLevel' Term])
    -> ([PlusLevel' Term] -> [(Term, Integer)])
    -> [PlusLevel' Term]
    -> [PlusLevel' Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
          Map Term Integer -> [(Term, Integer)]
    forall k a. Map k a -> [(k, a)]
    MapS.toAscList (Map Term Integer -> [(Term, Integer)])
    -> ([PlusLevel' Term] -> Map Term Integer)
    -> [PlusLevel' Term]
    -> [(Term, Integer)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
          (Integer -> Integer -> Integer)
    -> [(Term, Integer)] -> Map Term Integer
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    MapS.fromListWith Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max ([(Term, Integer)] -> Map Term Integer)
    -> ([PlusLevel' Term] -> [(Term, Integer)])
    -> [PlusLevel' Term]
    -> Map Term Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
          (PlusLevel' Term -> (Term, Integer))
    -> [PlusLevel' Term] -> [(Term, Integer)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Plus Integer
    n Term
    a) -> (Term
    a, Integer
    n))

    -- | Given two levels @a@ and @b@, compute @a ⊔ b@ and return its
    --   canonical form.
    levelLub :: Level -> Level -> Level
    levelLub :: Level -> Level -> Level
    levelLub (Max Integer
    m [PlusLevel' Term]
    as) (Max Integer
    n [PlusLevel' Term]
    bs) = Integer -> [PlusLevel' Term] -> Level
    levelMax (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
    forall a b. (a -> b) -> a -> b
    $ [PlusLevel' Term]
    as [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. [a] -> [a] -> [a]
    ++ [PlusLevel' Term]
    bs

    levelTm :: Level -> Term
    levelTm :: Level -> Term
    levelTm Level
    l =
      case Level
    l of
        Max Integer
    0 [Plus Integer
    0 Term
    l] -> Term
    l
        Level
    _                -> Level -> Term
    Level Level
    l