    {-# 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
      ar <- Type -> TCM Type
    reconstructParametersInType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
      addContext (absName tel, a) $
        ExtendTel (ar <$ a) <$> traverse reconstructParametersInTel tel

    reconstructParametersInEqView :: EqualityView -> TCM EqualityView
    reconstructParametersInEqView :: EqualityView -> TCM EqualityView
    reconstructParametersInEqView (EqualityType Range
    r Sort
    s QName
    eq [Arg Term]
    l Arg Term
    a Arg Term
    u Arg Term
    v) =
      Range
    -> Sort
    -> QName
    -> [Arg Term]
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType Range
    r 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 ] ]
      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

      reportSDoc "tc.reconstruct" 30 $
        nest 2 $ "-->" <+> prettyTCM v
      return 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
            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 tel dataTy <- telView ty
            reportSDoc "tc.reconstruct" 50 $
              sep [ "reconstructing"
                  , nest 2 $ sep [ prettyTCM v <+> ":"
                                 , nest 2 $ prettyTCM dataTy ] ]
            pars <- addContext tel $ extractParameters (conName h) dataTy
            -- If the constructor is underapplied, we need to escape from the telescope.
            let 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
            return $ Con hh ci $ map Apply (escape pars) ++ 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
              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)
              pars <- extractParameters f recTy
              loop ty (Def f . (map Apply pars ++) . (Apply a:)) 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
                pars <- QName -> Type -> TCMT IO [Arg Term]
    extractParameters QName
    f (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    recTy)
                return $ Def f $ map Apply pars
              Term
    _ -> TCMT IO Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            NoProjection{} -> do
              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
              loop ty (Def f) es
          Var Int
    i Elims
    es -> do
            ty <- Int -> TCM Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
            loop ty (Var i) es
          MetaV MetaId
    m Elims
    es -> do
            ty <- MetaId -> TCM Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType MetaId
    m
            loop ty (MetaV m) 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 [])
          uu <- Arg Term -> TCMT IO (Arg Term)
    forall a. TermLike a => a -> TCM a
    dropParameters Arg Term
    u
          reportSDoc "tc.reconstruct" 50 $ "The app is:" <+> pretty uu
          ty' <- piApplyM ty uu
          reportSDoc "tc.reconstruct" 50 $ "The type after app is:" <+> pretty ty'
          loop ty' (f . (Apply u :)) 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
          pars <- QName -> Type -> TCMT IO [Arg Term]
    extractParameters QName
    p Type
    ty
          ~(Just (El _ (Pi _ b))) <- getDefType p =<< reduce ty
          let fTm = Elims -> Term
    f []
          fe <- dropParameters fTm
          loop (absApp b fe) (Def p . (map Apply pars ++) . (Apply (defaultArg fTm) :)) 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
        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
        reportSDoc "tc.reconstruct" 50 $ "Start traversing parameters: " <+> pretty prePs
        postPs <- checkInternal' reconstructAction prePs CmpEq (dt , Def d)
        reportSDoc "tc.reconstruct" 50 $ "Traversed parameters:" <+> pretty postPs
        info <- getConstInfo q
        let 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 = n, conErasure = e } <- theDef info ->
               return $ map (mkParam e) $ take n postPs
           -- Case: regular projection
           | isProperProjection (theDef info) ->
             case theDef 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
           | otherwise -> do
               TelV tel _ <- telViewUpTo (size postPs) $ defType info
               return $ zipWith ($>) (teleArgs tel :: Args) $ map (unArg . isApplyElim' __IMPOSSIBLE__) 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 = 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 n <- defParameters <$> getConstInfo d
              return $ Con c ci $ drop n 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