1 2-- | The monad for the termination checker. 3-- 4-- The termination monad @TerM@ is an extension of 5-- the type checking monad 'TCM' by an environment 6-- with information needed by the termination checker. 7 8module Agda.Termination.Monad where 9 10import Prelude hiding (null) 11 12import Control.Applicative hiding (empty) 13 14import qualified Control.Monad.Fail as Fail 15 16import Control.Monad.Except 17import Control.Monad.Reader 18 19import Data.Semigroup ( Semigroup(..) ) 20import qualified Data.Set as Set 21 22import Agda.Interaction.Options (optTerminationDepth) 23 24import Agda.Syntax.Common 25import Agda.Syntax.Internal 26import Agda.Syntax.Internal.Pattern 27import Agda.Syntax.Literal 28import Agda.Syntax.Position (noRange) 29 30import Agda.Termination.CutOff 31import Agda.Termination.Order (Order,le,unknown) 32import Agda.Termination.RecCheck (anyDefs) 33 34import Agda.TypeChecking.Monad 35import Agda.TypeChecking.Monad.Benchmark 36import Agda.TypeChecking.Pretty 37import Agda.TypeChecking.Records 38import Agda.TypeChecking.Reduce 39import Agda.TypeChecking.Substitute 40 41import Agda.Utils.Benchmark as B 42import Agda.Utils.Function 43import Agda.Utils.Functor 44import Agda.Utils.Lens 45import Agda.Utils.List ( hasElem ) 46import Agda.Utils.Maybe 47import Agda.Utils.Monad 48import Agda.Utils.Monoid 49import Agda.Utils.Null 50import Agda.Utils.Pretty (Pretty, prettyShow) 51import qualified Agda.Utils.Pretty as P 52import Agda.Utils.VarSet (VarSet) 53import qualified Agda.Utils.VarSet as VarSet 54 55import Agda.Utils.Impossible 56 57-- | The mutual block we are checking. 58-- 59-- The functions are numbered according to their order of appearance 60-- in this list. 61 62type MutualNames = [QName] 63 64-- | The target of the function we are checking. 65 66type Target = QName 67 68-- | The current guardedness level. 69 70type Guarded = Order 71 72-- | The termination environment. 73 74data TerEnv = TerEnv 75 76 -- First part: options, configuration. 77 78 { terUseDotPatterns :: Bool 79 -- ^ Are we mining dot patterns to find evindence of structal descent? 80 , terSizeSuc :: Maybe QName 81 -- ^ The name of size successor, if any. 82 , terSharp :: Maybe QName 83 -- ^ The name of the delay constructor (sharp), if any. 84 , terCutOff :: CutOff 85 -- ^ Depth at which to cut off the structural order. 86 87 -- Second part: accumulated info during descent into decls./term. 88 89 , terCurrent :: QName 90 -- ^ The name of the function we are currently checking. 91 , terMutual :: MutualNames 92 -- ^ The names of the functions in the mutual block we are checking. 93 -- This includes the internally generated functions 94 -- (with, extendedlambda, coinduction). 95 , terUserNames :: [QName] 96 -- ^ The list of name actually appearing in the file (abstract syntax). 97 -- Excludes the internally generated functions. 98 , terHaveInlinedWith :: Bool 99 -- ^ Does the actual clause result from with-inlining? 100 -- (If yes, it may be ill-typed.) 101 , terTarget :: Maybe Target 102 -- ^ Target type of the function we are currently termination checking. 103 -- Only the constructors of 'Target' are considered guarding. 104 , terDelayed :: Delayed 105 -- ^ Are we checking a delayed definition? 106 , terMaskArgs :: [Bool] 107 -- ^ Only consider the 'notMasked' 'False' arguments for establishing termination. 108 -- See issue #1023. 109 , terMaskResult :: Bool 110 -- ^ Only consider guardedness if 'False' (not masked). 111 , _terSizeDepth :: Int -- lazy by intention! 112 -- ^ How many @SIZELT@ relations do we have in the context 113 -- (= clause telescope). Used to approximate termination 114 -- for metas in call args. 115 , terPatterns :: MaskedDeBruijnPatterns 116 -- ^ The patterns of the clause we are checking. 117 , terPatternsRaise :: !Int 118 -- ^ Number of additional binders we have gone under 119 -- (and consequently need to raise the patterns to compare to terms). 120 -- Updated during call graph extraction, hence strict. 121 , terGuarded :: !Guarded 122 -- ^ The current guardedness status. Changes as we go deeper into the term. 123 -- Updated during call graph extraction, hence strict. 124 , terUseSizeLt :: Bool 125 -- ^ When extracting usable size variables during construction of the call 126 -- matrix, can we take the variable for use with SIZELT constraints from the context? 127 -- Yes, if we are under an inductive constructor. 128 -- No, if we are under a record constructor. 129 -- (See issue #1015). 130 , terUsableVars :: VarSet 131 -- ^ Pattern variables that can be compared to argument variables using SIZELT. 132 } 133 134-- | An empty termination environment. 135-- 136-- Values are set to a safe default meaning that with these 137-- initial values the termination checker will not miss 138-- termination errors it would have seen with better settings 139-- of these values. 140-- 141-- Values that do not have a safe default are set to 142-- @__IMPOSSIBLE__@. 143 144defaultTerEnv :: TerEnv 145defaultTerEnv = TerEnv 146 { terUseDotPatterns = False -- must be False initially! 147 , terSizeSuc = Nothing 148 , terSharp = Nothing 149 , terCutOff = defaultCutOff 150 , terUserNames = __IMPOSSIBLE__ -- needs to be set! 151 , terMutual = __IMPOSSIBLE__ -- needs to be set! 152 , terCurrent = __IMPOSSIBLE__ -- needs to be set! 153 , terHaveInlinedWith = False 154 , terTarget = Nothing 155 , terDelayed = NotDelayed 156 , terMaskArgs = repeat False -- use all arguments (mask none) 157 , terMaskResult = False -- use result (do not mask) 158 , _terSizeDepth = __IMPOSSIBLE__ -- needs to be set! 159 , terPatterns = __IMPOSSIBLE__ -- needs to be set! 160 , terPatternsRaise = 0 161 , terGuarded = le -- not initially guarded 162 , terUseSizeLt = False -- initially, not under data constructor 163 , terUsableVars = VarSet.empty 164 } 165 166-- | Termination monad service class. 167 168class (Functor m, Monad m) => MonadTer m where 169 terAsk :: m TerEnv 170 terLocal :: (TerEnv -> TerEnv) -> m a -> m a 171 172 terAsks :: (TerEnv -> a) -> m a 173 terAsks f = f <$> terAsk 174 175-- | Termination monad. 176 177newtype TerM a = TerM { terM :: ReaderT TerEnv TCM a } 178 deriving ( Functor 179 , Applicative 180 , Monad 181 , Fail.MonadFail 182 , MonadError TCErr 183 , MonadStatistics 184 , HasOptions 185 , HasBuiltins 186 , MonadDebug 187 , HasConstInfo 188 , MonadIO 189 , MonadTCEnv 190 , MonadTCState 191 , MonadTCM 192 , ReadTCState 193 , MonadReduce 194 , MonadAddContext 195 , PureTCM 196 ) 197 198-- This could be derived automatically, but the derived type family becomes `BenchPhase (ReaderT TerEnv TCM)` which 199-- is *fine* but triggers complaints that the "type family application is no smaller than the instance head, why not 200-- nuke everything with UndecidableInstances". 201instance MonadBench TerM where 202 type BenchPhase TerM = Phase 203 getBenchmark = TerM $ B.getBenchmark 204 putBenchmark = TerM . B.putBenchmark 205 modifyBenchmark = TerM . B.modifyBenchmark 206 finally (TerM m) (TerM f) = TerM $ (B.finally m f) 207 208instance MonadTer TerM where 209 terAsk = TerM $ ask 210 terLocal f = TerM . local f . terM 211 212-- | Generic run method for termination monad. 213runTer :: TerEnv -> TerM a -> TCM a 214runTer tenv (TerM m) = runReaderT m tenv 215 216-- | Run TerM computation in default environment (created from options). 217 218runTerDefault :: TerM a -> TCM a 219runTerDefault cont = do 220 221 -- Assemble then initial configuration of the termination environment. 222 223 cutoff <- optTerminationDepth <$> pragmaOptions 224 225 -- Get the name of size suc (if sized types are enabled) 226 suc <- sizeSucName 227 228 -- The name of sharp (if available). 229 sharp <- fmap nameOfSharp <$> coinductionKit 230 231 let tenv = defaultTerEnv 232 { terSizeSuc = suc 233 , terSharp = sharp 234 , terCutOff = cutoff 235 } 236 237 runTer tenv cont 238 239-- -- * Termination monad is a 'MonadTCM'. 240 241-- instance MonadError TCErr TerM where 242-- throwError = liftTCM . throwError 243-- catchError m handler = TerM $ ReaderT $ \ tenv -> do 244-- runTer tenv m `catchError` (\ err -> runTer tenv $ handler err) 245 246instance Semigroup m => Semigroup (TerM m) where 247 (<>) = liftA2 (<>) 248 249instance (Semigroup m, Monoid m) => Monoid (TerM m) where 250 mempty = pure mempty 251 mappend = (<>) 252 mconcat = mconcat <.> sequence 253 254-- * Modifiers and accessors for the termination environment in the monad. 255 256terGetUseDotPatterns :: TerM Bool 257terGetUseDotPatterns = terAsks terUseDotPatterns 258 259terSetUseDotPatterns :: Bool -> TerM a -> TerM a 260terSetUseDotPatterns b = terLocal $ \ e -> e { terUseDotPatterns = b } 261 262terGetSizeSuc :: TerM (Maybe QName) 263terGetSizeSuc = terAsks terSizeSuc 264 265terGetCurrent :: TerM QName 266terGetCurrent = terAsks terCurrent 267 268terSetCurrent :: QName -> TerM a -> TerM a 269terSetCurrent q = terLocal $ \ e -> e { terCurrent = q } 270 271terGetSharp :: TerM (Maybe QName) 272terGetSharp = terAsks terSharp 273 274terGetCutOff :: TerM CutOff 275terGetCutOff = terAsks terCutOff 276 277terGetMutual :: TerM MutualNames 278terGetMutual = terAsks terMutual 279 280terGetUserNames :: TerM [QName] 281terGetUserNames = terAsks terUserNames 282 283terGetTarget :: TerM (Maybe Target) 284terGetTarget = terAsks terTarget 285 286terSetTarget :: Maybe Target -> TerM a -> TerM a 287terSetTarget t = terLocal $ \ e -> e { terTarget = t } 288 289terGetHaveInlinedWith :: TerM Bool 290terGetHaveInlinedWith = terAsks terHaveInlinedWith 291 292terSetHaveInlinedWith :: TerM a -> TerM a 293terSetHaveInlinedWith = terLocal $ \ e -> e { terHaveInlinedWith = True } 294 295terGetDelayed :: TerM Delayed 296terGetDelayed = terAsks terDelayed 297 298terSetDelayed :: Delayed -> TerM a -> TerM a 299terSetDelayed b = terLocal $ \ e -> e { terDelayed = b } 300 301terGetMaskArgs :: TerM [Bool] 302terGetMaskArgs = terAsks terMaskArgs 303 304terSetMaskArgs :: [Bool] -> TerM a -> TerM a 305terSetMaskArgs b = terLocal $ \ e -> e { terMaskArgs = b } 306 307terGetMaskResult :: TerM Bool 308terGetMaskResult = terAsks terMaskResult 309 310terSetMaskResult :: Bool -> TerM a -> TerM a 311terSetMaskResult b = terLocal $ \ e -> e { terMaskResult = b } 312 313terGetPatterns :: TerM (MaskedDeBruijnPatterns) 314terGetPatterns = do 315 n <- terAsks terPatternsRaise 316 mps <- terAsks terPatterns 317 return $ if n == 0 then mps else map (fmap (raise n)) mps 318 319terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a 320terSetPatterns ps = terLocal $ \ e -> e { terPatterns = ps } 321 322terRaise :: TerM a -> TerM a 323terRaise = terLocal $ \ e -> e { terPatternsRaise = terPatternsRaise e + 1 } 324 325terGetGuarded :: TerM Guarded 326terGetGuarded = terAsks terGuarded 327 328terModifyGuarded :: (Order -> Order) -> TerM a -> TerM a 329terModifyGuarded f = terLocal $ \ e -> e { terGuarded = f $ terGuarded e } 330 331terSetGuarded :: Order -> TerM a -> TerM a 332terSetGuarded = terModifyGuarded . const 333 334terUnguarded :: TerM a -> TerM a 335terUnguarded = terSetGuarded unknown 336 337-- | Lens for '_terSizeDepth'. 338 339terSizeDepth :: Lens' Int TerEnv 340terSizeDepth f e = f (_terSizeDepth e) <&> \ i -> e { _terSizeDepth = i } 341 342-- | Lens for 'terUsableVars'. 343 344terGetUsableVars :: TerM VarSet 345terGetUsableVars = terAsks terUsableVars 346 347terModifyUsableVars :: (VarSet -> VarSet) -> TerM a -> TerM a 348terModifyUsableVars f = terLocal $ \ e -> e { terUsableVars = f $ terUsableVars e } 349 350terSetUsableVars :: VarSet -> TerM a -> TerM a 351terSetUsableVars = terModifyUsableVars . const 352 353-- | Lens for 'terUseSizeLt'. 354 355terGetUseSizeLt :: TerM Bool 356terGetUseSizeLt = terAsks terUseSizeLt 357 358terModifyUseSizeLt :: (Bool -> Bool) -> TerM a -> TerM a 359terModifyUseSizeLt f = terLocal $ \ e -> e { terUseSizeLt = f $ terUseSizeLt e } 360 361terSetUseSizeLt :: Bool -> TerM a -> TerM a 362terSetUseSizeLt = terModifyUseSizeLt . const 363 364-- | Compute usable vars from patterns and run subcomputation. 365withUsableVars :: UsableSizeVars a => a -> TerM b -> TerM b 366withUsableVars pats m = do 367 vars <- usableSizeVars pats 368 reportSLn "term.size" 70 $ "usableSizeVars = " ++ show vars 369 reportSDoc "term.size" 20 $ if null vars then "no usuable size vars" else 370 "the size variables amoung these variables are usable: " <+> 371 sep (map (prettyTCM . var) $ VarSet.toList vars) 372 terSetUsableVars vars $ m 373 374-- | Set 'terUseSizeLt' when going under constructor @c@. 375conUseSizeLt :: QName -> TerM a -> TerM a 376conUseSizeLt c m = do 377 ifM (liftTCM $ isEtaOrCoinductiveRecordConstructor c) -- Non-eta inductive records are the same as datatypes 378 (terSetUseSizeLt False m) 379 (terSetUseSizeLt True m) 380 381-- | Set 'terUseSizeLt' for arguments following projection @q@. 382-- We disregard j<i after a non-coinductive projection. 383-- However, the projection need not be recursive (Issue 1470). 384projUseSizeLt :: QName -> TerM a -> TerM a 385projUseSizeLt q m = do 386 co <- isCoinductiveProjection False q 387 reportSLn "term.size" 20 $ applyUnless co ("not " ++) $ 388 "using SIZELT vars after projection " ++ prettyShow q 389 terSetUseSizeLt co m 390 391-- | For termination checking purposes flat should not be considered a 392-- projection. That is, it flat doesn't preserve either structural order 393-- or guardedness like other projections do. 394-- Andreas, 2012-06-09: the same applies to projections of recursive records. 395isProjectionButNotCoinductive :: MonadTCM tcm => QName -> tcm Bool 396isProjectionButNotCoinductive qn = liftTCM $ do 397 b <- isProjectionButNotCoinductive' qn 398 reportSDoc "term.proj" 60 $ do 399 "identifier" <+> prettyTCM qn <+> do 400 text $ 401 if b then "is an inductive projection" 402 else "is either not a projection or coinductive" 403 return b 404 where 405 isProjectionButNotCoinductive' qn = do 406 flat <- fmap nameOfFlat <$> coinductionKit 407 if Just qn == flat 408 then return False 409 else do 410 mp <- isProjection qn 411 case mp of 412 Just Projection{ projProper = Just{}, projFromType = t } 413 -> isInductiveRecord (unArg t) 414 _ -> return False 415 416-- | Check whether a projection belongs to a coinductive record 417-- and is actually recursive. 418-- E.g. 419-- @ 420-- isCoinductiveProjection (Stream.head) = return False 421-- 422-- isCoinductiveProjection (Stream.tail) = return True 423-- @ 424isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool 425isCoinductiveProjection mustBeRecursive q = liftTCM $ do 426 reportSLn "term.guardedness" 40 $ "checking isCoinductiveProjection " ++ prettyShow q 427 flat <- fmap nameOfFlat <$> coinductionKit 428 -- yes for ♭ 429 if Just q == flat then return True else do 430 pdef <- getConstInfo q 431 case isProjection_ (theDef pdef) of 432 Just Projection{ projProper = Just{}, projFromType = Arg _ r, projIndex = n } -> 433 caseMaybeM (isRecord r) __IMPOSSIBLE__ $ \ rdef -> do 434 -- no for inductive or non-recursive record 435 if recInduction rdef /= Just CoInductive then return False else do 436 reportSLn "term.guardedness" 40 $ prettyShow q ++ " is coinductive; record type is " ++ prettyShow r 437 if not mustBeRecursive then return True else do 438 reportSLn "term.guardedness" 40 $ prettyShow q ++ " must be recursive" 439 if not (safeRecRecursive rdef) then return False else do 440 reportSLn "term.guardedness" 40 $ prettyShow q ++ " has been declared recursive, doing actual check now..." 441 -- TODO: the following test for recursiveness of a projection should be cached. 442 -- E.g., it could be stored in the @Projection@ component. 443 -- Now check if type of field mentions mutually recursive symbol. 444 -- Get the type of the field by dropping record parameters and record argument. 445 let TelV tel core = telView' (defType pdef) 446 (pars, tel') = splitAt n $ telToList tel 447 mut = fromMaybe __IMPOSSIBLE__ $ recMutual rdef 448 -- Check if any recursive symbols appear in the record type. 449 -- Q (2014-07-01): Should we normalize the type? 450 -- A (2017-01-13): Yes, since we also normalize during positivity check? 451 -- See issue #1899. 452 reportSDoc "term.guardedness" 40 $ inTopContext $ sep 453 [ "looking for recursive occurrences of" 454 , sep (map prettyTCM mut) 455 , "in" 456 , addContext pars $ prettyTCM (telFromList tel') 457 , "and" 458 , addContext tel $ prettyTCM core 459 ] 460 when (null mut) __IMPOSSIBLE__ 461 names <- anyDefs (mut `hasElem`) (map (snd . unDom) tel', core) 462 reportSDoc "term.guardedness" 40 $ 463 "found" <+> if null names then "none" else sep (map prettyTCM $ Set.toList names) 464 return $ not $ null names 465 _ -> do 466 reportSLn "term.guardedness" 40 $ prettyShow q ++ " is not a proper projection" 467 return False 468 where 469 -- Andreas, 2018-02-24, issue #2975, example: 470 -- @ 471 -- record R : Set where 472 -- coinductive 473 -- field force : R 474 475 -- r : R 476 -- force r = r 477 -- @ 478 -- The termination checker expects the positivity checker to have run on the 479 -- record declaration R to know whether R is recursive. 480 -- However, here, because the awkward processing of record declarations (see #434), 481 -- that has not happened. To avoid crashing (as in Agda 2.5.3), 482 -- we rather give the possibly wrong answer here, 483 -- restoring the behavior of Agda 2.5.2. TODO: fix record declaration checking. 484 safeRecRecursive :: Defn -> Bool 485 safeRecRecursive (Record { recMutual = Just qs }) = not $ null qs 486 safeRecRecursive _ = False 487 488-- * De Bruijn pattern stuff 489 490-- | How long is the path to the deepest atomic pattern? 491patternDepth :: forall a. Pattern' a -> Int 492patternDepth = getMaxNat . foldrPattern depth where 493 depth :: Pattern' a -> MaxNat -> MaxNat 494 depth ConP{} = succ -- add 1 to the maximum of the depth of the subpatterns 495 depth _ = id -- atomic pattern (leaf) has depth 0 496 497-- | A dummy pattern used to mask a pattern that cannot be used 498-- for structural descent. 499 500unusedVar :: DeBruijnPattern 501unusedVar = litP (LitString "term.unused.pat.var") 502 503-- | Extract variables from 'DeBruijnPattern's that could witness a decrease 504-- via a SIZELT constraint. 505-- 506-- These variables must be under an inductive constructor (with no record 507-- constructor in the way), or after a coinductive projection (with no 508-- inductive one in the way). 509 510class UsableSizeVars a where 511 usableSizeVars :: a -> TerM VarSet 512 513instance UsableSizeVars DeBruijnPattern where 514 usableSizeVars = foldrPattern $ \case 515 VarP _ x -> const $ ifM terGetUseSizeLt (return $ VarSet.singleton $ dbPatVarIndex x) $ 516 {-else-} return mempty 517 ConP c _ _ -> conUseSizeLt $ conName c 518 LitP{} -> none 519 DotP{} -> none 520 ProjP{} -> none 521 IApplyP{} -> none 522 DefP{} -> none 523 where none _ = return mempty 524 525instance UsableSizeVars [DeBruijnPattern] where 526 usableSizeVars ps = 527 case ps of 528 [] -> return mempty 529 (ProjP _ q : ps) -> projUseSizeLt q $ usableSizeVars ps 530 (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps 531 532instance UsableSizeVars (Masked DeBruijnPattern) where 533 usableSizeVars (Masked m p) = (`foldrPattern` p) $ \case 534 VarP _ x -> const $ ifM terGetUseSizeLt (return $ VarSet.singleton $ dbPatVarIndex x) $ 535 {-else-} return mempty 536 ConP c _ _ -> if m then none else conUseSizeLt $ conName c 537 LitP{} -> none 538 DotP{} -> none 539 ProjP{} -> none 540 IApplyP{} -> none 541 DefP{} -> none 542 where none _ = return mempty 543 544instance UsableSizeVars MaskedDeBruijnPatterns where 545 usableSizeVars ps = 546 case ps of 547 [] -> return mempty 548 (Masked _ (ProjP _ q) : ps) -> projUseSizeLt q $ usableSizeVars ps 549 (p : ps) -> mappend <$> usableSizeVars p <*> usableSizeVars ps 550 551-- * Masked patterns (which are not eligible for structural descent, only for size descent) 552-- See issue #1023. 553 554type MaskedDeBruijnPatterns = [Masked DeBruijnPattern] 555 556data Masked a = Masked 557 { getMask :: Bool -- ^ True if thing not eligible for structural descent. 558 , getMasked :: a -- ^ Thing. 559 } deriving (Eq, Ord, Show, Functor, Foldable, Traversable) 560 561masked :: a -> Masked a 562masked = Masked True 563 564notMasked :: a -> Masked a 565notMasked = Masked False 566 567instance Decoration Masked where 568 traverseF f (Masked m a) = Masked m <$> f a 569 570-- | Print masked things in double parentheses. 571instance PrettyTCM a => PrettyTCM (Masked a) where 572 prettyTCM (Masked m a) = applyWhen m (parens . parens) $ prettyTCM a 573 574-- * Call pathes 575 576-- | The call information is stored as free monoid 577-- over 'CallInfo'. As long as we never look at it, 578-- only accumulate it, it does not matter whether we use 579-- 'Set', (nub) list, or 'Tree'. 580-- Internally, due to lazyness, it is anyway a binary tree of 581-- 'mappend' nodes and singleton leafs. 582-- Since we define no order on 'CallInfo' (expensive), 583-- we cannot use a 'Set' or nub list. 584-- Performance-wise, I could not see a difference between Set and list. 585 586newtype CallPath = CallPath { callInfos :: [CallInfo] } 587 deriving (Show, Semigroup, Monoid) 588 589-- | Only show intermediate nodes. (Drop last 'CallInfo'). 590instance Pretty CallPath where 591 pretty (CallPath cis0) = if null cis then empty else 592 P.hsep (map (\ ci -> arrow P.<+> P.pretty ci) cis) P.<+> arrow 593 where 594 cis = init cis0 595 arrow = "-->" 596 597-- * Size depth estimation 598 599-- | A very crude way of estimating the @SIZELT@ chains 600-- @i > j > k@ in context. Returns 3 in this case. 601-- Overapproximates. 602 603-- TODO: more precise analysis, constructing a tree 604-- of relations between size variables. 605terSetSizeDepth :: Telescope -> TerM a -> TerM a 606terSetSizeDepth tel cont = do 607 n <- liftTCM $ sum <$> do 608 forM (telToList tel) $ \ dom -> do 609 a <- reduce $ snd $ unDom dom 610 ifM (isJust <$> isSizeType a) (return 1) {- else -} $ 611 case unEl a of 612 MetaV{} -> return 1 613 _ -> return 0 614 terLocal (set terSizeDepth n) cont 615