    -- | Reconstruct dropped parameters from constructors.  Used by
    --   with-abstraction to avoid ill-typed abstractions (#745). Note that the
    --   term is invalid after parameter reconstruction. Parameters need to be
    --   dropped again before using it.

    module Agda.TypeChecking.ReconstructParameters where

    import Data.Maybe
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.Irrelevance
    import Agda.TypeChecking.ProjectionLike
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Datatypes

    import Agda.Utils.Size
    import Agda.Utils.Either
    import Agda.Utils.Function (applyWhen)

    import Agda.Utils.Impossible

    reconstructParametersInType :: Type -> TCM Type
    reconstructParametersInType :: Type -> TCM Type
    reconstructParametersInType = Action (TCMT IO) -> Type -> TCM Type
    reconstructParametersInType' Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction

    reconstructParametersInType' :: Action TCM -> Type -> TCM Type
    reconstructParametersInType' :: Action (TCMT IO) -> Type -> TCM Type
    reconstructParametersInType' Action (TCMT IO)
    act Type
    a =
      (Term -> TCMT IO Term) -> Type -> TCM Type
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Action (TCMT IO) -> Type -> Term -> TCMT IO Term
    reconstructParameters' Action (TCMT IO)
    act (Sort -> Type
    sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    a)) Type
    a

    reconstructParametersInTel :: Telescope -> TCM Telescope
    reconstructParametersInTel :: Telescope -> TCM Telescope
    reconstructParametersInTel Telescope
    EmptyTel = Telescope -> TCM Telescope
    forall (m :: * -> *) a. Monad m => a -> m a
    return Telescope
    forall a. Tele a
    EmptyTel
    reconstructParametersInTel (ExtendTel Dom Type
    a Abs Telescope
    tel) = do
      Type
    ar <- Type -> TCM Type
    reconstructParametersInType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
      ([Char], Dom Type) -> TCM Telescope -> TCM Telescope
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs Telescope -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Telescope
    tel, Dom Type
    a) (TCM Telescope -> TCM Telescope) -> TCM Telescope -> TCM Telescope
    forall a b. (a -> b) -> a -> b
    $
        Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type
    ar Type -> Dom Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type
    a) (Abs Telescope -> Telescope)
    -> TCMT IO (Abs Telescope) -> TCM Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Telescope -> TCM Telescope)
    -> Abs Telescope -> TCMT IO (Abs Telescope)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Telescope -> TCM Telescope
    reconstructParametersInTel Abs Telescope
    tel

    reconstructParametersInEqView :: EqualityView -> TCM EqualityView
    reconstructParametersInEqView :: EqualityView -> TCM EqualityView
    reconstructParametersInEqView (EqualityType Sort
    s QName
    eq [Arg Term]
    l Arg Term
    a Arg Term
    u Arg Term
    v) =
      Sort
    -> QName
    -> [Arg Term]
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType Sort
    s QName
    eq [Arg Term]
    l (Arg Term -> Arg Term -> Arg Term -> EqualityView)
    -> TCMT IO (Arg Term)
    -> TCMT IO (Arg Term -> Arg Term -> EqualityView)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Type -> Term -> TCMT IO Term
    reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Type
    sort Sort
    s) Arg Term
    a
                          TCMT IO (Arg Term -> Arg Term -> EqualityView)
    -> TCMT IO (Arg Term) -> TCMT IO (Arg Term -> EqualityView)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Type -> Term -> TCMT IO Term
    reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) Arg Term
    u
                          TCMT IO (Arg Term -> EqualityView)
    -> TCMT IO (Arg Term) -> TCM EqualityView
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Type -> Term -> TCMT IO Term
    reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) Arg Term
    v
    reconstructParametersInEqView (OtherType Type
    a) = Type -> EqualityView
    OtherType (Type -> EqualityView) -> TCM Type -> TCM EqualityView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM Type
    reconstructParametersInType Type
    a
    reconstructParametersInEqView (IdiomType Type
    a) = Type -> EqualityView
    IdiomType (Type -> EqualityView) -> TCM Type -> TCM EqualityView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM Type
    reconstructParametersInType Type
    a

    reconstructParameters :: Type -> Term -> TCM Term
    reconstructParameters :: Type -> Term -> TCMT IO Term
    reconstructParameters = Action (TCMT IO) -> Type -> Term -> TCMT IO Term
    reconstructParameters' Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction

    reconstructParameters' :: Action TCM -> Type -> Term -> TCM Term
    reconstructParameters' :: Action (TCMT IO) -> Type -> Term -> TCMT IO Term
    reconstructParameters' Action (TCMT IO)
    act Type
    a Term
    v = do
      [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.with.reconstruct" Int
    30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCM Doc
    "reconstructing parameters in"
            , Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCM Doc
    ":", Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ] ]
      Term
    v <- Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action (TCMT IO)
    reconstructAction Term
    v Comparison
    CmpLeq Type
    a

      [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.with.reconstruct" Int
    30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "-->" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v
      Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
      where
        reconstructAction :: Action (TCMT IO)
    reconstructAction = Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction{ postAction :: Type -> Term -> TCMT IO Term
    postAction = Type -> Term -> TCMT IO Term
    reconstruct }

        reconstruct :: Type -> Term -> TCMT IO Term
    reconstruct Type
    a Term
    v = do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.with.reconstruct" Int
    30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCM Doc
    "reconstructing in"
            , Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCM Doc
    ":", Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ] ]
          case Term -> Term
    unSpine Term
    v of
            Con ConHead
    h ConInfo
    ci [Elim]
    vs -> do
              ConHead
    hh <- (SigError -> ConHead) -> Either SigError ConHead -> ConHead
    forall a b. (a -> b) -> Either a b -> b
    fromRight SigError -> ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Either SigError ConHead -> ConHead)
    -> TCM (Either SigError ConHead) -> TCM ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead (ConHead -> QName
    conName ConHead
    h)
              TelV Telescope
    tel Type
    a <- Type -> TCM (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
              let under :: Int
    under = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel  -- under-applied when under > 0
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCM Doc
    "reconstructing"
                    , Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCM Doc
    ":"
                                   , Int -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ] ]
              case (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a) of
                Def QName
    d [Elim]
    es -> do
                  Just Int
    n <- Definition -> Maybe Int
    defParameters (Definition -> Maybe Int) -> TCM Definition -> TCM (Maybe Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
                  let prePs :: [Elim]
    prePs = Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> Int -> Substitution' Term
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible Int
    under) ([Elim] -> [Elim]) -> ([Elim] -> [Elim]) -> [Elim] -> [Elim]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Elim] -> [Elim]
    forall a. Int -> [a] -> [a]
    take Int
    n ([Elim] -> [Elim]) -> [Elim] -> [Elim]
    forall a b. (a -> b) -> a -> b
    $ [Elim]
    es
                  let hiddenPs :: [Elim]
    hiddenPs = (Arg Term -> Elim) -> [Arg Term] -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> (Arg Term -> Arg Term) -> Arg Term -> Elim
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Arg Term
    forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams) ([Arg Term] -> [Elim]) -> [Arg Term] -> [Elim]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $
                                   [Elim] -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    prePs
                  [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The hiddenPs are" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Elim] -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Elim]
    hiddenPs
                  Type
    tyCon <- Definition -> Type
    defType (Definition -> Type) -> TCM Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    hh)
                  [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Here we start infering spine"
                  ((Term
    _,Con ConHead
    hh ConInfo
    ci [Elim]
    psAfterAct),Type
    _) <- Action (TCMT IO)
    -> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
    inferSpine' Action (TCMT IO)
    act Type
    tyCon (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    hh ConInfo
    ci []) (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    hh ConInfo
    ci []) [Elim]
    hiddenPs
                  ((Term
    _,Term
    conWithPars),Type
    _) <- Action (TCMT IO)
    -> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
    inferSpine' Action (TCMT IO)
    reconstructAction Type
    tyCon (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    hh ConInfo
    ci []) (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    hh ConInfo
    ci []) [Elim]
    psAfterAct
                  [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The spine has been inferred:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    conWithPars
                  Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term -> [Elim] -> Term
    applyWithoutReversing Term
    conWithPars [Elim]
    vs
                Term
    _ -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Term
    _  -> do
              Term
    vv <- ProjEliminator -> Term -> TCMT IO Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    EvenLone Term
    v
              Type -> Term -> TCMT IO Term
    unSpineAndReconstruct Type
    a Term
    vv
        unSpineAndReconstruct :: Type -> Term -> TCM Term
        unSpineAndReconstruct :: Type -> Term -> TCMT IO Term
    unSpineAndReconstruct Type
    a Term
    v =
          case Term
    v of
            Var Int
    i [Elim]
    vs -> do
              Type
    ty <- Int -> TCM Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m Type
    typeOfBV Int
    i
              Telescope
    ctx <- TCM Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> TCM Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Var case "[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++(Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i)[Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++[Char]
    " with context")) TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    ctx
              Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop Type
    ty (Int -> [Elim] -> Term
    Var Int
    i) [Elim]
    vs
            Def QName
    nam [Elim]
    vs -> do
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Def case"
              Type
    ty <- Definition -> Type
    defType (Definition -> Type) -> TCM Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    nam
              Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop Type
    ty (QName -> [Elim] -> Term
    Def QName
    nam) [Elim]
    vs
            MetaV MetaId
    id [Elim]
    vs -> do
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "MetaVar case"
              Type
    ty <- MetaId -> TCM Type
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    id
              Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop Type
    ty (MetaId -> [Elim] -> Term
    MetaV MetaId
    id) [Elim]
    vs
            Term
    _ -> do
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Another case" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v
              Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
        -- @loop ty f vs@ where @ty@ is the type of @f []@ and vs are valid
        -- arguments to something of type @ty@
        loop :: Type -> (Elims -> Term) -> Elims -> TCM Term
        loop :: Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop Type
    ty [Elim] -> Term
    f = Type
    -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop' Type
    ty [Elim] -> Term
    f [Elim] -> Term
    f
        -- We duplicate @f@ because we don't want the parameters to be reconstructed in
        -- type, since it would cause type-checking error when running @checkInternal'@.
        -- The first one @fTe@ is for term, the other one @fTy@ for type.
        loop' :: Type
    -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop' Type
    ty [Elim] -> Term
    fTe [Elim] -> Term
    _   []           = do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Loop ended" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Term -> TCM Doc) -> Term -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Term
    fTe [])
          Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Term
    fTe []
        loop' Type
    ty [Elim] -> Term
    fTe [Elim] -> Term
    fTy (Apply Arg Term
    u:[Elim]
    es) = do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The type before app is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    ty
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The term before app is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Elim] -> Term
    fTe [])
          Arg Term
    uu <- Arg Term -> TCMT IO (Arg Term)
    forall a. TermLike a => a -> TCM a
    dropParameters Arg Term
    u
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The app is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Arg Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Arg Term
    uu
          Type
    ty' <- Type -> Arg Term -> TCM Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    piApplyM Type
    ty Arg Term
    uu
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The type after app is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    ty'
          Type
    -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop' Type
    ty' ([Elim] -> Term
    fTe ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    u Elim -> [Elim] -> [Elim]
    forall a. a -> [a] -> [a]
    :)) ([Elim] -> Term
    fTy ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    uu Elim -> [Elim] -> [Elim]
    forall a. a -> [a] -> [a]
    :)) [Elim]
    es
        loop' Type
    ty [Elim] -> Term
    fTe [Elim] -> Term
    fTy (Proj ProjOrigin
    o QName
    p:[Elim]
    es) = do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The type is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    ty
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The term is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ([Elim] -> Term
    fTe [])
          [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The proj is:" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    p
          Type
    ty' <- Type -> TCM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    ty
          case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    ty' of
            Def QName
    r [Elim]
    pars -> do
              ~(Just (El Sort
    _ (Pi Dom Type
    _ Abs Type
    b))) <- QName -> Type -> TCMT IO (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    p Type
    ty'
              Type
    tyProj <- Definition -> Type
    defType (Definition -> Type) -> TCM Definition -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    p
              let reconstructWithoutPostFixing :: Action (TCMT IO)
    reconstructWithoutPostFixing = Action (TCMT IO)
    reconstructAction { elimViewAction :: Term -> TCMT IO Term
    elimViewAction = ProjEliminator -> Term -> TCMT IO Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    NoPostfix }
              let hiddenPs :: [Elim]
    hiddenPs = (Arg Term -> Elim) -> [Arg Term] -> [Elim]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> [Elim]) -> [Arg Term] -> [Elim]
    forall a b. (a -> b) -> a -> b
    $ Type -> [Arg Term] -> [Arg Term]
    forall {a}. (LensHiding a, LensRelevance a) => Type -> [a] -> [a]
    mapHide Type
    tyProj ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $
                                   [Elim] -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    pars
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "The params are" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Elim] -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Elim]
    hiddenPs
              ((Term
    _,Def QName
    p [Elim]
    psAfterAct),Type
    _) <- Action (TCMT IO)
    -> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
    inferSpine' Action (TCMT IO)
    act Type
    tyProj (QName -> [Elim] -> Term
    Def QName
    p []) (QName -> [Elim] -> Term
    Def QName
    p []) [Elim]
    hiddenPs
              ((Term
    _,Term
    projWithPars),Type
    _) <- Action (TCMT IO)
    -> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), Type)
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m
    -> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
    inferSpine' Action (TCMT IO)
    reconstructWithoutPostFixing Type
    tyProj (QName -> [Elim] -> Term
    Def QName
    p []) (QName -> [Elim] -> Term
    Def QName
    p []) [Elim]
    psAfterAct
              [Char] -> Int -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.reconstruct" Int
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Spine infered" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    projWithPars
              let fTe' :: [Elim] -> Term
    fTe' [Elim]
    x = Term -> [Elim] -> Term
    applyWithoutReversing Term
    projWithPars ((Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Term
    fTe [])Elim -> [Elim] -> [Elim]
    forall a. a -> [a] -> [a]
    :[Elim]
    x)
              Type
    -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
    loop' (Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b ([Elim] -> Term
    fTy [])) [Elim] -> Term
    fTe' ([Elim] -> Term
    fTy ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    pElim -> [Elim] -> [Elim]
    forall a. a -> [a] -> [a]
    :)) [Elim]
    es
            Term
    _ -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        loop' Type
    ty [Elim] -> Term
    _   [Elim] -> Term
    _   (IApply {}:[Elim]
    vs) = TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        applyWithoutReversing :: Term -> Elims -> Term
        applyWithoutReversing :: Term -> [Elim] -> Term
    applyWithoutReversing (Var Int
    i [Elim]
    es)   [Elim]
    ess = Int -> [Elim] -> Term
    Var Int
    i ([Elim]
    es[Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++[Elim]
    ess)
        applyWithoutReversing (Def QName
    n [Elim]
    es)   [Elim]
    ess = QName -> [Elim] -> Term
    Def QName
    n ([Elim]
    es[Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++[Elim]
    ess)
        applyWithoutReversing (Con ConHead
    h ConInfo
    i [Elim]
    es) [Elim]
    ess = ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    h ConInfo
    i ([Elim]
    es[Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++[Elim]
    ess)
        applyWithoutReversing (MetaV MetaId
    i [Elim]
    es) [Elim]
    ess = MetaId -> [Elim] -> Term
    MetaV MetaId
    i ([Elim]
    es[Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++[Elim]
    ess)
        applyWithoutReversing (Dummy [Char]
    s [Elim]
    es) [Elim]
    ess = [Char] -> [Elim] -> Term
    Dummy [Char]
    s ([Elim]
    es[Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++[Elim]
    ess)
        applyWithoutReversing Term
    _            [Elim]
    _   = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        mapHide :: Type -> [a] -> [a]
    mapHide (El Sort
    _ (Pi Dom Type
    a Abs Type
    b)) (a
    p:[a]
    tl) =
          Bool -> (a -> a) -> a -> a
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (Dom Type -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding Dom Type
    a Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    Hidden) a -> a
    forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams a
    p a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : Type -> [a] -> [a]
    mapHide (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b) [a]
    tl
        mapHide Type
    t [a]
    l = [a]
    l

    dropParameters :: TermLike a => a -> TCM a
    dropParameters :: forall a. TermLike a => a -> TCM a
    dropParameters = (Term -> TCMT IO Term) -> a -> TCMT IO a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM ((Term -> TCMT IO Term) -> a -> TCMT IO a)
    -> (Term -> TCMT IO Term) -> a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $
        \case
            Con ConHead
    c ConInfo
    ci [Elim]
    vs -> do
              Constructor{ conData :: Defn -> QName
    conData = QName
    d } <- Definition -> Defn
    theDef (Definition -> Defn) -> TCM Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    c)
              Just Int
    n <- Definition -> Maybe Int
    defParameters (Definition -> Maybe Int) -> TCM Definition -> TCM (Maybe Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
              Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c ConInfo
    ci ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ Int -> [Elim] -> [Elim]
    forall a. Int -> [a] -> [a]
    drop Int
    n [Elim]
    vs
            v :: Term
    v@(Def QName
    f [Elim]
    vs) -> do
              QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f TCMT IO (Maybe Projection)
    -> (Maybe Projection -> TCMT IO Term) -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Maybe Projection
    Nothing -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
                Just Projection
    pr -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Term -> [Elim] -> Term
    forall t. Apply t => t -> [Elim] -> t
    applyE (Projection -> ProjOrigin -> Term
    projDropPars Projection
    pr ProjOrigin
    ProjSystem) [Elim]
    vs
            Term
    v -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v