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

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

    -- | 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 Control.Monad (guard)
    import Data.Coerce
    import Data.Function
    import qualified Data.List as List
    import Data.Map (Map)
    import Data.Maybe
    import Data.HashMap.Strict (HashMap)

    import Debug.Trace (trace)
    import Language.Haskell.TH.Syntax (thenCmp) -- lexicographic combination of Ordering

    import Agda.Interaction.Options

    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.Monad.Options (typeInType)
    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.Empty
    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.Utils.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
    coerce (Term -> t) -> Term -> t
    forall a b. (a -> b) -> a -> b
    $
        case t -> Term
    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
    coerce Abs Term
    b :: Abs t) (Term -> t
    coerce (Term -> t) -> Term -> t
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) t -> Elims -> Term
    forall x. Coercible t x => x -> 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
    coerce Abs Term
    b :: Abs t) (Term -> t
    coerce Term
    a)         t -> Elims -> Term
    forall x. Coercible t x => x -> 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 x. Coercible t x => x -> Elims -> Term
    `app` Elims
    es  -- Andreas, 2011-10-02
            -- need to go under DontCare, since "with" might resurrect irrelevant term
       where
         app :: Coercible t x => x -> Elims -> Term
         app :: forall x. Coercible t x => x -> Elims -> Term
    app x
    t Elims
    es = t -> Term
    coerce (t -> Term) -> t -> Term
    forall a b. (a -> b) -> a -> b
    $ (x -> t
    coerce x
    t :: 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
    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 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
        (Con (ConHead QName
    _ IsRecord{} Induction
    _ [Arg QName]
    fs) ConInfo
    _ Elims
    vs) -> do
          (Arg QName
    fld, Int
    i) <- (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
    forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
    findWithIndex ((QName
    fQName -> 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
          Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Arg QName -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Arg QName
    fld
          -- Andreas, 2018-06-12, issue #2170
          -- The ArgInfo from the ConHead is more accurate (relevance subtyping!).
          ArgInfo -> Arg Term -> Arg Term
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo (Arg QName -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Arg QName
    fld) (Arg Term -> Arg Term)
    -> (Elim' Term -> Maybe (Arg Term))
    -> Elim' Term
    -> Maybe (Arg Term)
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Elim' Term -> Maybe (Arg Term)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim (Elim' Term -> Maybe (Arg Term))
    -> Maybe (Elim' Term) -> Maybe (Arg Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Elims -> Maybe (Elim' Term)
    forall a. [a] -> Maybe a
    listToMaybe (Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    drop Int
    i Elims
    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
    fk ConHead
    ch                  ConInfo
    ci Elims
    args []             = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    ch ConInfo
    ci Elims
    args
    conApp Empty -> Term -> Elims -> Term
    fk 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
    fk ConHead
    ch ConInfo
    ci (Elims
    args Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term
    a]) Elims
    es
    conApp Empty -> Term -> Elims -> Term
    fk 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
    fk ConHead
    ch ConInfo
    ci (Elims
    args Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ [Elim' Term
    a]) Elims
    es
    conApp Empty -> Term -> Elims -> Term
    fk 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
    fk 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
    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
    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
    fQName -> 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 Term
    v
      | Relevance
    Irrelevant <- a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance a
    ai = Term -> Term
    dontCare Term
    v
      | Bool
    otherwise                     = Term
    v

    -- 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 NumGeneralizableArgs
    gens [Maybe Name]
    gpars [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe QName
    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]
    -> NumGeneralizableArgs
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe QName
    -> 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) (NumGeneralizableArgs -> Args -> NumGeneralizableArgs
    forall t. Apply t => t -> Args -> t
    apply NumGeneralizableArgs
    gens Args
    args) (Int -> [Maybe Name] -> [Maybe Name]
    forall a. Int -> [a] -> [a]
    drop (Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [Maybe Name]
    gpars) [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe QName
    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 :: Tele (Dom Type)
    newContext = Tele (Dom Type) -> Args -> Tele (Dom Type)
    forall t. Apply t => t -> Args -> t
    apply (RewriteRule -> Tele (Dom Type)
    rewContext RewriteRule
    r) Args
    args
            sub :: Substitution' NLPat
    sub        = Int -> Substitution' NLPat -> Substitution' NLPat
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 :: QName
    -> Tele (Dom Type)
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> RewriteRule
    RewriteRule
           { rewName :: QName
    rewName    = RewriteRule -> QName
    rewName RewriteRule
    r
           , rewContext :: Tele (Dom Type)
    rewContext = Tele (Dom Type)
    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
           }

      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 (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 (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 (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 (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 :: Int
    projIndex = Projection -> Int
    projIndex Projection
    p Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args
        , projLams :: ProjLams
    projLams  = Projection -> ProjLams
    projLams Projection
    p ProjLams -> Args -> ProjLams
    forall t. Apply t => t -> Args -> t
    `apply` Args
    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 (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 (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args)
        GeneralizableVar{} -> Defn
    d
        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 -> Maybe Projection
    funProjection = Maybe Projection
    Nothing } ->
          Defn
    d { funClauses :: [Clause]
    funClauses    = [Clause] -> Args -> [Clause]
    forall t. Apply t => t -> Args -> t
    apply [Clause]
    cs Args
    args
            , funCompiled :: Maybe CompiledClauses
    funCompiled   = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
    forall t. Apply t => t -> Args -> t
    apply Maybe CompiledClauses
    cc Args
    args
            , funCovering :: [Clause]
    funCovering   = [Clause] -> Args -> [Clause]
    forall t. Apply t => t -> Args -> t
    apply [Clause]
    cov Args
    args
            , funInv :: FunctionInverse
    funInv        = FunctionInverse -> Args -> FunctionInverse
    forall t. Apply t => t -> Args -> t
    apply FunctionInverse
    inv Args
    args
            , funExtLam :: Maybe ExtLamInfo
    funExtLam     = (System -> System) -> ExtLamInfo -> ExtLamInfo
    modifySystem (System -> Args -> System
    forall t. Apply t => t -> Args -> t
    `apply` Args
    args) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe ExtLamInfo
    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 -> Maybe Projection
    funProjection = Just 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 :: Maybe Projection
    funProjection = Maybe Projection
    forall a. HasCallStack => a
    __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 :: Maybe Projection
    funProjection = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    p }
              -- case: applied also to record value (n == 0)
              | Bool
    otherwise ->
                  Defn
    d { funClauses :: [Clause]
    funClauses        = [Clause] -> Args -> [Clause]
    forall t. Apply t => t -> Args -> t
    apply [Clause]
    cs Args
    args'
                    , funCompiled :: Maybe CompiledClauses
    funCompiled       = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
    forall t. Apply t => t -> Args -> t
    apply Maybe CompiledClauses
    cc Args
    args'
                    , funCovering :: [Clause]
    funCovering       = [Clause] -> Args -> [Clause]
    forall t. Apply t => t -> Args -> t
    apply [Clause]
    cov Args
    args'
                    , funInv :: FunctionInverse
    funInv            = FunctionInverse -> Args -> FunctionInverse
    forall t. Apply t => t -> Args -> t
    apply FunctionInverse
    inv Args
    args'
                    , funProjection :: Maybe Projection
    funProjection     = if Bool
    isVar0 then Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    p{ projIndex :: Int
    projIndex = Int
    0 } else Maybe Projection
    forall a. Maybe a
    Nothing
                    , funExtLam :: Maybe ExtLamInfo
    funExtLam         = (System -> System) -> ExtLamInfo -> ExtLamInfo
    modifySystem (\ System
    _ -> System
    forall a. HasCallStack => a
    __IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe ExtLamInfo
    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 :: Int
    dataPars = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args
            , dataClause :: Maybe Clause
    dataClause     = Maybe Clause -> Args -> Maybe Clause
    forall t. Apply t => t -> Args -> t
    apply Maybe Clause
    cl Args
    args
            }
        Record{ recPars :: Defn -> Int
    recPars = Int
    np, recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recTel :: Defn -> Tele (Dom Type)
    recTel = Tele (Dom Type)
    tel
              {-, recArgOccurrences = occ-} } ->
          Defn
    d { recPars :: Int
    recPars = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args
            , recClause :: Maybe Clause
    recClause = Maybe Clause -> Args -> Maybe Clause
    forall t. Apply t => t -> Args -> t
    apply Maybe Clause
    cl Args
    args, recTel :: Tele (Dom Type)
    recTel = Tele (Dom Type) -> Args -> Tele (Dom Type)
    forall t. Apply t => t -> Args -> t
    apply Tele (Dom Type)
    tel Args
    args
    --        , recArgOccurrences = List.drop (length args) occ
            }
        Constructor{ conPars :: Defn -> Int
    conPars = Int
    np } ->
          Defn
    d { conPars :: Int
    conPars = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args }
        Primitive{ primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cs } ->
          Defn
    d { primClauses :: [Clause]
    primClauses = [Clause] -> Args -> [Clause]
    forall t. Apply t => t -> Args -> t
    apply [Clause]
    cs Args
    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 Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def) Args
    args = QName
    -> Int
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    PrimFun QName
    x (Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Args -> Int
    forall a. Sized a => a -> Int
    size Args
    args) ((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)
      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 Tele (Dom Type)
    tel [NamedArg DeBruijnPattern]
    ps Maybe Term
    b Maybe (Arg Type)
    t Bool
    catchall Maybe Bool
    exact Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell) Args
    args
          | Args -> 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 (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg DeBruijnPattern]
    ps = Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          | Bool
    otherwise =
          Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause Range
    rl Range
    rf
                 Tele (Dom Type)
    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 (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
    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
    Substitution' (SubstArg (Maybe (Arg Type)))
    rho Maybe (Arg Type)
    t)
                 Bool
    catchall
                 Maybe Bool
    exact
                 Maybe Bool
    recursive
                 Maybe Bool
    unreachable
                 ExpandedEllipsis
    ell
          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 (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) [NamedArg DeBruijnPattern]
    ps
            n :: Int
    n     = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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' :: Tele (Dom Type)
    tel' = Int
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel Int
    n Tele (Dom Type)
    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
    rho  = (Term -> Term)
    -> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution
    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
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel Int
    n Tele (Dom Type)
    tel [] [] = Tele (Dom Type)
    tel
            newTel Int
    n Tele (Dom Type)
    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
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int -> SubstArg (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall {t} {a}.
    (Eq t, Num t, Subst a, Subst (SubstArg a)) =>
    t -> SubstArg a -> Tele a -> Tele a
    subTel (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 Tele (Dom Type)
    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
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel Int
    n Tele (Dom Type)
    tel [NamedArg DeBruijnPattern]
    ps [Term]
    vs
                ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    ps'        -> Int
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel Int
    n Tele (Dom Type)
    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{}  -> Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                LitP{}  -> Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                ProjP{} -> Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                IApplyP PatternInfo
    _ Term
    _ Term
    _ (DBPatVar [Char]
    _ Int
    i) -> Int
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> [Term]
    -> Tele (Dom Type)
    newTel (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) (Int -> SubstArg (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall {t} {a}.
    (Eq t, Num t, Subst a, Subst (SubstArg a)) =>
    t -> SubstArg a -> Tele a -> Tele a
    subTel (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 Tele (Dom Type)
    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
    _ Tele (Dom Type)
    tel [NamedArg DeBruijnPattern]
    _ [Term]
    _ = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            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 -> Term
    Def 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)]
                                  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 (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
    sub = [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> [Term] -> Substitution
    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 (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
    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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (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 Tele (Dom Type)
    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 Tele (Dom Type) -> [(Face, Term)] -> System
    System Tele (Dom Type)
    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
    Substitution' (SubstArg Term)
    sigma
          nargs :: Int
    nargs = Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args
          ntel :: Int
    ntel = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
          newTel :: Tele (Dom Type)
    newTel = Tele (Dom Type) -> Args -> Tele (Dom Type)
    forall t. Apply t => t -> Args -> t
    apply Tele (Dom Type)
    tel Args
    args
          -- newTel ⊢ σ : tel
          sigma :: Substitution
    sigma = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Int
    ntel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    nargs) ([Term] -> Substitution
    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 (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 (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)          Args
    args = Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    v Args
    args
      apply (DDot Term
    v)           Args
    args = Term -> DisplayTerm
    DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    v 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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Args
    args
      apply (DWithApp DisplayTerm
    v [DisplayTerm]
    ws Elims
    es) Args
    args = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp DisplayTerm
    v [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 = Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE Term
    v Elims
    es
      applyE (DDot Term
    v)            Elims
    es = Term -> DisplayTerm
    DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE Term
    v 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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Elims
    es
      applyE (DWithApp DisplayTerm
    v [DisplayTerm]
    ws Elims
    es') Elims
    es = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp DisplayTerm
    v [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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 :: Tele (Dom Type) -> Drop a -> Drop a
    abstract Tele (Dom Type)
    tel Drop a
    x = Int -> Drop a -> Drop a
    forall a. DoDrop a => Int -> Drop a -> Drop a
    unDrop (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 :: Tele (Dom Type) -> Permutation -> Permutation
    abstract Tele (Dom Type)
    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 = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 :: Tele (Dom Type) -> Term -> Term
    abstract = Tele (Dom Type) -> Term -> Term
    teleLam

    instance Abstract Type where
      abstract :: Tele (Dom Type) -> Type -> Type
    abstract = Tele (Dom Type) -> Type -> Type
    telePi_

    instance Abstract Sort where
      abstract :: Tele (Dom Type) -> Sort -> Sort
    abstract Tele (Dom Type)
    EmptyTel Sort
    s = Sort
    s
      abstract Tele (Dom Type)
    _        Sort
    s = Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__

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

    instance Abstract Definition where
      abstract :: Tele (Dom Type) -> Definition -> Definition
    abstract Tele (Dom Type)
    tel (Defn ArgInfo
    info QName
    x Type
    t [Polarity]
    pol [Occurrence]
    occ NumGeneralizableArgs
    gens [Maybe Name]
    gpars [LocalDisplayForm]
    df MutualId
    m CompiledRepresentation
    c Maybe QName
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang Defn
    d) =
        ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> NumGeneralizableArgs
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe QName
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn ArgInfo
    info QName
    x (Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Type
    t) (Tele (Dom Type) -> [Polarity] -> [Polarity]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel [Polarity]
    pol) (Tele (Dom Type) -> [Occurrence] -> [Occurrence]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel [Occurrence]
    occ) (Tele (Dom Type) -> NumGeneralizableArgs -> NumGeneralizableArgs
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel NumGeneralizableArgs
    gens)
          (Int -> Maybe Name -> [Maybe Name]
    forall a. Int -> a -> [a]
    replicate (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 QName
    inst Bool
    copy Set QName
    ma Bool
    nc Bool
    inj Bool
    copat Blocked_
    blk Language
    lang (Tele (Dom Type) -> Defn -> Defn
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    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 :: Tele (Dom Type) -> RewriteRule -> RewriteRule
    abstract Tele (Dom Type)
    tel (RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c) =
        QName
    -> Tele (Dom Type)
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> RewriteRule
    RewriteRule QName
    q (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Tele (Dom Type)
    gamma) QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c

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

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

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

    instance Abstract Projection where
      abstract :: Tele (Dom Type) -> Projection -> Projection
    abstract Tele (Dom Type)
    tel Projection
    p = Projection
    p
        { projIndex :: Int
    projIndex = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Projection -> Int
    projIndex Projection
    p
        , projLams :: ProjLams
    projLams  = Tele (Dom Type) -> ProjLams -> ProjLams
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel (ProjLams -> ProjLams) -> ProjLams -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ Projection -> ProjLams
    projLams Projection
    p
        }

    instance Abstract ProjLams where
      abstract :: Tele (Dom Type) -> ProjLams -> ProjLams
    abstract Tele (Dom Type)
    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)) (Tele (Dom Type) -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel) [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
    forall a. [a] -> [a] -> [a]
    ++ [Arg [Char]]
    lams

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

    instance Abstract Defn where
      abstract :: Tele (Dom Type) -> Defn -> Defn
    abstract Tele (Dom Type)
    tel Defn
    d = case Defn
    d of
        Axiom{} -> Defn
    d
        DataOrRecSig Int
    n -> Int -> Defn
    DataOrRecSig (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n)
        GeneralizableVar{} -> Defn
    d
        AbstractDefn Defn
    d -> Defn -> Defn
    AbstractDefn (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Defn -> Defn
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    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 -> Maybe Projection
    funProjection = Maybe Projection
    Nothing  } ->
          Defn
    d { funClauses :: [Clause]
    funClauses  = Tele (Dom Type) -> [Clause] -> [Clause]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel [Clause]
    cs
            , funCompiled :: Maybe CompiledClauses
    funCompiled = Tele (Dom Type) -> Maybe CompiledClauses -> Maybe CompiledClauses
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Maybe CompiledClauses
    cc
            , funCovering :: [Clause]
    funCovering = Tele (Dom Type) -> [Clause] -> [Clause]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel [Clause]
    cov
            , funInv :: FunctionInverse
    funInv      = Tele (Dom Type) -> FunctionInverse -> FunctionInverse
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel FunctionInverse
    inv
            , funExtLam :: Maybe ExtLamInfo
    funExtLam   = (System -> System) -> ExtLamInfo -> ExtLamInfo
    modifySystem (Tele (Dom Type) -> System -> System
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe ExtLamInfo
    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 -> Maybe Projection
    funProjection = Just 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' else
            Defn
    d' { funClauses :: [Clause]
    funClauses  = (Clause -> Clause) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (Tele (Dom Type) -> Clause -> Clause
    abstractClause Tele (Dom Type)
    tel1) [Clause]
    cs
               , funCompiled :: Maybe CompiledClauses
    funCompiled = Tele (Dom Type) -> Maybe CompiledClauses -> Maybe CompiledClauses
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel1 Maybe CompiledClauses
    cc
               , funCovering :: [Clause]
    funCovering = Tele (Dom Type) -> [Clause] -> [Clause]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel1 [Clause]
    cov
               , funInv :: FunctionInverse
    funInv      = Tele (Dom Type) -> FunctionInverse -> FunctionInverse
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel1 FunctionInverse
    inv
               , funExtLam :: Maybe ExtLamInfo
    funExtLam   = (System -> System) -> ExtLamInfo -> ExtLamInfo
    modifySystem (\ System
    _ -> System
    forall a. HasCallStack => a
    __IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe ExtLamInfo
    extLam
               }
            where
              d' :: Defn
    d' = Defn
    d { funProjection :: Maybe Projection
    funProjection = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Projection -> Projection
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Projection
    p
                     , funClauses :: [Clause]
    funClauses    = (Clause -> Clause) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (Tele (Dom Type) -> Clause -> Clause
    abstractClause Tele (Dom Type)
    forall a. Tele a
    EmptyTel) [Clause]
    cs }
              tel1 :: Tele (Dom Type)
    tel1 = [Dom' Term ([Char], Type)] -> Tele (Dom Type)
    telFromList ([Dom' Term ([Char], Type)] -> Tele (Dom Type))
    -> [Dom' Term ([Char], Type)] -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
    forall a. Int -> [a] -> [a]
    drop (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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
    $ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
              -- #5128: clause telescopes should be abstracted over the full telescope, regardless of
              --        projection shenanigans.
              abstractClause :: Tele (Dom Type) -> Clause -> Clause
    abstractClause Tele (Dom Type)
    tel1 Clause
    c = (Tele (Dom Type) -> Clause -> Clause
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel1 Clause
    c) { clauseTel :: Tele (Dom Type)
    clauseTel = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel (Tele (Dom Type) -> Tele (Dom Type))
    -> Tele (Dom Type) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Clause -> Tele (Dom Type)
    clauseTel Clause
    c }

        Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl } ->
          Defn
    d { dataPars :: Int
    dataPars       = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
            , dataClause :: Maybe Clause
    dataClause     = Tele (Dom Type) -> Maybe Clause -> Maybe Clause
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Maybe Clause
    cl
            }
        Record{ recPars :: Defn -> Int
    recPars = Int
    np, recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recTel :: Defn -> Tele (Dom Type)
    recTel = Tele (Dom Type)
    tel' } ->
          Defn
    d { recPars :: Int
    recPars    = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
            , recClause :: Maybe Clause
    recClause  = Tele (Dom Type) -> Maybe Clause -> Maybe Clause
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Maybe Clause
    cl
            , recTel :: Tele (Dom Type)
    recTel     = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Tele (Dom Type)
    tel'
            }
        Constructor{ conPars :: Defn -> Int
    conPars = Int
    np } ->
          Defn
    d { conPars :: Int
    conPars = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel }
        Primitive{ primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cs } ->
          Defn
    d { primClauses :: [Clause]
    primClauses = Tele (Dom Type) -> [Clause] -> [Clause]
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel [Clause]
    cs }
        PrimitiveSort{} -> Defn
    d

    instance Abstract PrimFun where
        abstract :: Tele (Dom Type) -> PrimFun -> PrimFun
    abstract Tele (Dom Type)
    tel (PrimFun QName
    x Int
    ar Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
    def) = QName
    -> Int
    -> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
    -> PrimFun
    PrimFun QName
    x (Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n) ((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 = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel

    instance Abstract Clause where
      abstract :: Tele (Dom Type) -> Clause -> Clause
    abstract Tele (Dom Type)
    tel (Clause Range
    rl Range
    rf Tele (Dom Type)
    tel' [NamedArg DeBruijnPattern]
    ps Maybe Term
    b Maybe (Arg Type)
    t Bool
    catchall Maybe Bool
    exact Maybe Bool
    recursive Maybe Bool
    unreachable ExpandedEllipsis
    ell) =
        Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause Range
    rl Range
    rf (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Tele (Dom Type)
    tel')
               (Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m Tele (Dom Type)
    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
               Bool
    catchall
               Maybe Bool
    exact
               Maybe Bool
    recursive
               Maybe Bool
    unreachable
               ExpandedEllipsis
    ell
          where m :: Int
    m = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel'

    instance Abstract CompiledClauses where
      abstract :: Tele (Dom Type) -> CompiledClauses -> CompiledClauses
    abstract Tele (Dom Type)
    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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Int
    i -> Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel) (Tele (Dom Type) -> Case CompiledClauses -> Case CompiledClauses
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    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 (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
    $ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel

    instance Abstract a => Abstract (WithArity a) where
      abstract :: Tele (Dom Type) -> WithArity a -> WithArity a
    abstract Tele (Dom Type)
    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
    $ Tele (Dom Type) -> a -> a
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel a
    a

    instance Abstract a => Abstract (Case a) where
      abstract :: Tele (Dom Type) -> Case a -> Case a
    abstract Tele (Dom Type)
    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 (Tele (Dom Type)
    -> Map QName (WithArity a) -> Map QName (WithArity a)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Map QName (WithArity a)
    cs) ((WithArity a -> WithArity a)
    -> (ConHead, WithArity a) -> (ConHead, WithArity a)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (Tele (Dom Type) -> WithArity a -> WithArity a
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    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)
                     (Tele (Dom Type) -> Map Literal a -> Map Literal a
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Map Literal a
    ls) (Tele (Dom Type) -> Maybe a -> Maybe a
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel Maybe a
    m) Maybe Bool
    b Bool
    lz

    telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
    telVars :: Int -> Tele (Dom Type) -> [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 (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])
    -> (Tele (Dom Type) -> [NamedArg DeBruijnPattern])
    -> Tele (Dom Type)
    -> [Arg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m)

    namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
    namedTelVars :: Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    namedTelVars Int
    m Tele (Dom Type)
    EmptyTel                     = []
    namedTelVars Int
    m (ExtendTel !Dom Type
    dom Abs (Tele (Dom Type))
    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 (Tele (Dom Type)) -> [Char]
    forall a. Abs a -> [Char]
    absName Abs (Tele (Dom Type))
    tel) NamedArg DeBruijnPattern
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. a -> [a] -> [a]
    :
      Int -> Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    namedTelVars (Int
    mInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) (Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. Abs a -> a
    unAbs Abs (Tele (Dom Type))
    tel)

    instance Abstract FunctionInverse where
      abstract :: Tele (Dom Type) -> FunctionInverse -> FunctionInverse
    abstract Tele (Dom Type)
    tel FunctionInverse
    NotInjective  = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
      abstract Tele (Dom Type)
    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
    $ Tele (Dom Type) -> InversionMap Clause -> InversionMap Clause
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel InversionMap Clause
    inv

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

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

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

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

    abstractArgs :: Abstract a => Args -> a -> a
    abstractArgs :: forall a. Abstract a => Args -> a -> a
    abstractArgs Args
    args a
    x = Tele (Dom Type) -> a -> a
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel a
    x
        where
            tel :: Tele (Dom Type)
    tel   = (Arg [Char] -> Tele (Dom Type) -> Tele (Dom Type))
    -> Tele (Dom Type) -> [Arg [Char]] -> Tele (Dom Type)
    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 (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type
    HasCallStack => Type
    __DUMMY_TYPE__ Type -> Dom' Term [Char] -> Dom Type
    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 (Tele (Dom Type)) -> Tele (Dom Type))
    -> (Tele (Dom Type) -> Abs (Tele (Dom Type)))
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    x)
                          Tele (Dom Type)
    forall a. Tele a
    EmptyTel
                  ([Arg [Char]] -> Tele (Dom Type))
    -> [Arg [Char]] -> Tele (Dom Type)
    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 (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$) [[Char]]
    names Args
    args
            names :: [[Char]]
    names = [[Char]] -> [[Char]]
    forall a. [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]
    _) = Permutation -> [a] -> [a]
    forall a. Permutation -> [a] -> [a]
    permute (Permutation -> Permutation
    reverseP Permutation
    p) ((Int -> a) -> [Int] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> a
    forall a. DeBruijn a => Int -> a
    deBruijnVar [Int
    0..]) [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

    -- | 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
    coerce (Term -> t) -> Term -> t
    forall a b. (a -> b) -> a -> b
    $ case t -> Term
    coerce t
    t of
        Var Int
    i Elims
    es    -> t -> Term
    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
    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
    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' (SubstArg Term) -> Term -> Term
    forall t.
    (Coercible t Term, EndoSubst t, Apply t) =>
    Substitution' t -> t -> t
    applySubstTerm

    instance Subst BraveTerm where
      type SubstArg BraveTerm = BraveTerm
      applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
    applySubst = 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
        Type Level' a
    n     -> Level' a -> Sort' a
    forall t. Level' t -> Sort' t
    Type (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
        Prop Level' a
    n     -> Level' a -> Sort' a
    forall t. Level' t -> Sort' t
    Prop (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 IsFibrant
    f Integer
    n    -> IsFibrant -> Integer -> Sort' a
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    n
        SSet Level' a
    n     -> Level' a -> Sort' a
    forall t. Level' t -> Sort' t
    SSet (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
        Sort' a
    SizeUniv   -> Sort' a
    forall t. Sort' t
    SizeUniv
        Sort' a
    LockUniv   -> Sort' a
    forall t. Sort' t
    LockUniv
        PiSort Dom' a a
    a Sort' a
    s1 Abs (Sort' a)
    s2 -> Sort -> Sort' a
    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
    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
    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
    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
    coerce (Sort -> Sort' a) -> Sort -> Sort' a
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Sort
    funSort (Sort' a -> Sort
    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
    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
    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
    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 :: Maybe (Arg Type)
    conPType = Substitution' (SubstArg (Maybe (Arg Type)))
    -> Maybe (Arg Type) -> Maybe (Arg Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Maybe (Arg Type)))
    Substitution' (SubstArg ConPatternInfo)
    rho (Maybe (Arg Type) -> Maybe (Arg Type))
    -> Maybe (Arg Type) -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ ConPatternInfo -> Maybe (Arg Type)
    conPType ConPatternInfo
    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 -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution -> a -> a)
    -> (Substitution' NLPat -> Substitution)
    -> Substitution' NLPat
    -> a
    -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NLPat -> Term) -> Substitution' NLPat -> Substitution
    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 (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 :: Maybe Term
    domTactic = Substitution' NLPat -> Maybe Term -> Maybe Term
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' NLPat
    rho (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Dom a -> Maybe Term
    forall t e. Dom' t e -> Maybe t
    domTactic Dom a
    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 (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
        PType NLPat
    l   -> NLPat -> NLPSort
    PType (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
        PProp NLPat
    l   -> NLPat -> NLPSort
    PProp (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 IsFibrant
    f Integer
    n  -> IsFibrant -> Integer -> NLPSort
    PInf IsFibrant
    f Integer
    n
        NLPSort
    PSizeUniv -> NLPSort
    PSizeUniv
        NLPSort
    PLockUniv -> NLPSort
    PLockUniv

    instance Subst RewriteRule where
      type SubstArg RewriteRule = NLPat
      applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule
    applySubst Substitution' (SubstArg RewriteRule)
    rho (RewriteRule QName
    q Tele (Dom Type)
    gamma QName
    f PElims
    ps Term
    rhs Type
    t Bool
    c) =
        QName
    -> Tele (Dom Type)
    -> QName
    -> PElims
    -> Term
    -> Type
    -> Bool
    -> RewriteRule
    RewriteRule QName
    q (Substitution' NLPat -> Tele (Dom Type) -> Tele (Dom Type)
    forall a. TermSubst a => Substitution' NLPat -> a -> a
    applyNLPatSubst Substitution' (SubstArg RewriteRule)
    Substitution' NLPat
    rho Tele (Dom Type)
    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
        where n :: Int
    n = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    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 (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 -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution
    Substitution' (SubstArg DisplayForm)
    rho) Elims
    ps)
                  (Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    n Substitution
    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)        = Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg DisplayTerm)
    rho Term
    v
      applySubst Substitution' (SubstArg DisplayTerm)
    rho (DDot Term
    v)         = Term -> DisplayTerm
    DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg DisplayTerm)
    rho Term
    v
      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 [DisplayTerm]
    vs Elims
    es) = (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
    -> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
    forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
    uncurry3 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp ((DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm)
    -> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (DisplayTerm, [DisplayTerm], Elims))
    -> (DisplayTerm, [DisplayTerm], Elims)
    -> (DisplayTerm, [DisplayTerm], Elims)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (DisplayTerm, [DisplayTerm], Elims))
    Substitution' (SubstArg DisplayTerm)
    rho (DisplayTerm
    v, [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 MetaId
    m Maybe [Candidate]
    cands     -> MetaId -> Maybe [Candidate] -> Constraint
    FindInstance MetaId
    m (Maybe [Candidate] -> Maybe [Candidate]
    forall a. TermSubst a => a -> a
    rf Maybe [Candidate]
    cands)
        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)
        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 Modality
    mod Term
    m   -> Modality -> Term -> Constraint
    UsableAtModality 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 (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 (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 (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 :: Maybe a
    domTactic = Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Maybe a))
    Substitution' (SubstArg (Dom' a b))
    rho (Dom' a b -> Maybe a
    forall t e. Dom' t e -> Maybe t
    domTactic Dom' a b
    dom) }

    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 (Ord k, Subst a) => Subst (Map k a) where
      type SubstArg (Map k 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 Bool
    ov) = CandidateKind -> Term -> Type -> Bool -> 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) Bool
    ov

    instance Subst EqualityView where
      type SubstArg EqualityView = Term
      applySubst :: Substitution' (SubstArg EqualityView)
    -> EqualityView -> EqualityView
    applySubst Substitution' (SubstArg EqualityView)
    rho (OtherType Type
    t) = Type -> EqualityView
    OtherType
        (Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityView)
    Substitution' (SubstArg Type)
    rho Type
    t)
      applySubst Substitution' (SubstArg EqualityView)
    rho (IdiomType Type
    t) = Type -> EqualityView
    IdiomType
        (Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityView)
    Substitution' (SubstArg Type)
    rho Type
    t)
      applySubst Substitution' (SubstArg EqualityView)
    rho (EqualityType Sort
    s QName
    eq Args
    l Arg Term
    t Arg Term
    a Arg Term
    b) = Sort
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType
        (Substitution' (SubstArg Sort) -> Sort -> Sort
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg EqualityView)
    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 EqualityView)
    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 EqualityView)
    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 EqualityView)
    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 EqualityView)
    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
    fromPatternSubstitution = (DeBruijnPattern -> Term) -> PatternSubstitution -> Substitution
    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 -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution -> a -> a)
    -> (PatternSubstitution -> Substitution)
    -> PatternSubstitution
    -> a
    -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatternSubstitution -> Substitution
    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 :: PatOrigin
    patOrigin = 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 :: Maybe (Arg Type)
    conPType = PatternSubstitution -> Maybe (Arg Type) -> Maybe (Arg Type)
    forall a. TermSubst a => PatternSubstitution -> a -> a
    applyPatSubst PatternSubstitution
    Substitution' (SubstArg DeBruijnPattern)
    rho (ConPatternInfo -> Maybe (Arg Type)
    conPType ConPatternInfo
    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 :: [Char]
    dbPatVarName = [Char]
    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 (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 (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
    showList :: [TelV a] -> [Char] -> [Char]
    $cshowList :: forall a. Show a => [TelV a] -> [Char] -> [Char]
    show :: TelV a -> [Char]
    $cshow :: forall a. Show a => TelV a -> [Char]
    showsPrec :: Int -> TelV a -> [Char] -> [Char]
    $cshowsPrec :: forall a. Show a => Int -> 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
    <$ :: forall a b. a -> TelV b -> TelV a
    $c<$ :: forall a b. a -> TelV b -> TelV a
    fmap :: forall a b. (a -> b) -> TelV a -> TelV b
    $cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
    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 = Tele (Dom Type) -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t
    telView'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
    _       -> Tele (Dom Type) -> Type -> TelView
    forall a. Tele (Dom a) -> a -> TelV a
    TelV Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t
      where
        absV :: Dom a -> [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 (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 -> [Name]
    forall a. NonEmpty a -> [a]
    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 -> [Name]
    forall a. NonEmpty a -> [a]
    List1.toList

    -- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
    namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
    namedBindsToTel :: [NamedArg Name] -> Type -> Tele (Dom Type)
    namedBindsToTel []       Type
    t = Tele (Dom Type)
    forall a. Tele a
    EmptyTel
    namedBindsToTel (NamedArg Name
    x : [NamedArg Name]
    xs) Type
    t =
      Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type
    t Type -> Dom' Term () -> Dom Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NamedArg Name -> Dom' Term ()
    domFromNamedArgName NamedArg Name
    x) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    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) (Tele (Dom Type) -> Abs (Tele (Dom Type)))
    -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Name] -> Type -> Tele (Dom Type)
    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 -> Tele (Dom Type)
    namedBindsToTel1 = [NamedArg Name] -> Type -> Tele (Dom Type)
    namedBindsToTel ([NamedArg Name] -> Type -> Tele (Dom Type))
    -> (List1 (NamedArg Name) -> [NamedArg Name])
    -> List1 (NamedArg Name)
    -> Type
    -> Tele (Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (NamedArg Name) -> [NamedArg Name]
    forall a. NonEmpty a -> [a]
    List1.toList

    domFromNamedArgName :: NamedArg Name -> Dom ()
    domFromNamedArgName :: NamedArg Name -> Dom' Term ()
    domFromNamedArgName NamedArg Name
    x = () () -> Dom' Term Name -> Dom' Term ()
    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 (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 (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 (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 (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) -> Tele (Dom Type) -> Type -> Type
    telePi' Abs Type -> Abs Type
    reAbs = Tele (Dom Type) -> Type -> Type
    telePi where
      telePi :: Tele (Dom Type) -> Type -> Type
    telePi Tele (Dom Type)
    EmptyTel          Type
    t = Type
    t
      telePi (ExtendTel Dom Type
    u Abs (Tele (Dom Type))
    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  = (Tele (Dom Type) -> Type -> Type
    `telePi` Type
    t) (Tele (Dom Type) -> Type) -> Abs (Tele (Dom Type)) -> Abs Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (Tele (Dom Type))
    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 :: Tele (Dom Type) -> Type -> Type
    telePi = (Abs Type -> Abs Type) -> Tele (Dom Type) -> 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_ :: Tele (Dom Type) -> Type -> Type
    telePi_ = (Abs Type -> Abs Type) -> Tele (Dom Type) -> 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 :: Tele (Dom Type) -> Type -> Type
    telePiVisible Tele (Dom Type)
    EmptyTel Type
    t = Type
    t
    telePiVisible (ExtendTel Dom Type
    u Abs (Tele (Dom Type))
    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 (Tele (Dom Type))
    tel Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> Type) -> Abs Type
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (Tele (Dom Type) -> 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 :: Tele (Dom Type) -> Term -> Term
    teleLam  Tele (Dom Type)
    EmptyTel         Term
    t = Term
    t
    teleLam (ExtendTel Dom Type
    u Abs (Tele (Dom Type))
    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
    $ (Tele (Dom Type) -> Term -> Term)
    -> Term -> Tele (Dom Type) -> Term
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Tele (Dom Type) -> Term -> Term
    teleLam Term
    t (Tele (Dom Type) -> Term) -> Abs (Tele (Dom Type)) -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs (Tele (Dom Type))
    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 (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 :: Tele (Dom Type) -> Term -> Term
    teleNoAbs Tele (Dom Type)
    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
    $ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    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 :: Tele (Dom Type) -> [Term] -> Maybe [Dom Type]
    typeArgsWithTel Tele (Dom Type)
    _ []                         = [Dom Type] -> Maybe [Dom Type]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    typeArgsWithTel (ExtendTel Dom Type
    dom Abs (Tele (Dom Type))
    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
    <$> Tele (Dom Type) -> [Term] -> Maybe [Dom Type]
    typeArgsWithTel (Abs (Tele (Dom Type))
    -> SubstArg (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs (Tele (Dom Type))
    tel Term
    SubstArg (Tele (Dom Type))
    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
    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 (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 -> PlusLevel -> 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 -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Int
    x Int
    a Ordering -> Ordering -> Ordering
    `thenCmp` Elims -> Elims -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Elims
    b 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 -> Maybe Sort
    univSort' :: Sort -> Maybe Sort
    univSort' (Type Level
    l) = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
    $ Level -> Level
    levelSuc Level
    l
    univSort' (Prop Level
    l) = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
    $ Level -> Level
    levelSuc Level
    l
    univSort' (Inf IsFibrant
    f Integer
    n) = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f (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' (SSet Level
    l) = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Level
    levelSuc Level
    l
    univSort' Sort
    SizeUniv = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    IsFibrant Integer
    0
    univSort' Sort
    LockUniv = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    IsFibrant Integer
    0 -- lock polymorphism is not actually supported
    univSort' Sort
    s        = Maybe Sort
    forall a. Maybe a
    Nothing

    univSort :: Sort -> Sort
    univSort :: Sort -> Sort
    univSort Sort
    s = Sort -> Maybe Sort -> Sort
    forall a. a -> Maybe a -> a
    fromMaybe (Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort Sort
    s) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Maybe 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)

    -- | Returns @Nothing@ for unknown (meta) sorts, and otherwise returns
    --   @Just (b,f)@ where @b@ indicates smallness and @f@ fibrancy.
    --   I.e., @b@ is @True@ for (relatively) small sorts like @Set l@ and
    --   @Prop l@, and instead @b@ is @False@ for large sorts such as @Setω@.
    isSmallSort :: Sort -> Maybe (Bool,IsFibrant)
    isSmallSort :: Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Type{}     = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    True,IsFibrant
    IsFibrant)
    isSmallSort Prop{}     = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    True,IsFibrant
    IsFibrant)
    isSmallSort Sort
    SizeUniv   = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    True,IsFibrant
    IsFibrant)
    isSmallSort Sort
    LockUniv   = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    True,IsFibrant
    IsFibrant)
    isSmallSort (Inf IsFibrant
    f Integer
    _)  = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    False,IsFibrant
    f)
    isSmallSort SSet{}     = (Bool, IsFibrant) -> Maybe (Bool, IsFibrant)
    forall a. a -> Maybe a
    Just (Bool
    True,IsFibrant
    IsStrict)
    isSmallSort MetaS{}    = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing
    isSmallSort FunSort{}  = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing
    isSmallSort PiSort{}   = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing
    isSmallSort UnivSort{} = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing
    isSmallSort DefS{}     = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing
    isSmallSort DummyS{}   = Maybe (Bool, IsFibrant)
    forall a. Maybe a
    Nothing

    fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    IsStrict IsFibrant
    a = IsFibrant
    IsStrict
    fibrantLub IsFibrant
    a IsFibrant
    IsStrict = IsFibrant
    IsStrict
    fibrantLub IsFibrant
    a IsFibrant
    b = IsFibrant
    a

    -- | Compute the sort of a function type from the sorts of its
    --   domain and codomain.
    funSort' :: Sort -> Sort -> Maybe Sort
    funSort' :: Sort -> Sort -> Maybe Sort
    funSort' Sort
    a Sort
    b = case (Sort
    a, Sort
    b) of
      (Inf IsFibrant
    af Integer
    m      , Inf IsFibrant
    bf Integer
    n     ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    af IsFibrant
    bf) (Integer -> Sort) -> Integer -> Sort
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n
      (Inf IsFibrant
    af Integer
    m      , Sort
    b            ) | Just (Bool
    True,IsFibrant
    bf) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    b -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    af IsFibrant
    bf) Integer
    m
      (Sort
    a             , Inf IsFibrant
    bf Integer
    n     ) | Just (Bool
    True,IsFibrant
    af) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    a -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    af IsFibrant
    bf) Integer
    n
      (Type Level
    a        , Type Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
    $ Level -> Level -> Level
    levelLub Level
    a Level
    b
      (Sort
    LockUniv      , Sort
    b            ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just Sort
    b
      -- No functions into lock types
      (Sort
    a             , Sort
    LockUniv     ) -> Maybe Sort
    forall a. Maybe a
    Nothing
      (Sort
    SizeUniv      , Sort
    b            ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just Sort
    b
      (Sort
    a             , Sort
    SizeUniv     ) | Just (Bool
    True,IsFibrant
    _) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    a -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just Sort
    forall t. Sort' t
    SizeUniv
      (Prop Level
    a        , Type Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
    $ Level -> Level -> Level
    levelLub Level
    a Level
    b
      (Type Level
    a        , Prop Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Level -> Level
    levelLub Level
    a Level
    b
      (Prop Level
    a        , Prop Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort) -> Level -> Sort
    forall a b. (a -> b) -> a -> b
    $ Level -> Level -> Level
    levelLub Level
    a Level
    b
      (SSet Level
    a        , SSet Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Level -> Level
    levelLub Level
    a Level
    b
      (Type Level
    a        , SSet Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Level -> Level
    levelLub Level
    a Level
    b
      (SSet Level
    a        , Type Level
    b       ) -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Level -> Level
    levelLub Level
    a Level
    b
      (Sort
    a             , Sort
    b            ) -> Maybe Sort
    forall a. Maybe a
    Nothing

    funSort :: Sort -> Sort -> Sort
    funSort :: Sort -> Sort -> Sort
    funSort Sort
    a Sort
    b = Sort -> Maybe Sort -> Sort
    forall a. a -> Maybe a -> a
    fromMaybe (Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort Sort
    a Sort
    b) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> Sort -> Maybe Sort
    funSort' Sort
    a Sort
    b

    -- | Compute the sort of a pi type from the sorts of its domain
    --   and codomain.
    piSort' :: Dom Term -> Sort -> Abs Sort -> Maybe Sort
    piSort' :: Dom Term -> Sort -> Abs Sort -> Maybe Sort
    piSort' Dom Term
    a Sort
    s1       (NoAbs [Char]
    _ Sort
    s2) = Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 | Just (Bool
    True, IsFibrant
    f1) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    s1, Just (Bool
    True, IsFibrant
    f2) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    s2 -> case FlexRig' ()
    o of
        FlexRig' ()
    StronglyRigid -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    f1 IsFibrant
    f2) Integer
    0
        FlexRig' ()
    Unguarded     -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    f1 IsFibrant
    f2) Integer
    0
        FlexRig' ()
    WeaklyRigid   -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    f1 IsFibrant
    f2) Integer
    0
        Flexible ()
    _    -> Maybe Sort
    forall a. Maybe a
    Nothing
      Just FlexRig' ()
    o | Inf IsFibrant
    f1 Integer
    n <- Sort
    s1 , Just (Bool
    True, IsFibrant
    f2) <- Sort -> Maybe (Bool, IsFibrant)
    isSmallSort Sort
    s2 -> Sort -> Maybe Sort
    forall a. a -> Maybe a
    Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf (IsFibrant -> IsFibrant -> IsFibrant
    fibrantLub IsFibrant
    f1 IsFibrant
    f2) Integer
    n
      Just FlexRig' ()
    _ -> Maybe Sort
    forall a. Maybe a
    Nothing

    -- 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 = case Dom Term -> Sort -> Abs Sort -> Maybe Sort
    piSort' Dom Term
    a Sort
    s1 Abs Sort
    s2 of
      Just Sort
    s  -> Sort
    s
      Maybe Sort
    Nothing -> 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

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

    -- ^ Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form.
    levelMax :: Integer -> [PlusLevel] -> Level
    levelMax :: Integer -> [PlusLevel] -> Level
    levelMax Integer
    n0 [PlusLevel]
    as0 = Integer -> [PlusLevel] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n [PlusLevel]
    as
      where
        -- step 1: flatten nested @Level@ expressions in @PlusLevel@s
        Max Integer
    n1 [PlusLevel]
    as1 = Level -> Level
    expandLevel (Level -> Level) -> Level -> Level
    forall a b. (a -> b) -> a -> b
    $ Integer -> [PlusLevel] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n0 [PlusLevel]
    as0
        -- step 2: remove subsumed @PlusLevel@s
        as2 :: [PlusLevel]
    as2       = [PlusLevel] -> [PlusLevel]
    forall {a}. Eq a => [PlusLevel' a] -> [PlusLevel' a]
    removeSubsumed [PlusLevel]
    as1
        -- step 3: sort remaining @PlusLevel@s
        as :: [PlusLevel]
    as        = [PlusLevel] -> [PlusLevel]
    forall a. Ord a => [a] -> [a]
    List.sort [PlusLevel]
    as2
        -- step 4: set constant to 0 if it is subsumed by one of the @PlusLevel@s
        greatestB :: Integer
    greatestB = [Integer] -> Integer
    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]
    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] -> [Level] -> Level
    lmax Integer
    m [PlusLevel]
    as []              = Integer -> [PlusLevel] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    m [PlusLevel]
    as
        lmax Integer
    m [PlusLevel]
    as (Max Integer
    n [PlusLevel]
    bs : [Level]
    ls) = Integer -> [PlusLevel] -> [Level] -> Level
    lmax (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n) ([PlusLevel]
    bs [PlusLevel] -> [PlusLevel] -> [PlusLevel]
    forall a. [a] -> [a] -> [a]
    ++ [PlusLevel]
    as) [Level]
    ls

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

        expandPlus :: PlusLevel -> Level
        expandPlus :: PlusLevel -> 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' a] -> [PlusLevel' a]
    removeSubsumed [] = []
        removeSubsumed (Plus Integer
    n a
    a : [PlusLevel' a]
    bs)
          | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Integer] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Integer]
    ns = [PlusLevel' a] -> [PlusLevel' a]
    removeSubsumed [PlusLevel' a]
    bs
          | Bool
    otherwise     = Integer -> a -> PlusLevel' a
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n a
    a PlusLevel' a -> [PlusLevel' a] -> [PlusLevel' a]
    forall a. a -> [a] -> [a]
    : [PlusLevel' a] -> [PlusLevel' a]
    removeSubsumed [ PlusLevel' a
    b | b :: PlusLevel' a
    b@(Plus Integer
    _ a
    a') <- [PlusLevel' a]
    bs, a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    a' ]
          where
            ns :: [Integer]
    ns = [ Integer
    m | Plus Integer
    m a
    a' <- [PlusLevel' a]
    bs, a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    a', Integer
    m Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 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]
    as) (Max Integer
    n [PlusLevel]
    bs) = Integer -> [PlusLevel] -> Level
    levelMax (Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    m Integer
    n) ([PlusLevel] -> Level) -> [PlusLevel] -> Level
    forall a b. (a -> b) -> a -> b
    $ [PlusLevel]
    as [PlusLevel] -> [PlusLevel] -> [PlusLevel]
    forall a. [a] -> [a] -> [a]
    ++ [PlusLevel]
    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