    {-# 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
    import Control.Monad.Except
    import Control.Monad.Reader

    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 Data.IntSet as IntSet
    import Data.IntSet (IntSet)

    import qualified Agda.Benchmarking as Bench

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

    import Agda.TypeChecking.Constraints () -- instances
    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.Substitute
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Records
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars

    import Agda.Utils.Either
    import Agda.Utils.Lens
    import Agda.Utils.List (downFrom)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Size

    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 = Lens' (Set QName) TCState
    stOccursCheckDefs Lens' (Set QName) TCState -> (Set QName -> Set QName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (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 (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:"
         Maybe MutualId
    mb <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock
         case Maybe MutualId
    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 (m :: * -> *) a. Monad m => a -> m a
    return Set QName
    forall a. Set a
    Set.empty
           Just MutualId
    b  -> do
             Set QName
    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
    lookupMutualBlock MutualId
    b
             [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([QName] -> [TCMT IO Doc]) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    ds
             Set QName -> TCMT IO (Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set QName
    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' (Set QName) TCState -> TCMT IO (Set QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Set QName) TCState
    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 -> VarMap
    occVars    :: VarMap          -- ^ The allowed variables with their variance.
      , OccursExtra -> MetaId
    occMeta    :: MetaId          -- ^ The meta we want to solve.
      , 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
      OccursCtx
    cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      let irr :: Bool
    irr = OccursCtx -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant OccursCtx
    cxt
          er :: Bool
    er  = OccursCtx -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 OccursCtx
    cxt
          m :: MetaId
    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.
      Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Bool
    irr Bool -> Bool -> Bool
    && Bool
    er) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> ReaderT OccursCtx (TCMT IO) (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    d ReaderT OccursCtx (TCMT IO) (Either SigError Definition)
    -> (Either SigError Definition -> OccursM ()) -> OccursM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
    prettyTCM QName
    d
            , TCMT IO Doc
    "has relevance"
            , Relevance -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (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
    $ QName -> Elims -> Term
    Def QName
    d []
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
    prettyTCM QName
    d
            , TCMT IO Doc
    "has quantity"
            , Quantity -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (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
    $ QName -> Elims -> Term
    Def QName
    d []

    metaCheck :: MetaId -> OccursM MetaId
    metaCheck :: MetaId -> OccursM MetaId
    metaCheck MetaId
    m = do
      OccursCtx
    cxt <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      let rel :: Relevance
    rel = OccursCtx -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance OccursCtx
    cxt
          qnt :: Quantity
    qnt = OccursCtx -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity OccursCtx
    cxt
          m0 :: MetaId
    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'
      Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MetaId
    m MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    m0) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Nat -> [Char] -> OccursM ()
    forall (m :: * -> *) a.
    MonadTCM m =>
    Blocker -> Nat -> [Char] -> m a
    patternViolation' Blocker
    neverUnblock Nat
    50 ([Char] -> OccursM ()) -> [Char] -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "occursCheck failed: Found " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m

      MetaVariable
    mv <- MetaId -> ReaderT OccursCtx (TCMT IO) MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      let mmod :: Modality
    mmod = MetaVariable -> Modality
    getMetaModality MetaVariable
    mv
          mmod' :: Modality
    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 (Modality
    mmod Modality -> Modality -> Bool
    `moreUsableModality` Modality
    mmod') then MetaId -> OccursM MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    m else 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: meta variable"
          , MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m
          , TCMT IO Doc
    "has relevance"
          , Relevance -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    mmod)
          , TCMT IO Doc
    "and quantity"
          , Quantity -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity Modality
    mmod)
          ]
        Bool
    allowAssign <- (TCEnv -> Bool) -> ReaderT OccursCtx (TCMT IO) Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    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.
        let fail :: TCMT IO Doc -> OccursM ()
    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 (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> OccursM ()) -> Blocker -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MetaVariable -> Frozen
    mvFrozen MetaVariable
    mv Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    == Frozen
    Frozen)             (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> OccursM ()
    fail TCMT IO Doc
    "meta is frozen"
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (MetaInstantiation -> Bool
    isOpenMeta (MetaInstantiation -> Bool) -> MetaInstantiation -> Bool
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> OccursM ()
    fail TCMT IO Doc
    "meta is already solved"
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    allowAssign                       (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> OccursM ()
    fail TCMT IO Doc
    "assigning metas is not allowed here"
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (OccursCtx -> Bool
    forall a o. LensFlexRig a o => o -> Bool
    isFlexible OccursCtx
    cxt)                    (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> OccursM ()
    fail TCMT IO Doc
    "occurrence is flexible"
        Bool -> OccursM () -> OccursM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (OccursCtx -> Bool
    forall a o. LensFlexRig a o => o -> Bool
    isUnguarded OccursCtx
    cxt)                   (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> OccursM ()
    fail TCMT IO Doc
    "occurrence is unguarded"

        [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
    "Promoting 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "to modality" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Modality -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Modality
    mmod'
        let info' :: MetaInfo
    info' = Modality -> MetaInfo -> MetaInfo
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    mmod' (MetaInfo -> MetaInfo) -> MetaInfo -> MetaInfo
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv
        MetaId
    m' <- TCM MetaId -> OccursM MetaId
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM MetaId -> OccursM MetaId) -> TCM MetaId -> OccursM MetaId
    forall a b. (a -> b) -> a -> b
    $ Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement MetaId
    -> TCM MetaId
    forall (m :: * -> *) a.
    MonadMetaSolver m =>
    Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta Frozen
    Instantiable MetaInfo
    info' (MetaVariable -> MetaPriority
    mvPriority MetaVariable
    mv) (MetaVariable -> Permutation
    mvPermutation MetaVariable
    mv) (MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv)
        [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs.qnt" Nat
    20 (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: new meta variable"
           , MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM MetaId
    m'
           ]
        TCM () -> OccursM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> OccursM ()) -> TCM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Arg [Char]] -> Term -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m [] (Term -> TCM ()) -> Term -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    m' []
        [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
    "New name for" 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
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is" 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
    prettyTCM MetaId
    m'
        MetaId -> OccursM MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    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.
      Nat
    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 :: * -> *). (Applicative 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))
      IntSet
    xs <- (OccursCtx -> IntSet) -> ReaderT OccursCtx (TCMT IO) IntSet
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((IntMap (VarOcc' MetaSet) -> IntSet
    forall a. IntMap a -> IntSet
    IntMap.keysSet (IntMap (VarOcc' MetaSet) -> IntSet)
    -> (VarMap -> IntMap (VarOcc' MetaSet)) -> VarMap -> IntSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VarMap -> IntMap (VarOcc' MetaSet)
    forall a. VarMap' a -> TheVarMap' a
    theVarMap) (VarMap -> IntSet) -> (OccursCtx -> VarMap) -> OccursCtx -> IntSet
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (OccursExtra -> VarMap
    occVars (OccursExtra -> VarMap)
    -> (OccursCtx -> OccursExtra) -> OccursCtx -> VarMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccursCtx -> OccursExtra
    forall a b c. FreeEnv' a b c -> b
    feExtra))
      -- Bound variables are allowed, and those mentioned in occVars.
      (Nat -> Bool) -> OccursM (Nat -> Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Nat -> Bool) -> OccursM (Nat -> Bool))
    -> (Nat -> Bool) -> OccursM (Nat -> Bool)
    forall a b. (a -> b) -> a -> b
    $ \ 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 -> IntSet -> Bool
    `IntSet.member` IntSet
    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
    /= :: UnfoldStrategy -> UnfoldStrategy -> Bool
    $c/= :: UnfoldStrategy -> UnfoldStrategy -> Bool
    == :: UnfoldStrategy -> UnfoldStrategy -> Bool
    $c== :: 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
    showList :: [UnfoldStrategy] -> [Char] -> [Char]
    $cshowList :: [UnfoldStrategy] -> [Char] -> [Char]
    show :: UnfoldStrategy -> [Char]
    $cshow :: UnfoldStrategy -> [Char]
    showsPrec :: Nat -> UnfoldStrategy -> [Char] -> [Char]
    $cshowsPrec :: Nat -> 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 (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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      UnfoldStrategy
    YesUnfold -> OccursM a
    m
      UnfoldStrategy
    NoUnfold | [()] -> 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
      UnfoldStrategy
    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
      Modality
    rel    <- (OccursCtx -> Modality) -> ReaderT OccursCtx (TCMT IO) Modality
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks OccursCtx -> Modality
    forall a b c. FreeEnv' a b c -> Modality
    feModality
      case UnfoldStrategy
    unfold of
        UnfoldStrategy
    YesUnfold | Bool -> Bool
    not (Modality -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Modality
    rel) -> t -> OccursM (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 -> OccursM (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 (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 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' (FlexRig' ()) OccursCtx -> LensMap (FlexRig' ()) OccursCtx
    forall i o. Lens' i o -> LensMap i o
    over forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' ()) OccursCtx
    lensFlexRig LensMap (FlexRig' ()) OccursCtx -> LensMap (FlexRig' ()) OccursCtx
    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 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' (FlexRig' ()) OccursCtx -> LensMap (FlexRig' ()) OccursCtx
    forall i o. Lens' i o -> LensMap i o
    over forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' ()) OccursCtx
    lensFlexRig LensMap (FlexRig' ()) OccursCtx -> LensMap (FlexRig' ()) OccursCtx
    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 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' (FlexRig' ()) OccursCtx -> LensSet (FlexRig' ()) OccursCtx
    forall i o. Lens' i o -> LensSet i o
    set forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' ()) OccursCtx
    lensFlexRig LensSet (FlexRig' ()) OccursCtx -> LensSet (FlexRig' ()) OccursCtx
    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 (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 (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
      OccursCtx
    ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      TCM a -> OccursM a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM a -> OccursM a) -> TCM a -> OccursM a
    forall a b. (a -> b) -> a -> b
    $ do
        if | OccursCtx -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant OccursCtx
    ctx                    -> TCM a
    soft
           | FlexRig' ()
    StronglyRigid <- OccursCtx
    ctx OccursCtx -> Lens' (FlexRig' ()) OccursCtx -> FlexRig' ()
    forall o i. o -> Lens' i o -> i
    ^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' ()) OccursCtx
    lensFlexRig -> TCM a
    hard
           | Bool
    otherwise -> TCM a
    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 occurs :: (Traversable f, Occurs a, f a ~ t) => t -> OccursM t
      occurs = (a -> ReaderT OccursCtx (TCMT IO) a)
    -> f a -> ReaderT OccursCtx (TCMT IO) (f a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs

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

    -- | 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
      :: (Occurs a, InstantiateFull a, PrettyTCM a)
      => MetaId -> VarMap -> a -> TCM a
    occursCheck :: forall a.
    (Occurs a, InstantiateFull a, PrettyTCM a) =>
    MetaId -> VarMap -> a -> TCM a
    occursCheck MetaId
    m VarMap
    xs a
    v = Account (BenchPhase (TCMT IO)) -> TCMT IO a -> TCMT IO a
    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 ] (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ do
      MetaVariable
    mv <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      Nat
    n  <- TCMT IO Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
      [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    35 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "occursCheck " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Show a => a -> [Char]
    show MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ VarMap -> [Char]
    forall a. Show a => a -> [Char]
    show VarMap
    xs
      let initEnv :: UnfoldStrategy -> OccursCtx
    initEnv UnfoldStrategy
    unf = FreeEnv :: forall a b c.
    b -> FlexRig' a -> Modality -> (Maybe Nat -> c) -> FreeEnv' a b c
    FreeEnv
            {  feExtra :: OccursExtra
    feExtra = OccursExtra :: UnfoldStrategy -> VarMap -> MetaId -> Nat -> OccursExtra
    OccursExtra
              { occUnfold :: UnfoldStrategy
    occUnfold  = UnfoldStrategy
    unf
              , occVars :: VarMap
    occVars    = VarMap
    xs
              , occMeta :: MetaId
    occMeta    = MetaId
    m
              , occCxtSize :: Nat
    occCxtSize = Nat
    n
              }
            , feFlexRig :: FlexRig' ()
    feFlexRig   = FlexRig' ()
    forall a. FlexRig' a
    StronglyRigid -- ? Unguarded
            , feModality :: Modality
    feModality  = MetaVariable -> Modality
    getMetaModality MetaVariable
    mv
            , feSingleton :: Maybe Nat -> AllowedVar
    feSingleton = VarMap -> Maybe Nat -> AllowedVar
    variableCheck VarMap
    xs
            }
      MetaVariable -> TCM ()
    initOccursCheck MetaVariable
    mv
      TCMT IO a -> TCMT IO a
    forall a. TCM a -> TCM a
    nicerErrorMessage (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ do
        -- First try without normalising the term
        (a -> OccursM a
    forall t. Occurs t => t -> OccursM t
    occurs a
    v OccursM a -> OccursCtx -> TCMT IO a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` UnfoldStrategy -> OccursCtx
    initEnv UnfoldStrategy
    NoUnfold) TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `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
    getMetaModality MetaVariable
    mv) -> do
              MetaVariable -> TCM ()
    initOccursCheck MetaVariable
    mv
              a -> OccursM a
    forall t. Occurs t => t -> OccursM t
    occurs a
    v OccursM a -> OccursCtx -> TCMT IO a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` UnfoldStrategy -> OccursCtx
    initEnv UnfoldStrategy
    YesUnfold
            TCErr
    _ -> TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

      where
        -- Produce nicer error messages
        nicerErrorMessage :: TCM a -> TCM a
        nicerErrorMessage :: forall a. TCM a -> TCM a
    nicerErrorMessage TCM a
    f = TCM a
    f TCM a -> (TCErr -> TCM a) -> TCM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    err -> case TCErr
    err of
          TypeError CallStack
    _ TCState
    _ Closure TypeError
    cl -> case Closure TypeError -> TypeError
    forall a. Closure a -> a
    clValue Closure TypeError
    cl of
            MetaOccursInItself{} ->
              TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Refuse to construct infinite term by instantiating " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to")
                     , a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (a -> TCMT IO Doc) -> TCMT IO a -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> TCMT IO a
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull a
    v
                     ]
            MetaCannotDependOn MetaId
    _ Nat
    i ->
              TCM Bool -> TCM a -> TCM a -> TCM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCM Bool
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isSortMeta MetaId
    m TCM Bool -> TCM Bool -> TCM Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` (Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    hasUniversePolymorphism))
              ( TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Cannot instantiate the metavariable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to")
                     , a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
                     , TCMT IO Doc
    "since universe polymorphism is disabled"
                     ]
              ) {- else -}
              ( TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                  [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Cannot instantiate the metavariable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to solution")
                       , a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
                       , TCMT IO Doc
    "since it contains the variable"
                       , Closure TypeError -> (TypeError -> TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeError
    cl ((TypeError -> TCMT IO Doc) -> TCMT IO Doc)
    -> (TypeError -> TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ \TypeError
    _ -> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Nat -> Elims -> Term
    Var Nat
    i [])
                       , TCMT IO Doc
    "which is not in scope of the metavariable"
                       ]
                )
            MetaIrrelevantSolution MetaId
    _ Term
    _ ->
              TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Cannot instantiate the metavariable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to solution")
                     , a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
                     , TCMT IO Doc
    "since (part of) the solution was created in an irrelevant context"
                     ]
            MetaErasedSolution MetaId
    _ Term
    _ ->
              TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Cannot instantiate the metavariable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to solution")
                     , a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
                     , TCMT IO Doc
    "since (part of) the solution was created in an erased context"
                     ]
            TypeError
    _ -> TCErr -> TCM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
          TCErr
    _ -> TCErr -> TCM 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
        Blocked Term
    vb  <- Term -> OccursM (Blocked Term)
    forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
    unfoldB Term
    v
        -- occurs' ctx $ ignoreBlocking v  -- fails test/succeed/DontPruneBlocked
        let flexIfBlocked :: OccursM Term -> OccursM Term
    flexIfBlocked = case Blocked Term
    vb of
              -- Don't fail on blocked terms or metas
              Blocked Blocker
    _ MetaV{} -> OccursM Term -> OccursM Term
    forall a. a -> a
    id
              Blocked Blocker
    b Term
    _ -> 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. MonadBlock m => Blocker -> m a -> m a
    addOrUnblocker Blocker
    b
              -- 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} -> OccursM Term -> OccursM Term
    forall a. OccursM a -> OccursM a
    flexibly
              NotBlocked{} -> OccursM Term -> OccursM Term
    forall a. a -> a
    id
        let v :: Term
    v = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    vb
        OccursM Term -> OccursM Term
    flexIfBlocked (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ do
            OccursCtx
    ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
            let m :: MetaId
    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
            [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    45 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $
              [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "occursCheck " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ FlexRig' () -> [Char]
    forall a. Show a => a -> [Char]
    show (OccursCtx -> FlexRig' ()
    forall a b c. FreeEnv' a b c -> FlexRig' a
    feFlexRig OccursCtx
    ctx) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ") of ") 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
    prettyTCM Term
    v
            [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.occurs" Nat
    70 (TCMT IO Doc -> OccursM ()) -> TCMT IO Doc -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $
              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
    $ Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v
            case Term
    v of
              Var Nat
    i Elims
    es   -> do
                Bool
    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 Bool
    allowed then Nat -> Elims -> Term
    Var Nat
    i (Elims -> Term)
    -> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT OccursCtx (TCMT IO) Elims
    -> ReaderT OccursCtx (TCMT IO) Elims
    forall a. OccursM a -> OccursM a
    weakly (Elims -> ReaderT OccursCtx (TCMT IO) Elims
    forall t. Occurs t => t -> OccursM t
    occurs Elims
    es) else do
                  -- if the offending variable is of singleton type,
                  -- eta-expand it away
                  [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
    "offending variable: " 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
    prettyTCM (Nat -> Term
    var Nat
    i)
                  Type
    t <-  Nat -> ReaderT OccursCtx (TCMT IO) Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m Type
    typeOfBV Nat
    i
                  [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
    $ 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
    "of type " 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
    prettyTCM Type
    t
                  Maybe Term
    isST <- Type -> ReaderT OccursCtx (TCMT IO) (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> m (Maybe Term)
    isSingletonType Type
    t
                  [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
    $ 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
    "(after singleton test)"
                  case Maybe Term
    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 -> Nat -> TypeError
    MetaCannotDependOn MetaId
    m Nat
    i)
                    -- is a singleton type with unique inhabitant sv
                    (Just Term
    sv) -> Term -> OccursM Term
    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     -> 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 => t -> OccursM t
    occurs Level
    l
              Lit Literal
    l       -> Term -> OccursM Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
              Dummy{}     -> Term -> OccursM Term
    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 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) -> (Dom Type, Abs Type) -> Term
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> Term
    Pi ((Dom Type, Abs Type) -> Term)
    -> ReaderT OccursCtx (TCMT IO) (Dom Type, Abs Type) -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Dom Type, Abs Type)
    -> ReaderT OccursCtx (TCMT IO) (Dom Type, Abs Type)
    forall t. Occurs t => t -> OccursM t
    occurs (Dom Type
    a,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
    NonStrict (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 => t -> OccursM t
    occurs Sort
    s
              MetaV MetaId
    m' Elims
    es -> do
                MetaId
    m' <- MetaId -> OccursM MetaId
    metaCheck MetaId
    m'

                Blocker -> OccursM Term -> OccursM Term
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
    addOrUnblocker (MetaId -> Blocker
    unblockOnMeta MetaId
    m') (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ do
                             -- If getting stuck here, we need to trigger wakeup if this meta is
                             -- solved.
                  -- The arguments of a meta are in a flexible position
                  (MetaId -> Elims -> Term
    MetaV MetaId
    m' (Elims -> Term)
    -> ReaderT OccursCtx (TCMT IO) Elims -> OccursM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do ReaderT OccursCtx (TCMT IO) Elims
    -> ReaderT OccursCtx (TCMT IO) Elims
    forall a. OccursM a -> OccursM a
    flexibly (ReaderT OccursCtx (TCMT IO) Elims
     -> ReaderT OccursCtx (TCMT IO) Elims)
    -> ReaderT OccursCtx (TCMT IO) Elims
    -> ReaderT OccursCtx (TCMT IO) Elims
    forall a b. (a -> b) -> a -> b
    $ Elims -> ReaderT OccursCtx (TCMT IO) Elims
    forall t. Occurs t => t -> OccursM t
    occurs Elims
    es) OccursM Term -> (TCErr -> OccursM Term) -> OccursM Term
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    err -> do
                    OccursCtx
    ctx <- ReaderT OccursCtx (TCMT IO) OccursCtx
    forall r (m :: * -> *). MonadReader r m => m r
    ask
                    [Char] -> Nat -> TCMT IO Doc -> OccursM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.kill" Nat
    25 (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
    vcat
                      [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "error during flexible occurs check, we are " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ FlexRig' () -> [Char]
    forall a. Show a => a -> [Char]
    show (OccursCtx
    ctx OccursCtx -> Lens' (FlexRig' ()) OccursCtx -> FlexRig' ()
    forall o i. o -> Lens' i o -> i
    ^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
    Lens' (FlexRig' ()) OccursCtx
    lensFlexRig)
                      , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCErr -> [Char]
    forall a. Show a => a -> [Char]
    show TCErr
    err
                      ]
                    case TCErr
    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 a o. LensFlexRig a o => 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 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
                          PruneResult
    killResult <- TCM PruneResult -> ReaderT OccursCtx (TCMT IO) PruneResult
    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 (PruneResult
    killResult PruneResult -> PruneResult -> Bool
    forall a. Eq a => a -> a -> Bool
    == PruneResult
    PrunedEverything)
                            -- after successful pruning, restart occurs check
                            then Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs (Term -> OccursM Term) -> OccursM Term -> OccursM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> OccursM Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate (MetaId -> Elims -> Term
    MetaV MetaId
    m' Elims
    es)
                            else TCErr -> OccursM Term
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
                      TCErr
    _ -> TCErr -> OccursM Term
    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
                  MetaId
    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)
                  TCM () -> OccursM ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> OccursM ()) -> TCM () -> OccursM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> QName -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m QName
    d
                  ReaderT OccursCtx (TCMT IO) Bool
    -> ReaderT OccursCtx (TCMT IO) b
    -> ReaderT OccursCtx (TCMT IO) b
    -> ReaderT OccursCtx (TCMT IO) b
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCM Bool -> ReaderT OccursCtx (TCMT IO) Bool
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> ReaderT OccursCtx (TCMT IO) Bool)
    -> TCM Bool -> ReaderT OccursCtx (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ Maybe DataOrRecord -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe DataOrRecord -> Bool)
    -> TCMT IO (Maybe DataOrRecord) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe DataOrRecord)
    isDataOrRecordType QName
    d)
                    {-then-} (b -> ReaderT OccursCtx (TCMT IO) b
    forall t. Occurs t => t -> OccursM t
    occurs b
    vs)
                    {-else-} (ReaderT OccursCtx (TCMT IO) b -> ReaderT OccursCtx (TCMT IO) b
    forall a. OccursM a -> OccursM a
    defArgs (ReaderT OccursCtx (TCMT IO) b -> ReaderT OccursCtx (TCMT IO) b)
    -> ReaderT OccursCtx (TCMT IO) b -> ReaderT OccursCtx (TCMT IO) b
    forall a b. (a -> b) -> a -> b
    $ b -> ReaderT OccursCtx (TCMT IO) b
    forall t. Occurs t => t -> OccursM t
    occurs b
    vs)

      metaOccurs :: MetaId -> Term -> TCM ()
    metaOccurs MetaId
    m Term
    v = do
        Term
    v <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v
        case Term
    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 (m :: * -> *) a. Monad m => a -> m a
    return ()
          Dummy{}    -> () -> TCM ()
    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 -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m QName
    d TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> MetaId -> Elims -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m 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 t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs 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. 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 -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.occurs" Nat
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Checking for occurrences in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Show a => a -> [Char]
    show 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 (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m DataOrRecSig{}               = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls } = 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 (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m Primitive{}                  = () -> TCM ()
    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 = MetaId -> Maybe Term -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Maybe Term -> TCM ())
    -> (Clause -> Maybe Term) -> Clause -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody

    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]
    forall t. Occurs 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. 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
    $ 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 -> OccursM (PlusLevel' Term)
    occurs (Plus Integer
    n Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term)
    -> OccursM Term -> OccursM (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) -> (Sort, Term) -> Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El ((Sort, Term) -> Type)
    -> ReaderT OccursCtx (TCMT IO) (Sort, Term)
    -> ReaderT OccursCtx (TCMT IO) Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Sort, Term) -> ReaderT OccursCtx (TCMT IO) (Sort, Term)
    forall t. Occurs t => t -> OccursM t
    occurs (Sort
    s,Term
    v)

      metaOccurs :: MetaId -> Type -> TCM ()
    metaOccurs MetaId
    m (El Sort
    s Term
    v) = MetaId -> (Sort, Term) -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> do
            Sort
    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 => t -> OccursM t
    occurs Sort
    s1
            Dom' Term Term
    a'  <- (Dom' Term Term
    a Dom' Term Term -> Term -> Dom' Term Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>) (Term -> Dom' Term Term)
    -> OccursM Term -> ReaderT OccursCtx (TCMT IO) (Dom' Term Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do OccursM Term -> OccursM Term
    forall a. OccursM a -> OccursM a
    flexibly (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 -> OccursM Term) -> Term -> OccursM Term
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Term -> Term
    forall t e. Dom' t e -> e
    unDom Dom' Term Term
    a
            Abs Sort
    s2' <- Dom Type
    -> (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Abs Sort
    -> ReaderT OccursCtx (TCMT IO) (Abs Sort)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s1' (Term -> Type) -> Dom' Term Term -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Term
    a') (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)
    -> (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b c (m :: * -> *) z.
    MonadReader (FreeEnv' a b c) m =>
    m z -> m z
    underBinder (ReaderT OccursCtx (TCMT IO) Sort
     -> ReaderT OccursCtx (TCMT IO) Sort)
    -> (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall t. Occurs t => t -> OccursM t
    occurs) Abs Sort
    s2
            Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort Dom' Term Term
    a' Sort
    s1' Abs Sort
    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 => t -> OccursM t
    occurs Sort
    s1) ReaderT OccursCtx (TCMT IO) (Sort -> Sort)
    -> ReaderT OccursCtx (TCMT IO) Sort
    -> ReaderT OccursCtx (TCMT IO) Sort
    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 => t -> OccursM t
    occurs Sort
    s2)
          Type Level
    a     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type (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 => t -> OccursM t
    occurs Level
    a
          Prop Level
    a     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (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 => t -> OccursM t
    occurs Level
    a
          s :: Sort
    s@Inf{}    -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          SSet Level
    a     -> Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (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 => t -> OccursM t
    occurs Level
    a
          s :: Sort
    s@Sort
    SizeUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
          s :: Sort
    s@Sort
    LockUniv -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    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 => t -> OccursM t
    occurs Sort
    s
          MetaS MetaId
    x Elims
    es -> do
            MetaV MetaId
    x Elims
    es <- Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs (MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es)
            Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x Elims
    es
          DefS QName
    x Elims
    es -> do
            Def QName
    x Elims
    es <- Term -> OccursM Term
    forall t. Occurs t => t -> OccursM t
    occurs (QName -> Elims -> Term
    Def QName
    x Elims
    es)
            Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Sort -> ReaderT OccursCtx (TCMT IO) Sort)
    -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    x Elims
    es
          DummyS{}   -> Sort -> ReaderT OccursCtx (TCMT IO) Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s

      metaOccurs :: MetaId -> Sort -> TCM ()
    metaOccurs MetaId
    m Sort
    s = do
        Sort
    s <- Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Sort
    s
        case Sort
    s of
          PiSort Dom' Term Term
    a Sort
    s1 Abs Sort
    s2 -> MetaId -> (Dom' Term Term, Sort, Abs Sort) -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Dom' Term Term
    a,Sort
    s1,Abs Sort
    s2)
          FunSort Sort
    s1 Sort
    s2 -> MetaId -> (Sort, Sort) -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (Sort
    s1,Sort
    s2)
          Type Level
    a     -> MetaId -> Level -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Level
    a
          Prop Level
    a     -> MetaId -> Level -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Level
    a
          Inf IsFibrant
    _ Integer
    _    -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          SSet Level
    a     -> MetaId -> Level -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Level
    a
          Sort
    SizeUniv   -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Sort
    LockUniv   -> () -> TCM ()
    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 (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance Occurs a => Occurs (Elim' a) where
      occurs :: Elim' a -> OccursM (Elim' a)
    occurs e :: Elim' a
    e@(Proj ProjOrigin
    _ QName
    f)   = Elim' a
    e Elim' a -> OccursM () -> OccursM (Elim' a)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ QName -> OccursM ()
    definitionCheck QName
    f
      occurs (Apply Arg a
    a)      = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply  (Arg a -> Elim' a)
    -> ReaderT OccursCtx (TCMT IO) (Arg a) -> OccursM (Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg a -> ReaderT OccursCtx (TCMT IO) (Arg a)
    forall t. Occurs t => t -> OccursM t
    occurs Arg a
    a
      occurs (IApply a
    x a
    y a
    a) = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply (a -> a -> a -> Elim' a)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) (a -> a -> Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    x ReaderT OccursCtx (TCMT IO) (a -> a -> Elim' a)
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) (a -> Elim' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    y ReaderT OccursCtx (TCMT IO) (a -> Elim' a)
    -> ReaderT OccursCtx (TCMT IO) a -> OccursM (Elim' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    a

      metaOccurs :: MetaId -> Elim' a -> TCM ()
    metaOccurs MetaId
    m (Proj{} ) = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      metaOccurs MetaId
    m (Apply Arg a
    a) = MetaId -> Arg a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m Arg a
    a
      metaOccurs MetaId
    m (IApply a
    x a
    y a
    a) = MetaId -> (a, (a, a)) -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m (a
    x,(a
    y,a
    a))

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

      metaOccurs :: MetaId -> Abs a -> TCM ()
    metaOccurs MetaId
    m (Abs   [Char]
    _ a
    x) = MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m a
    x
      metaOccurs MetaId
    m (NoAbs [Char]
    _ a
    x) = MetaId -> a -> TCM ()
    forall t. Occurs t => MetaId -> t -> TCM ()
    metaOccurs MetaId
    m a
    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 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
    instance Occurs a => Occurs [a] where
    instance Occurs a => Occurs (Maybe a) where

    instance (Occurs a, Occurs b) => Occurs (a,b) where
      occurs :: (a, b) -> OccursM (a, b)
    occurs (a
    x,b
    y) = (,) (a -> b -> (a, b))
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    x ReaderT OccursCtx (TCMT IO) (b -> (a, b))
    -> ReaderT OccursCtx (TCMT IO) b -> OccursM (a, b)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> ReaderT OccursCtx (TCMT IO) b
    forall t. Occurs t => t -> OccursM t
    occurs b
    y

      metaOccurs :: MetaId -> (a, b) -> TCM ()
    metaOccurs 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 (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

    instance (Occurs a, Occurs b, Occurs c) => Occurs (a,b,c) where
      occurs :: (a, b, c) -> OccursM (a, b, c)
    occurs (a
    x,b
    y,c
    z) = (,,) (a -> b -> c -> (a, b, c))
    -> ReaderT OccursCtx (TCMT IO) a
    -> ReaderT OccursCtx (TCMT IO) (b -> c -> (a, b, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> ReaderT OccursCtx (TCMT IO) a
    forall t. Occurs t => t -> OccursM t
    occurs a
    x ReaderT OccursCtx (TCMT IO) (b -> c -> (a, b, c))
    -> ReaderT OccursCtx (TCMT IO) b
    -> ReaderT OccursCtx (TCMT IO) (c -> (a, b, c))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> ReaderT OccursCtx (TCMT IO) b
    forall t. Occurs t => t -> OccursM t
    occurs b
    y ReaderT OccursCtx (TCMT IO) (c -> (a, b, c))
    -> ReaderT OccursCtx (TCMT IO) c -> OccursM (a, b, c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> c -> ReaderT OccursCtx (TCMT IO) c
    forall t. Occurs t => t -> OccursM t
    occurs c
    z

      metaOccurs :: MetaId -> (a, b, c) -> TCM ()
    metaOccurs 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 (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 (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

    ---------------------------------------------------------------------------
    -- * 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)
    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 (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, Semigroup (m Doc), 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
    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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ()
      Blocked Term
    tb <- Term -> ExceptT () m (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    t
      let t :: Term
    t = Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    tb
      case Term
    t of
        Var Nat
    x Elims
    _      -> Bool -> ExceptT () m Bool
    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 (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 (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 (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 (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)
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
          no :: m Bool
    no  = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      if Bool -> Bool
    not (Set QName -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Set QName -> Bool) -> Set QName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Definition -> Set QName
    defMatchable Definition
    def) then m Bool
    no else do
      case Definition -> Defn
    theDef Definition
    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
      Nat
    n0 <- m Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
      let -- allowed variables as de Bruijn levels
          levels :: Nat -> Bool
    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 -> m Bool
    test Nat
    i = do
            Nat
    n <- m Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
            -- get de Bruijn level for i
            let l :: Nat
    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 :: Bool
    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)
            Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    forbidden (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
              [Char] -> Nat -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.kill" Nat
    20 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $
                [Char]
    "found forbidden de Bruijn level " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show Nat
    l
            Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    forbidden
      (Nat -> m Bool) -> a -> m Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> m Bool
    test a
    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
        Blocked Term
    b <- Term -> tcm (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    t
        case Blocked Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Term
    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
    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
    anyRigid Nat -> tcm Bool
    f Abs Term
    t
          Lit{}      -> Bool -> tcm Bool
    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 (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 NotBlocked' Term
    MissingClauses Term
    _ -> Bool -> tcm Bool
    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
    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
    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
    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
    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
    anyRigid Nat -> tcm Bool
    f Level
    l
          MetaV{}    -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DontCare{} -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Dummy{}    -> Bool -> tcm Bool
    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
    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
          Type Level
    l     -> (Nat -> tcm Bool) -> Level -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Level
    l
          Prop Level
    l     -> (Nat -> tcm Bool) -> Level -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Level
    l
          Inf IsFibrant
    _ Integer
    _    -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          SSet Level
    l     -> (Nat -> tcm Bool) -> Level -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, PureTCM tcm) =>
    (Nat -> tcm Bool) -> a -> tcm Bool
    anyRigid Nat -> tcm Bool
    f Level
    l
          Sort
    SizeUniv   -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Sort
    LockUniv   -> Bool -> tcm Bool
    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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          FunSort Sort
    s1 Sort
    s2 -> Bool -> tcm Bool
    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
    anyRigid Nat -> tcm Bool
    f Sort
    s
          MetaS{}    -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DefS{}     -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          DummyS{}   -> Bool -> tcm Bool
    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
    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
    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
    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 =
        case Arg a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Arg a
    a of
          -- Irrelevant arguments are definitionally equal to
          -- values, so the variables there are not considered
          -- "definitely rigid".
          Relevance
    Irrelevant -> Bool -> tcm Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          Relevance
    _          -> (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, 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 Dom a
    dom = (Nat -> tcm Bool) -> a -> tcm Bool
    forall a (tcm :: * -> *).
    (AnyRigid a, 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
    $ Dom a -> a
    forall t e. Dom' t e -> e
    unDom Dom a
    dom

    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
    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
    anyRigid Nat -> tcm Bool
    f (a
    x,(a
    y,a
    a))
      anyRigid Nat -> tcm Bool
    f Proj{}         = Bool -> tcm Bool
    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 Nat -> tcm Bool
    f [a]
    xs = [a] -> (a -> tcm Bool) -> tcm Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    anyM [a]
    xs ((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
    anyRigid Nat -> tcm Bool
    f

    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
    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
    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
    /= :: PruneResult -> PruneResult -> Bool
    $c/= :: PruneResult -> PruneResult -> Bool
    == :: PruneResult -> PruneResult -> Bool
    $c== :: 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
    showList :: [PruneResult] -> [Char] -> [Char]
    $cshowList :: [PruneResult] -> [Char] -> [Char]
    show :: PruneResult -> [Char]
    $cshow :: PruneResult -> [Char]
    showsPrec :: Nat -> PruneResult -> [Char] -> [Char]
    $cshowsPrec :: Nat -> 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 (m :: * -> *) a. Monad m => a -> m a
    return PruneResult
    NothingToPrune  -- nothing to kill
    killArgs [Bool]
    kills MetaId
    m = do
      MetaVariable
    mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      Bool
    allowAssign <- (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas
      if MetaVariable -> Frozen
    mvFrozen MetaVariable
    mv Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    == Frozen
    Frozen Bool -> Bool -> Bool
    || Bool -> Bool
    not Bool
    allowAssign then PruneResult -> m PruneResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return PruneResult
    PrunedNothing else do
          -- Andreas 2011-04-26, we allow pruning in MetaV and MetaS
          let a :: Type
    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 Tele (Dom Type)
    tel Type
    b <- Type -> TelV Type
    telView' (Type -> TelV Type) -> m Type -> m (TelV Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    a
          let args :: [(Dom ([Char], Type), Bool)]
    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)
          ([Arg Bool]
    kills', Type
    a') <- [(Dom ([Char], Type), Bool)] -> Type -> m ([Arg Bool], Type)
    forall (m :: * -> *).
    MonadReduce m =>
    [(Dom ([Char], Type), Bool)] -> Type -> m ([Arg Bool], Type)
    killedType [(Dom ([Char], Type), Bool)]
    args Type
    b
          [Arg Bool] -> Type -> Type -> m ()
    dbg [Arg Bool]
    kills' Type
    a Type
    a'
          -- If there is any prunable argument, perform the pruning
          if Bool -> Bool
    not ((Arg Bool -> Bool) -> [Arg Bool] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Arg Bool -> Bool
    forall e. Arg e -> e
    unArg [Arg Bool]
    kills') then PruneResult -> m PruneResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return PruneResult
    PrunedNothing else do
            Tele (Dom Type) -> m () -> m ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Arg Bool] -> MetaId -> Type -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [Arg Bool] -> MetaId -> Type -> m ()
    performKill [Arg Bool]
    kills' MetaId
    m Type
    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
            PruneResult -> m PruneResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PruneResult -> m PruneResult) -> PruneResult -> m PruneResult
    forall a b. (a -> b) -> a -> b
    $ if ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> [Bool] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Bool -> Bool -> Bool
    implies [Bool]
    kills ([Bool] -> [Bool]) -> [Bool] -> [Bool]
    forall a b. (a -> b) -> a -> b
    $ (Arg Bool -> Bool) -> [Arg Bool] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Bool -> Bool
    forall e. Arg e -> e
    unArg [Arg Bool]
    kills')
                       then PruneResult
    PrunedEverything
                       else PruneResult
    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
    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, 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 Arg Bool -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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
    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

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

      -- First, check the free variables of b to see if they prevent any kills.
      (IntSet
    tokill, Type
    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.
      (IntSet
    killed, Type
    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)] -> [Dom ([Char], Type)]
    forall a. [a] -> [a]
    reverse ([Dom ([Char], Type)] -> [Dom ([Char], Type)])
    -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ ((Dom ([Char], Type), Bool) -> Dom ([Char], Type))
    -> [(Dom ([Char], Type), Bool)] -> [Dom ([Char], Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom ([Char], Type), Bool) -> Dom ([Char], Type)
    forall a b. (a, b) -> a
    fst [(Dom ([Char], Type), Bool)]
    args) IntSet
    tokill Type
    b

      -- Turn the IntSet of killed variables into the list of Arg Bool's to return.
      let kills :: [Arg Bool]
    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
    IntSet.member Nat
    i IntSet
    killed)
                  | (Nat
    i, (Dom ([Char], Type)
    dom, Bool
    _)) <- [(Nat, (Dom ([Char], Type), Bool))]
    -> [(Nat, (Dom ([Char], Type), Bool))]
    forall a. [a] -> [a]
    reverse ([(Nat, (Dom ([Char], Type), Bool))]
     -> [(Nat, (Dom ([Char], Type), Bool))])
    -> [(Nat, (Dom ([Char], Type), Bool))]
    -> [(Nat, (Dom ([Char], Type), Bool))]
    forall a b. (a -> b) -> a -> b
    $ [Nat]
    -> [(Dom ([Char], Type), Bool)]
    -> [(Nat, (Dom ([Char], Type), Bool))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat
    0..] ([(Dom ([Char], Type), Bool)]
     -> [(Nat, (Dom ([Char], Type), Bool))])
    -> [(Dom ([Char], Type), Bool)]
    -> [(Nat, (Dom ([Char], Type), Bool))]
    forall a b. (a -> b) -> a -> b
    $ [(Dom ([Char], Type), Bool)] -> [(Dom ([Char], Type), Bool)]
    forall a. [a] -> [a]
    reverse [(Dom ([Char], Type), Bool)]
    args ]
      ([Arg Bool], Type) -> m ([Arg Bool], Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg Bool]
    kills, Type
    b)
      where
        down :: IntSet -> IntSet
    down = (Nat -> Nat) -> IntSet -> IntSet
    IntSet.map Nat -> Nat
    forall a. Enum a => a -> a
    pred
        up :: IntSet -> IntSet
    up   = (Nat -> Nat) -> IntSet -> IntSet
    IntSet.map 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)] -> IntSet -> Type -> m (IntSet, Type)
        go :: forall (m :: * -> *).
    MonadReduce m =>
    [Dom ([Char], Type)] -> IntSet -> Type -> m (IntSet, Type)
    go [] IntSet
    xs Type
    b | IntSet -> Bool
    IntSet.null IntSet
    xs = (IntSet, Type) -> m (IntSet, Type)
    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
    IntSet.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
    IntSet.delete Nat
    0 IntSet
    xs)
              (IntSet
    ys, Type
    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.
              (IntSet, Type) -> m (IntSet, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat -> IntSet -> IntSet
    IntSet.insert Nat
    0 (IntSet -> IntSet) -> IntSet -> IntSet
    forall a b. (a -> b) -> a -> b
    $ IntSet -> IntSet
    up IntSet
    ys, Type
    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
              (IntSet
    ys, Type
    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.
              (IntSet
    zs, Type
    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 (Dom ([Char], Type) -> Type -> Type
    mkPi (([Char]
    name, Type
    a) ([Char], Type) -> Dom ([Char], Type) -> Dom ([Char], Type)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom ([Char], Type)
    arg) Type
    b)
              -- Shift back up to make it relative to Δ (x : A) again.
              (IntSet, Type) -> m (IntSet, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntSet -> IntSet
    up IntSet
    zs, Type
    b)

    reallyNotFreeIn :: (MonadReduce m) => IntSet -> Type -> m (IntSet, Type)
    reallyNotFreeIn :: forall (m :: * -> *).
    MonadReduce m =>
    IntSet -> Type -> m (IntSet, Type)
    reallyNotFreeIn IntSet
    xs Type
    a | IntSet -> Bool
    IntSet.null IntSet
    xs = (IntSet, Type) -> m (IntSet, Type)
    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
    IntSet.unions [VarMap -> IntSet
    stronglyRigidVars VarMap
    fvs, VarMap -> IntSet
    unguardedVars VarMap
    fvs]
          nonrigid :: IntSet
    nonrigid = IntSet -> IntSet -> IntSet
    IntSet.difference IntSet
    anywhere IntSet
    rigid
          hasNo :: IntSet -> Bool
    hasNo    = IntSet -> IntSet -> Bool
    IntSet.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 (m :: * -> *) a. Monad m => a -> m a
    return (IntSet -> IntSet -> IntSet
    IntSet.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).
          (IntMap IsFree
    fvs, Type
    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
    IntSet.difference IntSet
    xs IntSet
    rigid) Type
    a
          let xs :: IntSet
    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
          (IntSet, Type) -> m (IntSet, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IntSet
    xs, Type
    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
      MetaVariable
    mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MetaVariable -> Frozen
    mvFrozen MetaVariable
    mv Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    == Frozen
    Frozen) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      -- Arity of the old meta.
      let n :: Nat
    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 :: Permutation
    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 :: Permutation
    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 :: Judgement Any
    judg = case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
            HasType{ jComparison :: forall a. Judgement a -> Comparison
    jComparison = Comparison
    cmp } -> Any -> Comparison -> Type -> Judgement Any
    forall a. a -> Comparison -> Type -> Judgement a
    HasType Any
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Comparison
    cmp Type
    a
            IsSort{}  -> Any -> Type -> Judgement Any
    forall a. a -> Type -> Judgement a
    IsSort  Any
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Type
    a
      MetaId
    m' <- Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement Any
    -> m MetaId
    forall (m :: * -> *) a.
    MonadMetaSolver m =>
    Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta Frozen
    Instantiable (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv) (MetaVariable -> MetaPriority
    mvPriority MetaVariable
    mv) (Permutation -> Permutation -> Permutation
    composeP Permutation
    perm Permutation
    oldPerm) Judgement Any
    judg
      -- Andreas, 2010-10-15 eta expand new meta variable if necessary
      MetaId -> m ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    etaExpandMetaSafe MetaId
    m'
      let -- Arguments to new meta (de Bruijn indices)
          -- in left to right order.
          vars :: [Arg Term]
    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 :: Term
    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 [Char]]
    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 (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [Arg Bool]
    kills
      MetaId -> Term -> m ()
    dbg MetaId
    m' Term
    u
      MetaId -> [Arg [Char]] -> Term -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m [Arg [Char]]
    tel Term
    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
    prettyTCM Term
    u
            ]
          ]