    {-# 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 :: [Char] -> TCM ()
    requireGuarded [Char]
    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
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Missing option --guarded " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    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
      [Char] -> Variable -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Variable -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.term.lock" Variable
    40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "Checking locked vars.."
      [Char] -> Variable -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Variable -> TCM Doc -> m ()
    reportSDoc [Char]
    "tc.term.lock" Variable
    50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Variable -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Variable -> m Doc -> m Doc
    nest Variable
    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
         [ [Char] -> TCM Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "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
         , [Char] -> TCM Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "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
         , [Char] -> TCM Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "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
         , [Char] -> TCM Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "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 Variable
    mi <- Term -> TCMT IO (Maybe Variable)
    getLockVar (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    lk)
      Maybe Variable -> TCM () -> (Variable -> TCM ()) -> TCM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Variable
    mi (() -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((Variable -> TCM ()) -> TCM ()) -> (Variable -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Variable
    i -> do

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

      let fv :: VarMap
    fv = IgnoreSorts -> (Term, Type) -> VarMap
    forall a c t.
    (IsVarSet a c, Singleton Variable 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 = [Variable] -> VarSet
    ISet.fromList [Variable
    iVariable -> Variable -> Variable
    forall a. Num a => a -> a -> a
    +Variable
    1 .. [Dom (Name, Type)] -> Variable
    forall a. Sized a => a -> Variable
    size [Dom (Name, Type)]
    cxt Variable -> Variable -> Variable
    forall a. Num a => a -> a -> a
    - Variable
    1]
      if VarSet
    termVars VarSet -> VarSet -> Bool
    `ISet.isSubsetOf` VarSet
    earlierVars then () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return () else do

      [Variable]
    checked <- ([Maybe Variable] -> [Variable])
    -> TCMT IO [Maybe Variable] -> TCMT IO [Variable]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Maybe Variable] -> [Variable]
    forall a. [Maybe a] -> [a]
    catMaybes (TCMT IO [Maybe Variable] -> TCMT IO [Variable])
    -> (((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
        -> TCMT IO [Maybe Variable])
    -> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
    -> TCMT IO [Variable]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Variable, Dom (Name, Type))]
    -> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
    -> TCMT IO [Maybe Variable]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Variable, Dom (Name, Type))]
    toCheck (((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
     -> TCMT IO [Variable])
    -> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
    -> TCMT IO [Variable]
    forall a b. (a -> b) -> a -> b
    $ \ (Variable
    j,Dom (Name, Type)
    dom) -> do
        TCMT IO Bool
    -> TCMT IO (Maybe Variable)
    -> TCMT IO (Maybe Variable)
    -> TCMT IO (Maybe Variable)
    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 Variable -> TCMT IO (Maybe Variable)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Variable -> TCMT IO (Maybe Variable))
    -> Maybe Variable -> TCMT IO (Maybe Variable)
    forall a b. (a -> b) -> a -> b
    $ Variable -> Maybe Variable
    forall a. a -> Maybe a
    Just Variable
    j)
            (Maybe Variable -> TCMT IO (Maybe Variable)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Variable -> TCMT IO (Maybe Variable))
    -> Maybe Variable -> TCMT IO (Maybe Variable)
    forall a b. (a -> b) -> a -> b
    $ Maybe Variable
    forall a. Maybe a
    Nothing)

      let allowedVars :: VarSet
    allowedVars = VarSet -> VarSet -> VarSet
    ISet.union VarSet
    earlierVars ([Variable] -> VarSet
    ISet.fromList [Variable]
    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 -> [Variable] -> TCM ()
    forall b. Term -> [Variable] -> TCM b
    notAllowedVarsError (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    lk) (VarSet -> [Variable]
    ISet.toList VarSet
    illegalVars)

    getLockVar :: Term -> TCMT IO (Maybe Int)
    getLockVar :: Term -> TCMT IO (Maybe Variable)
    getLockVar Term
    lk = do
      let
        fv :: VarMap
    fv = IgnoreSorts -> Term -> VarMap
    forall a c t.
    (IsVarSet a c, Singleton Variable 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

      [Variable]
    is <- (Variable -> TCMT IO Bool) -> [Variable] -> TCMT IO [Variable]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM Variable -> TCMT IO Bool
    forall {m :: * -> *}.
    (MonadFail m, MonadTCEnv m) =>
    Variable -> m Bool
    isLock ([Variable] -> TCMT IO [Variable])
    -> [Variable] -> TCMT IO [Variable]
    forall a b. (a -> b) -> a -> b
    $ VarSet -> [Variable]
    ISet.toList (VarSet -> [Variable]) -> VarSet -> [Variable]
    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 Variable
    mi | [Variable] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Prelude.null [Variable]
    is   = Maybe Variable
    forall a. Maybe a
    Nothing
             | Bool
    otherwise = Variable -> Maybe Variable
    forall a. a -> Maybe a
    Just (Variable -> Maybe Variable) -> Variable -> Maybe Variable
    forall a b. (a -> b) -> a -> b
    $ [Variable] -> Variable
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Variable]
    is

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

      where
       isLock :: Variable -> m Bool
    isLock Variable
    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
    <$> Variable -> m (Dom (Name, Type))
    forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m) =>
    Variable -> m (Dom (Name, Type))
    lookupBV Variable
    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 <- ([Char] -> TCMT IO (Maybe QName))
    -> [[Char]] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getName' [[Char]
    builtinInterval, [Char]
    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 :: forall b. Term -> [Variable] -> TCM b
    notAllowedVarsError Term
    lk [Variable]
    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 ((Variable -> Term) -> [Variable] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Variable -> Term
    var ([Variable] -> [Term]) -> [Variable] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Variable]
    is))

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