    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation  #-}

    {- | The occurs check for unification.  Does pruning on the fly.

      When hitting a meta variable:

      - Compute flex/rigid for its arguments.
      - Compare to allowed variables.
      - Mark arguments with rigid occurrences of disallowed variables for deletion.
      - Attempt to delete marked arguments.
      - We don't need to check for success, we can just continue occurs checking.
    -}

    module Agda.TypeChecking.MetaVars.Occurs where

    import Control.Monad.Except ( ExceptT, runExceptT, catchError, throwError )
    import Control.Monad.Reader ( ReaderT, runReaderT, ask, asks, local )

    import Data.Foldable (traverse_)
    import Data.Functor
    import Data.Monoid
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.IntMap as IntMap

    import qualified Agda.Benchmarking as Bench

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

    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Monad
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Lazy
    import Agda.TypeChecking.Free.Reduce
    import Agda.TypeChecking.ProjectionLike
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Records
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import Agda.Interaction.Options (optFirstOrder)

    import Agda.Utils.Either
    import Agda.Utils.Function
    import Agda.Utils.Lens
    import Agda.Utils.List (downFrom)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Utils.Size
    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * MetaOccursCheck: going into definitions to exclude cyclic solutions

    {- To address issue 585 (meta var occurrences in mutual defs)

    data B : Set where
      inn : A -> B

    out : B -> A
    out (inn a) = a

    postulate
      P : (y : A) (z : Unit -> B) → Set
      p : (x : Unit -> B) → P (out (x unit)) x

    mutual
      d : Unit -> B
      d unit = inn _           -- Y

      g : P (out (d unit)) d
      g = p _             -- X

    -- Agda solves  d unit = inn (out (d unit))
    --
    -- out (X unit) = out (d unit) = out (inn Y) = Y
    -- X = d

    When doing the occurs check on d, we need to look at the definition of
    d to discover that it mentions X.

    To this end, we extend the state by names of definitions that have to
    be checked when they occur.  At the beginning, this is initialized
    with the names in the current mutual block.  Each time we encounter a
    name in the list during occurs check, we delete it (if check is
    successful).  This way, we do not duplicate work.

    -}

    modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
    modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
    modifyOccursCheckDefs Set QName -> Set QName
    f = (Set QName -> f (Set QName)) -> TCState -> f TCState
    Lens' TCState (Set QName)
    stOccursCheckDefs Lens' TCState (Set QName) -> (Set QName -> Set QName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` Set QName -> Set QName
    f

    -- | Set the names of definitions to be looked at
    --   to the defs in the current mutual block.
    initOccursCheck :: MetaVariable -> TCM ()
    initOccursCheck :: MetaVariable -> TCM ()
    initOccursCheck MetaVariable
    mv = (Set QName -> Set QName) -> TCM ()
    modifyOccursCheckDefs ((Set QName -> Set QName) -> TCM ())
    -> (Set QName -> Set QName -> Set QName) -> Set QName -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set QName -> Set QName -> Set QName
    forall a b. a -> b -> a
    const (Set QName -> TCM ()) -> TCMT IO (Set QName) -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
      if (MetaInfo -> RunMetaOccursCheck
    miMetaOccursCheck (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv) RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == RunMetaOccursCheck
    DontRunMetaOccursCheck)
       then do
         [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
           [Char]
    "initOccursCheck: we do not look into definitions"
         Set QName -> TCMT IO (Set QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set QName
    forall a. Set a
    Set.empty
       else do
         [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
           [Char]
    "initOccursCheck: we look into the following definitions:"
         mb <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock
         case mb of
           Maybe MutualId
    Nothing -> do
             [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "(none)"
             Set QName -> TCMT IO (Set QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set QName
    forall a. Set a
    Set.empty
           Just MutualId
    b  -> do
             ds <- MutualBlock -> Set QName
    mutualNames (MutualBlock -> Set QName)
    -> TCMT IO MutualBlock -> TCMT IO (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualId -> TCMT IO MutualBlock
    forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock MutualId
    b
             reportSDoc "tc.meta.occurs" 20 $ sep $ map prettyTCM $ Set.toList ds
             return ds

    -- | Is a def in the list of stuff to be checked?
    defNeedsChecking :: QName -> TCM Bool
    defNeedsChecking :: QName -> TCM Bool
    defNeedsChecking QName
    d = QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    d (Set QName -> Bool) -> TCMT IO (Set QName) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (Set QName) -> TCMT IO (Set QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Set QName -> f (Set QName)) -> TCState -> f TCState
    Lens' TCState (Set QName)
    stOccursCheckDefs

    -- | Remove a def from the list of defs to be looked at.
    tallyDef :: QName -> TCM ()
    tallyDef :: QName -> TCM ()
    tallyDef QName
    d = (Set QName -> Set QName) -> TCM ()
    modifyOccursCheckDefs ((Set QName -> Set QName) -> TCM ())
    -> (Set QName -> Set QName) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete QName
    d

    ---------------------------------------------------------------------------
    -- * OccursM monad and its services

    -- | Extra environment for the occurs check.  (Complements 'FreeEnv'.)
    data OccursExtra = OccursExtra
      { OccursExtra -> UnfoldStrategy
    occUnfold  :: UnfoldStrategy
      , OccursExtra -> MetaId
    occMeta    :: MetaId          -- ^ The meta @m@ we want to solve.
      , OccursExtra -> VarMap
    occVars    :: VarMap          -- ^ The allowed variables @xs@ with their variance.
      , OccursExtra -> Term
    occRHS     :: Term            -- ^ The proposed solution @v@ for the meta (@m xs := v@).
      , OccursExtra -> Nat
    occCxtSize :: Nat             -- ^ The size of the typing context upon invocation.
      }

    type OccursCtx  = FreeEnv' () OccursExtra AllowedVar
    type OccursM    = ReaderT OccursCtx TCM

    -- ** Modality handling.

    -- | The passed modality is the one of the current context.
    type AllowedVar = Modality -> All

    instance IsVarSet () AllowedVar where
      withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar
    withVarOcc VarOcc' ()
    o AllowedVar
    f = AllowedVar
    f AllowedVar -> (Modality -> Modality) -> AllowedVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Modality -> Modality -> Modality
    composeModality (VarOcc' () -> Modality
    forall a. LensModality a => a -> Modality
    getModality VarOcc' ()
    o)

    -- | Check whether a free variable is allowed in the context as
    --   specified by the modality.
    variableCheck :: VarMap -> Maybe Variable -> AllowedVar
    variableCheck :: VarMap -> Maybe Nat -> AllowedVar
    variableCheck VarMap
    xs Maybe Nat
    mi Modality
    q = Bool -> All
    All (Bool -> All) -> Bool -> All
    forall a b. (a -> b) -> a -> b
    $
      -- Bound variables are always allowed to occur:
      Maybe Nat -> Bool -> (Nat -> Bool) -> Bool
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Nat
    mi Bool
    True ((Nat -> Bool) -> Bool) -> (Nat -> Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ \ Nat
    i ->
        -- Free variables not listed in @xs@ are forbidden:
        Maybe (VarOcc' MetaSet)
    -> Bool -> (VarOcc' MetaSet -> Bool) -> Bool
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Nat -> VarMap -> Maybe (VarOcc' MetaSet)
    forall a. Nat -> VarMap' a -> Maybe (VarOcc' a)
    lookupVarMap Nat
    i VarMap
    xs) Bool
    False ((VarOcc' MetaSet -> Bool) -> Bool)
    -> (VarOcc' MetaSet -> Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ \ VarOcc' MetaSet
    o ->
          -- For listed variables it holds:
          -- The ascribed modality @o@ must be submodality of the
          -- modality @q@ of the current context.
          -- E.g. irrelevant variables (ascribed, lhs) can only
          -- be used in irrelevant position (rhs).
          VarOcc' MetaSet -> Modality
    forall a. LensModality a => a -> Modality
    getModality VarOcc' MetaSet
    o Modality -> Modality -> Bool
    `moreUsableModality` Modality
    q

    -- | Occurs check fails if a defined name is not available
    --   since it was declared in irrelevant or erased context.
    definitionCheck :: QName -> OccursM ()
    definitionCheck :: QName -> OccursM ()
    definitionCheck QName
    d = do
      cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      let irr = OccursCtx -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant OccursCtx
    cxt
          er  = OccursCtx -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 OccursCtx
    cxt
          m   = OccursExtra -> MetaId
    occMeta (OccursExtra -> MetaId) -> OccursExtra -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra OccursCtx
    cxt
      -- Anything goes if we are both irrelevant and erased.
      -- Otherwise, have to check the modality of the defined name.
      unless (irr && er) $ getConstInfo' d >>= \case
       Left SigError
    _ -> do
        -- Andreas, 2021-07-29.
        -- The definition is not in scope.
        -- This shouldn't happen, but does so in issue #5492.
        -- Let's bail out...
        Blocker -> Nat -> [Char] -> OccursM ()
    forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    alwaysUnblock Nat
    35 ([Char] -> OccursM ()) -> [Char] -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $
          [[Char]] -> [Char]
    unwords [[Char]
    "occursCheck: definition", QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    d, [Char]
    "not in scope" ]
       Right Definition
    def -> do
        let dmod :: Modality
    dmod = Definition -> Modality
    forall a. LensModality a => a -> Modality
    getModality Definition
    def
        Bool -> OccursM () -> OccursM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Bool
    irr Bool -> Bool -> Bool
    || Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    usableRelevance Modality
    dmod) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    35 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ TCMT IO Doc
    "occursCheck: definition"
            , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
            , TCMT IO Doc
    "has relevance"
            , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Relevance -> [Char]) -> Relevance -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Relevance -> [Char]
    forall a. Show a => a -> [Char]
    show (Relevance -> TCMT IO Doc) -> Relevance -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    dmod
            ]
          Blocker -> TypeError -> OccursM ()
    forall a. Blocker -> TypeError -> OccursM a
    abort Blocker
    neverUnblock (TypeError -> OccursM ()) -> TypeError -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Term -> TypeError
    MetaIrrelevantSolution MetaId
    m (Term -> TypeError) -> Term -> TypeError
    forall a b. (a -> b) -> a -> b
    $ OccursExtra -> Term
    occRHS (OccursExtra -> Term) -> OccursExtra -> Term
    forall a b. (a -> b) -> a -> b
    $ OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra OccursCtx
    cxt
        Bool -> OccursM () -> OccursM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Bool
    er Bool -> Bool -> Bool
    || Modality -> Bool
    forall a. LensQuantity a => a -> Bool
    usableQuantity Modality
    dmod) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    35 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ TCMT IO Doc
    "occursCheck: definition"
            , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
            , TCMT IO Doc
    "has quantity"
            , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Quantity -> [Char]) -> Quantity -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> [Char]
    forall a. Show a => a -> [Char]
    show (Quantity -> TCMT IO Doc) -> Quantity -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    dmod
            ]
          Blocker -> TypeError -> OccursM ()
    forall a. Blocker -> TypeError -> OccursM a
    abort Blocker
    neverUnblock (TypeError -> OccursM ()) -> TypeError -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Term -> TypeError
    MetaErasedSolution MetaId
    m (Term -> TypeError) -> Term -> TypeError
    forall a b. (a -> b) -> a -> b
    $ OccursExtra -> Term
    occRHS (OccursExtra -> Term) -> OccursExtra -> Term
    forall a b. (a -> b) -> a -> b
    $ OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra OccursCtx
    cxt

    metaCheck :: MetaId -> OccursM MetaId
    metaCheck :: MetaId -> OccursM MetaId
    metaCheck MetaId
    m = do
      cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      let rel = OccursCtx -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance OccursCtx
    cxt
          qnt = OccursCtx -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity OccursCtx
    cxt
          m0  = OccursExtra -> MetaId
    occMeta (OccursExtra -> MetaId) -> OccursExtra -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra OccursCtx
    cxt

      -- Check for loop
      --   don't fail hard on this, since we might still be on the top-level
      --   after some killing (Issue 442)
      --
      -- Andreas, 2013-02-18  Issue 795 demonstrates that a recursive
      -- occurrence of a meta could be solved by the identity.
      --   ? (Q A) = Q (? A)
      -- So, do not throw an error.
      -- I guess the error was there from times when occurrence check
      -- was done after the "lhs=linear variables" check, but now
      -- occurrence check comes first.
      -- WAS:
      -- when (m == m') $ if ctx == Top then patternViolation else
      --   abort ctx $ MetaOccursInItself m'
      -- Andreas, 2024-09-28: removed error MetaOccursInItself from code base.
      when (m == m0) $ patternViolation' neverUnblock 50 $ "occursCheck failed: Found " ++ prettyShow m

      mv <- lookupLocalMeta m
      let mmod = MetaVariable -> Modality
    forall a. LensModality a => a -> Modality
    getModality MetaVariable
    mv
          mmod' = Relevance -> Modality -> Modality
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    rel (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $ Quantity -> Modality -> Modality
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    qnt (Modality -> Modality) -> Modality -> Modality
    forall a b. (a -> b) -> a -> b
    $ Modality
    mmod
      if (mmod `moreUsableModality` mmod') then return m else do
        reportSDoc "tc.meta.occurs" 35 $ hsep
          [ "occursCheck: meta variable"
          , prettyTCM m
          , "has relevance"
          , text . show $ getRelevance mmod
          , "and quantity"
          , text . show $ getQuantity mmod
          ]
        allowAssign <- asksTC envAssignMetas
        -- Jesper, 2020-11-10: if we encounter a metavariable that is
        -- unusable because of its modality (e.g. irrelevant or erased) we
        -- try to *promote* the meta to the required modality, by creating
        -- a new meta with that modality and solving the old one with
        -- it. Don't do this if the meta occurs in a flexible or unguarded
        -- position:
        -- - If it is in a flexible position, it could disappear when
        --   another meta is solved, so promotion is maybe not necessary.
        -- - If it is in a top-level position, we can instead solve the
        --   equation by instantiating the other way around, so promotion
        --   is not necessary.

        -- Actually, this is not the case anymore, no new meta is created and
        -- instead the metavar itself gets modified with the new modality.
        let fail TCMT IO Doc
    reason = do
              [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    20 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Meta occurs check found bad relevance"
              [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    20 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "aborting because" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    reason
              Blocker -> OccursM ()
    forall a. Blocker -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> OccursM ()) -> Blocker -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
        when (mvFrozen mv == Frozen)             $ fail "meta is frozen"
        unless (isOpenMeta $ mvInstantiation mv) $ fail "meta is already solved"
        unlessM (asksTC envAssignMetas)          $ fail "assigning metas is not allowed here"
        -- Jesper, 2023-09-03, issue #6759: When --lossy-unification is enabled,
        -- we already lose the guarantee that we only throw an error when a
        -- problem is really unsolvable in favor of taking the "obvious" solution.
        -- In this case the "obvious" solution is to promote the meta even if
        -- it is in a flexible position, so that is what we do.
        whenM (pure (isFlexible cxt) `and2M` (not . optFirstOrder <$> pragmaOptions))
                                                 $ fail "occurrence is flexible"
        when (isUnguarded cxt)                   $ fail "occurrence is unguarded"

        reportSDoc "tc.meta.occurs" 20 $ "Promoting meta" <+> prettyTCM m <+> "to modality" <+> prettyTCM mmod'
        -- The meta gets updated here
        updateMetaVar m $ \ MetaVariable
    mv -> MetaVariable
    mv { mvInfo = setModality mmod' $ mvInfo mv }
        etaExpandListeners m
        wakeupConstraints m
        return m

    -- | Construct a test whether a de Bruijn index is allowed
    --   or needs to be pruned.
    allowedVars :: OccursM (Nat -> Bool)
    allowedVars :: OccursM (Nat -> Bool)
    allowedVars = do
      -- @n@ is the number of binders we have stepped under.
      n  <- (Nat -> Nat -> Nat)
    -> ReaderT OccursCtx (TCMT IO) Nat
    -> ReaderT OccursCtx (TCMT IO) Nat
    -> ReaderT OccursCtx (TCMT IO) Nat
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (-) ReaderT OccursCtx (TCMT IO) Nat
    forall (m :: * -> *). MonadTCEnv m => m Nat
    getContextSize ((OccursCtx -> Nat) -> ReaderT OccursCtx (TCMT IO) Nat
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OccursExtra -> Nat
    occCxtSize (OccursExtra -> Nat)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra))
      xs <- asks (theVarMap . occVars . feExtra)
      -- Bound variables are allowed, and those mentioned in occVars.
      return $ \ Nat
    i -> Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n Bool -> Bool -> Bool
    || (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) Nat -> TheVarMap' MetaSet -> Bool
    forall a. Nat -> IntMap a -> Bool
    `IntMap.member` TheVarMap' MetaSet
    xs

    -- ** Unfolding during occurs check.

    -- | Unfold definitions during occurs check?
    --   This effectively runs the occurs check on the normal form.
    data UnfoldStrategy = YesUnfold | NoUnfold
      deriving (UnfoldStrategy -> UnfoldStrategy -> Bool
    (UnfoldStrategy -> UnfoldStrategy -> Bool)
    -> (UnfoldStrategy -> UnfoldStrategy -> Bool) -> Eq UnfoldStrategy
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: UnfoldStrategy -> UnfoldStrategy -> Bool
    == :: UnfoldStrategy -> UnfoldStrategy -> Bool
    $c/= :: UnfoldStrategy -> UnfoldStrategy -> Bool
    /= :: UnfoldStrategy -> UnfoldStrategy -> Bool
    Eq, Nat -> UnfoldStrategy -> [Char] -> [Char]
    [UnfoldStrategy] -> [Char] -> [Char]
    UnfoldStrategy -> [Char]
    (Nat -> UnfoldStrategy -> [Char] -> [Char])
    -> (UnfoldStrategy -> [Char])
    -> ([UnfoldStrategy] -> [Char] -> [Char])
    -> Show UnfoldStrategy
    forall a.
    (Nat -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Nat -> UnfoldStrategy -> [Char] -> [Char]
    showsPrec :: Nat -> UnfoldStrategy -> [Char] -> [Char]
    $cshow :: UnfoldStrategy -> [Char]
    show :: UnfoldStrategy -> [Char]
    $cshowList :: [UnfoldStrategy] -> [Char] -> [Char]
    showList :: [UnfoldStrategy] -> [Char] -> [Char]
    Show)

    defArgs :: OccursM a -> OccursM a
    defArgs :: forall a. OccursM a -> OccursM a
    defArgs OccursM a
    m = (OccursCtx -> UnfoldStrategy)
    -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OccursExtra -> UnfoldStrategy
    occUnfold (OccursExtra -> UnfoldStrategy)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    -> (UnfoldStrategy -> OccursM a) -> OccursM a
    forall a b.
    ReaderT OccursCtx (TCMT IO) a
    -> (a -> ReaderT OccursCtx (TCMT IO) b)
    -> ReaderT OccursCtx (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      UnfoldStrategy
    NoUnfold  -> OccursM a -> OccursM a
    forall a. OccursM a -> OccursM a
    flexibly OccursM a
    m
      UnfoldStrategy
    YesUnfold -> OccursM a -> OccursM a
    forall a. OccursM a -> OccursM a
    weakly OccursM a
    m

    -- | For a path constructor `c : ... -> Path D a b`, we have that e.g. `c es i0` reduces to `a`.
    --   So we have to consider its arguments as flexible when we do not actually unfold.
    conArgs :: Elims -> OccursM a -> OccursM a
    conArgs :: forall a. Elims -> OccursM a -> OccursM a
    conArgs Elims
    es OccursM a
    m = (OccursCtx -> UnfoldStrategy)
    -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OccursExtra -> UnfoldStrategy
    occUnfold (OccursExtra -> UnfoldStrategy)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    -> (UnfoldStrategy -> OccursM a) -> OccursM a
    forall a b.
    ReaderT OccursCtx (TCMT IO) a
    -> (a -> ReaderT OccursCtx (TCMT IO) b)
    -> ReaderT OccursCtx (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      UnfoldStrategy
    YesUnfold -> OccursM a
    m
      UnfoldStrategy
    NoUnfold | [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [ () | IApply{} <- Elims
    es ]
                -> OccursM a
    m
      UnfoldStrategy
    NoUnfold  -> OccursM a -> OccursM a
    forall a. OccursM a -> OccursM a
    flexibly OccursM a
    m

    unfoldB :: (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
    unfoldB :: forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
    unfoldB t
    v = do
      unfold <- (OccursCtx -> UnfoldStrategy)
    -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((OccursCtx -> UnfoldStrategy)
     -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy)
    -> (OccursCtx -> UnfoldStrategy)
    -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    forall a b. (a -> b) -> a -> b
    $ OccursExtra -> UnfoldStrategy
    occUnfold (OccursExtra -> UnfoldStrategy)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra
      rel    <- asks feModality
      case unfold of
        UnfoldStrategy
    YesUnfold | Bool -> Bool
    not (Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Modality
    rel) -> t -> ReaderT OccursCtx (TCMT IO) (Blocked t)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB t
    v
        UnfoldStrategy
    _                                  -> t -> Blocked t
    forall a t. a -> Blocked' t a
    notBlocked (t -> Blocked t)
    -> ReaderT OccursCtx (TCMT IO) t
    -> ReaderT OccursCtx (TCMT IO) (Blocked t)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> ReaderT OccursCtx (TCMT IO) t
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate t
    v

    unfold :: (Instantiate t, Reduce t) => t -> OccursM t
    unfold :: forall t. (Instantiate t, Reduce t) => t -> OccursM t
    unfold t
    v = (OccursCtx -> UnfoldStrategy)
    -> ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OccursExtra -> UnfoldStrategy
    occUnfold (OccursExtra -> UnfoldStrategy)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> UnfoldStrategy
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra) ReaderT OccursCtx (TCMT IO) UnfoldStrategy
    -> (UnfoldStrategy -> ReaderT OccursCtx (TCMT IO) t)
    -> ReaderT OccursCtx (TCMT IO) t
    forall a b.
    ReaderT OccursCtx (TCMT IO) a
    -> (a -> ReaderT OccursCtx (TCMT IO) b)
    -> ReaderT OccursCtx (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      UnfoldStrategy
    NoUnfold  -> t -> ReaderT OccursCtx (TCMT IO) t
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate t
    v
      UnfoldStrategy
    YesUnfold -> t -> ReaderT OccursCtx (TCMT IO) t
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce t
    v

    -- ** Managing rigidiy during occurs check.

    -- | Leave the strongly rigid position.
    weakly :: OccursM a -> OccursM a
    weakly :: forall a. OccursM a -> OccursM a
    weakly = (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall a.
    (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((OccursCtx -> OccursCtx)
     -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ Lens' OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
    forall o i. Lens' o i -> LensMap o i
    over (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' OccursCtx (FlexRig' ())
    lensFlexRig LensMap OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
    forall a b. (a -> b) -> a -> b
    $ FlexRig' () -> FlexRig' () -> FlexRig' ()
    forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
    composeFlexRig FlexRig' ()
    forall a. FlexRig' a
    WeaklyRigid

    strongly :: OccursM a -> OccursM a
    strongly :: forall a. OccursM a -> OccursM a
    strongly = (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall a.
    (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((OccursCtx -> OccursCtx)
     -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ Lens' OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
    forall o i. Lens' o i -> LensMap o i
    over (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' OccursCtx (FlexRig' ())
    lensFlexRig LensMap OccursCtx (FlexRig' ()) -> LensMap OccursCtx (FlexRig' ())
    forall a b. (a -> b) -> a -> b
    $ \case
      FlexRig' ()
    WeaklyRigid -> FlexRig' ()
    forall a. FlexRig' a
    StronglyRigid
      FlexRig' ()
    Unguarded   -> FlexRig' ()
    forall a. FlexRig' a
    StronglyRigid
      FlexRig' ()
    ctx -> FlexRig' ()
    ctx

    flexibly :: OccursM a -> OccursM a
    flexibly :: forall a. OccursM a -> OccursM a
    flexibly = (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall a.
    (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((OccursCtx -> OccursCtx)
     -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> (OccursCtx -> OccursCtx)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ Lens' OccursCtx (FlexRig' ()) -> LensSet OccursCtx (FlexRig' ())
    forall o i. Lens' o i -> LensSet o i
    set (FlexRig' () -> f (FlexRig' ())) -> OccursCtx -> f OccursCtx
    forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
    Lens' OccursCtx (FlexRig' ())
    lensFlexRig LensSet OccursCtx (FlexRig' ()) -> LensSet OccursCtx (FlexRig' ())
    forall a b. (a -> b) -> a -> b
    $ () -> FlexRig' ()
    forall a. a -> FlexRig' a
    Flexible ()

    -- ** Error throwing during occurs check.

    patternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a
    patternViolation' :: forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    unblock Nat
    n [Char]
    err = TCM a -> m a
    forall a. TCM a -> m a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM a -> m a) -> TCM a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    n [Char]
    err
      Blocker -> TCM a
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    unblock

    abort :: Blocker -> TypeError -> OccursM a
    abort :: forall a. Blocker -> TypeError -> OccursM a
    abort Blocker
    unblock TypeError
    err = do
      ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      lift $ do
        if | isIrrelevant ctx                    -> soft
           | StronglyRigid <- ctx ^. lensFlexRig -> hard
           | otherwise -> soft
      where
      hard :: TCM a
    hard = TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    err -- here, throw an uncatchable error (unsolvable constraint)
      soft :: TCM a
    soft = Blocker -> Nat -> [Char] -> TCM a
    forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    unblock Nat
    70 (TypeError -> [Char]
    forall a. Show a => a -> [Char]
    show TypeError
    err) -- throws a PatternErr, which leads to delayed constraint

    ---------------------------------------------------------------------------
    -- * Implementation of the occurs check.

    -- | Extended occurs check.
    class Occurs t where
      occurs :: t -> OccursM t
      metaOccurs :: MetaId -> t -> TCM ()  -- raise exception if meta occurs in t

      default metaOccurs :: (Foldable f, Occurs a, f a ~ t) => MetaId -> t -> TCM ()
      metaOccurs = (a -> TCM ()) -> t -> TCM ()
    (a -> TCM ()) -> f a -> TCM ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    (a -> f b) -> t a -> f ()
    traverse_ ((a -> TCM ()) -> t -> TCM ())
    -> (MetaId -> a -> TCM ()) -> MetaId -> t -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs

    occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ :: forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ t
    t = t -> OccursM t
    forall t. Occurs t => t -> OccursM t
    occurs t
    t

    metaOccurs2 :: (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 :: forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 MetaId
    m a
    x b
    y = MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m a
    x TCM () -> TCM () -> TCM ()
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MetaId -> b -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m b
    y

    metaOccurs3 :: (Occurs a, Occurs b, Occurs c) => MetaId -> a -> b -> c -> TCM ()
    metaOccurs3 :: forall a b c.
    (Occurs a, Occurs b, Occurs c) =>
    MetaId -> a -> b -> c -> TCM ()
    metaOccurs3 MetaId
    m a
    x b
    y c
    z = MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m a
    x TCM () -> TCM () -> TCM ()
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MetaId -> b -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m b
    y TCM () -> TCM () -> TCM ()
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MetaId -> c -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m c
    z

    -- | When assigning @m xs := v@, check that @m@ does not occur in @v@
    --   and that the free variables of @v@ are contained in @xs@.
    occursCheck
      :: MetaId -> VarMap -> Term -> TCM Term
    occursCheck :: MetaId -> VarMap -> Term -> TCM Term
    occursCheck MetaId
    m VarMap
    xs Term
    v = Account (BenchPhase (TCMT IO)) -> TCM Term -> TCM Term
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [ BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.OccursCheck ] (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ do
      mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      n  <- getContextSize
      reportSDoc "tc.meta.occurs" 65 $ "occursCheck" <+> pretty m <+> text (show xs)
      let initEnv UnfoldStrategy
    unf = FreeEnv
            { feExtra :: OccursExtra
    feExtra = OccursExtra
              { occUnfold :: UnfoldStrategy
    occUnfold  = UnfoldStrategy
    unf
              , occMeta :: MetaId
    occMeta    = MetaId
    m
              , occVars :: VarMap
    occVars    = VarMap
    xs
              , occRHS :: Term
    occRHS     = Term
    v
              , occCxtSize :: Nat
    occCxtSize = Nat
    n
              }
            , feFlexRig :: FlexRig' ()
    feFlexRig   = FlexRig' ()
    forall a. FlexRig' a
    StronglyRigid -- ? Unguarded
            , feModality :: Modality
    feModality  = MetaVariable -> Modality
    forall a. LensModality a => a -> Modality
    getModality MetaVariable
    mv
            , feSingleton :: Maybe Nat -> AllowedVar
    feSingleton = VarMap -> Maybe Nat -> AllowedVar
    variableCheck VarMap
    xs
            }
      initOccursCheck mv
      do
        -- First try without normalising the term
        (occurs v `runReaderT` initEnv NoUnfold) `catchError` \TCErr
    err -> do
          -- If first run is inconclusive, try again with normalization
          -- (unless metavariable is irrelevant, in which case the
          -- constraint will anyway be dropped)
          case TCErr
    err of
            PatternErr{} | Bool -> Bool
    not (Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant (Modality -> Bool) -> Modality -> Bool
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Modality
    forall a. LensModality a => a -> Modality
    getModality MetaVariable
    mv) -> do
              MetaVariable -> TCM ()
    initOccursCheck MetaVariable
    mv
              Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    v OccursM Term -> OccursCtx -> TCM Term
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` UnfoldStrategy -> OccursCtx
    initEnv UnfoldStrategy
    YesUnfold
            TCErr
    _ -> TCErr -> TCM Term
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

    instance Occurs Term where
      occurs :: Term -> OccursM Term
    occurs Term
    v = do
        vb  <- Term -> OccursM (Blocked Term)
    forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
    unfoldB Term
    v
        let block = Blocked Term -> Blocker
    forall t a. Blocked' t a -> Blocker
    getBlocker Blocked Term
    vb
            -- On a failure, we should retry when any meta that is blocking
            -- the term is solved.
            flexIfBlocked = if
              -- In the metavariable case we should not yet become flexible
              -- because otherwise pruning won't fire.
              | MetaV{} <- Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    vb -> Blocker -> OccursM Term -> OccursM Term
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker Blocker
    block
              | Blocker
    block Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Blocker
    neverUnblock -> OccursM Term -> OccursM Term
    forall a. OccursM a -> OccursM a
    flexibly (OccursM Term -> OccursM Term)
    -> (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> OccursM Term -> OccursM Term
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker Blocker
    block
              -- Re #3594, do not fail hard when Underapplied:
              -- the occurrence could be computed away after eta expansion.
              | NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
    blockingStatus = NotBlocked' Term
    Underapplied} <- Blocked Term
    vb -> OccursM Term -> OccursM Term
    forall a. OccursM a -> OccursM a
    flexibly
              | Bool
    otherwise -> OccursM Term -> OccursM Term
    forall a. a -> a
    id
        v <- reduceProjectionLike $ ignoreBlocking vb
        flexIfBlocked $ do
            ctx <- ask
            let m = OccursExtra -> MetaId
    occMeta (OccursExtra -> MetaId)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> MetaId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra (OccursCtx -> MetaId) -> OccursCtx -> MetaId
    forall a b. (a -> b) -> a -> b
    $ OccursCtx
    ctx
            reportSDoc "tc.meta.occurs" 45 $
              text ("occursCheck " ++ prettyShow m ++ " (" ++ show (feFlexRig ctx) ++ ") of ") <+> prettyTCM v
            reportSDoc "tc.meta.occurs" 70 $
              nest 2 $ pretty v
            case v of
              Var Nat
    i Elims
    es   -> do
                allowed <- All -> Bool
    getAll (All -> Bool) -> (AllowedVar -> All) -> AllowedVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AllowedVar -> AllowedVar
    forall a b. (a -> b) -> a -> b
    $ Modality
    unitModality) (AllowedVar -> Bool)
    -> ReaderT OccursCtx (TCMT IO) AllowedVar
    -> ReaderT OccursCtx (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat -> ReaderT OccursCtx (TCMT IO) AllowedVar
    forall (m :: * -> *) a c b.
    (Monad m, IsVarSet a c) =>
    Nat -> FreeT a b m c
    variable Nat
    i
                if allowed then Var i <$> weakly (occurs es) else do
                  -- if the offending variable is of singleton type,
                  -- eta-expand it away
                  reportSDoc "tc.meta.occurs" 35 $ "offending variable: " <+> prettyTCM (var i)
                  t <-  typeOfBV i
                  reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "of type " <+> prettyTCM t
                  isST <- typeLevelReductions $ isSingletonType t
                  reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "(after singleton test)"
                  case isST of
                    -- not a singleton type
                    Maybe Term
    Nothing ->
                      -- #4480: Only hard fail if the variable is not in scope. Wrong modality/relevance
                      -- could potentially be salvaged by eta expansion.
                      ReaderT OccursCtx (TCMT IO) Bool
    -> OccursM Term -> OccursM Term -> OccursM Term
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (((Nat -> Bool) -> Nat -> Bool
    forall a b. (a -> b) -> a -> b
    $ Nat
    i) ((Nat -> Bool) -> Bool)
    -> OccursM (Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> OccursM (Nat -> Bool)
    allowedVars) -- vv TODO: neverUnblock is not correct! What could trigger this eta expansion though?
                          (Blocker -> Nat -> [Char] -> OccursM Term
    forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    neverUnblock Nat
    70 ([Char] -> OccursM Term) -> [Char] -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Disallowed var " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show Nat
    i [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " due to modality/relevance")
                          (OccursM Term -> OccursM Term
    forall a. OccursM a -> OccursM a
    strongly (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Blocker -> TypeError -> OccursM Term
    forall a. Blocker -> TypeError -> OccursM a
    abort Blocker
    neverUnblock (TypeError -> OccursM Term) -> TypeError -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Term -> Nat -> TypeError
    MetaCannotDependOn MetaId
    m (OccursExtra -> Term
    occRHS (OccursExtra -> Term) -> OccursExtra -> Term
    forall a b. (a -> b) -> a -> b
    $ OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra OccursCtx
    ctx) Nat
    i)
                    -- is a singleton type with unique inhabitant sv
                    (Just Term
    sv) -> Term -> OccursM Term
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> OccursM Term) -> Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Term
    sv Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es
              Lam ArgInfo
    h Abs Term
    f     -> do
                ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h (Abs Term -> Term)
    -> ReaderT OccursCtx (TCMT IO) (Abs Term) -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
    forall t. Occurs t => t -> OccursM t
    occurs Abs Term
    f
              Level Level
    l     -> Level -> Term
    Level (Level -> Term)
    -> ReaderT OccursCtx (TCMT IO) Level -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> ReaderT OccursCtx (TCMT IO) Level
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Level
    l
              Lit Literal
    l       -> Term -> OccursM Term
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
              Dummy{}     -> Term -> OccursM Term
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
              DontCare Term
    v  -> Term -> Term
    dontCare (Term -> Term) -> OccursM Term -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                OccursM Term -> OccursM Term
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Relevance -> OccursM Term -> OccursM Term
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensRelevance r, LensRelevance o) =>
    o -> m z -> m z
    underRelevance Relevance
    irrelevant (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    v
              Def QName
    d Elims
    es    -> do
                QName -> OccursM ()
    definitionCheck QName
    d
                QName -> Elims -> Term
    Def QName
    d (Elims -> Term)
    -> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Elims -> ReaderT OccursCtx (TCMT IO) Elims
    forall {b}. Occurs b => QName -> b -> ReaderT OccursCtx (TCMT IO) b
    occDef QName
    d Elims
    es
              Con ConHead
    c ConInfo
    ci Elims
    vs -> do
                QName -> OccursM ()
    definitionCheck (ConHead -> QName
    conName ConHead
    c)
                ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term)
    -> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims
    -> ReaderT OccursCtx (TCMT IO) Elims
    -> ReaderT OccursCtx (TCMT IO) Elims
    forall a. Elims -> OccursM a -> OccursM a
    conArgs Elims
    vs (Elims -> ReaderT OccursCtx (TCMT IO) Elims
    forall t. Occurs t => t -> OccursM t
    occurs Elims
    vs)  -- if strongly rigid, remain so, except with unreduced IApply arguments.
              Pi Dom Type
    a Abs Type
    b      -> Dom Type -> Abs Type -> Term
    Pi (Dom Type -> Abs Type -> Term)
    -> ReaderT OccursCtx (TCMT IO) (Dom Type)
    -> ReaderT OccursCtx (TCMT IO) (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> ReaderT OccursCtx (TCMT IO) (Dom Type)
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Dom Type
    a ReaderT OccursCtx (TCMT IO) (Abs Type -> Term)
    -> ReaderT OccursCtx (TCMT IO) (Abs Type) -> OccursM Term
    forall a b.
    ReaderT OccursCtx (TCMT IO) (a -> b)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
    forall t. Occurs t => t -> OccursM t
    occurs Abs Type
    b
              Sort Sort
    s      -> Sort -> Term
    Sort (Sort -> Term) -> ReaderT OccursCtx (TCMT IO) Sort -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Relevance
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensRelevance r, LensRelevance o) =>
    o -> m z -> m z
    underRelevance Relevance
    shapeIrrelevant (ReaderT OccursCtx (TCMT IO) Sort
     -> ReaderT OccursCtx (TCMT IO) Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s
              MetaV MetaId
    m' Elims
    es -> do
                m' <- MetaId -> OccursM MetaId
    metaCheck MetaId
    m'
                -- The arguments of a meta are in a flexible position
                (MetaV m' <$> do flexibly $ occurs es) `catchError` \ TCErr
    err -> do
                    ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
                    reportSDoc "tc.meta.kill" 25 $ vcat
                      [ text $ "error during flexible occurs check, we are " ++ show (ctx ^. lensFlexRig)
                      , text $ show err
                      ]
                    case err of
                      -- On pattern violations try to remove offending
                      -- flexible occurrences (if not already in a flexible context)
                      PatternErr{} | Bool -> Bool
    not (OccursCtx -> Bool
    forall o a. LensFlexRig o a => o -> Bool
    isFlexible OccursCtx
    ctx) -> do
                        [Char] -> Nat -> [Char] -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.kill" Nat
    20 ([Char] -> OccursM ()) -> [Char] -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $
                          [Char]
    "oops, pattern violation for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m'
                        -- Andreas, 2014-03-02, see issue 1070:
                        -- Do not prune when meta is projected!
                        Maybe [Arg Term]
    -> OccursM Term -> ([Arg Term] -> OccursM Term) -> OccursM Term
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es) (TCErr -> OccursM Term
    forall a. TCErr -> ReaderT OccursCtx (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err) (([Arg Term] -> OccursM Term) -> OccursM Term)
    -> ([Arg Term] -> OccursM Term) -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ \ [Arg Term]
    vs -> do
                          killResult <- TCM PruneResult -> ReaderT OccursCtx (TCMT IO) PruneResult
    forall (m :: * -> *) a. Monad m => m a -> ReaderT OccursCtx m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM PruneResult -> ReaderT OccursCtx (TCMT IO) PruneResult)
    -> ((Nat -> Bool) -> TCM PruneResult)
    -> (Nat -> Bool)
    -> ReaderT OccursCtx (TCMT IO) PruneResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> [Arg Term] -> (Nat -> Bool) -> TCM PruneResult
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    MetaId -> [Arg Term] -> (Nat -> Bool) -> m PruneResult
    prune MetaId
    m' [Arg Term]
    vs ((Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) PruneResult)
    -> OccursM (Nat -> Bool) -> ReaderT OccursCtx (TCMT IO) PruneResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< OccursM (Nat -> Bool)
    allowedVars
                          if (killResult == PrunedEverything) then do
                            -- after successful pruning, restart occurs check
                            reportSDoc "tc.meta.prune" 40 $ "Pruned everything"
                            v' <- instantiate (MetaV m' es)
                            occurs v'
                          else throwError err
                      TCErr
    _ -> TCErr -> OccursM Term
    forall a. TCErr -> ReaderT OccursCtx (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
              where
                -- a data or record type constructor propagates strong occurrences
                -- since e.g. x = List x is unsolvable
                occDef :: QName -> b -> ReaderT OccursCtx (TCMT IO) b
    occDef QName
    d b
    vs = do
                  m   <- (OccursCtx -> MetaId) -> OccursM MetaId
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (OccursExtra -> MetaId
    occMeta (OccursExtra -> MetaId)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> MetaId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra)
                  lift $ metaOccurs m d
                  ifM (liftTCM $ isJust <$> isDataOrRecordType d)
                    {-then-} (occurs vs)
                    {-else-} (defArgs $ occurs vs)

      metaOccurs :: MetaId -> Term -> TCM ()
    metaOccurs MetaId
    m Term
    v = do
        v <- Term -> TCM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v
        case v of
          Var Nat
    i Elims
    vs   -> MetaId -> Elims -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Elims
    vs
          Lam ArgInfo
    h Abs Term
    f    -> MetaId -> Abs Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Abs Term
    f
          Level Level
    l    -> MetaId -> Level -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Level
    l
          Lit Literal
    l      -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Dummy{}    -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          DontCare Term
    v -> MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Term
    v
          Def QName
    d Elims
    vs   -> MetaId -> QName -> Elims -> TCM ()
    forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 MetaId
    m QName
    d Elims
    vs
          Con ConHead
    c ConInfo
    _ Elims
    vs -> MetaId -> Elims -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Elims
    vs
          Pi Dom Type
    a Abs Type
    b     -> MetaId -> Dom Type -> Abs Type -> TCM ()
    forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 MetaId
    m Dom Type
    a Abs Type
    b
          Sort Sort
    s     -> MetaId -> Sort -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Sort
    s              -- vv m is already an unblocker
          MetaV MetaId
    m' Elims
    vs | MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m'   -> Blocker -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    neverUnblock Nat
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Found occurrence of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m
                      | Bool
    otherwise -> Blocker -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker (MetaId -> Blocker
    unblockOnMeta MetaId
    m') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Elims
    vs

    instance Occurs QName where
      occurs :: QName -> OccursM QName
    occurs QName
    d = OccursM QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      metaOccurs :: MetaId -> QName -> TCM ()
    metaOccurs MetaId
    m QName
    d = TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (QName -> TCM Bool
    defNeedsChecking QName
    d) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        QName -> TCM ()
    tallyDef QName
    d
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking for occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    d
        MetaId -> QName -> TCM ()
    metaOccursQName MetaId
    m QName
    d

    metaOccursQName :: MetaId -> QName -> TCM ()
    metaOccursQName :: MetaId -> QName -> TCM ()
    metaOccursQName MetaId
    m QName
    x = MetaId -> Defn -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Defn -> TCM ()) -> (Definition -> Defn) -> Definition -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
      TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      -- Andreas, 2019-05-03, issue #3742:
      -- ignoreAbstractMode necessary, as abstract
      -- constructors are also called up.

    instance Occurs Defn where
      occurs :: Defn -> OccursM Defn
    occurs Defn
    def = OccursM Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      metaOccurs :: MetaId -> Defn -> TCM ()
    metaOccurs MetaId
    m Axiom{}                      = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m DataOrRecSig{}               = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls } = (Clause -> TCM ()) -> [Clause] -> TCM ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    (a -> f b) -> t a -> f ()
    traverse_ (MetaId -> Clause -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m) [Clause]
    cls
      -- since a datatype is isomorphic to the sum of its constructor types
      -- we check the constructor types
      metaOccurs MetaId
    m Datatype{ dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs }    = (QName -> TCM ()) -> [QName] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (MetaId -> QName -> TCM ()
    metaOccursQName MetaId
    m) [QName]
    cs
      metaOccurs MetaId
    m Record{ recConHead :: Defn -> ConHead
    recConHead = ConHead
    c }     = MetaId -> QName -> TCM ()
    metaOccursQName MetaId
    m (QName -> TCM ()) -> QName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
      metaOccurs MetaId
    m Constructor{}                = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m Primitive{}                  = () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m PrimitiveSort{}              = TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      metaOccurs MetaId
    m AbstractDefn{}               = TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      metaOccurs MetaId
    m GeneralizableVar{}           = TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Occurs Clause where
      occurs :: Clause -> OccursM Clause
    occurs Clause
    cl = OccursM Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      metaOccurs :: MetaId -> Clause -> TCM ()
    metaOccurs MetaId
    m Clause
    cl = Maybe Term -> (Term -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Clause -> Maybe Term
    clauseBody Clause
    cl) ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m

    instance Occurs Level where
      occurs :: Level -> ReaderT OccursCtx (TCMT IO) Level
    occurs (Max Integer
    n [PlusLevel' Term]
    as) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level)
    -> ReaderT OccursCtx (TCMT IO) [PlusLevel' Term]
    -> ReaderT OccursCtx (TCMT IO) Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term))
    -> [PlusLevel' Term]
    -> ReaderT OccursCtx (TCMT IO) [PlusLevel' Term]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ [PlusLevel' Term]
    as

      metaOccurs :: MetaId -> Level -> TCM ()
    metaOccurs MetaId
    m (Max Integer
    _ [PlusLevel' Term]
    as) =
        Blocker -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker ([PlusLevel' Term] -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn [PlusLevel' Term]
    as) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (PlusLevel' Term -> TCM ()) -> [PlusLevel' Term] -> TCM ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    (a -> f b) -> t a -> f ()
    traverse_ (MetaId -> PlusLevel' Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m) [PlusLevel' Term]
    as
        -- TODO: Should only be blocking metas in as. But any meta that can
        --       let the Max make progress needs to be included. For instance,
        --       _1 ⊔ _2 = _1 should unblock on _2, even though _1 is the meta
        --       failing occurs check.

    instance Occurs PlusLevel where
      occurs :: PlusLevel' Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
    occurs (Plus Integer
    n Term
    l) = do
        Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term)
    -> OccursM Term -> ReaderT OccursCtx (TCMT IO) (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    l

      metaOccurs :: MetaId -> PlusLevel' Term -> TCM ()
    metaOccurs MetaId
    m (Plus Integer
    n Term
    l) = MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Term
    l

    instance Occurs Type where
      occurs :: Type -> ReaderT OccursCtx (TCMT IO) Type
    occurs (El Sort
    s Term
    v) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Term -> Type)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s ReaderT OccursCtx (TCMT IO) (Term -> Type)
    -> OccursM Term -> ReaderT OccursCtx (TCMT IO) Type
    forall a b.
    ReaderT OccursCtx (TCMT IO) (a -> b)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    v

      metaOccurs :: MetaId -> Type -> TCM ()
    metaOccurs MetaId
    m (El Sort
    s Term
    v) = MetaId -> Sort -> Term -> TCM ()
    forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 MetaId
    m Sort
    s Term
    v

    instance Occurs Sort where
      occurs :: Sort -> ReaderT OccursCtx (TCMT IO) Sort
    occurs Sort
    s = do
        Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Instantiate t, Reduce t) => t -> OccursM t
    unfold Sort
    s ReaderT OccursCtx (TCMT IO) Sort
    -> (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b.
    ReaderT OccursCtx (TCMT IO) a
    -> (a -> ReaderT OccursCtx (TCMT IO) b)
    -> ReaderT OccursCtx (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> do
            s1' <- ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. OccursM a -> OccursM a
    flexibly (ReaderT OccursCtx (TCMT IO) Sort
     -> ReaderT OccursCtx (TCMT IO) Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s1
            a'  <- (a $>) <$> do flexibly $ occurs (unDom a)
            s2' <- mapAbstraction (El s1' <$> a') (flexibly . underBinder . occurs_) s2
            return $ PiSort a' s1' s2'
          FunSort Sort
    s1 Sort
    s2 -> Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort (Sort -> Sort -> Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) (Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. OccursM a -> OccursM a
    flexibly (Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s1) ReaderT OccursCtx (TCMT IO) (Sort -> Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b.
    ReaderT OccursCtx (TCMT IO) (a -> b)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. OccursM a -> OccursM a
    flexibly (Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s2)
          Univ Univ
    u Level
    a   -> Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level -> Sort)
    -> ReaderT OccursCtx (TCMT IO) Level
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> ReaderT OccursCtx (TCMT IO) Level
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Level
    a
          s :: Sort
    s@Inf{}    -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          s :: Sort
    s@Sort
    SizeUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          s :: Sort
    s@Sort
    LockUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          s :: Sort
    s@Sort
    LevelUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          s :: Sort
    s@Sort
    IntervalUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          UnivSort Sort
    s -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. OccursM a -> OccursM a
    flexibly (ReaderT OccursCtx (TCMT IO) Sort
     -> ReaderT OccursCtx (TCMT IO) Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Sort
    s
          MetaS MetaId
    x Elims
    es -> do
            MetaV x es <- Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs (MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es)
            return $ MetaS x es
          DefS QName
    x Elims
    es -> do
            Def x es <- Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs (QName -> Elims -> Term
    Def QName
    x Elims
    es)
            return $ DefS x es
          DummyS{}   -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s

      metaOccurs :: MetaId -> Sort -> TCM ()
    metaOccurs MetaId
    m Sort
    s = do
        s <- Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Sort
    s
        case s of
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> do
            MetaId -> Dom' Term Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Dom' Term Term
    a
            MetaId -> Sort -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Sort
    s1
            MetaId -> Sort -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Abs Sort -> Sort
    forall a. Subst a => Abs a -> a
    absBody Abs Sort
    s2)
          FunSort Sort
    s1 Sort
    s2 -> MetaId -> Sort -> Sort -> TCM ()
    forall a b. (Occurs a, Occurs b) => MetaId -> a -> b -> TCM ()
    metaOccurs2 MetaId
    m Sort
    s1 Sort
    s2
          Univ Univ
    _ Level
    a   -> MetaId -> Level -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Level
    a
          Inf Univ
    _ Integer
    _    -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Sort
    SizeUniv   -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Sort
    LockUniv   -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Sort
    LevelUniv  -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Sort
    IntervalUniv -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          UnivSort Sort
    s -> MetaId -> Sort -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Sort
    s
          MetaS MetaId
    x Elims
    es -> MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Term -> TCM ()) -> Term -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es
          DefS QName
    d Elims
    es  -> MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Term -> TCM ()) -> Term -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d Elims
    es
          DummyS{}   -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance Occurs Elims where
      occurs :: Elims -> ReaderT OccursCtx (TCMT IO) Elims
    occurs []     = Elims -> ReaderT OccursCtx (TCMT IO) Elims
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      occurs (Elim' Term
    e:Elims
    es) = do
        [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs.elim" Nat
    45 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "occurs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elim' Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
    prettyTCM Elim' Term
    e
        [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs.elim" Nat
    70 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "occurs" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elim' Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Elim' Term
    e
        e' <- case Elim' Term
    e of
          (Proj ProjOrigin
    o QName
    f)     -> do
            QName -> OccursM ()
    definitionCheck QName
    f
            Elim' Term -> ReaderT OccursCtx (TCMT IO) (Elim' Term)
    forall a. a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elim' Term
    e
          (Apply Arg Term
    u)      -> do
            u' <- Arg Term -> OccursM (Arg Term)
    forall t. Occurs t => t -> OccursM t
    occurs Arg Term
    u
            return (Apply u')
          (IApply Term
    x Term
    y Term
    u) -> do
            x' <- Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    x
            y' <- occurs y
            u' <- occurs u
            return (IApply x' y' u')
        (e':) <$> occurs es

      metaOccurs :: MetaId -> Elims -> TCM ()
    metaOccurs MetaId
    m Elims
    es = Elims -> (Elim' Term -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ Elims
    es ((Elim' Term -> TCM ()) -> TCM ())
    -> (Elim' Term -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \case
        Proj{} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Apply Arg Term
    a -> MetaId -> Arg Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Arg Term
    a
        IApply Term
    x Term
    y Term
    a -> MetaId -> Term -> Term -> Term -> TCM ()
    forall a b c.
    (Occurs a, Occurs b, Occurs c) =>
    MetaId -> a -> b -> c -> TCM ()
    metaOccurs3 MetaId
    m Term
    x Term
    y Term
    a

    instance Occurs (Abs Term) where
      occurs :: Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
    occurs (NoAbs [Char]
    s Term
    x) = [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    s (Term -> Abs Term)
    -> OccursM Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    x
      occurs Abs Term
    x = (Term -> OccursM Term)
    -> Abs Term -> ReaderT OccursCtx (TCMT IO) (Abs Term)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction_ (\Term
    body -> OccursM Term -> OccursM Term
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    m z -> m z
    underBinder (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs Term
    body) Abs Term
    x

      metaOccurs :: MetaId -> Abs Term -> TCM ()
    metaOccurs MetaId
    m (Abs   [Char]
    _ Term
    x) = MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Term
    x
      metaOccurs MetaId
    m (NoAbs [Char]
    _ Term
    x) = MetaId -> Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Term
    x

    instance Occurs (Abs Type) where
      occurs :: Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
    occurs (NoAbs [Char]
    s Type
    x) = [Char] -> Type -> Abs Type
    forall a. [Char] -> a -> Abs a
    NoAbs [Char]
    s (Type -> Abs Type)
    -> ReaderT OccursCtx (TCMT IO) Type
    -> ReaderT OccursCtx (TCMT IO) (Abs Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> ReaderT OccursCtx (TCMT IO) Type
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Type
    x
      occurs Abs Type
    x = (Type -> ReaderT OccursCtx (TCMT IO) Type)
    -> Abs Type -> ReaderT OccursCtx (TCMT IO) (Abs Type)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction_ (\Type
    body -> ReaderT OccursCtx (TCMT IO) Type
    -> ReaderT OccursCtx (TCMT IO) Type
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    m z -> m z
    underBinder (ReaderT OccursCtx (TCMT IO) Type
     -> ReaderT OccursCtx (TCMT IO) Type)
    -> ReaderT OccursCtx (TCMT IO) Type
    -> ReaderT OccursCtx (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ Type -> ReaderT OccursCtx (TCMT IO) Type
    forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
    occurs_ Type
    body) Abs Type
    x

      metaOccurs :: MetaId -> Abs Type -> TCM ()
    metaOccurs MetaId
    m (Abs   [Char]
    _ Type
    x) = MetaId -> Type -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Type
    x
      metaOccurs MetaId
    m (NoAbs [Char]
    _ Type
    x) = MetaId -> Type -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Type
    x

    instance Occurs a => Occurs (Arg a) where
      occurs :: Arg a -> OccursM (Arg a)
    occurs (Arg ArgInfo
    info a
    v) = ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (a -> Arg a) -> ReaderT OccursCtx (TCMT IO) a -> OccursM (Arg a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        Bool
    -> (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    info) ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $
          ArgInfo
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall r (m :: * -> *) o z.
    (MonadReader r m, LensModality r, LensModality o) =>
    o -> m z -> m z
    underModality ArgInfo
    info (ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a)
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall a b. (a -> b) -> a -> b
    $ a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    v
      metaOccurs :: MetaId -> Arg a -> TCM ()
    metaOccurs MetaId
    m = MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (a -> TCM ()) -> (Arg a -> a) -> Arg a -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg a -> a
    forall e. Arg e -> e
    unArg

    instance Occurs a => Occurs (Dom a) where
      occurs :: Occurs a => Dom a -> OccursM (Dom a)
      occurs :: Occurs a => Dom a -> OccursM (Dom a)
    occurs (Dom ArgInfo
    info Maybe NamedName
    n Bool
    f Maybe Term
    t a
    x) =
        ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
    forall t e.
    ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
    Dom ArgInfo
    info Maybe NamedName
    n Bool
    f Maybe Term
    t (a -> Dom a) -> ReaderT OccursCtx (TCMT IO) a -> OccursM (Dom a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgInfo
    -> ReaderT OccursCtx (TCMT IO) a -> ReaderT OccursCtx (TCMT IO) a
    forall r (m :: * -> *) o a.
    (MonadReader r m, LensQuantity r, LensQuantity o) =>
    o -> m a -> m a
    underQuantity ArgInfo
    info (a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    x)

    ---------------------------------------------------------------------------
    -- * Pruning: getting rid of flexible occurrences.

    -- | @prune m' vs xs@ attempts to remove all arguments from @vs@ whose
    --   free variables are not contained in @xs@.
    --   If successful, @m'@ is solved by the new, pruned meta variable and we
    --   return @True@ else @False@.
    --
    --   Issue 1147:
    --   If any of the meta args @vs@ is matchable, e.g., is a constructor term,
    --   we cannot prune, because the offending variables could be removed by
    --   reduction for a suitable instantiation of the meta variable.
    prune
      :: (PureTCM m, MonadMetaSolver m)
      => MetaId         -- ^ Meta to prune.
      -> Args           -- ^ Arguments to meta variable.
      -> (Nat -> Bool)  -- ^ Test for allowed variable (de Bruijn index).
      -> m PruneResult
    prune :: forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    MetaId -> [Arg Term] -> (Nat -> Bool) -> m PruneResult
    prune MetaId
    m' [Arg Term]
    vs Nat -> Bool
    xs = do
      m (Either () [Bool])
    -> (() -> m PruneResult)
    -> ([Bool] -> m PruneResult)
    -> m PruneResult
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (ExceptT () m [Bool] -> m (Either () [Bool])
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT () m [Bool] -> m (Either () [Bool]))
    -> ExceptT () m [Bool] -> m (Either () [Bool])
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> ExceptT () m Bool)
    -> [Arg Term] -> ExceptT () m [Bool]
    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 (((Nat -> Bool) -> Term -> ExceptT () m Bool
    forall (m :: * -> *).
    PureTCM m =>
    (Nat -> Bool) -> Term -> ExceptT () m Bool
    hasBadRigid Nat -> Bool
    xs) (Term -> ExceptT () m Bool)
    -> (Arg Term -> Term) -> Arg Term -> ExceptT () m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) [Arg Term]
    vs)
        (m PruneResult -> () -> m PruneResult
    forall a b. a -> b -> a
    const (m PruneResult -> () -> m PruneResult)
    -> m PruneResult -> () -> m PruneResult
    forall a b. (a -> b) -> a -> b
    $ PruneResult -> m PruneResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PruneResult
    PrunedNothing) (([Bool] -> m PruneResult) -> m PruneResult)
    -> ([Bool] -> m PruneResult) -> m PruneResult
    forall a b. (a -> b) -> a -> b
    $ \ [Bool]
    kills -> do
        [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.kill" Nat
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "attempting kills"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "m'    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty MetaId
    m'
            -- , "xs    =" <+> prettyList (map (prettyTCM . var) xs)  -- no longer printable
            , TCMT IO Doc
    "vs    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM [Arg Term]
    vs)
            , TCMT IO Doc
    "kills =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Bool] -> [Char]
    forall a. Show a => a -> [Char]
    show [Bool]
    kills)
            ]
          ]
        [Bool] -> MetaId -> m PruneResult
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [Bool] -> MetaId -> m PruneResult
    killArgs [Bool]
    kills MetaId
    m'

    -- | @hasBadRigid xs v = Just True@ iff one of the rigid variables in @v@ is not in @xs@.
    --   Actually we can only prune if a bad variable is in the head. See issue 458.
    --   Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).
    --
    --   @hasBadRigid xs v = Nothing@ means that
    --   we cannot prune at all as one of the meta args is matchable.
    --   (See issue 1147.)
    hasBadRigid
      :: PureTCM m
      => (Nat -> Bool)      -- ^ Test for allowed variable (de Bruijn index).
      -> Term               -- ^ Argument of meta variable.
      -> ExceptT () m Bool  -- ^ Exception if argument is matchable.
    hasBadRigid :: forall (m :: * -> *).
    PureTCM m =>
    (Nat -> Bool) -> Term -> ExceptT () m Bool
    hasBadRigid Nat -> Bool
    xs Term
    t = do
      -- We fail if we encounter a matchable argument.
      let failure :: ExceptT () m a
    failure = () -> ExceptT () m a
    forall a. () -> ExceptT () m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ()
      tb <- Term -> ExceptT () m (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    t
      let t = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    tb
      case t of
        Var Nat
    x Elims
    _      -> Bool -> ExceptT () m Bool
    forall a. a -> ExceptT () m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> ExceptT () m Bool) -> Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Nat -> Bool
    xs Nat
    x
        -- Issue 1153: A lambda has to be considered matchable.
        -- Lam _ v    -> hasBadRigid (0 : map (+1) xs) (absBody v)
        Lam ArgInfo
    _ Abs Term
    v      -> ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure
        DontCare Term
    v   -> (Nat -> Bool) -> Term -> ExceptT () m Bool
    forall (m :: * -> *).
    PureTCM m =>
    (Nat -> Bool) -> Term -> ExceptT () m Bool
    hasBadRigid Nat -> Bool
    xs Term
    v
        -- The following types of arguments cannot be eliminated by a pattern
        -- match: data, record, Pi, levels, sorts
        -- Thus, their offending rigid variables are bad.
        v :: Term
    v@(Def QName
    f Elims
    es) -> ExceptT () m Bool
    -> ExceptT () m Bool -> ExceptT () m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (Blocked Term -> QName -> Elims -> ExceptT () m Bool
    forall (m :: * -> *) t.
    HasConstInfo m =>
    Blocked t -> QName -> Elims -> m Bool
    isNeutral Blocked Term
    tb QName
    f Elims
    es) ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure (ExceptT () m Bool -> ExceptT () m Bool)
    -> ExceptT () m Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
          m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ Elims
    es Elims -> (Nat -> Bool) -> m Bool
    forall (m :: * -> *) a.
    (PureTCM m, AnyRigid a) =>
    a -> (Nat -> Bool) -> m Bool
    `rigidVarsNotContainedIn` Nat -> Bool
    xs
        -- Andreas, 2012-05-03: There is room for further improvement.
        -- We could also consider a defined f which is not blocked by a meta.
        Pi Dom Type
    a Abs Type
    b       -> m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ (Dom Type
    a,Abs Type
    b) (Dom Type, Abs Type) -> (Nat -> Bool) -> m Bool
    forall (m :: * -> *) a.
    (PureTCM m, AnyRigid a) =>
    a -> (Nat -> Bool) -> m Bool
    `rigidVarsNotContainedIn` Nat -> Bool
    xs
        Level Level
    v      -> m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ Level
    v Level -> (Nat -> Bool) -> m Bool
    forall (m :: * -> *) a.
    (PureTCM m, AnyRigid a) =>
    a -> (Nat -> Bool) -> m Bool
    `rigidVarsNotContainedIn` Nat -> Bool
    xs
        Sort Sort
    s       -> m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
    forall a b. (a -> b) -> a -> b
    $ Sort
    s Sort -> (Nat -> Bool) -> m Bool
    forall (m :: * -> *) a.
    (PureTCM m, AnyRigid a) =>
    a -> (Nat -> Bool) -> m Bool
    `rigidVarsNotContainedIn` Nat -> Bool
    xs
        -- Since constructors can be eliminated by pattern-matching,
        -- offending variables under a constructor could be removed by
        -- the right instantiation of the meta variable.
        -- Thus, they are not rigid.
        Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term]
    args <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es -> do
          ExceptT () m Bool
    -> ExceptT () m Bool -> ExceptT () m Bool -> ExceptT () m Bool
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> ExceptT () m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaCon (ConHead -> QName
    conName ConHead
    c))
            -- in case of a record con, we can in principle prune
            -- (but not this argument; the meta could become a projection!)
            ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> ExceptT () m [Bool] -> ExceptT () m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg Term -> ExceptT () m Bool)
    -> [Arg Term] -> ExceptT () m [Bool]
    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 ((Nat -> Bool) -> Term -> ExceptT () m Bool
    forall (m :: * -> *).
    PureTCM m =>
    (Nat -> Bool) -> Term -> ExceptT () m Bool
    hasBadRigid Nat -> Bool
    xs (Term -> ExceptT () m Bool)
    -> (Arg Term -> Term) -> Arg Term -> ExceptT () m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) [Arg Term]
    args)  -- not andM, we need to force the exceptions!
            ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure
        Con ConHead
    c ConInfo
    _ Elims
    es | Bool
    otherwise -> ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure
        Lit{}        -> ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure -- matchable
        MetaV{}      -> ExceptT () m Bool
    forall {a}. ExceptT () m a
    failure -- potentially matchable
        Dummy{}      -> Bool -> ExceptT () m Bool
    forall a. a -> ExceptT () m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Check whether a term @Def f es@ is finally stuck.
    --   Currently, we give only a crude approximation.
    isNeutral :: (HasConstInfo m) => Blocked t -> QName -> Elims -> m Bool
    isNeutral :: forall (m :: * -> *) t.
    HasConstInfo m =>
    Blocked t -> QName -> Elims -> m Bool
    isNeutral Blocked t
    b QName
    f Elims
    es = do
      let yes :: m Bool
    yes = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
          no :: m Bool
    no  = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      if not (null $ defMatchable def) then no else do
      case theDef def of
        AbstractDefn{} -> m Bool
    yes
        Axiom{}    -> m Bool
    yes
        Datatype{} -> m Bool
    yes
        Record{}   -> m Bool
    yes
        Function{} -> case Blocked t
    b of
          NotBlocked StuckOn{}   t
    _ -> m Bool
    yes
          NotBlocked NotBlocked' Term
    AbsurdMatch t
    _ -> m Bool
    yes
          Blocked t
    _                        -> m Bool
    no
        GeneralizableVar{} -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Defn
    _          -> m Bool
    no

    -- | Check whether any of the variables (given as de Bruijn indices)
    --   occurs *definitely* in the term in a rigid position.
    --   Reduces the term successively to remove variables in dead subterms.
    --   This fixes issue 1386.
    rigidVarsNotContainedIn
      :: (PureTCM m, AnyRigid a)
      => a
      -> (Nat -> Bool)   -- ^ Test for allowed variable (de Bruijn index).
      -> m Bool
    rigidVarsNotContainedIn :: forall (m :: * -> *) a.
    (PureTCM m, AnyRigid a) =>
    a -> (Nat -> Bool) -> m Bool
    rigidVarsNotContainedIn a
    v Nat -> Bool
    is = do
      n0 <- m Nat
    forall (m :: * -> *). MonadTCEnv m => m Nat
    getContextSize
      let -- allowed variables as de Bruijn levels
          levels = Nat -> Bool
    is (Nat -> Bool) -> (Nat -> Nat) -> Nat -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat
    n0Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -)
          -- test if index is forbidden by converting it to level
          test Nat
    i = do
            n <- m Nat
    forall (m :: * -> *). MonadTCEnv m => m Nat
    getContextSize
            -- get de Bruijn level for i
            let l = Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    i
                -- If l >= n0 then it is a bound variable and can be
                -- ignored.  Otherwise, it has to be in the allowed levels.
                forbidden = Nat
    l Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n0 Bool -> Bool -> Bool
    && Bool -> Bool
    not (Nat -> Bool
    levels Nat
    l)
            when forbidden $
              reportSLn "tc.meta.kill" 20 $
                "found forbidden de Bruijn level " ++ show l
            return forbidden
      anyRigid test v

    -- | Collect the *definitely* rigid variables in a monoid.
    --   We need to successively reduce the expression to do this.

    class AnyRigid a where
      anyRigid :: (PureTCM tcm)
               => (Nat -> tcm Bool) -> a -> tcm Bool

    instance AnyRigid Term where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Term -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Term
    t = do
        b <- Term -> tcm (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    t
        case ignoreBlocking b of
          -- Upon entry, we are in rigid position, thus,
          -- bound variables are rigid ones.
          Var Nat
    i Elims
    es   -> Nat -> tcm Bool
    f Nat
    i tcm Bool -> tcm Bool -> tcm Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (Nat -> tcm Bool) -> Elims -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Elims -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Elims
    es
          Lam ArgInfo
    _ Abs Term
    t    -> (Nat -> tcm Bool) -> Abs Term -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Abs Term -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Abs Term
    t
          Lit{}      -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Def QName
    _ Elims
    es   -> case Blocked Term
    b of
            -- If the definition is blocked by a meta, its arguments
            -- may be in flexible positions.
            Blocked{}                   -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            -- If the definition is incomplete, arguments might disappear
            -- by reductions that come with more clauses, thus, these
            -- arguments are not rigid.
            NotBlocked (MissingClauses QName
    _) Term
    _ -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            -- _        -> mempty -- breaks: ImproveInertRHS, Issue442, PruneRecord, PruningNonMillerPattern
            Blocked Term
    _        -> (Nat -> tcm Bool) -> Elims -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Elims -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Elims
    es
          Con ConHead
    _ ConInfo
    _ Elims
    ts -> (Nat -> tcm Bool) -> Elims -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Elims -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Elims
    ts
          Pi Dom Type
    a Abs Type
    b     -> (Nat -> tcm Bool) -> (Dom Type, Abs Type) -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> (Dom Type, Abs Type) -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (Dom Type
    a,Abs Type
    b)
          Sort Sort
    s     -> (Nat -> tcm Bool) -> Sort -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Sort -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Sort
    s
          Level Level
    l    -> (Nat -> tcm Bool) -> Level -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Level -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Level
    l
          MetaV{}    -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DontCare{} -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Dummy{}    -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    instance AnyRigid Type where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Type -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (El Sort
    s Term
    t) = (Nat -> tcm Bool) -> (Sort, Term) -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> (Sort, Term) -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (Sort
    s,Term
    t)

    instance AnyRigid Sort where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Sort -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Sort
    s =
        case Sort
    s of
          Univ Univ
    _ Level
    l   -> (Nat -> tcm Bool) -> Level -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Level -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Level
    l
          Inf Univ
    _ Integer
    _    -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Sort
    SizeUniv   -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Sort
    LockUniv   -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Sort
    LevelUniv  -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Sort
    IntervalUniv -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          FunSort Sort
    s1 Sort
    s2 -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          UnivSort Sort
    s -> (Nat -> tcm Bool) -> Sort -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Sort -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Sort
    s
          MetaS{}    -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DefS{}     -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DummyS{}   -> Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    instance AnyRigid Level where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Level -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (Max Integer
    _ [PlusLevel' Term]
    ls) = (Nat -> tcm Bool) -> [PlusLevel' Term] -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> [PlusLevel' Term] -> tcm Bool
    anyRigid Nat -> tcm Bool
    f [PlusLevel' Term]
    ls

    instance AnyRigid PlusLevel where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> PlusLevel' Term -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (Plus Integer
    _ Term
    l) = (Nat -> tcm Bool) -> Term -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Term -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Term
    l

    instance (Subst a, AnyRigid a) => AnyRigid (Abs a) where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Abs a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Abs a
    b = Abs a -> (a -> tcm Bool) -> tcm Bool
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs a
    b ((a -> tcm Bool) -> tcm Bool) -> (a -> tcm Bool) -> tcm Bool
    forall a b. (a -> b) -> a -> b
    $ (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f

    instance AnyRigid a => AnyRigid (Arg a) where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Arg a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Arg a
    a =
          -- Irrelevant arguments are definitionally equal to
          -- values, so the variables there are not considered
          -- "definitely rigid".
        if Arg a -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Arg a
    a then Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False else
          (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (a -> tcm Bool) -> a -> tcm Bool
    forall a b. (a -> b) -> a -> b
    $ Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    a

    instance AnyRigid a => AnyRigid (Dom a) where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Dom a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f = (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (a -> tcm Bool) -> (Dom a -> a) -> Dom a -> tcm Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom a -> a
    forall t e. Dom' t e -> e
    unDom

    instance AnyRigid a => AnyRigid (Elim' a) where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Elim' a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (Apply Arg a
    a)      = (Nat -> tcm Bool) -> Arg a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> Arg a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Arg a
    a
      anyRigid Nat -> tcm Bool
    f (IApply a
    x a
    y a
    a) = (Nat -> tcm Bool) -> (a, (a, a)) -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> (a, (a, a)) -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (a
    x,(a
    y,a
    a))
      anyRigid Nat -> tcm Bool
    f Proj{}         = Bool -> tcm Bool
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    instance AnyRigid a => AnyRigid [a] where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> [a] -> tcm Bool
    anyRigid = (a -> tcm Bool) -> [a] -> tcm Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    anyM ((a -> tcm Bool) -> [a] -> tcm Bool)
    -> ((Nat -> tcm Bool) -> a -> tcm Bool)
    -> (Nat -> tcm Bool)
    -> [a]
    -> tcm Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid

    instance (AnyRigid a, AnyRigid b) => AnyRigid (a,b) where
      anyRigid :: forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> (a, b) -> tcm Bool
    anyRigid Nat -> tcm Bool
    f (a
    a,b
    b) = (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f a
    a tcm Bool -> tcm Bool -> tcm Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (Nat -> tcm Bool) -> b -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    forall (tcm :: * -> *).
    PureTCM tcm =>
    (Nat -> tcm Bool) -> b -> tcm Bool
    anyRigid Nat -> tcm Bool
    f b
    b

    data PruneResult
      = NothingToPrune   -- ^ the kill list is empty or only @False@s
      | PrunedNothing    -- ^ there is no possible kill (because of type dep.)
      | PrunedSomething  -- ^ managed to kill some args in the list
      | PrunedEverything -- ^ all prescribed kills where performed
        deriving (PruneResult -> PruneResult -> Bool
    (PruneResult -> PruneResult -> Bool)
    -> (PruneResult -> PruneResult -> Bool) -> Eq PruneResult
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PruneResult -> PruneResult -> Bool
    == :: PruneResult -> PruneResult -> Bool
    $c/= :: PruneResult -> PruneResult -> Bool
    /= :: PruneResult -> PruneResult -> Bool
    Eq, Nat -> PruneResult -> [Char] -> [Char]
    [PruneResult] -> [Char] -> [Char]
    PruneResult -> [Char]
    (Nat -> PruneResult -> [Char] -> [Char])
    -> (PruneResult -> [Char])
    -> ([PruneResult] -> [Char] -> [Char])
    -> Show PruneResult
    forall a.
    (Nat -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Nat -> PruneResult -> [Char] -> [Char]
    showsPrec :: Nat -> PruneResult -> [Char] -> [Char]
    $cshow :: PruneResult -> [Char]
    show :: PruneResult -> [Char]
    $cshowList :: [PruneResult] -> [Char] -> [Char]
    showList :: [PruneResult] -> [Char] -> [Char]
    Show)

    -- | @killArgs [k1,...,kn] X@ prunes argument @i@ from metavar @X@ if @ki==True@.
    --   Pruning is carried out whenever > 0 arguments can be pruned.
    killArgs :: (MonadMetaSolver m) => [Bool] -> MetaId -> m PruneResult
    killArgs :: forall (m :: * -> *).
    MonadMetaSolver m =>
    [Bool] -> MetaId -> m PruneResult
    killArgs [Bool]
    kills MetaId
    _
      | Bool -> Bool
    not ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or [Bool]
    kills) = PruneResult -> m PruneResult
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PruneResult
    NothingToPrune  -- nothing to kill
    killArgs [Bool]
    kills MetaId
    m = do
      mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      allowAssign <- asksTC envAssignMetas
      if mvFrozen mv == Frozen || not allowAssign then return PrunedNothing else do
          -- Andreas 2011-04-26, we allow pruning in MetaV and MetaS
          let a = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv
          TelV tel b <- telView' <$> instantiateFull a
          let args         = [Dom ([Char], Type)] -> [Bool] -> [(Dom ([Char], Type), Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel) ([Bool]
    kills [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False)
          (kills', a') <- killedType args b
          dbg kills' a a'
          -- If there is any prunable argument, perform the pruning
          if not (any unArg kills') then return PrunedNothing else do
            addContext tel $ performKill kills' m a'
            -- Only successful if all occurrences were killed
            -- Andreas, 2011-05-09 more precisely, check that at least
            -- the in 'kills' prescribed kills were carried out
            return $ if (and $ zipWith implies kills $ map unArg kills')
                       then PrunedEverything
                       else PrunedSomething
      where
        implies :: Bool -> Bool -> Bool
        implies :: Bool -> Bool -> Bool
    implies Bool
    False Bool
    _ = Bool
    True
        implies Bool
    True  Bool
    x = Bool
    x
        dbg :: [Arg Bool] -> Type -> Type -> m ()
    dbg [Arg Bool]
    kills' Type
    a Type
    a' =
          [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.kill" Nat
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "after kill analysis"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "metavar =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m
              , TCMT IO Doc
    "kills   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Bool] -> [Char]
    forall a. Show a => a -> [Char]
    show [Bool]
    kills)
              , TCMT IO Doc
    "kills'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Arg Bool -> TCMT IO Doc) -> [Arg Bool] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Bool -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
    prettyTCM [Arg Bool]
    kills')
              , TCMT IO Doc
    "oldType =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
              , TCMT IO Doc
    "newType =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a'
              ]
            ]

    -- | @killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')@
    --   (ignoring @Dom@).  Let @t' = (xs:as) -> b@.
    --   Invariant: @k'i == True@ iff @ki == True@ and pruning the @i@th argument from
    --   type @b@ is possible without creating unbound variables.
    --   @t'@ is type @t@ after pruning all @k'i==True@.
    killedType :: (MonadReduce m) => [(Dom (ArgName, Type), Bool)] -> Type -> m ([Arg Bool], Type)
    killedType :: forall (m :: * -> *).
    MonadReduce m =>
    [(Dom ([Char], Type), Bool)] -> Type -> m ([Arg Bool], Type)
    killedType [(Dom ([Char], Type), Bool)]
    args Type
    b = do

      let n :: Nat
    n = [(Dom ([Char], Type), Bool)] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [(Dom ([Char], Type), Bool)]
    args
      let iargs :: [(Nat, (Dom ([Char], Type), Bool))]
    iargs = [Nat]
    -> [(Dom ([Char], Type), Bool)]
    -> [(Nat, (Dom ([Char], Type), Bool))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n) [(Dom ([Char], Type), Bool)]
    args

      -- Turn list of bools into an VarSet containing the variables we want to kill
      -- (indices relative to b).
      let tokill :: IntSet
    tokill = [Nat] -> IntSet
    VarSet.fromList [ Nat
    i | (Nat
    i, (Dom ([Char], Type)
    _, Bool
    True)) <- [(Nat, (Dom ([Char], Type), Bool))]
    iargs ]

      -- First, check the free variables of b to see if they prevent any kills.
      (tokill, b) <- IntSet -> Type -> m (IntSet, Type)
    forall (m :: * -> *).
    MonadReduce m =>
    IntSet -> Type -> m (IntSet, Type)
    reallyNotFreeIn IntSet
    tokill Type
    b

      -- Then recurse over the telescope (right-to-left), building up the final type.
      (killed, b) <- go (reverse $ map fst args) tokill b

      -- Turn the VarSet of killed variables into the list of Arg Bool's to return.
      let kills = [ ArgInfo -> Bool -> Arg Bool
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom ([Char], Type) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Dom ([Char], Type)
    dom) (Nat -> IntSet -> Bool
    VarSet.member Nat
    i IntSet
    killed)
                  | (Nat
    i, (Dom ([Char], Type)
    dom, Bool
    _)) <- [(Nat, (Dom ([Char], Type), Bool))]
    iargs ]
      return (kills, b)
      where
        down :: IntSet -> IntSet
    down = (Nat -> Nat) -> IntSet -> IntSet
    VarSet.mapMonotonic Nat -> Nat
    forall a. Enum a => a -> a
    pred
        up :: IntSet -> IntSet
    up   = (Nat -> Nat) -> IntSet -> IntSet
    VarSet.mapMonotonic Nat -> Nat
    forall a. Enum a => a -> a
    succ

        -- go Δ xs B
        -- Invariants:
        --   - Δ ⊢ B
        --   - Δ is represented as a list in right-to-left order
        --   - xs are deBruijn indices into Δ
        --   - xs ∩ FV(B) = Ø
        -- Result: (ys, Δ' → B')
        --    where Δ' ⊆ Δ  (possibly reduced to remove dependencies, see #3177)
        --          ys ⊆ xs are the variables that were dropped from Δ
        --          B' = strengthen ys B
        go :: (MonadReduce m) => [Dom (ArgName, Type)] -> VarSet -> Type -> m (VarSet, Type)
        go :: forall (m :: * -> *).
    MonadReduce m =>
    [Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
    go [] IntSet
    xs Type
    b | IntSet -> Bool
    VarSet.null IntSet
    xs = (IntSet, Type) -> m (IntSet, Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntSet
    xs, Type
    b)
                   | Bool
    otherwise      = m (IntSet, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        go (Dom ([Char], Type)
    arg : [Dom ([Char], Type)]
    args) IntSet
    xs Type
    b  -- go (Δ (x : A)) xs B, (x = deBruijn index 0)
          | Nat -> IntSet -> Bool
    VarSet.member Nat
    0 IntSet
    xs = do
              -- Case x ∈ xs. We know x ∉ FV(B), so we can safely drop x from the
              -- telescope. Drop x from xs (and shift indices) and recurse with
              -- `strengthen x B`.
              let ys :: IntSet
    ys = IntSet -> IntSet
    down (Nat -> IntSet -> IntSet
    VarSet.delete Nat
    0 IntSet
    xs)
              (ys, b) <- [Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
    forall (m :: * -> *).
    MonadReduce m =>
    [Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
    go [Dom ([Char], Type)]
    args IntSet
    ys (Type -> m (IntSet, Type)) -> Type -> m (IntSet, Type)
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Type -> Type
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible Type
    b
              -- We need to return a set of killed variables relative to Δ (x : A), so
              -- shift ys and add x back in.
              return (VarSet.insert 0 $ up ys, b)
          | Bool
    otherwise = do
              -- Case x ∉ xs. We either can't or don't want to get rid of x. In
              -- this case we have to check A for potential dependencies preventing
              -- us from killing variables in xs.
              let xs' :: IntSet
    xs'       = IntSet -> IntSet
    down IntSet
    xs -- Shift to make relative to Δ ⊢ A
                  ([Char]
    name, Type
    a) = Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom Dom ([Char], Type)
    arg
              (ys, a) <- IntSet -> Type -> m (IntSet, Type)
    forall (m :: * -> *).
    MonadReduce m =>
    IntSet -> Type -> m (IntSet, Type)
    reallyNotFreeIn IntSet
    xs' Type
    a
              -- Recurse on Δ, ys, and (x : A') → B, where A reduces to A' and ys ⊆ xs'
              -- not free in A'. We already know ys not free in B.
              (zs, b) <- go args ys $ mkPi ((name, a) <$ arg) b
              -- Shift back up to make it relative to Δ (x : A) again.
              return (up zs, b)

    reallyNotFreeIn :: (MonadReduce m) => VarSet -> Type -> m (VarSet, Type)
    reallyNotFreeIn :: forall (m :: * -> *).
    MonadReduce m =>
    IntSet -> Type -> m (IntSet, Type)
    reallyNotFreeIn IntSet
    xs Type
    a | IntSet -> Bool
    VarSet.null IntSet
    xs = (IntSet, Type) -> m (IntSet, Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntSet
    xs, Type
    a) -- Shortcut
    reallyNotFreeIn IntSet
    xs Type
    a = do
      let fvs :: VarMap
    fvs      = Type -> VarMap
    forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
    freeVars Type
    a
          anywhere :: IntSet
    anywhere = VarMap -> IntSet
    allVars VarMap
    fvs
          rigid :: IntSet
    rigid    = [IntSet] -> IntSet
    forall (f :: * -> *). Foldable f => f IntSet -> IntSet
    VarSet.unions [VarMap -> IntSet
    stronglyRigidVars VarMap
    fvs, VarMap -> IntSet
    unguardedVars VarMap
    fvs]
          nonrigid :: IntSet
    nonrigid = IntSet -> IntSet -> IntSet
    VarSet.difference IntSet
    anywhere IntSet
    rigid
          hasNo :: IntSet -> Bool
    hasNo    = IntSet -> IntSet -> Bool
    VarSet.disjoint IntSet
    xs
      if IntSet -> Bool
    hasNo IntSet
    nonrigid
        then
           -- No non-rigid occurrences. We can't do anything about the rigid
           -- occurrences so drop those and leave `a` untouched.
           (IntSet, Type) -> m (IntSet, Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntSet -> IntSet -> IntSet
    VarSet.difference IntSet
    xs IntSet
    rigid, Type
    a)
        else do
          -- If there are non-rigid occurrences we need to reduce a to see if
          -- we can get rid of them (#3177).
          (fvs, a) <- IntSet -> Type -> m (IntMap IsFree, Type)
    forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree (IntSet -> IntSet -> IntSet
    VarSet.difference IntSet
    xs IntSet
    rigid) Type
    a
          let xs = IntMap IsFree -> IntSet
    forall a. IntMap a -> IntSet
    IntMap.keysSet (IntMap IsFree -> IntSet) -> IntMap IsFree -> IntSet
    forall a b. (a -> b) -> a -> b
    $ (IsFree -> Bool) -> IntMap IsFree -> IntMap IsFree
    forall a. (a -> Bool) -> IntMap a -> IntMap a
    IntMap.filter (IsFree -> IsFree -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFree
    NotFree) IntMap IsFree
    fvs
          return (xs, a)

    -- | Instantiate a meta variable with a new one that only takes
    --   the arguments which are not pruneable.
    performKill
      :: MonadMetaSolver m
      => [Arg Bool]    -- ^ Arguments to old meta var in left to right order
                       --   with @Bool@ indicating whether they can be pruned.
      -> MetaId        -- ^ The old meta var to receive pruning.
      -> Type          -- ^ The pruned type of the new meta var.
      -> m ()
    performKill :: forall (m :: * -> *).
    MonadMetaSolver m =>
    [Arg Bool] -> MetaId -> Type -> m ()
    performKill [Arg Bool]
    kills MetaId
    m Type
    a = do
      mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      when (mvFrozen mv == Frozen) __IMPOSSIBLE__
      -- Arity of the old meta.
      let n = [Arg Bool] -> Nat
    forall a. Sized a => a -> Nat
    size [Arg Bool]
    kills
      -- The permutation of the new meta picks the arguments
      -- which are not pruned in left to right order
      -- (de Bruijn level order).
      let perm = Nat -> [Nat] -> Permutation
    Perm Nat
    n
                 [ Nat
    i | (Nat
    i, Arg ArgInfo
    _ Bool
    False) <- [Nat] -> [Arg Bool] -> [(Nat, Arg Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat
    0..] [Arg Bool]
    kills ]
          -- The permutation for the old meta might range over a prefix of the arguments
          oldPerm = Nat -> Permutation -> Permutation
    liftP (Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    0 (Nat -> Nat) -> Nat -> Nat
    forall a b. (a -> b) -> a -> b
    $ Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    m) Permutation
    p
            where p :: Permutation
    p = MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv
                  m :: Nat
    m = Permutation -> Nat
    forall a. Sized a => a -> Nat
    size Permutation
    p
          judg = case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
            HasType{ jComparison :: forall a. Judgement a -> Comparison
    jComparison = Comparison
    cmp } -> ZonkAny 0 -> Comparison -> Type -> Judgement (ZonkAny 0)
    forall a. a -> Comparison -> Type -> Judgement a
    HasType ZonkAny 0
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Comparison
    cmp Type
    a
            IsSort{}  -> ZonkAny 0 -> Type -> Judgement (ZonkAny 0)
    forall a. a -> Type -> Judgement a
    IsSort  ZonkAny 0
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Type
    a
      m' <- newMeta Instantiable (mvInfo mv) (mvPriority mv) (composeP perm oldPerm) judg
      -- Andreas, 2010-10-15 eta expand new meta variable if necessary
      etaExpandMetaSafe m'
      let -- Arguments to new meta (de Bruijn indices)
          -- in left to right order.
          vars = [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Nat -> Term
    var Nat
    i)
                 | (Nat
    i, Arg ArgInfo
    info Bool
    False) <- [Nat] -> [Arg Bool] -> [(Nat, Arg Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n) [Arg Bool]
    kills ]
          u       = MetaId -> Elims -> Term
    MetaV MetaId
    m' (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    vars
          -- Arguments to the old meta (just arg infos and name hints)
          -- in left to right order.
          tel     = (Arg Bool -> Arg [Char]) -> [Arg Bool] -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "v" [Char] -> Arg Bool -> Arg [Char]
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [Arg Bool]
    kills
      dbg m' u
      assignTerm m tel u  -- m tel := u
      where
        dbg :: MetaId -> Term -> m ()
    dbg MetaId
    m' Term
    u = [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.kill" Nat
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "actual killing"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "new meta:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty MetaId
    m'
            , TCMT IO Doc
    "kills   :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Bool -> TCMT IO Doc) -> [Arg Bool] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Arg Bool -> [Char]) -> Arg Bool -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> [Char]
    forall a. Show a => a -> [Char]
    show (Bool -> [Char]) -> (Arg Bool -> Bool) -> Arg Bool -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Bool -> Bool
    forall e. Arg e -> e
    unArg) [Arg Bool]
    kills)
            , TCMT IO Doc
    "inst    :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
            ]
          ]