    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE PatternSynonyms #-}

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

    import Control.Arrow       ( first, second )
    import Control.Monad.State ( StateT, evalStateT )

    import Data.Map (Map)
    import qualified Data.Map as Map

    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    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 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.Syntax.Common.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' ESt (Map QName FunInfo)
    funMap :: Lens' ESt (Map QName FunInfo)
    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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Map QName FunInfo
    a -> ESt
    r { _funMap = a }

    typeMap :: Lens' ESt (Map QName TypeInfo)
    typeMap :: Lens' ESt (Map QName TypeInfo)
    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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Map QName TypeInfo
    a -> ESt
    r { _typeMap = 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 -> TCMT IO 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
      cs <- QName -> TCM [QName]
    getNotErasedConstructors QName
    d
      runE $ mapM_ getFunInfo 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 a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    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
          (_, h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    q
          case h of
            TypeInfo
    Erasable -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
            TypeInfo
    Empty    -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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
            (rs, h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    c
            when (length rs < length vs) __IMPOSSIBLE__
            case h of
              TypeInfo
    Erasable -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    Empty    -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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
            (rs, h) <- QName -> StateT ESt (TCMT IO) FunInfo
    getFunInfo QName
    f
            case h of
              TypeInfo
    Erasable -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
              TypeInfo
    Empty    -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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 a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TDef{}         -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TPrim{}        -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TLit{}         -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TCon{}         -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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 a b.
    StateT ESt (TCMT IO) (a -> b)
    -> StateT ESt (TCMT IO) a -> StateT ESt (TCMT IO) b
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
              e <- TTerm -> E TTerm
    erase TTerm
    e
              if isErased e
                then case 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 tLet e <$> erase b
            TCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs -> do
              (d, bs) <- Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable Int
    x (CaseInfo -> Erased
    caseErased CaseInfo
    t) (CaseInfo -> CaseType
    caseType CaseInfo
    t) TTerm
    d [TAlt]
    bs
              d       <- erase d
              bs      <- mapM eraseAlt bs
              tCase x t d bs

            TTerm
    TUnit          -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TTerm
    TSort          -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TTerm
    TErased        -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    t
            TError{}       -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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 a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
          | Bool
    otherwise = case [TAlt]
    bs of
            [b :: TAlt
    b@(TACon QName
    c Int
    _ TTerm
    _)] -> do
              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 h of
                TypeInfo
    NotErasable -> E TTerm
    fallback
                TypeInfo
    Empty       -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    TErased
                TypeInfo
    Erasable    -> TAlt -> E TTerm
    erasedBody TAlt
    b
            [TAlt]
    _ -> E TTerm
    fallback
          where
            noerase :: E TTerm
    noerase = TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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

            erasedBody :: TAlt -> E TTerm
    erasedBody = \case
              TACon QName
    _ Int
    arity TTerm
    body ->
                (if Int
    arity Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    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
    $
                   -- might enable more erasure
                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
    arity TTerm
    TErased [TTerm] -> Substitution' TTerm -> Substitution' TTerm
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Substitution' TTerm
    forall a. Substitution' a
    idS) TTerm
    body
              TALit Literal
    _ TTerm
    body   -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    body
              TAGuard TTerm
    _ TTerm
    body -> TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TTerm
    body

            fallback :: E TTerm
    fallback = case (CaseInfo -> Erased
    caseErased CaseInfo
    t, [TAlt]
    bs) of
              (Erased{}, [TAlt
    b]) ->
                -- The case variable is erased, and there is exactly one
                -- case: use the case's body.
                TAlt -> E TTerm
    erasedBody TAlt
    b
              (Erased{}, [])  ->
                -- The case variable is erased, and there is no case: use
                -- the default.
                TTerm -> E TTerm
    forall a. a -> StateT ESt (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TTerm -> E TTerm) -> TTerm -> E TTerm
    forall a b. (a -> b) -> a -> b
    $ if TTerm -> Bool
    isErased TTerm
    d then TTerm
    TErased else TTerm
    d
              (Erased{}, TAlt
    _ : TAlt
    _ : [TAlt]
    _) ->
                -- The case variable is erased, and there are at least two
                -- cases: crash.
                E TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              (Erased, [TAlt])
    _ ->
                -- The case variable is not erased: do not erase anything.
                E TTerm
    noerase

        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 a. a -> StateT ESt (TCMT IO) a
    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
            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 = (Bool -> Substitution' TTerm -> Substitution' TTerm)
    -> Substitution' TTerm -> [Bool] -> Substitution' TTerm
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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
            TACon c a <$> erase (applySubst sub 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 a b.
    StateT ESt (TCMT IO) (a -> b)
    -> StateT ESt (TCMT IO) a -> StateT ESt (TCMT IO) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> E TTerm
    erase TTerm
    b

    pruneUnreachable ::
      Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable :: Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable Int
    x Erased
    erased CaseType
    t TTerm
    d [TAlt]
    bs = case Erased
    erased of
      NotErased{} -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable' Int
    x Erased
    erased CaseType
    t TTerm
    d [TAlt]
    bs
      Erased{}    ->
        -- If the match is on an erased argument, then the first branch
        -- should match.
        case [TAlt]
    bs of
          []    -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable' Int
    x Erased
    erased CaseType
    t TTerm
    d            []
          TAlt
    b : [TAlt]
    _ -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable' Int
    x Erased
    erased CaseType
    t TTerm
    tUnreachable [TAlt
    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 -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable' :: Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
    pruneUnreachable' Int
    _ Erased
    erased (CTData QName
    q) TTerm
    d [TAlt]
    bs' = do
      -- Erased constructors are pruned iff the match is made on a
      -- non-erased argument.
      cs <- TCM [QName] -> StateT ESt (TCMT IO) [QName]
    forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    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 Erased -> Bool
    isErased Erased
    erased
            then QName -> TCM [QName]
    getConstructors QName
    q
            else QName -> TCM [QName]
    getNotErasedConstructors QName
    q
      let bs | Erased -> Bool
    isErased Erased
    erased = [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 a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    cs
                 TAGuard{} -> Bool
    True
                 TALit{}   -> Bool
    True
      let -- In the case of a match on an erased argument the value d is
          -- equal to tUnreachable, except perhaps if bs is empty. In the
          -- latter case complete is True exactly when the type has zero
          -- constructors (erased or not), in which case it makes sense to
          -- replace d with tUnreachable.
          complete = [QName] -> Int
    forall a. [a] -> 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 a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ TAlt
    b | b :: TAlt
    b@TACon{} <- [TAlt]
    bs ]
          d' | Bool
    complete  = TTerm
    tUnreachable
             | Bool
    otherwise = TTerm
    d
      return (d', bs)
    pruneUnreachable' Int
    x Erased
    _ CaseType
    CTNat TTerm
    d [TAlt]
    bs =
      (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall a. a -> StateT ESt (TCMT IO) a
    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 Erased
    _ CaseType
    CTInt TTerm
    d [TAlt]
    bs =
      (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall a. a -> StateT ESt (TCMT IO) a
    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
    _ Erased
    _ CaseType
    _ TTerm
    d [TAlt]
    bs =
      (TTerm, [TAlt]) -> E (TTerm, [TAlt])
    forall a. a -> StateT ESt (TCMT IO) a
    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 $mBelow :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
    $bBelow :: Int -> Integer -> TTerm
    Below x n = TApp (TPrim PLt)  [TVar x, TLit (LitNat n)]

    pattern Above :: Int -> Integer -> TTerm
    pattern $mAbove :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
    $bAbove :: Int -> Integer -> TTerm
    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 b c d. (b -> c) -> (d, b) -> (d, c)
    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 b c d. (b -> c) -> (d, b) -> (d, c)
    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
    $c== :: TypeInfo -> TypeInfo -> Bool
    == :: TypeInfo -> TypeInfo -> Bool
    $c/= :: TypeInfo -> TypeInfo -> Bool
    /= :: 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
    $cshowsPrec :: Int -> TypeInfo -> ShowS
    showsPrec :: Int -> TypeInfo -> ShowS
    $cshow :: TypeInfo -> ArgName
    show :: TypeInfo -> ArgName
    $cshowList :: [TypeInfo] -> ShowS
    showList :: [TypeInfo] -> ShowS
    Show)

    sumTypeInfo :: [TypeInfo] -> TypeInfo
    sumTypeInfo :: [TypeInfo] -> TypeInfo
    sumTypeInfo [TypeInfo]
    is = (TypeInfo -> TypeInfo -> TypeInfo)
    -> TypeInfo -> [TypeInfo] -> TypeInfo
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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' ESt (Maybe FunInfo)
    -> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
    forall s (m :: * -> *) a.
    MonadState s m =>
    Lens' s (Maybe a) -> m a -> m a
    memo ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt
    Lens' ESt (Map QName FunInfo)
    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' (Map QName FunInfo) (Maybe FunInfo)
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe 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
          (rs, t) <- do
            (tel, t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    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
            is     <- mapM (getTypeInfo . snd . dget) tel
            used   <- lift $ (++ repeat ArgUsed) . fromMaybe [] <$> getCompiledArgUse q
            forced <- lift $ (++ repeat NotForced) <$> getForcedArgs q
            return (zipWith3 (uncurry . mkR . getModality) tel (zip forced used) is, t)
          h <- if isAbsurdLambdaName q then pure Erasable else getTypeInfo t
          lift $ reportSLn "treeless.opt.erase.info" 50 $ "type info for " ++ prettyShow q ++ ": " ++ show rs ++ " -> " ++ show h
          lift $ setErasedConArgs q $ map erasable rs
          return (rs, 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 =
      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 tel t <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
      return (telToList tel, t)

    typeWithoutParams :: QName -> TCM (ListTel, Type)
    typeWithoutParams :: QName -> TCMT IO (ListTel, Type)
    typeWithoutParams QName
    q = do
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let d = case Definition -> Defn
    I.theDef Definition
    def of
            Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right 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
      first (drop d) <$> telListView (defType def)

    getTypeInfo :: Type -> E TypeInfo
    getTypeInfo :: Type -> StateT ESt (TCMT IO) TypeInfo
    getTypeInfo Type
    t0 = do
      (tel, t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    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
      et <- case I.unEl 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!
          oldMap <- Lens' ESt (Map QName TypeInfo)
    -> StateT ESt (TCMT IO) (Map QName TypeInfo)
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
    Lens' ESt (Map QName TypeInfo)
    typeMap
          dInfo <- typeInfo d
          typeMap .= Map.insert d dInfo oldMap
          return dInfo
        Sort{}    -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a. a -> StateT ESt (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Erasable
        Term
    _         -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a. a -> StateT ESt (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    NotErasable
      is <- mapM (getTypeInfo . snd . dget) tel
      let e | TypeInfo
    Empty TypeInfo -> [TypeInfo] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TypeInfo]
    is = TypeInfo
    Erasable
            | [TypeInfo] -> Bool
    forall a. [a] -> 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
      lift $ reportSDoc "treeless.opt.erase.type" 50 $ prettyTCM t0 <+> text ("is " ++ show e)
      return 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 a. a -> StateT ESt (TCMT IO) a
    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' ESt (Maybe TypeInfo)
    -> TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    -> StateT ESt (TCMT IO) TypeInfo
    forall s (m :: * -> *) a.
    MonadState s m =>
    Lens' s (Maybe a) -> a -> m a -> m a
    memoRec ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
    Lens' ESt (Map QName TypeInfo)
    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' (Map QName TypeInfo) (Maybe TypeInfo)
    forall k v. Ord k => k -> Lens' (Map k v) (Maybe 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
          msizes <- TCM [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName]
    forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName])
    -> TCM [Maybe QName] -> StateT ESt (TCMT IO) [Maybe QName]
    forall a b. (a -> b) -> a -> b
    $ (BuiltinId -> TCMT IO (Maybe QName))
    -> [BuiltinId] -> TCM [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM BuiltinId -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName
                             [BuiltinId
    builtinSize, BuiltinId
    builtinSizeLt]
          def    <- lift $ getConstInfo q
          let 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 mcs of
            Maybe [QName]
    _ | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> [Maybe QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName]
    msizes -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a. a -> StateT ESt (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Erasable
            Just [QName
    c] -> do
              (ts, _) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
    forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    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 = (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
              is <- mapM (getTypeInfo . snd . dget) ts
              let 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 ]
              return $ if er then Erasable else NotErasable
            Just []      -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a. a -> StateT ESt (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TypeInfo
    Empty
            Just (QName
    _:QName
    _:[QName]
    _) -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
    forall a. a -> StateT ESt (TCMT IO) a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> StateT ESt (TCMT IO) a
    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 a. a -> StateT ESt (TCMT IO) a
    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 (m :: * -> *) a. Monad m => m a -> StateT ESt m a
    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