{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Lock
  ( isTimeless
  , checkLockedVars
  , checkEarlierThan
  , requireGuarded
  )
where

import Control.Monad            ( filterM, forM, forM_ )

import qualified Data.IntMap as IMap
import qualified Data.IntSet as ISet
import qualified Data.Set as Set


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

import Agda.Interaction.Options ( optGuarded )

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Free

import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.VarSet as VSet

import Agda.Utils.Impossible

requireGuarded :: String -> TCM ()
requireGuarded :: String -> TCM ()
requireGuarded String
s = do
  Bool
guarded <- PragmaOptions -> Bool
optGuarded (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
guarded (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Missing option --guarded " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s


checkLockedVars
  :: Term
     -- ^ term to check
  -> Type
     -- ^ its type
  -> Arg Term
     -- ^ the lock
  -> Type
     -- ^ type of the lock
  -> TCM ()
checkLockedVars :: Term -> Type -> Arg Term -> Type -> TCM ()
checkLockedVars Term
t Type
ty Arg Term
lk Type
lk_ty = Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars Term
t Type
ty Arg Term
lk Type
lk_ty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  String -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.term.lock" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking locked vars.."
  String -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.term.lock" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
     [ String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"t     = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
t
     , String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ty    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
     , String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"lk    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
lk
     , String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"lk_ty = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
lk_ty
     ]

  -- Strategy: compute allowed variables, check that @t@ doesn't use more.
  Maybe VerboseLevel
mi <- Term -> TCMT IO (Maybe VerboseLevel)
getLockVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lk)
  Maybe VerboseLevel -> TCM () -> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe VerboseLevel
mi (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i -> do

  [Dom (Name, Type)]
cxt <- TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
  let toCheck :: [(VerboseLevel, Dom (Name, Type))]
toCheck = [VerboseLevel]
-> [Dom (Name, Type)] -> [(VerboseLevel, Dom (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] ([Dom (Name, Type)] -> [(VerboseLevel, Dom (Name, Type))])
-> [Dom (Name, Type)] -> [(VerboseLevel, Dom (Name, Type))]
forall a b. (a -> b) -> a -> b
$ (VerboseLevel -> Dom (Name, Type) -> Dom (Name, Type))
-> [VerboseLevel] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel -> Dom (Name, Type) -> Dom (Name, Type)
forall a. Subst a => VerboseLevel -> a -> a
raise [VerboseLevel
1..] (VerboseLevel -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
i [Dom (Name, Type)]
cxt)

  let fv :: VarMap
fv = IgnoreSorts -> (Term, Type) -> VarMap
forall a c t.
(IsVarSet a c, Singleton VerboseLevel c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore IgnoreSorts
IgnoreInAnnotations (Term
t,Type
ty)
  let
    rigid :: VarSet
rigid = VarMap -> VarSet
rigidVars VarMap
fv
    -- flexible = IMap.keysSet $ flexibleVars fv
    termVars :: VarSet
termVars = VarMap -> VarSet
allVars VarMap
fv -- ISet.union rigid flexible
    earlierVars :: VarSet
earlierVars = [VerboseLevel] -> VarSet
ISet.fromList [VerboseLevel
iVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1 .. [Dom (Name, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (Name, Type)]
cxt VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1]
  if VarSet
termVars VarSet -> VarSet -> Bool
`ISet.isSubsetOf` VarSet
earlierVars then () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else do

  [VerboseLevel]
checked <- ([Maybe VerboseLevel] -> [VerboseLevel])
-> TCMT IO [Maybe VerboseLevel] -> TCMT IO [VerboseLevel]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe VerboseLevel] -> [VerboseLevel]
forall a. [Maybe a] -> [a]
catMaybes (TCMT IO [Maybe VerboseLevel] -> TCMT IO [VerboseLevel])
-> (((VerboseLevel, Dom (Name, Type))
     -> TCMT IO (Maybe VerboseLevel))
    -> TCMT IO [Maybe VerboseLevel])
-> ((VerboseLevel, Dom (Name, Type))
    -> TCMT IO (Maybe VerboseLevel))
-> TCMT IO [VerboseLevel]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(VerboseLevel, Dom (Name, Type))]
-> ((VerboseLevel, Dom (Name, Type))
    -> TCMT IO (Maybe VerboseLevel))
-> TCMT IO [Maybe VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(VerboseLevel, Dom (Name, Type))]
toCheck (((VerboseLevel, Dom (Name, Type)) -> TCMT IO (Maybe VerboseLevel))
 -> TCMT IO [VerboseLevel])
-> ((VerboseLevel, Dom (Name, Type))
    -> TCMT IO (Maybe VerboseLevel))
-> TCMT IO [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ \ (VerboseLevel
j,Dom (Name, Type)
dom) -> do
    TCMT IO Bool
-> TCMT IO (Maybe VerboseLevel)
-> TCMT IO (Maybe VerboseLevel)
-> TCMT IO (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Type -> TCMT IO Bool
isTimeless ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom (Name, Type) -> Type) -> Dom (Name, Type) -> Type
forall a b. (a -> b) -> a -> b
$ Dom (Name, Type)
dom))
        (Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
j)
        (Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ Maybe VerboseLevel
forall a. Maybe a
Nothing)

  let allowedVars :: VarSet
allowedVars = VarSet -> VarSet -> VarSet
ISet.union VarSet
earlierVars ([VerboseLevel] -> VarSet
ISet.fromList [VerboseLevel]
checked)

  if VarSet
termVars VarSet -> VarSet -> Bool
`ISet.isSubsetOf` VarSet
allowedVars then () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else do
  let
    illegalVars :: VarSet
illegalVars = VarSet
rigid VarSet -> VarSet -> VarSet
ISet.\\ VarSet
allowedVars
    -- flexVars = flexibleVars fv
    -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
  if VarSet -> Bool
ISet.null VarSet
illegalVars then  -- only flexible vars are infringing
    -- TODO: be more precise about which metas
    -- flexVars = flexibleVars fv
    -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
    Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
  else do
    Term -> [VerboseLevel] -> TCM ()
forall b. Term -> [VerboseLevel] -> TCM b
notAllowedVarsError (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lk) (VarSet -> [VerboseLevel]
ISet.toList VarSet
illegalVars)


getLockVar :: Term -> TCMT IO (Maybe Int)
getLockVar :: Term -> TCMT IO (Maybe VerboseLevel)
getLockVar Term
lk = do
  let
    fv :: VarMap
fv = IgnoreSorts -> Term -> VarMap
forall a c t.
(IsVarSet a c, Singleton VerboseLevel c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore IgnoreSorts
IgnoreInAnnotations Term
lk
    flex :: IntMap MetaSet
flex = VarMap -> IntMap MetaSet
flexibleVars VarMap
fv

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IntMap MetaSet -> Bool
forall a. IntMap a -> Bool
IMap.null IntMap MetaSet
flex) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let metas :: Set MetaId
metas = [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (MetaSet -> Set MetaId) -> [MetaSet] -> [Set MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((MetaId -> Set MetaId -> Set MetaId)
-> Set MetaId -> MetaSet -> Set MetaId
forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert Set MetaId
forall a. Set a
Set.empty) ([MetaSet] -> [Set MetaId]) -> [MetaSet] -> [Set MetaId]
forall a b. (a -> b) -> a -> b
$ IntMap MetaSet -> [MetaSet]
forall a. IntMap a -> [a]
IMap.elems IntMap MetaSet
flex
    Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> Blocker -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> Blocker
unblockOnAnyMeta (Set MetaId -> Blocker) -> Set MetaId -> Blocker
forall a b. (a -> b) -> a -> b
$ Set MetaId
metas

  [VerboseLevel]
is <- (VerboseLevel -> TCMT IO Bool)
-> [VerboseLevel] -> TCMT IO [VerboseLevel]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM VerboseLevel -> TCMT IO Bool
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Bool
isLock ([VerboseLevel] -> TCMT IO [VerboseLevel])
-> [VerboseLevel] -> TCMT IO [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VarSet -> [VerboseLevel]
ISet.toList (VarSet -> [VerboseLevel]) -> VarSet -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VarMap -> VarSet
rigidVars VarMap
fv

  -- Out of the lock variables that appear in @lk@ the one in the
  -- left-most position in the context is what will determine the
  -- available context for the head.
  let mi :: Maybe VerboseLevel
mi | [VerboseLevel] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [VerboseLevel]
is   = Maybe VerboseLevel
forall a. Maybe a
Nothing
         | Bool
otherwise = VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just (VerboseLevel -> Maybe VerboseLevel)
-> VerboseLevel -> Maybe VerboseLevel
forall a b. (a -> b) -> a -> b
$ [VerboseLevel] -> VerboseLevel
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [VerboseLevel]
is

  Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCMT IO (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ Maybe VerboseLevel
mi

  where
   isLock :: VerboseLevel -> m Bool
isLock VerboseLevel
i = do
     Lock
islock <- ArgInfo -> Lock
forall a. LensLock a => a -> Lock
getLock (ArgInfo -> Lock)
-> (Dom (Name, Type) -> ArgInfo) -> Dom (Name, Type) -> Lock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo (Dom (Name, Type) -> Lock) -> m (Dom (Name, Type)) -> m Lock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel -> m (Dom (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m (Dom (Name, Type))
lookupBV VerboseLevel
i
     Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Lock
islock Lock -> Lock -> Bool
forall a. Eq a => a -> a -> Bool
== Lock
IsLock

isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCMT IO Bool
isTimeless Type
t = do
  Type
t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  [Maybe QName]
timeless <- (String -> TCMT IO (Maybe QName))
-> [String] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' [String
builtinInterval, String
builtinIsOne]
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
q Elims
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
timeless -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Term
_                                -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

notAllowedVarsError :: Term -> [Int] -> TCM b
notAllowedVarsError :: Term -> [VerboseLevel] -> TCM b
notAllowedVarsError Term
lk [VerboseLevel]
is = do
        TypeError -> TCM b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM b) -> (Doc -> TypeError) -> Doc -> TCM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM b) -> TCM Doc -> TCM b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
         (TCM Doc
"The following vars are not allowed in a later value applied to"
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lk TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ((VerboseLevel -> Term) -> [VerboseLevel] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> Term
var ([VerboseLevel] -> [Term]) -> [VerboseLevel] -> [Term]
forall a b. (a -> b) -> a -> b
$ [VerboseLevel]
is))

checkEarlierThan :: Term -> VarSet -> TCM ()
checkEarlierThan :: Term -> VarSet -> TCM ()
checkEarlierThan Term
lk VarSet
fvs = do
  Maybe VerboseLevel
mv <- Term -> TCMT IO (Maybe VerboseLevel)
getLockVar Term
lk
  Maybe VerboseLevel -> TCM () -> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe VerboseLevel
mv (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i -> do
    let problems :: [VerboseLevel]
problems = (VerboseLevel -> Bool) -> [VerboseLevel] -> [VerboseLevel]
forall a. (a -> Bool) -> [a] -> [a]
filter (VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
i) ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VarSet -> [VerboseLevel]
VSet.toList VarSet
fvs
    [VerboseLevel] -> (VerboseLevel -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [VerboseLevel]
problems ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
j -> do
      Type
ty <- VerboseLevel -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
j
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> TCMT IO Bool
isTimeless Type
ty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Term -> [VerboseLevel] -> TCM ()
forall b. Term -> [VerboseLevel] -> TCM b
notAllowedVarsError Term
lk [VerboseLevel
j]