content: 
  -- | The monad for the termination checker.
  --
  --   The termination monad @TerM@ is an extension of
  --   the type checking monad 'TCM' by an environment
  --   with information needed by the termination checker.
  
  module Agda.Termination.Monad where
  
  import Prelude hiding (null, zip, zipWith)
  
  import Control.Applicative hiding (empty)
  
  import Control.Monad.IO.Class ( MonadIO(..) )
  import Control.Monad.Except   ( MonadError(..) )
  import Control.Monad.Reader   ( MonadReader(..), ReaderT(..) )
  
  import Data.DList (DList)
  import qualified Data.DList as DL
  import Data.Set (Set)
  import qualified Data.Set as Set
  
  import Agda.Interaction.Options (optTerminationDepth)
  
  import Agda.Syntax.Common
  import Agda.Syntax.Internal
  import Agda.Syntax.Internal.Pattern
  import Agda.Syntax.Literal
  
  import Agda.Termination.CutOff
  import Agda.Termination.Order (Order,le,unknown)
  import Agda.Termination.RecCheck (MutualNames, anyDefs)
  
  import Agda.TypeChecking.Monad
  import Agda.TypeChecking.Monad.Benchmark
  import Agda.TypeChecking.Pretty
  import Agda.TypeChecking.Records
  import Agda.TypeChecking.Reduce
  import Agda.TypeChecking.Substitute
  
  import Agda.Utils.Benchmark as B
  import Agda.Utils.Function
  import Agda.Utils.Functor
  import Agda.Utils.Lens
  import Agda.Utils.List   ( hasElem )
  import Agda.Utils.ListInf ( ListInf )
  import Agda.Utils.ListInf qualified as ListInf
  import Agda.Utils.Maybe
  import Agda.Utils.Monad
  import Agda.Utils.Monoid
  import Agda.Utils.Null
  import Agda.Syntax.Common.Pretty (Pretty, prettyShow)
  import Agda.Utils.Singleton
  import qualified Agda.Syntax.Common.Pretty as P
  import Agda.Utils.VarSet (VarSet)
  import qualified Agda.Utils.VarSet as VarSet
  import Agda.Utils.Zip
  
  import Agda.Utils.Impossible
  
  -- | The target of the function we are checking.
  
  data Target
    = TargetDef QName
        -- ^ The target of recursion is a @record@, @data@, or unreducible @Def@.
    | TargetRecord
        -- ^ We are termination-checking a record.
    | TargetOther
        -- ^ None of the above two or unknown.
    deriving (Eq, Show)
  
  -- | The current guardedness level.
  
  type Guarded = Order
  
  -- | The termination environment.
  
  data TerEnv = TerEnv
  
    -- First part: options, configuration.
  
    { terUseDotPatterns :: Bool
      -- ^ Are we mining dot patterns to find evindence of structal descent?
    , terSizeSuc :: Maybe QName
      -- ^ The name of size successor, if any.
    , terSharp   :: Maybe QName
      -- ^ The name of the delay constructor (sharp), if any.
    , terCutOff  :: CutOff
      -- ^ Depth at which to cut off the structural order.
  
    -- Second part: accumulated info during descent into decls./term.
  
    , terCurrent :: QName
      -- ^ The name of the function we are currently checking.
    , terMutual  :: MutualNames
      -- ^ The names of the functions in the mutual block we are checking.
      --   This includes the internally generated functions
      --   (with, extendedlambda, coinduction).
    , terUserNames :: Set QName
      -- ^ The list of name actually appearing in the file (abstract syntax).
      --   Excludes the internally generated functions.
    , terHaveInlinedWith :: Bool
      -- ^ Does the actual clause result from with-inlining?
      --   (If yes, it may be ill-typed.)
    , terTarget  :: Target
      -- ^ Target type of the function we are currently termination checking.
      --   Only the constructors of 'Target' are considered guarding.
    , terMaskArgs :: ListInf Bool
      -- ^ Only consider the 'notMasked' 'False' arguments for establishing termination.
      --   See issue #1023.
    , terMaskResult :: Bool
      -- ^ Only consider guardedness if 'False' (not masked).
    , _terSizeDepth :: Int  -- lazy by intention!
      -- ^ How many @SIZELT@ relations do we have in the context
      --   (= clause telescope).  Used to approximate termination
      --   for metas in call args.
    , terPatterns :: MaskedDeBruijnPatterns
      -- ^ The patterns of the clause we are checking.
    , terPatternsRaise :: !Int
      -- ^ Number of additional binders we have gone under
      --   (and consequently need to raise the patterns to compare to terms).
      --   Updated during call graph extraction, hence strict.
    , terGuarded :: !Guarded
      -- ^ The current guardedness status.  Changes as we go deeper into the term.
      --   Updated during call graph extraction, hence strict.
    , terUseSizeLt :: Bool
      -- ^ When extracting usable size variables during construction of the call
      --   matrix, can we take the variable for use with SIZELT constraints from the context?
      --   Yes, if we are under an inductive constructor.
      --   No, if we are under a record constructor.
      --   (See issue #1015).
    , terUsableVars :: VarSet
      -- ^ Pattern variables that can be compared to argument variables using SIZELT.
    }
  
  -- | An empty termination environment.
  --
  --   Values are set to a safe default meaning that with these
  --   initial values the termination checker will not miss
  --   termination errors it would have seen with better settings
  --   of these values.
  --
  --   Values that do not have a safe default are set to
  --   @__IMPOSSIBLE__@.
  
  defaultTerEnv :: TerEnv
  defaultTerEnv = TerEnv
    { terUseDotPatterns           = False -- must be False initially!
    , terSizeSuc                  = Nothing
    , terSharp                    = Nothing
    , terCutOff                   = defaultCutOff
    , terUserNames                = __IMPOSSIBLE__ -- needs to be set!
    , terMutual                   = __IMPOSSIBLE__ -- needs to be set!
    , terCurrent                  = __IMPOSSIBLE__ -- needs to be set!
    , terHaveInlinedWith          = False
    , terTarget                   = TargetOther
    , terMaskArgs                 = ListInf.repeat False   -- use all arguments (mask none)
    , terMaskResult               = False          -- use result (do not mask)
    , _terSizeDepth               = __IMPOSSIBLE__ -- needs to be set!
    , terPatterns                 = __IMPOSSIBLE__ -- needs to be set!
    , terPatternsRaise            = 0
    , terGuarded                  = le -- not initially guarded
    , terUseSizeLt                = False -- initially, not under data constructor
    , terUsableVars               = empty
    }
  
  -- | Termination monad service class.
  
  class (Functor m, Monad m) => MonadTer m where
    terAsk   :: m TerEnv
    terLocal :: (TerEnv -> TerEnv) -> m a -> m a
  
    terAsks :: (TerEnv -> a) -> m a
    terAsks f = f <$> terAsk
  
  -- | Termination monad.
  
  newtype TerM a = TerM { terM :: ReaderT TerEnv TCM a }
    deriving ( Functor
             , Applicative
             , Monad
             , MonadError TCErr
             , MonadStatistics
             , HasOptions
             , HasBuiltins
             , MonadDebug
             , MonadFileId
             , HasConstInfo
             , MonadIO
             , MonadTCEnv
             , MonadTCState
             , MonadTCM
             , ReadTCState
             , MonadReduce
             , MonadAddContext
             , PureTCM
             )
  
  -- This could be derived automatically, but the derived type family becomes `BenchPhase (ReaderT TerEnv TCM)` which
  -- is *fine* but triggers complaints that the "type family application is no smaller than the instance head, why not
  -- nuke everything with UndecidableInstances".
  instance MonadBench TerM where
    type BenchPhase TerM = Phase
    getBenchmark              = TerM $ B.getBenchmark
    putBenchmark              = TerM . B.putBenchmark
    modifyBenchmark           = TerM . B.modifyBenchmark
    finally (TerM m) (TerM f) = TerM $ (B.finally m f)
  
  instance MonadTer TerM where
    terAsk     = TerM $ ask
    terLocal f = TerM . local f . terM
  
  -- | Generic run method for termination monad.
  runTer :: TerEnv -> TerM a -> TCM a
  runTer tenv (TerM m) = runReaderT m tenv
  
  -- | Run TerM computation in default environment (created from options).
  
  runTerDefault :: TerM a -> TCM a
  runTerDefault cont = do
  
    -- Assemble then initial configuration of the termination environment.
  
    cutoff <- optTerminationDepth <$> pragmaOptions
  
    -- Get the name of size suc (if sized types are enabled)
    suc <- sizeSucName
  
    -- The name of sharp (if available).
    sharp <- fmap nameOfSharp <$> coinductionKit
  
    let tenv = defaultTerEnv
          { terSizeSuc                  = suc
          , terSharp                    = sharp
          , terCutOff                   = cutoff
          }
  
    runTer tenv cont
  
  -- -- * Termination monad is a 'MonadTCM'.
  
  -- instance MonadError TCErr TerM where
  --   throwError = liftTCM . throwError
  --   catchError m handler = TerM $ ReaderT $ \ tenv -> do
  --     runTer tenv m `catchError` (\ err -> runTer tenv $ handler err)
  
  instance Semigroup m => Semigroup (TerM m) where
    (<>) = liftA2 (<>)
  
  instance (Semigroup m, Monoid m) => Monoid (TerM m) where
    mempty  = pure mempty
    mappend = (<>)
    mconcat = mconcat <.> sequence
  
  -- * Modifiers and accessors for the termination environment in the monad.
  
  terGetUseDotPatterns :: TerM Bool
  terGetUseDotPatterns = terAsks terUseDotPatterns
  
  terSetUseDotPatterns :: Bool -> TerM a -> TerM a
  terSetUseDotPatterns b = terLocal $ \ e -> e { terUseDotPatterns = b }
  
  terGetSizeSuc :: TerM (Maybe QName)
  terGetSizeSuc = terAsks terSizeSuc
  
  terGetCurrent :: TerM QName
  terGetCurrent = terAsks terCurrent
  
  terSetCurrent :: QName -> TerM a -> TerM a
  terSetCurrent q = terLocal $ \ e -> e { terCurrent = q }
  
  terGetSharp :: TerM (Maybe QName)
  terGetSharp = terAsks terSharp
  
  terGetCutOff :: TerM CutOff
  terGetCutOff = terAsks terCutOff
  
  terGetMutual :: TerM MutualNames
  terGetMutual = terAsks terMutual
  
  terGetUserNames :: TerM (Set QName)
  terGetUserNames = terAsks terUserNames
  
  terGetTarget :: TerM Target
  terGetTarget = terAsks terTarget
  
  terSetTarget :: Target -> TerM a -> TerM a
  terSetTarget t = terLocal $ \ e -> e { terTarget = t }
  
  terGetHaveInlinedWith :: TerM Bool
  terGetHaveInlinedWith = terAsks terHaveInlinedWith
  
  terSetHaveInlinedWith :: TerM a -> TerM a
  terSetHaveInlinedWith = terLocal $ \ e -> e { terHaveInlinedWith = True }
  
  terGetMaskArgs :: TerM (ListInf Bool)
  terGetMaskArgs = terAsks terMaskArgs
  
  terSetMaskArgs :: ListInf Bool -> TerM a -> TerM a
  terSetMaskArgs b = terLocal $ \ e -> e { terMaskArgs = b }
  
  terGetMaskResult :: TerM Bool
  terGetMaskResult = terAsks terMaskResult
  
  terSetMaskResult :: Bool -> TerM a -> TerM a
  terSetMaskResult b = terLocal $ \ e -> e { terMaskResult = b }
  
  terGetPatterns :: TerM (MaskedDeBruijnPatterns)
  terGetPatterns = do
    n   <- terAsks terPatternsRaise
    mps <- terAsks terPatterns
    return $ if n == 0 then mps else map (fmap (raise n)) mps
  
  terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
  terSetPatterns ps = terLocal $ \ e -> e { terPatterns = ps }
  
  terRaise :: TerM a -> TerM a
  terRaise = terLocal $ \ e -> e { terPatternsRaise = terPatternsRaise e + 1 }
  
  terGetGuarded :: TerM Guarded
  terGetGuarded = terAsks terGuarded
  
  terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a
  terModifyGuarded f = terLocal $ \ e -> e { terGuarded = f $ terGuarded e }
  
  terSetGuarded :: Order -> TerM a -> TerM a
  terSetGuarded = terModifyGuarded . const
  
  terUnguarded :: TerM a -> TerM a
  terUnguarded = terSetGuarded unknown
  
  -- | Lens for '_terSizeDepth'.
  
  terSizeDepth :: Lens' TerEnv Int
  terSizeDepth f e = f (_terSizeDepth e) <&> \ i -> e { _terSizeDepth = i }
  
  -- | Lens for 'terUsableVars'.
  
  terGetUsableVars :: TerM VarSet
  terGetUsableVars = terAsks terUsableVars
  
  terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a
  terModifyUsableVars f = terLocal $ \ e -> e { terUsableVars = f $ terUsableVars e }
  
  terSetUsableVars :: VarSet -> TerM a -> TerM a
  terSetUsableVars = terModifyUsableVars . const
  
  -- | Lens for 'terUseSizeLt'.
  
  terGetUseSizeLt :: TerM Bool
  terGetUseSizeLt = terAsks terUseSizeLt
  
  terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a
  terModifyUseSizeLt f = terLocal $ \ e -> e { terUseSizeLt = f $ terUseSizeLt e }
  
  terSetUseSizeLt :: Bool -> TerM a -> TerM a
  terSetUseSizeLt = terModifyUseSizeLt . const
  
  -- | Compute usable vars from patterns and run subcomputation.
  withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b
  withUsableVars pats m = do
    vars <- usableSizeVars pats
    reportSLn "term.size" 70 $ "usableSizeVars = " ++ show vars
    reportSDoc "term.size" 20 $ if null vars then "no usuable size vars" else
      "the size variables amoung these variables are usable: " <+>
        sep (map (prettyTCM . var) $ VarSet.toAscList vars)
    terSetUsableVars vars $ m
  
  -- | Set 'terUseSizeLt' when going under constructor @c@.
  conUseSizeLt :: QName -> TerM a -> TerM a
  conUseSizeLt c m = do
    ifM (liftTCM $ isEtaOrCoinductiveRecordConstructor c)  -- Non-eta inductive records are the same as datatypes
      (terSetUseSizeLt False m)
      (terSetUseSizeLt True m)
  
  -- | Set 'terUseSizeLt' for arguments following projection @q@.
  --   We disregard j<i after a non-coinductive projection.
  --   However, the projection need not be recursive (Issue 1470).
  projUseSizeLt :: QName -> TerM a -> TerM a
  projUseSizeLt q m = do
    co <- isCoinductiveProjection False q
    reportSLn "term.size" 20 $ applyUnless co ("not " ++) $
      "using SIZELT vars after projection " ++ prettyShow q
    terSetUseSizeLt co m
  
  -- | For termination checking purposes flat should not be considered a
  --   projection. That is, it flat doesn't preserve either structural order
  --   or guardedness like other projections do.
  --   Andreas, 2012-06-09: the same applies to projections of recursive records.
  isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool
  isProjectionButNotCoinductive qn = liftTCM $ do
    b <- isProjectionButNotCoinductive' qn
    reportSDoc "term.proj" 60 $ do
      "identifier" <+> prettyTCM qn <+> do
        text $
          if b then "is an inductive projection"
            else "is either not a projection or coinductive"
    return b
    where
      isProjectionButNotCoinductive' qn = do
        flat <- fmap nameOfFlat <$> coinductionKit
        if Just qn == flat
          then return False
          else do
            mp <- isProjection qn
            case mp of
              Just Projection{ projProper = Just{}, projFromType = t }
                -> isInductiveRecord (unArg t)
              _ -> return False
  
  -- | Check whether a projection belongs to a coinductive record
  --   and is actually recursive.
  --   E.g.
  --   @
  --      isCoinductiveProjection (Stream.head) = return False
  --
  --      isCoinductiveProjection (Stream.tail) = return True
  --   @
  isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
  isCoinductiveProjection mustBeRecursive q = liftTCM $ do
    reportSLn "term.guardedness" 40 $ "checking isCoinductiveProjection " ++ prettyShow q
    flat <- fmap nameOfFlat <$> coinductionKit
    -- yes for ♭
    if Just q == flat then return True else do
      pdef <- getConstInfo q
      case isProjection_ (theDef pdef) of
        Just Projection{ projProper = Just{}, projFromType = Arg _ r, projIndex = n } ->
          caseMaybeM (isRecord r) __IMPOSSIBLE__ $ \ rdef -> do
            -- no for inductive or non-recursive record
            if _recInduction rdef /= Just CoInductive then return False else do
              reportSLn "term.guardedness" 40 $ prettyShow q ++ " is coinductive; record type is " ++ prettyShow r
              if not mustBeRecursive then return True else do
                reportSLn "term.guardedness" 40 $ prettyShow q ++ " must be recursive"
                if notSafeRecRecursive rdef then return False else do
                  reportSLn "term.guardedness" 40 $ prettyShow q ++ " has been declared recursive, doing actual check now..."
                  -- TODO: the following test for recursiveness of a projection should be cached.
                  -- E.g., it could be stored in the @Projection@ component.
                  -- Now check if type of field mentions mutually recursive symbol.
                  -- Get the type of the field by dropping record parameters and record argument.
                  let TelV tel core = telView' (defType pdef)
                      (pars, tel') = splitAt n $ telToList tel
                      mut = fromMaybe __IMPOSSIBLE__ $ _recMutual rdef
                  -- Check if any recursive symbols appear in the record type.
                  -- Q (2014-07-01): Should we normalize the type?
                  -- A (2017-01-13): Yes, since we also normalize during positivity check?
                  -- See issue #1899.
                  reportSDoc "term.guardedness" 40 $ inTopContext $ sep
                    [ "looking for recursive occurrences of"
                    , sep (map prettyTCM mut)
                    , "in"
                    , addContext pars $ prettyTCM (telFromList tel')
                    , "and"
                    , addContext tel $ prettyTCM core
                    ]
                  when (null mut) __IMPOSSIBLE__
                  names <- anyDefs (mut `hasElem`) (map (snd . unDom) tel', core)
                  reportSDoc "term.guardedness" 40 $
                    "found" <+> if null names then "none" else sep (map prettyTCM $ Set.toList names)
                  return $ not $ null names
        _ -> do
          reportSLn "term.guardedness" 40 $ prettyShow q ++ " is not a proper projection"
          return False
    where
    -- Andreas, 2018-02-24, issue #2975, example:
    -- @
    -- record R : Set where
    --   coinductive
    --   field force : R
  
    --   r : R
    --   force r = r
    -- @
    -- The termination checker expects the positivity checker to have run on the
    -- record declaration R to know whether R is recursive.
    -- However, here, because the awkward processing of record declarations (see #434),
    -- that has not happened.  To avoid crashing (as in Agda 2.5.3),
    -- we rather give the possibly wrong answer here,
    -- restoring the behavior of Agda 2.5.2.  TODO: fix record declaration checking.
    notSafeRecRecursive :: RecordData -> Bool
    notSafeRecRecursive = maybe True null . _recMutual
      -- @_recMutual@ should be something (@Just (_:_)@) to be safe
  
  -- * De Bruijn pattern stuff
  
  -- | How long is the path to the deepest atomic pattern?
  patternDepth :: forall a. Pattern' a -> Int
  patternDepth = getMaxNat . foldrPattern depth where
    depth :: Pattern' a -> MaxNat -> MaxNat
    depth ConP{} = succ      -- add 1 to the maximum of the depth of the subpatterns
    depth _      = id        -- atomic pattern (leaf) has depth 0
  
  -- | A dummy pattern used to mask a pattern that cannot be used
  --   for structural descent.
  
  unusedVar :: DeBruijnPattern
  unusedVar = litP (LitString "term.unused.pat.var")
  
  -- | Extract variables from 'DeBruijnPattern's that could witness a decrease
  --   via a SIZELT constraint.
  --
  --   These variables must be under an inductive constructor (with no record
  --   constructor in the way), or after a coinductive projection (with no
  --   inductive one in the way).
  
  class UsableSizeVars a where
    usableSizeVars :: a -> TerM VarSet
  
  instance UsableSizeVars DeBruijnPattern where
    usableSizeVars = foldrPattern $ \case
      VarP _ x   -> const $ ifM terGetUseSizeLt (return $ singleton $ dbPatVarIndex x) $
                     {-else-} return mempty
      ConP c _ _ -> conUseSizeLt $ conName c
      LitP{}     -> none
      DotP{}     -> none
      ProjP{}    -> none
      IApplyP{}  -> none
      DefP{} -> none
      where none _ = return mempty
  
  instance UsableSizeVars [DeBruijnPattern] where
    usableSizeVars ps =
      case ps of
        []               -> return mempty
        (ProjP _ q : ps) -> projUseSizeLt q $ usableSizeVars ps
        (p         : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
  
  instance UsableSizeVars (Masked DeBruijnPattern) where
    usableSizeVars (Masked m p) = (`foldrPattern` p) $ \case
      VarP _ x   -> const $ ifM terGetUseSizeLt (return $ singleton $ dbPatVarIndex x) $
                     {-else-} return mempty
      ConP c _ _ -> if m then none else conUseSizeLt $ conName c
      LitP{}     -> none
      DotP{}     -> none
      ProjP{}    -> none
      IApplyP{}  -> none
      DefP{}     -> none
      where none _ = return mempty
  
  instance UsableSizeVars MaskedDeBruijnPatterns where
    usableSizeVars ps =
      case ps of
        []                          -> return mempty
        (Masked _ (ProjP _ q) : ps) -> projUseSizeLt q $ usableSizeVars ps
        (p                    : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps
  
  -- * Masked patterns (which are not eligible for structural descent, only for size descent)
  --   See issue #1023.
  
  type MaskedDeBruijnPatterns = [Masked DeBruijnPattern]
  
  data Masked a = Masked
    { getMask   :: Bool  -- ^ True if thing not eligible for structural descent.
    , getMasked :: a     -- ^ Thing.
    } deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
  
  masked :: a -> Masked a
  masked = Masked True
  
  notMasked :: a -> Masked a
  notMasked = Masked False
  
  instance Decoration Masked where
    traverseF f (Masked m a) = Masked m <$> f a
  
  -- | Print masked things in double parentheses.
  instance PrettyTCM a => PrettyTCM (Masked a) where
    prettyTCM (Masked m a) = applyWhen m (parens . parens) $ prettyTCM a
  
  -- * Call pathes
  
  -- | Call paths.
  
  -- An old comment:
  --
  --   The call information is stored as free monoid
  --   over 'CallInfo'.  As long as we never look at it,
  --   only accumulate it, it does not matter whether we use
  --   'Set', (nub) list, or 'Tree'.
  --   Internally, due to lazyness, it is anyway a binary tree of
  --   'mappend' nodes and singleton leafs.
  --   Since we define no order on 'CallInfo' (expensive),
  --   we cannot use a 'Set' or nub list.
  --   Performance-wise, I could not see a difference between Set and list.
  --
  -- If the binary tree is balanced "incorrectly", then forcing it could
  -- be expensive, so a switch was made to difference lists.
  
  newtype CallPath = CallPath (DList CallInfo)
    deriving (Show, Semigroup, Monoid)
  
  -- | The calls making up the call path.
  
  callInfos :: CallPath -> [CallInfo]
  callInfos (CallPath cs) = DL.toList cs
  
  -- | Only show intermediate nodes.  (Drop last 'CallInfo').
  instance Pretty CallPath where
    pretty cis0 = if null cis then empty else
      P.hsep (map (\ ci -> arrow P.<+> P.pretty ci) cis) P.<+> arrow
      where
        cis   = init (callInfos cis0)
        arrow = "-->"
  
  -- * Size depth estimation
  
  -- | A very crude way of estimating the @SIZELT@ chains
  --   @i > j > k@ in context.  Returns 3 in this case.
  --   Overapproximates.
  class TerSetSizeDepth b where
    terSetSizeDepth :: b -> TerM a -> TerM a
  
  instance TerSetSizeDepth Telescope where
    terSetSizeDepth = terSetSizeDepth . telToList
  
  -- TODO: more precise analysis, constructing a tree
  -- of relations between size variables.
  instance TerSetSizeDepth ListTel where
    terSetSizeDepth doms cont = do
      n <- liftTCM $ sum <$> do
        forM doms $ \ dom -> do
          -- Andreas, 2022-03-12, TODO:
          -- use ifBlocked?  Shouldn't blocked types be treated like metas?
          a <- reduce $ snd $ unDom dom
          ifM (isJust <$> isSizeType a) (return 1) {- else -} $
            case unEl a of
              MetaV{} -> return 1
              _       -> return 0
      terLocal (set terSizeDepth n) cont
  