    -- | Compute eta long normal forms.
    module Agda.TypeChecking.EtaExpand where

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

    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    -- | Eta-expand a term if its type is a function type or an eta-record type.
    etaExpandOnce :: PureTCM m => Type -> Term -> m Term
    etaExpandOnce :: forall (m :: * -> *). PureTCM m => Type -> Term -> m Term
    etaExpandOnce Type
    a Term
    v = Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a m Type -> (Type -> m Term) -> m Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      El Sort' Term
    _ (Pi Dom Type
    a Abs Type
    b) -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $
        ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    ai (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Term -> Abs Term
    forall a. (Subst a, Free a) => ArgName -> a -> Abs a
    mkAbs (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b) (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0 ]
        where ai :: ArgInfo
    ai = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a

      Type
    a -> Type -> m (Maybe (QName, Args))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, Args))
    isEtaRecordType Type
    a m (Maybe (QName, Args))
    -> (Maybe (QName, Args) -> m Term) -> m Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just (QName
    r, Args
    pars) -> do
          Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r
          (Telescope
    _, ConHead
    con, ConInfo
    ci, Args
    args) <- QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ QName
    r Args
    pars Defn
    def Term
    v
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Args -> Term
    mkCon ConHead
    con ConInfo
    ci Args
    args
        Maybe (QName, Args)
    Nothing -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    -- | Eta-expand functions and expressions of eta-record
    -- type wherever possible.
    deepEtaExpand :: Term -> Type -> TCM Term
    deepEtaExpand :: Term -> Type -> TCM Term
    deepEtaExpand Term
    v Type
    a = Action (TCMT IO) -> Term -> Comparison -> Type -> TCM Term
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Action m -> Term -> Comparison -> Type -> m Term
    checkInternal' Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    etaExpandAction Term
    v Comparison
    CmpLeq Type
    a

    etaExpandAction :: PureTCM m => Action m
    etaExpandAction :: forall (m :: * -> *). PureTCM m => Action m
    etaExpandAction = Action m
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction { preAction :: Type -> Term -> m Term
    preAction = Type -> Term -> m Term
    forall (m :: * -> *). PureTCM m => Type -> Term -> m Term
    etaExpandOnce  }