    {-# LANGUAGE PatternSynonyms #-}

    module Agda.Compiler.Treeless.Erase
           ( eraseTerms
           , computeErasedConstructorArgs
           , isErasable
           ) where

    import Control.Arrow (first, second)
    import Control.Monad
    import Control.Monad.State
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.List as List

    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Position
    import Agda.Syntax.Treeless
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Monad as I
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive

    import {-# SOURCE #-} Agda.Compiler.Backend
    import Agda.Compiler.Treeless.Subst
    import Agda.Compiler.Treeless.Unused

    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Memo
    import Agda.Utils.Monad
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.IntSet.Infinite (IntSet)
    import qualified Agda.Utils.IntSet.Infinite as IntSet

    import Agda.Utils.Impossible

    -- | State of the eraser.
    data ESt = ESt
      { ESt -> Map QName FunInfo
    _funMap  :: Map QName FunInfo
          -- ^ Memoize computed `FunInfo` for functions/constructors/... `QName`.
      , ESt -> Map QName TypeInfo
    _typeMap :: Map QName TypeInfo
          -- ^ Memoize computed `TypeInfo` for data/record types `QName`.
      }

    funMap :: Lens' (Map QName FunInfo) ESt
    funMap :: Lens' (Map QName FunInfo) ESt
    funMap Map QName FunInfo -> f (Map QName FunInfo)
    f ESt
    r = Map QName FunInfo -> f (Map QName FunInfo)
    f (ESt -> Map QName FunInfo
    _funMap ESt
    r) f (Map QName FunInfo) -> (Map QName FunInfo -> ESt) -> f ESt
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Map QName FunInfo
    a -> ESt
    r { _funMap :: Map QName FunInfo
    _funMap = Map QName FunInfo
    a }

    typeMap :: Lens' (Map QName TypeInfo) ESt
    typeMap :: Lens' (Map QName TypeInfo) ESt
    typeMap Map QName TypeInfo -> f (Map QName TypeInfo)
    f ESt
    r = Map QName TypeInfo -> f (Map QName TypeInfo)
    f (ESt -> Map QName TypeInfo
    _typeMap ESt
    r) f (Map QName TypeInfo) -> (Map QName TypeInfo -> ESt) -> f ESt
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Map QName TypeInfo
    a -> ESt
    r { _typeMap :: Map QName TypeInfo
    _typeMap = Map QName TypeInfo
    a }

    -- | Eraser monad.
    type E = StateT ESt TCM

    runE :: E a -> TCM a
    runE :: forall a. E a -> TCM a
    runE E a
    m = E a -> ESt -> TCM a
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT E a
    m (Map QName FunInfo -> Map QName TypeInfo -> ESt
    ESt Map QName FunInfo
    forall k a. Map k a
    Map.empty Map QName TypeInfo
    forall k a. Map k a
    Map.empty)

    -- | Takes the name of the data/record type.
    computeErasedConstructorArgs :: QName -> TCM ()
    computeErasedConstructorArgs :: QName -> TCM ()
    computeErasedConstructorArgs QName
    d = do
      [QName]
    cs <- QName -> TCM [QName]
    getNotErasedConstructors QName
    d
      E () -> TCM ()
    forall a. E a -> TCM a
    runE (E () -> TCM ()) -> E () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (QName -> StateT ESt (TCMT IO) FunInfo) -> [QName] -> E ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo [QName]
    cs

    eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm
    eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm
    eraseTerms QName
    q EvaluationStrategy
    eval TTerm
    t = QName -> TTerm -> TCM [ArgUsage]
    usedArguments QName
    q TTerm
    t TCM [ArgUsage] -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> E TTerm -> TCM TTerm
    forall a. E a -> TCM a
    runE (QName -> TTerm -> E TTerm
    eraseTop QName
    q TTerm
    t)
      where
        eraseTop :: QName -> TTerm -> E TTerm
    eraseTop QName
    q TTerm
    t = do
          ([TypeInfo]
    _, TypeInfo
    h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    q
          case TypeInfo
    h of
            TypeInfo
    Erasable -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
            TypeInfo
    Empty    -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
            TypeInfo
    _        -> TTerm -> E TTerm
    erase TTerm
    t

        erase :: TTerm -> E TTerm
    erase TTerm
    t = case TTerm -> (TTerm, [TTerm])
    tAppView TTerm
    t of

          (TCon QName
    c, [TTerm]
    vs) -> do
            ([TypeInfo]
    rs, TypeInfo
    h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    c
            Bool -> E () -> E ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([TypeInfo] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TypeInfo]
    rs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [TTerm] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TTerm]
    vs) E ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            case TypeInfo
    h of
              TypeInfo
    Erasable -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    Empty    -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    _        -> TTerm -> [TTerm] -> TTerm
    tApp (QName -> TTerm
    TCon QName
    c) ([TTerm] -> TTerm) -> StateT ESt (TCMT IO) [TTerm] -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TypeInfo -> TTerm -> E TTerm)
    -> [TypeInfo] -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM TypeInfo -> TTerm -> E TTerm
    eraseRel [TypeInfo]
    rs [TTerm]
    vs

          (TDef QName
    f, [TTerm]
    vs) -> do
            ([TypeInfo]
    rs, TypeInfo
    h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    f
            case TypeInfo
    h of
              TypeInfo
    Erasable -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    Empty    -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    _        -> TTerm -> [TTerm] -> TTerm
    tApp (QName -> TTerm
    TDef QName
    f) ([TTerm] -> TTerm) -> StateT ESt (TCMT IO) [TTerm] -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TypeInfo -> TTerm -> E TTerm)
    -> [TypeInfo] -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM TypeInfo -> TTerm -> E TTerm
    eraseRel ([TypeInfo]
    rs [TypeInfo] -> [TypeInfo] -> [TypeInfo]
    forall a. [a] -> [a] -> [a]
    ++ TypeInfo -> [TypeInfo]
    forall a. a -> [a]
    repeat TypeInfo
    NotErasable) [TTerm]
    vs

          (TTerm, [TTerm])
    _ -> case TTerm
    t of
            TVar{}         -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TDef{}         -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TPrim{}        -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TLit{}         -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TCon{}         -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TApp TTerm
    f [TTerm]
    es      -> TTerm -> [TTerm] -> TTerm
    tApp (TTerm -> [TTerm] -> TTerm)
    -> E TTerm -> StateT ESt (TCMT IO) ([TTerm] -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    f StateT ESt (TCMT IO) ([TTerm] -> TTerm)
    -> StateT ESt (TCMT IO) [TTerm] -> E TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> E TTerm) -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TTerm -> E TTerm
    erase [TTerm]
    es
            TLam TTerm
    b         -> TTerm -> TTerm
    tLam (TTerm -> TTerm) -> E TTerm -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    b
            TLet TTerm
    e TTerm
    b       -> do
              TTerm
    e <- TTerm -> E TTerm
    erase TTerm
    e
              if TTerm -> Bool
    isErased TTerm
    e
                then case TTerm
    b of
                       TCase Int
    0 CaseInfo
    _ TTerm
    _ [TAlt]
    _ -> TTerm -> TTerm -> TTerm
    tLet TTerm
    TErased (TTerm -> TTerm) -> E TTerm -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    b
                       TTerm
    _             -> TTerm -> E TTerm
    erase (TTerm -> E TTerm) -> TTerm -> E TTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    0 TTerm
    SubstArg TTerm
    TErased TTerm
    b
                else TTerm -> TTerm -> TTerm
    tLet TTerm
    e (TTerm -> TTerm) -> E TTerm -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    b
            TCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs -> do
              (TTerm
    d, [TAlt]
    bs) <- Int -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable Int
    x (CaseInfo -> CaseType
    caseType CaseInfo
    t) TTerm
    d [TAlt]
    bs
              TTerm
    d       <- TTerm -> E TTerm
    erase TTerm
    d
              [TAlt]
    bs      <- (TAlt -> StateT ESt (TCMT IO) TAlt)
    -> [TAlt] -> StateT ESt (TCMT IO) [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TAlt -> StateT ESt (TCMT IO) TAlt
    eraseAlt [TAlt]
    bs
              Int -> CaseInfo -> TTerm -> [TAlt] -> E TTerm
    tCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs

            TTerm
    TUnit          -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TTerm
    TSort          -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TTerm
    TErased        -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TError{}       -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TCoerce TTerm
    e      -> TTerm -> TTerm
    TCoerce (TTerm -> TTerm) -> E TTerm -> E TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    e

        -- #3380: this is not safe for strict backends
        tLam :: TTerm -> TTerm
    tLam TTerm
    TErased | EvaluationStrategy
    eval EvaluationStrategy -> EvaluationStrategy -> Bool
    forall a. Eq a => a -> a -> Bool
    == EvaluationStrategy
    LazyEvaluation = TTerm
    TErased
        tLam TTerm
    t                                = TTerm -> TTerm
    TLam TTerm
    t

        tLet :: TTerm -> TTerm -> TTerm
    tLet TTerm
    e TTerm
    b
          | Int -> TTerm -> Bool
    forall a. HasFree a => Int -> a -> Bool
    freeIn Int
    0 TTerm
    b = TTerm -> TTerm -> TTerm
    TLet TTerm
    e TTerm
    b
          | Bool
    otherwise  = Impossible -> TTerm -> TTerm
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible TTerm
    b

        tApp :: TTerm -> [TTerm] -> TTerm
    tApp TTerm
    f []                  = TTerm
    f
        tApp TTerm
    TErased [TTerm]
    _             = TTerm
    TErased
        tApp TTerm
    f [TTerm]
    _ | TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable TTerm
    f = TTerm
    tUnreachable
        tApp TTerm
    f [TTerm]
    es                  = TTerm -> [TTerm] -> TTerm
    mkTApp TTerm
    f [TTerm]
    es

        tCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> E TTerm
    tCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs
          | TTerm -> Bool
    isErased TTerm
    d Bool -> Bool -> Bool
    && (TAlt -> Bool) -> [TAlt] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (TTerm -> Bool
    isErased (TTerm -> Bool) -> (TAlt -> TTerm) -> TAlt -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TAlt -> TTerm
    aBody) [TAlt]
    bs = TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
          | Bool
    otherwise = case [TAlt]
    bs of
            [TACon QName
    c Int
    a TTerm
    b] -> do
              TypeInfo
    h <- FunInfo -> TypeInfo
    forall a b. (a, b) -> b
    snd (FunInfo -> TypeInfo)
    -> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    c
              case TypeInfo
    h of
                TypeInfo
    NotErasable -> E TTerm
    noerase
                TypeInfo
    Empty       -> TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
                TypeInfo
    Erasable    -> (if Int
    a Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure else TTerm -> E TTerm
    erase) (TTerm -> E TTerm) -> TTerm -> E TTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> TTerm -> [TTerm]
    forall a. Int -> a -> [a]
    replicate Int
    a TTerm
    TErased [TTerm] -> Substitution' TTerm -> Substitution' TTerm
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Substitution' TTerm
    forall a. Substitution' a
    idS) TTerm
    b
                                  -- might enable more erasure
            [TAlt]
    _ -> E TTerm
    noerase
          where
            noerase :: E TTerm
    noerase = TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TTerm -> E TTerm) -> TTerm -> E TTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs

        isErased :: TTerm -> Bool
    isErased TTerm
    t = TTerm
    t TTerm -> TTerm -> Bool
    forall a. Eq a => a -> a -> Bool
    == TTerm
    TErased Bool -> Bool -> Bool
    || TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable TTerm
    t

        eraseRel :: TypeInfo -> TTerm -> E TTerm
    eraseRel TypeInfo
    r TTerm
    t | TypeInfo -> Bool
    erasable TypeInfo
    r = TTerm -> E TTerm
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
                     | Bool
    otherwise  = TTerm -> E TTerm
    erase TTerm
    t

        eraseAlt :: TAlt -> StateT ESt (TCMT IO) TAlt
    eraseAlt = \case
          TALit Literal
    l TTerm
    b   -> Literal -> TTerm -> TAlt
    TALit Literal
    l   (TTerm -> TAlt) -> E TTerm -> StateT ESt (TCMT IO) TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    b
          TACon QName
    c Int
    a TTerm
    b -> do
            [Bool]
    rs <- (TypeInfo -> Bool) -> [TypeInfo] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeInfo -> Bool
    erasable ([TypeInfo] -> [Bool])
    -> (FunInfo -> [TypeInfo]) -> FunInfo -> [Bool]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FunInfo -> [TypeInfo]
    forall a b. (a, b) -> a
    fst (FunInfo -> [Bool])
    -> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) [Bool]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    c
            let sub :: Substitution' TTerm
    sub = (Bool -> Substitution' TTerm -> Substitution' TTerm)
    -> Substitution' TTerm -> [Bool] -> Substitution' TTerm
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ Bool
    e -> if Bool
    e then (TTerm
    TErased TTerm -> Substitution' TTerm -> Substitution' TTerm
    forall a. a -> Substitution' a -> Substitution' a
    :#) (Substitution' TTerm -> Substitution' TTerm)
    -> (Substitution' TTerm -> Substitution' TTerm)
    -> Substitution' TTerm
    -> Substitution' TTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    wkS Int
    1 else Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    1) Substitution' TTerm
    forall a. Substitution' a
    idS ([Bool] -> Substitution' TTerm) -> [Bool] -> Substitution' TTerm
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> [Bool]
    forall a. [a] -> [a]
    reverse [Bool]
    rs
            QName -> Int -> TTerm -> TAlt
    TACon QName
    c Int
    a (TTerm -> TAlt) -> E TTerm -> StateT ESt (TCMT IO) TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' TTerm
    Substitution' (SubstArg TTerm)
    sub TTerm
    b)
          TAGuard TTerm
    g TTerm
    b -> TTerm -> TTerm -> TAlt
    TAGuard   (TTerm -> TTerm -> TAlt)
    -> E TTerm -> StateT ESt (TCMT IO) (TTerm -> TAlt)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> E TTerm
    erase TTerm
    g StateT ESt (TCMT IO) (TTerm -> TAlt)
    -> E TTerm -> StateT ESt (TCMT IO) TAlt
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> E TTerm
    erase TTerm
    b

    -- | Doesn't have any type information (other than the name of the data type),
    --   so we can't do better than checking if all constructors are present.
    pruneUnreachable :: Int -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable :: Int -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable Int
    _ (CTData Quantity
    quantity QName
    q) TTerm
    d [TAlt]
    bs' = do
      -- In an erased setting erased constructors are not treated
      -- specially.
      [QName]
    cs <- TCM [QName] -> StateT ESt (TCMT IO) [QName]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [QName] -> StateT ESt (TCMT IO) [QName])
    -> TCM [QName] -> StateT ESt (TCMT IO) [QName]
    forall a b. (a -> b) -> a -> b
    $
            if Quantity -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 Quantity
    quantity
            then QName -> TCM [QName]
    getConstructors QName
    q
            else QName -> TCM [QName]
    getNotErasedConstructors QName
    q
      let bs :: [TAlt]
    bs | Quantity -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 Quantity
    quantity = [TAlt]
    bs'
             | Bool
    otherwise             =
               ((TAlt -> Bool) -> [TAlt] -> [TAlt])
    -> [TAlt] -> (TAlt -> Bool) -> [TAlt]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (TAlt -> Bool) -> [TAlt] -> [TAlt]
    forall a. (a -> Bool) -> [a] -> [a]
    filter [TAlt]
    bs' ((TAlt -> Bool) -> [TAlt]) -> (TAlt -> Bool) -> [TAlt]
    forall a b. (a -> b) -> a -> b
    $ \case
                 a :: TAlt
    a@TACon{} -> (TAlt -> QName
    aCon TAlt
    a) QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    cs
                 TAGuard{} -> Bool
    True
                 TALit{}   -> Bool
    True
      let complete :: Bool
    complete =[QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [QName]
    cs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [TAlt] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ TAlt
    b | b :: TAlt
    b@TACon{} <- [TAlt]
    bs ]
      let d' :: TTerm
    d' | Bool
    complete  = TTerm
    tUnreachable
             | Bool
    otherwise = TTerm
    d
      (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm
    d', [TAlt]
    bs)
    pruneUnreachable Int
    x CaseType
    CTNat TTerm
    d [TAlt]
    bs = (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TTerm, [TAlt]) -> E (TTerm, [TAlt]))
    -> (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall a b. (a -> b) -> a -> b
    $ Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
    pruneIntCase Int
    x TTerm
    d [TAlt]
    bs (Integer -> IntSet
    IntSet.below Integer
    0)
    pruneUnreachable Int
    x CaseType
    CTInt TTerm
    d [TAlt]
    bs = (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TTerm, [TAlt]) -> E (TTerm, [TAlt]))
    -> (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall a b. (a -> b) -> a -> b
    $ Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
    pruneIntCase Int
    x TTerm
    d [TAlt]
    bs IntSet
    IntSet.empty
    pruneUnreachable Int
    _ CaseType
    _ TTerm
    d [TAlt]
    bs = (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TTerm
    d, [TAlt]
    bs)

    -- These are the guards we generate for Int/Nat pattern matching
    pattern Below :: Int -> Integer -> TTerm
    pattern $bBelow :: Int -> Integer -> TTerm
    $mBelow :: forall {r}. TTerm -> (Int -> Integer -> r) -> (Void# -> r) -> r
    Below x n = TApp (TPrim PLt)  [TVar x, TLit (LitNat n)]

    pattern Above :: Int -> Integer -> TTerm
    pattern $bAbove :: Int -> Integer -> TTerm
    $mAbove :: forall {r}. TTerm -> (Int -> Integer -> r) -> (Void# -> r) -> r
    Above x n = TApp (TPrim PGeq) [TVar x, TLit (LitNat n)]

    -- | Strip unreachable clauses (replace by tUnreachable for the default).
    --   Fourth argument is the set of ints covered so far.
    pruneIntCase :: Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
    pruneIntCase :: Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
    pruneIntCase Int
    x TTerm
    d [TAlt]
    bs IntSet
    cover = [TAlt] -> IntSet -> (TTerm, [TAlt])
    go [TAlt]
    bs IntSet
    cover
      where
        go :: [TAlt] -> IntSet -> (TTerm, [TAlt])
    go [] IntSet
    cover
          | IntSet
    cover IntSet -> IntSet -> Bool
    forall a. Eq a => a -> a -> Bool
    == IntSet
    IntSet.full = (TTerm
    tUnreachable, [])
          | Bool
    otherwise            = (TTerm
    d, [])
        go (TAlt
    b : [TAlt]
    bs) IntSet
    cover =
          case TAlt
    b of
            TAGuard (Below Int
    y Integer
    n) TTerm
    _ | Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    y -> IntSet -> (TTerm, [TAlt])
    rec (Integer -> IntSet
    IntSet.below Integer
    n)
            TAGuard (Above Int
    y Integer
    n) TTerm
    _ | Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    y -> IntSet -> (TTerm, [TAlt])
    rec (Integer -> IntSet
    IntSet.above Integer
    n)
            TALit (LitNat Integer
    n) TTerm
    _             -> IntSet -> (TTerm, [TAlt])
    rec (Integer -> IntSet
    IntSet.singleton Integer
    n)
            TAlt
    _                                -> ([TAlt] -> [TAlt]) -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (TAlt
    b TAlt -> [TAlt] -> [TAlt]
    forall a. a -> [a] -> [a]
    :) ((TTerm, [TAlt]) -> (TTerm, [TAlt]))
    -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
    forall a b. (a -> b) -> a -> b
    $ [TAlt] -> IntSet -> (TTerm, [TAlt])
    go [TAlt]
    bs IntSet
    cover
          where
            rec :: IntSet -> (TTerm, [TAlt])
    rec IntSet
    this = ([TAlt] -> [TAlt]) -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second [TAlt] -> [TAlt]
    addAlt ((TTerm, [TAlt]) -> (TTerm, [TAlt]))
    -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
    forall a b. (a -> b) -> a -> b
    $ [TAlt] -> IntSet -> (TTerm, [TAlt])
    go [TAlt]
    bs IntSet
    cover'
              where
                this' :: IntSet
    this'  = IntSet -> IntSet -> IntSet
    IntSet.difference IntSet
    this IntSet
    cover
                cover' :: IntSet
    cover' = IntSet
    this' IntSet -> IntSet -> IntSet
    forall a. Semigroup a => a -> a -> a
    <> IntSet
    cover
                addAlt :: [TAlt] -> [TAlt]
    addAlt = case IntSet -> Maybe [Integer]
    IntSet.toFiniteList IntSet
    this' of
                           Just []  -> [TAlt] -> [TAlt]
    forall a. a -> a
    id                                     -- unreachable case
                           Just [Integer
    n] -> (Literal -> TTerm -> TAlt
    TALit (Integer -> Literal
    LitNat Integer
    n) (TAlt -> TTerm
    aBody TAlt
    b) TAlt -> [TAlt] -> [TAlt]
    forall a. a -> [a] -> [a]
    :) -- possibly refined case
                           Maybe [Integer]
    _        -> (TAlt
    b TAlt -> [TAlt] -> [TAlt]
    forall a. a -> [a] -> [a]
    :)                                  -- unchanged case

    data TypeInfo = Empty | Erasable | NotErasable
      deriving (TypeInfo -> TypeInfo -> Bool
    (TypeInfo -> TypeInfo -> Bool)
    -> (TypeInfo -> TypeInfo -> Bool) -> Eq TypeInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: TypeInfo -> TypeInfo -> Bool
    $c/= :: TypeInfo -> TypeInfo -> Bool
    == :: TypeInfo -> TypeInfo -> Bool
    $c== :: TypeInfo -> TypeInfo -> Bool
    Eq, Int -> TypeInfo -> ShowS
    [TypeInfo] -> ShowS
    TypeInfo -> ArgName
    (Int -> TypeInfo -> ShowS)
    -> (TypeInfo -> ArgName) -> ([TypeInfo] -> ShowS) -> Show TypeInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [TypeInfo] -> ShowS
    $cshowList :: [TypeInfo] -> ShowS
    show :: TypeInfo -> ArgName
    $cshow :: TypeInfo -> ArgName
    showsPrec :: Int -> TypeInfo -> ShowS
    $cshowsPrec :: Int -> TypeInfo -> ShowS
    Show)

    sumTypeInfo :: [TypeInfo] -> TypeInfo
    sumTypeInfo :: [TypeInfo] -> TypeInfo
    sumTypeInfo [TypeInfo]
    is = (TypeInfo -> TypeInfo -> TypeInfo)
    -> TypeInfo -> [TypeInfo] -> TypeInfo
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TypeInfo -> TypeInfo -> TypeInfo
    plus TypeInfo
    Empty [TypeInfo]
    is
      where
        plus :: TypeInfo -> TypeInfo -> TypeInfo
    plus TypeInfo
    Empty       TypeInfo
    r           = TypeInfo
    r
        plus TypeInfo
    r           TypeInfo
    Empty       = TypeInfo
    r
        plus TypeInfo
    Erasable    TypeInfo
    r           = TypeInfo
    r
        plus TypeInfo
    r           TypeInfo
    Erasable    = TypeInfo
    r
        plus TypeInfo
    NotErasable TypeInfo
    NotErasable = TypeInfo
    NotErasable

    erasable :: TypeInfo -> Bool
    erasable :: TypeInfo -> Bool
    erasable TypeInfo
    Erasable    = Bool
    True
    erasable TypeInfo
    Empty       = Bool
    True
    erasable TypeInfo
    NotErasable = Bool
    False

    type FunInfo = ([TypeInfo], TypeInfo)

    getFunInfo :: QName -> E FunInfo
    getFunInfo :: QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    q = Lens' (Maybe FunInfo) ESt
    -> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
    forall s (m :: * -> *) a.
    MonadState s m =>
    Lens' (Maybe a) s -> m a -> m a
    memo ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt
    Lens' (Map QName FunInfo) ESt
    funMap ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt)
    -> ((Maybe FunInfo -> f (Maybe FunInfo))
        -> Map QName FunInfo -> f (Map QName FunInfo))
    -> (Maybe FunInfo -> f (Maybe FunInfo))
    -> ESt
    -> f ESt
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Lens' (Maybe FunInfo) (Map QName FunInfo)
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key QName
    q) (StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo)
    -> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
    forall a b. (a -> b) -> a -> b
    $ QName -> StateT ESt (TCMT IO) FunInfo
    getInfo QName
    q
      where
        getInfo :: QName -> E FunInfo
        getInfo :: QName -> StateT ESt (TCMT IO) FunInfo
    getInfo QName
    q = do
          ([TypeInfo]
    rs, Type
    t) <- do
            (ListTel
    tel, Type
    t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
    -> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO (ListTel, Type)
    typeWithoutParams QName
    q
            [TypeInfo]
    is     <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
    -> ListTel -> StateT ESt (TCMT IO) [TypeInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
    -> (Dom (ArgName, Type) -> Type)
    -> Dom (ArgName, Type)
    -> StateT ESt (TCMT IO) TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget) ListTel
    tel
            [ArgUsage]
    used   <- TCM [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage])
    -> TCM [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ ([ArgUsage] -> [ArgUsage] -> [ArgUsage]
    forall a. [a] -> [a] -> [a]
    ++ ArgUsage -> [ArgUsage]
    forall a. a -> [a]
    repeat ArgUsage
    ArgUsed) ([ArgUsage] -> [ArgUsage])
    -> (Maybe [ArgUsage] -> [ArgUsage])
    -> Maybe [ArgUsage]
    -> [ArgUsage]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
    -> TCM (Maybe [ArgUsage]) -> TCM [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Maybe [ArgUsage])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    q
            [IsForced]
    forced <- TCM [IsForced] -> StateT ESt (TCMT IO) [IsForced]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [IsForced] -> StateT ESt (TCMT IO) [IsForced])
    -> TCM [IsForced] -> StateT ESt (TCMT IO) [IsForced]
    forall a b. (a -> b) -> a -> b
    $ ([IsForced] -> [IsForced] -> [IsForced]
    forall a. [a] -> [a] -> [a]
    ++ IsForced -> [IsForced]
    forall a. a -> [a]
    repeat IsForced
    NotForced) ([IsForced] -> [IsForced]) -> TCM [IsForced] -> TCM [IsForced]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM [IsForced]
    forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
    getForcedArgs QName
    q
            ([TypeInfo], Type) -> StateT ESt (TCMT IO) ([TypeInfo], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Dom (ArgName, Type)
     -> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo)
    -> ListTel -> [(IsForced, ArgUsage)] -> [TypeInfo] -> [TypeInfo]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 ((IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
    -> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
     -> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo)
    -> (Dom (ArgName, Type)
        -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
    -> Dom (ArgName, Type)
    -> (IsForced, ArgUsage)
    -> TypeInfo
    -> TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
    mkR (Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
    -> (Dom (ArgName, Type) -> Modality)
    -> Dom (ArgName, Type)
    -> IsForced
    -> ArgUsage
    -> TypeInfo
    -> TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> Modality
    forall a. LensModality a => a -> Modality
    getModality) ListTel
    tel ([IsForced] -> [ArgUsage] -> [(IsForced, ArgUsage)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [IsForced]
    forced [ArgUsage]
    used) [TypeInfo]
    is, Type
    t)
          TypeInfo
    h <- if QName -> Bool
    isAbsurdLambdaName QName
    q then TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TypeInfo
    Erasable else Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo Type
    t
          TCM () -> E ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> E ()) -> TCM () -> E ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Int -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "treeless.opt.erase.info" Int
    50 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "type info for " ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    ": " ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [TypeInfo] -> ArgName
    forall a. Show a => a -> ArgName
    show [TypeInfo]
    rs ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " -> " ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TypeInfo -> ArgName
    forall a. Show a => a -> ArgName
    show TypeInfo
    h
          TCM () -> E ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> E ()) -> TCM () -> E ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Bool] -> TCM ()
    setErasedConArgs QName
    q ([Bool] -> TCM ()) -> [Bool] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (TypeInfo -> Bool) -> [TypeInfo] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeInfo -> Bool
    erasable [TypeInfo]
    rs
          FunInfo -> StateT ESt (TCMT IO) FunInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TypeInfo]
    rs, TypeInfo
    h)

        -- Treat empty, erasable, or unused arguments as Erasable
        mkR :: Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
        mkR :: Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
    mkR Modality
    m IsForced
    f ArgUsage
    u TypeInfo
    i
          | Bool -> Bool
    not (Modality -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Modality
    m) = TypeInfo
    Erasable
          | ArgUsage
    ArgUnused <- ArgUsage
    u         = TypeInfo
    Erasable
          | IsForced
    Forced <- IsForced
    f            = TypeInfo
    Erasable
          | Bool
    otherwise              = TypeInfo
    i

    isErasable :: QName -> TCM Bool
    isErasable :: QName -> TCM Bool
    isErasable QName
    qn =
      -- The active backend should be set
      TCMT IO (Maybe ArgName)
    -> TCM Bool -> (ArgName -> TCM Bool) -> TCM Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Lens' (Maybe ArgName) TCEnv -> TCMT IO (Maybe ArgName)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Maybe ArgName) TCEnv
    eActiveBackendName) TCM Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((ArgName -> TCM Bool) -> TCM Bool)
    -> (ArgName -> TCM Bool) -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ \ ArgName
    bname ->
      -- However it may not be part of the set of available backends
      -- in which case we default to not erasable to avoid false negatives.
      TCMT IO (Maybe Backend)
    -> TCM Bool -> (Backend -> TCM Bool) -> TCM Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (ArgName -> TCMT IO (Maybe Backend)
    lookupBackend ArgName
    bname)       (Bool -> TCM Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False)   ((Backend -> TCM Bool) -> TCM Bool)
    -> (Backend -> TCM Bool) -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ \ Backend
    _ ->
      TypeInfo -> Bool
    erasable (TypeInfo -> Bool) -> (FunInfo -> TypeInfo) -> FunInfo -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FunInfo -> TypeInfo
    forall a b. (a, b) -> b
    snd (FunInfo -> Bool) -> TCMT IO FunInfo -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT ESt (TCMT IO) FunInfo -> TCMT IO FunInfo
    forall a. E a -> TCM a
    runE (QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    qn)

    telListView :: Type -> TCM (ListTel, Type)
    telListView :: Type -> TCMT IO (ListTel, Type)
    telListView Type
    t = do
      TelV Tele (Dom Type)
    tel Type
    t <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
      (ListTel, Type) -> TCMT IO (ListTel, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type) -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel, Type
    t)

    typeWithoutParams :: QName -> TCM (ListTel, Type)
    typeWithoutParams :: QName -> TCMT IO (ListTel, Type)
    typeWithoutParams QName
    q = do
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let d :: Int
    d = case Definition -> Defn
    I.theDef Definition
    def of
            Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection{ projIndex :: Projection -> Int
    projIndex = Int
    i } } -> Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
            Constructor{ conPars :: Defn -> Int
    conPars = Int
    n } -> Int
    n
            Defn
    _                          -> Int
    0
      (ListTel -> ListTel) -> (ListTel, Type) -> (ListTel, Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (Int -> ListTel -> ListTel
    forall a. Int -> [a] -> [a]
    drop Int
    d) ((ListTel, Type) -> (ListTel, Type))
    -> TCMT IO (ListTel, Type) -> TCMT IO (ListTel, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (ListTel, Type)
    telListView (Definition -> Type
    defType Definition
    def)

    getTypeInfo :: Type -> E TypeInfo
    getTypeInfo :: Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo Type
    t0 = do
      (ListTel
    tel, Type
    t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
    -> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO (ListTel, Type)
    telListView Type
    t0
      TypeInfo
    et <- case Type -> Term
    forall t a. Type'' t a -> a
    I.unEl Type
    t of
        I.Def QName
    d Elims
    _ -> do
          -- #2916: Only update the memo table for d. Results for other types are
          -- under the assumption that d is erasable!
          Map QName TypeInfo
    oldMap <- Lens' (Map QName TypeInfo) ESt
    -> StateT ESt (TCMT IO) (Map QName TypeInfo)
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' (Map QName TypeInfo) ESt
    typeMap
          TypeInfo
    dInfo <- QName -> StateT ESt (TCMT IO) TypeInfo
    typeInfo QName
    d
          Lens' (Map QName TypeInfo) ESt
    typeMap Lens' (Map QName TypeInfo) ESt -> Map QName TypeInfo -> E ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= QName -> TypeInfo -> Map QName TypeInfo -> Map QName TypeInfo
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert QName
    d TypeInfo
    dInfo Map QName TypeInfo
    oldMap
          TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    dInfo
        Sort{}    -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Erasable
        Term
    _         -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    NotErasable
      [TypeInfo]
    is <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
    -> ListTel -> StateT ESt (TCMT IO) [TypeInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
    -> (Dom (ArgName, Type) -> Type)
    -> Dom (ArgName, Type)
    -> StateT ESt (TCMT IO) TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget) ListTel
    tel
      let e :: TypeInfo
    e | TypeInfo
    Empty TypeInfo -> [TypeInfo] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TypeInfo]
    is = TypeInfo
    Erasable
            | [TypeInfo] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TypeInfo]
    is         = TypeInfo
    et        -- TODO: guard should really be "all inhabited is"
            | TypeInfo
    et TypeInfo -> TypeInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == TypeInfo
    Empty     = TypeInfo
    Erasable
            | Bool
    otherwise       = TypeInfo
    et
      TCM () -> E ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> E ()) -> TCM () -> E ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "treeless.opt.erase.type" Int
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t0 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName
    "is " ArgName -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TypeInfo -> ArgName
    forall a. Show a => a -> ArgName
    show TypeInfo
    e)
      TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    e
      where
      typeInfo :: QName -> E TypeInfo
      typeInfo :: QName -> StateT ESt (TCMT IO) TypeInfo
    typeInfo QName
    q = StateT ESt (TCMT IO) Bool
    -> StateT ESt (TCMT IO) TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> StateT ESt (TCMT IO) Bool
    erasureForbidden QName
    q) (TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    NotErasable) (StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
    -> StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a b. (a -> b) -> a -> b
    $ {-else-} do
        Lens' (Maybe TypeInfo) ESt
    -> TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    forall s (m :: * -> *) a.
    MonadState s m =>
    Lens' (Maybe a) s -> a -> m a -> m a
    memoRec ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
    Lens' (Map QName TypeInfo) ESt
    typeMap ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt)
    -> ((Maybe TypeInfo -> f (Maybe TypeInfo))
        -> Map QName TypeInfo -> f (Map QName TypeInfo))
    -> (Maybe TypeInfo -> f (Maybe TypeInfo))
    -> ESt
    -> f ESt
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Lens' (Maybe TypeInfo) (Map QName TypeInfo)
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key QName
    q) TypeInfo
    Erasable (StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
    -> StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a b. (a -> b) -> a -> b
    $ do  -- assume recursive occurrences are erasable
          [Maybe QName]
    msizes <- TCMT IO [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName])
    -> TCMT IO [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName]
    forall a b. (a -> b) -> a -> b
    $ (ArgName -> TCMT IO (Maybe QName))
    -> [ArgName] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ArgName -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    ArgName -> m (Maybe QName)
    getBuiltinName
                             [ArgName
    builtinSize, ArgName
    builtinSizeLt]
          Definition
    def    <- TCMT IO Definition -> StateT ESt (TCMT IO) Definition
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Definition -> StateT ESt (TCMT IO) Definition)
    -> TCMT IO Definition -> StateT ESt (TCMT IO) Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          let mcs :: Maybe [QName]
    mcs = case Definition -> Defn
    I.theDef Definition
    def of
                      I.Datatype{ dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    cs
                      I.Record{ recConHead :: Defn -> ConHead
    recConHead = ConHead
    c }  -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [ConHead -> QName
    conName ConHead
    c]
                      Defn
    _                           -> Maybe [QName]
    forall a. Maybe a
    Nothing
          case Maybe [QName]
    mcs of
            Maybe [QName]
    _ | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> [Maybe QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName]
    msizes -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Erasable
            Just [QName
    c] -> do
              (ListTel
    ts, Type
    _) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
    -> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO (ListTel, Type)
    typeWithoutParams QName
    c
              let rs :: [Modality]
    rs = (Dom (ArgName, Type) -> Modality) -> ListTel -> [Modality]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (ArgName, Type) -> Modality
    forall a. LensModality a => a -> Modality
    getModality ListTel
    ts
              [TypeInfo]
    is <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
    -> ListTel -> StateT ESt (TCMT IO) [TypeInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
    -> (Dom (ArgName, Type) -> Type)
    -> Dom (ArgName, Type)
    -> StateT ESt (TCMT IO) TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget) ListTel
    ts
              let er :: Bool
    er = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [ TypeInfo -> Bool
    erasable TypeInfo
    i Bool -> Bool -> Bool
    || Bool -> Bool
    not (Modality -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Modality
    r) | (TypeInfo
    i, Modality
    r) <- [TypeInfo] -> [Modality] -> [(TypeInfo, Modality)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TypeInfo]
    is [Modality]
    rs ]
              TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
    -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a b. (a -> b) -> a -> b
    $ if Bool
    er then TypeInfo
    Erasable else TypeInfo
    NotErasable
            Just []      -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Empty
            Just (QName
    _:QName
    _:[QName]
    _) -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    NotErasable
            Maybe [QName]
    Nothing ->
              case Definition -> Defn
    I.theDef Definition
    def of
                I.Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs } ->
                  [TypeInfo] -> TypeInfo
    sumTypeInfo ([TypeInfo] -> TypeInfo)
    -> StateT ESt (TCMT IO) [TypeInfo] -> StateT ESt (TCMT IO) TypeInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Clause -> StateT ESt (TCMT IO) TypeInfo)
    -> [Clause] -> StateT ESt (TCMT IO) [TypeInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (StateT ESt (TCMT IO) TypeInfo
    -> (Term -> StateT ESt (TCMT IO) TypeInfo)
    -> Maybe Term
    -> StateT ESt (TCMT IO) TypeInfo
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Empty) (Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
    -> (Term -> Type) -> Term -> StateT ESt (TCMT IO) TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    HasCallStack => Sort' Term
    __DUMMY_SORT__) (Maybe Term -> StateT ESt (TCMT IO) TypeInfo)
    -> (Clause -> Maybe Term)
    -> Clause
    -> StateT ESt (TCMT IO) TypeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody) [Clause]
    cs
                Defn
    _ -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    NotErasable
      -- The backend also has a say whether a type is eraseable or not.
      erasureForbidden :: QName -> E Bool
      erasureForbidden :: QName -> StateT ESt (TCMT IO) Bool
    erasureForbidden QName
    q = TCM Bool -> StateT ESt (TCMT IO) Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Bool -> StateT ESt (TCMT IO) Bool)
    -> TCM Bool -> StateT ESt (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM Bool
    activeBackendMayEraseType QName
    q