{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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.Functor ( ($>) )

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic

import Agda.TypeChecking.Monad
import Agda.TypeChecking.CheckInternal
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.Either
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Lens
import Agda.Utils.Size

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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Type'' Term a -> f (Type'' Term 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 :: Tele (Dom Type) -> TCM (Tele (Dom Type))
reconstructParametersInTel Tele (Dom Type)
EmptyTel = Tele (Dom Type) -> TCM (Tele (Dom Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom Type)
forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) = do
  Type
ar <- Type -> TCM Type
reconstructParametersInType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
  (ArgName, Dom Type)
-> TCM (Tele (Dom Type)) -> TCM (Tele (Dom Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom Type) -> m a -> m a
addContext (Abs (Tele (Dom Type)) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Tele (Dom Type))
tel, Dom Type
a) (TCM (Tele (Dom Type)) -> TCM (Tele (Dom Type)))
-> TCM (Tele (Dom Type)) -> TCM (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
    Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
ar Type -> Dom Type -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> TCMT IO (Abs (Tele (Dom Type))) -> TCM (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Tele (Dom Type) -> TCM (Tele (Dom Type)))
-> Abs (Tele (Dom Type)) -> TCMT IO (Abs (Tele (Dom Type)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse Tele (Dom Type) -> TCM (Tele (Dom Type))
reconstructParametersInTel Abs (Tele (Dom Type))
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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
  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"reconstructing parameters in"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a ] ]
  Term
v <- Action (TCMT IO)
-> Term -> Comparison -> TypeOf Term -> TCMT IO Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' (Action (TCMT IO) -> Action (TCMT IO)
reconstructAction' Action (TCMT IO)
act) Term
v Comparison
CmpLeq TypeOf Term
Type
a

  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
  Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

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

reconstructAction' :: Action TCM -> Action TCM
reconstructAction' :: Action (TCMT IO) -> Action (TCMT IO)
reconstructAction' Action (TCMT IO)
act = Action (TCMT IO)
act{ postAction = \Type
ty Term
tm -> Action (TCMT IO) -> Type -> Term -> TCMT IO Term
forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action (TCMT IO)
act Type
ty Term
tm TCMT IO Term -> (Term -> TCMT IO Term) -> TCMT IO Term
forall a b. TCM a -> (a -> TCM b) -> TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Term -> TCMT IO Term
reconstruct Type
ty }

reconstruct :: Type -> Term -> TCM Term
reconstruct :: Type -> Term -> TCMT IO Term
reconstruct Type
ty Term
v = do
    ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"reconstructing in"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty ] ]
    case Term
v of
      Con ConHead
h ConInfo
ci Elims
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)
-> TCMT IO (Either SigError ConHead) -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Either SigError ConHead)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
h)
        TelV Tele (Dom Type)
tel Type
dataTy <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ty
        ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"reconstructing"
              , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                             , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
dataTy ] ]
        [Arg Term]
pars <- Tele (Dom Type) -> TCMT IO [Arg Term] -> TCMT IO [Arg Term]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel (TCMT IO [Arg Term] -> TCMT IO [Arg Term])
-> TCMT IO [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCMT IO [Arg Term]
extractParameters (ConHead -> QName
conName ConHead
h) Type
dataTy
        -- If the constructor is underapplied, we need to escape from the telescope.
        let escape :: [Arg Term] -> [Arg Term]
escape = Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term])
-> Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Impossible -> Int -> Substitution' (SubstArg [Arg Term])
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (Int -> Substitution' (SubstArg [Arg Term]))
-> Int -> Substitution' (SubstArg [Arg Term])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
        Term -> TCMT IO Term
forall a. a -> TCMT IO a
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 -> Elims -> Term
Con ConHead
hh ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> [Arg Term]
escape [Arg Term]
pars) Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
vs
      Def QName
f Elims
es -> Term -> TCMT IO ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v TCMT IO ProjectionView
-> (ProjectionView -> TCMT IO Term) -> TCMT IO Term
forall a b. TCM a -> (a -> TCM b) -> TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        ProjectionView QName
_f Arg Term
a Elims
es -> do
          Type
