    -- | Compute eta short normal forms.
    module Agda.TypeChecking.EtaContract where

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

    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce.Monad () --instance only
    import {-# SOURCE #-} Agda.TypeChecking.Records
    import {-# SOURCE #-} Agda.TypeChecking.Datatypes

    import Agda.Utils.Monad
    import Agda.Utils.List (initLast)

    import Agda.Utils.Impossible

    -- TODO: move to Agda.Syntax.Internal.SomeThing
    data BinAppView = App Term (Arg Term)
                    | NoApp Term

    binAppView :: Term -> BinAppView
    binAppView :: Term -> BinAppView
    binAppView Term
    t = case Term
    t of
      Var Int
    i Elims
    xs   -> (Elims -> Term) -> Elims -> BinAppView
    appE (Int -> Elims -> Term
    Var Int
    i) Elims
    xs
      Def QName
    c Elims
    xs   -> (Elims -> Term) -> Elims -> BinAppView
    appE (QName -> Elims -> Term
    Def QName
    c) Elims
    xs
      -- Andreas, 2013-09-17: do not eta-contract when body is (record) constructor
      -- like in \ x -> s , x!  (See interaction/DoNotEtaContractFunIntoRecord)
      -- (Cf. also issue 889 (fixed differently).)
      -- At least record constructors should be fully applied where possible!
      -- TODO: also for ordinary constructors (\ x -> suc x  vs.  suc)?
      Con ConHead
    c ConInfo
    ci Elims
    xs
        | DataOrRecord
    IsData <- ConHead -> DataOrRecord
    conDataRecord ConHead
    c
                 -> (Elims -> Term) -> Elims -> BinAppView
    appE (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) Elims
    xs
        | Bool
    otherwise
                 -> BinAppView
    noApp
      Lit Literal
    _      -> BinAppView
    noApp
      Level Level
    _    -> BinAppView
    noApp   -- could be an application, but let's not eta contract levels
      Lam ArgInfo
    _ Abs Term
    _    -> BinAppView
    noApp
      Pi Dom Type
    _ Abs Type
    _     -> BinAppView
    noApp
      Sort Sort
    _     -> BinAppView
    noApp
      MetaV MetaId
    _ Elims
    _  -> BinAppView
    noApp
      DontCare Term
    _ -> BinAppView
    noApp
      Dummy{}    -> BinAppView
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        noApp :: BinAppView
    noApp = Term -> BinAppView
    NoApp Term
    t
        appE :: (Elims -> Term) -> Elims -> BinAppView
    appE Elims -> Term
    f Elims
    es0 | Just (Elims
    es, Apply Arg Term
    v) <- Elims -> Maybe (Elims, Elim' Term)
    forall a. [a] -> Maybe ([a], a)
    initLast Elims
    es0 = Term -> Arg Term -> BinAppView
    App (Elims -> Term
    f Elims
    es) Arg Term
    v
        appE Elims -> Term
    _ Elims
    _ = BinAppView
    noApp

    -- | Contracts all eta-redexes it sees without reducing.
    {-# SPECIALIZE etaContract :: TermLike a => a -> TCM a #-}
    {-# SPECIALIZE etaContract :: TermLike a => a -> ReduceM a #-}
    etaContract :: (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) => a -> m a
    etaContract :: forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
    a -> m a
    etaContract = (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    Term -> m Term
    etaOnce

    {-# SPECIALIZE etaOnce :: Term -> TCM Term #-}
    {-# SPECIALIZE etaOnce :: Term -> ReduceM Term #-}
    etaOnce :: (MonadTCEnv m, HasConstInfo m, HasOptions m) => Term -> m Term
    etaOnce :: forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    Term -> m Term
    etaOnce = \case
      -- Andreas, 2012-11-18: this call to reportSDoc seems to cost me 2%
      -- performance on the std-lib
      -- reportSDoc "tc.eta" 70 $ "eta-contracting" <+> prettyTCM v
      Lam ArgInfo
    i (Abs ArgName
    x Term
    b) -> ArgInfo -> ArgName -> Term -> m Term
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ArgInfo -> ArgName -> Term -> m Term
    etaLam ArgInfo
    i ArgName
    x Term
    b  -- NoAbs can't be eta'd

      -- Andreas, 2012-12-18:  Abstract definitions could contain
      -- abstract records whose constructors are not in scope.
      -- To be able to eta-contract them, we ignore abstract.
      Con ConHead
    c ConInfo
    ci Elims
    es -> ConHead
    -> ConInfo
    -> Elims
    -> (QName -> ConHead -> ConInfo -> Args -> m Term)
    -> m Term
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ConHead
    -> ConInfo
    -> Elims
    -> (QName -> ConHead -> ConInfo -> Args -> m Term)
    -> m Term
    etaCon ConHead
    c ConInfo
    ci Elims
    es QName -> ConHead -> ConInfo -> Args -> m Term
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> ConHead -> ConInfo -> Args -> m Term
    etaContractRecord

      Term
    v -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    -- | If record constructor, call eta-contraction function.
    etaCon :: (MonadTCEnv m, HasConstInfo m, HasOptions m)
      => ConHead  -- ^ Constructor name @c@.
      -> ConInfo  -- ^ Constructor info @ci@.
      -> Elims     -- ^ Constructor arguments @args@.
      -> (QName -> ConHead -> ConInfo -> Args -> m Term)
                  -- ^ Eta-contraction workhorse, gets also name of record type.
      -> m Term   -- ^ Returns @Con c ci args@ or its eta-contraction.
    etaCon :: forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ConHead
    -> ConInfo
    -> Elims
    -> (QName -> ConHead -> ConInfo -> Args -> m Term)
    -> m Term
    etaCon ConHead
    c ConInfo
    ci Elims
    es QName -> ConHead -> ConInfo -> Args -> m Term
    cont = m Term -> m Term
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ do
      let fallback :: m Term
    fallback = 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 -> Elims -> Term
    Con ConHead
    c ConInfo
    ci Elims
    es
      -- reportSDoc "tc.eta" 20 $ "eta-contracting record" <+> prettyTCM t
      QName
    r <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData (QName -> m QName) -> QName -> m QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c -- fails in ConcreteMode if c is abstract
      m Bool -> m Term -> m Term -> m Term
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    r) m Term
    fallback (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
        -- reportSDoc "tc.eta" 20 $ "eta-contracting record" <+> prettyTCM t
        let Just Args
    args = Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
        QName -> ConHead -> ConInfo -> Args -> m Term
    cont QName
    r ConHead
    c ConInfo
    ci Args
    args

    -- | Try to contract a lambda-abstraction @Lam i (Abs x b)@.
    etaLam :: (MonadTCEnv m, HasConstInfo m, HasOptions m)
      => ArgInfo  -- ^ Info @i@ of the 'Lam'.
      -> ArgName  -- ^ Name @x@ of the abstraction.
      -> Term     -- ^ Body ('Term') @b@ of the 'Abs'.
      -> m Term   -- ^ @Lam i (Abs x b)@, eta-contracted if possible.
    etaLam :: forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ArgInfo -> ArgName -> Term -> m Term
    etaLam ArgInfo
    i ArgName
    x Term
    b = do
        let fallback :: m Term
    fallback = 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
    i (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    x Term
    b
        case Term -> BinAppView
    binAppView Term
    b of
          App Term
    u (Arg ArgInfo
    info Term
    v) -> do
            Bool
    tyty <- m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    typeInType
            if Bool -> Term -> Bool
    forall {t}. t -> Term -> Bool
    isVar0 Bool
    tyty Term
    v
            -- Andreas, 2017-02-20 issue #2464
            -- Contracting with any irrelevant argument breaks subject reduction.
            -- E.g. \ .x -> f .(subst P eq x)  can in general not be contracted to f.
            -- -- (isIrrelevant info || isVar0 tyty v)
                 Bool -> Bool -> Bool
    && ArgInfo -> ArgInfo -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding ArgInfo
    i ArgInfo
    info
                 Bool -> Bool -> Bool
    && ArgInfo -> ArgInfo -> Bool
    forall a b. (LensModality a, LensModality b) => a -> b -> Bool
    sameModality ArgInfo
    i ArgInfo
    info
                 Bool -> Bool -> Bool
    && Bool -> Bool
    not (Int -> Term -> Bool
    forall a. Free a => Int -> a -> Bool
    freeIn Int
    0 Term
    u)
               then 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
    $ Impossible -> Term -> Term
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible Term
    u
               else m Term
    fallback
          BinAppView
    _ -> m Term
    fallback
      where
        isVar0 :: t -> Term -> Bool
    isVar0 t
    _ (Var Int
    0 [])               = Bool
    True
        -- Andreas, 2016-01-08 If --type-in-type, all levels are equal.
        -- Jesper, 2019-10-15 issue #3073
        -- Contracting level arguments is not sound unless the domain type
        -- is in fact @Level@, e.g. @\(A : Set) → F lzero@ should not be
        -- eta-contracted to @F@.
        -- isVar0 True Level{}               = True
        isVar0 t
    tyty (Level (Max Integer
    0 [Plus Integer
    0 Term
    l])) = t -> Term -> Bool
    isVar0 t
    tyty Term
    l
        isVar0 t
    _ Term
    _ = Bool
    False