recTy <- Term -> TCM Type
forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer (Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a. TermLike a => a -> TCM a
dropParameters (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
          [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
f Type
recTy
          Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty (QName -> Elims -> Term
Def QName
f (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
pars Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++) (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
aElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
        LoneProjectionLike QName
_f ArgInfo
i -> Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty) TCMT IO Term -> (Term -> TCMT IO Term) -> TCMT IO Term
forall a b. TCM a -> (a -> TCM b) -> TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Pi Dom Type
recTy Abs Type
_ -> do
            [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
f (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
recTy)
            Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
pars
          Term
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
        NoProjection{} -> do
          Type
ty <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
          Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty (QName -> Elims -> Term
Def QName
f) Elims
es
      Var Int
i Elims
es -> do
        Type
ty <- Int -> TCM Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
        Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty (Int -> Elims -> Term
Var Int
i) Elims
es
      MetaV MetaId
m Elims
es -> do
        Type
ty <- MetaId -> TCM Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m
        Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty (MetaId -> Elims -> Term
MetaV MetaId
m) Elims
es
      Term
_ -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

  where
    -- @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 -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty Elims -> Term
f []           = do
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Loop ended" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Elims -> Term
f [])
      Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Elims -> Term
f []
    loop Type
ty Elims -> Term
f (Apply Arg Term
u:Elims
es) = do
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The type before app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The term before app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Elims -> Term
f [])
      Arg Term
uu <- Arg Term -> TCMT IO (Arg Term)
forall a. TermLike a => a -> TCM a
dropParameters Arg Term
u
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO 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
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Arg Term -> m Type
piApplyM Type
ty Arg Term
uu
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The type after app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty'
      Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop Type
ty' (Elims -> Term
f (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
u Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
    loop Type
ty Elims -> Term
f (Proj ProjOrigin
o QName
p:Elims
es) = do
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The type is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The term is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Elims -> Term
f [])
      ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The proj is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p
      [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
p Type
ty
      ~(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 -> TCMT IO (Maybe Type)) -> TCM Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
      let fTm :: Term
fTm = Elims -> Term
f []
      Term
fe <- Term -> TCMT IO Term
forall a. TermLike a => a -> TCM a
dropParameters Term
fTm
      Type -> (Elims -> Term) -> Elims -> TCMT IO Term
loop (Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
SubstArg Type
fe) (QName -> Elims -> Term
Def QName
p (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
pars Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++) (Elims -> Elims) -> (Elims -> Elims) -> Elims -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
fTm) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)) Elims
es
    loop Type
ty Elims -> Term
_ (IApply {}:Elims
vs) = TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__

-- Extract the parameters from the type of a constructor
-- application or the type of the principal argument of a
-- projection.
extractParameters :: QName -> Type -> TCM Args
extractParameters :: QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
q Type
ty = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
ty) TCMT IO Term -> (Term -> TCMT IO [Arg Term]) -> TCMT IO [Arg Term]
forall a b. TCM a -> (a -> TCM b) -> TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
d Elims
prePs -> do
    Type
dt <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
    ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Start traversing parameters: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Elims
prePs
    Elims
postPs <- Action (TCMT IO)
-> Elims -> Comparison -> TypeOf Elims -> TCMT IO Elims
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims
checkInternal' Action (TCMT IO)
reconstructAction Elims
prePs Comparison
CmpEq (Type
dt , QName -> Elims -> Term
Def QName
d)
    ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Traversed parameters:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Elims
postPs
    Definition
info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
    let mkParam :: b -> Elim' a -> Arg a
mkParam b
erasure =
            b -> (Arg a -> Arg a) -> Arg a -> Arg a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen b
erasure (Quantity -> Arg a -> Arg a
forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity)
          (Arg a -> Arg a) -> (Elim' a -> Arg a) -> Elim' a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> Arg a
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams
          (Arg a -> Arg a) -> (Elim' a -> Arg a) -> Elim' a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Empty -> Elim' a -> Arg a
forall a. Empty -> Elim' a -> Arg a
isApplyElim' Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
    if -- Case: data or record constructor
       | Constructor{ conPars :: Defn -> Int
conPars = Int
n, conErasure :: Defn -> Bool
conErasure = Bool
e } <- Definition -> Defn
theDef Definition
info ->
           [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> TCMT IO [Arg Term])
-> [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Arg Term) -> Elims -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Elim' Term -> Arg Term
forall {b} {a}. IsBool b => b -> Elim' a -> Arg a
mkParam Bool
e) (Elims -> [Arg Term]) -> Elims -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
take Int
n Elims
postPs
       -- Case: regular projection
       | Defn -> Bool
isProperProjection (Definition -> Defn
theDef Definition
info) ->
         case Definition -> Defn
theDef Definition
info of
           d :: Defn
d@Function{} ->
             [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> TCMT IO [Arg Term])
-> [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Arg Term) -> Elims -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Elim' Term -> Arg Term
forall {b} {a}. IsBool b => b -> Elim' a -> Arg a
mkParam (Defn
d Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funErasure)) Elims
postPs
           Defn
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
       -- Case: projection-like function
       | Bool
otherwise -> do
           TelV Tele (Dom Type)
tel Type
_ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (Elims -> Int
forall a. Sized a => a -> Int
size Elims
postPs) (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
info
           [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> TCMT IO [Arg Term])
-> [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term -> Arg Term)
-> [Arg Term] -> [Term] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
($>) (Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel :: Args) ([Term] -> [Arg Term]) -> [Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Term) -> Elims -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term)
-> (Elim' Term -> Arg Term) -> Elim' Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Empty -> Elim' Term -> Arg Term
forall a. Empty -> Elim' a -> Arg a
isApplyElim' Empty
forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
postPs
  Term
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__

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