{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# 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.

We also check modality usability for all bound variables; see issue 8570. In the example there, we
elaborate a term as a type (using resourcing rules for types), but then solve a term metavariable
with it. Hence, well-resourcing needs to be re-checked when we solve the metavariable.
-}

module Agda.TypeChecking.MetaVars.Occurs (
    PruneResult(..)
  , killArgs
  , occursCheck
  , prune
  , rigidVarsNotContainedIn
  ) where

import Prelude hiding (null, zip, zipWith)

import Control.Monad.Except ( ExceptT, runExceptT, catchError, throwError )

import Data.Foldable (traverse_)
import Data.Functor

import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntMap.Strict as IntMap

import qualified Agda.Benchmarking as Bench

import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars

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

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.List
import Agda.Utils.ListInf qualified as ListInf
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Zip
import Agda.Utils.ExpandCase
import Agda.Utils.StrictReader

import Agda.Utils.Impossible

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

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

data B : Set where
  inn : A -> B

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

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

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

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

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

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

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

-}

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

-- | Set the names of definitions to be looked at
--   to the defs in the current mutual block.
initOccursCheck :: MetaId -> MetaVariable -> TCM ()
initOccursCheck :: MetaId -> MetaVariable -> TCM ()
initOccursCheck MetaId
m 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
     String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.occurs" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
       String
"initOccursCheck: we do not look into definitions"
     Set QName -> TCMT IO (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
forall a. Set a
Set.empty
   else do
    mb <- Lens' TCEnv (Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe MutualId -> f (Maybe MutualId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe MutualId)
eMutualBlock TCMT IO (Maybe MutualId)
-> (Maybe MutualId -> TCMT IO (Set QName)) -> TCMT IO (Set QName)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe MutualId
Nothing -> Set QName -> TCMT IO (Set QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set QName
forall a. Set a
Set.empty
      Just MutualId
b  -> do
        ds <- MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> TCMT IO MutualBlock -> TCMT IO (Set QName)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> MutualId -> TCMT IO MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
b
        return ds
    reportSDoc "tc.meta.occurs" 20 $ vcat
      [ "initOccursCheck for metavariable" <+> pretty m
      , nest 2 $ "definitions:" <+> prettyTCM mb
      , nest 2 $ "modality:   " <+> pretty (getModality mv)
      ]
    pure mb


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

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

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

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

data OccursCxt = OccursCxt
  { OccursCxt -> UnfoldStrategy
occUnfold   :: !UnfoldStrategy
  , OccursCxt -> MetaId
occMeta     :: !MetaId            -- ^ The meta @m@ we want to solve.
  , OccursCxt -> VarMap' MetaSet
occVars     :: !VarMap            -- ^ The allowed variables @xs@ with their variance.
  , OccursCxt -> Term
occRHS      :: !Term              -- ^ The proposed solution @v@ for the meta (@m xs := v@).
  , OccursCxt -> Int
occLocals   :: !Int               -- ^ Number of local binders (relative to the invocation of
                                      --   occurs checking).
  , OccursCxt -> [Modality]
occLocalModalities :: ![Modality] -- ^ Modalities of local variables.
  , OccursCxt -> Modality
occModality :: !Modality          -- ^ Modality of current position.
  , OccursCxt -> FlexRig' ()
occFlexRig  :: !(FlexRig' ())     -- ^ Flexibility of current position.
  }

instance LensFlexRig OccursCxt () where
  {-# INLINE lensFlexRig #-}
  lensFlexRig :: Lens' OccursCxt (FlexRig' ())
lensFlexRig = \FlexRig' () -> f (FlexRig' ())
f OccursCxt
e -> FlexRig' () -> f (FlexRig' ())
f (OccursCxt -> FlexRig' ()
occFlexRig OccursCxt
e) f (FlexRig' ()) -> (FlexRig' () -> OccursCxt) -> f OccursCxt
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \FlexRig' ()
fr -> OccursCxt
e {occFlexRig = fr}

instance LensModality OccursCxt where
  {-# INLINE getModality #-}
  getModality :: OccursCxt -> Modality
getModality = OccursCxt -> Modality
occModality
  {-# INLINE mapModality #-}
  mapModality :: (Modality -> Modality) -> OccursCxt -> OccursCxt
mapModality = \Modality -> Modality
f OccursCxt
e -> OccursCxt
e {occModality = f (occModality e)}

instance LensRelevance OccursCxt where
instance LensQuantity OccursCxt where

type OccursM = ReaderT OccursCxt TCM

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

metaCheck :: MetaId -> OccursM MetaId
metaCheck :: MetaId -> OccursM MetaId
metaCheck MetaId
m = do
  cxt <- ReaderT OccursCxt (TCMT IO) OccursCxt
forall r (m :: * -> *). MonadReader r m => m r
ask
  let rel = Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (OccursCxt -> Modality
occModality OccursCxt
cxt)
      qnt = Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (OccursCxt -> Modality
occModality OccursCxt
cxt)
      m0  = OccursCxt -> MetaId
occMeta OccursCxt
cxt

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

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

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

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

{-# INLINE allowedVars #-}
-- | Construct a test whether a de Bruijn index is allowed
--   or needs to be pruned.
allowedVars :: OccursM (Nat -> Bool)
allowedVars :: OccursM (Int -> Bool)
allowedVars = do
  -- @n@ is the number of binders we have stepped under.
  n <- (OccursCxt -> Int) -> ReaderT OccursCxt (TCMT IO) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> Int
occLocals
  xs <- asks (theVarMap . occVars)
  -- Bound variables are allowed, and those mentioned in occVars.
  return $! \Int
i -> Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Bool -> Bool -> Bool
|| (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) Int -> IntMap (VarOcc' MetaSet) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (VarOcc' MetaSet)
xs

{-# INLINE defArgs #-}
defArgs :: OccursM a -> OccursM a
defArgs :: forall a. OccursM a -> OccursM a
defArgs OccursM a
m = (OccursCxt -> UnfoldStrategy)
-> ReaderT OccursCxt (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> UnfoldStrategy
occUnfold ReaderT OccursCxt (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> OccursM a) -> OccursM a
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> (a -> ReaderT OccursCxt (TCMT IO) b)
-> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  UnfoldStrategy
NoUnfold  -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
flexibly OccursM a
m
  UnfoldStrategy
YesUnfold -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
weakly OccursM a
m

{-# INLINE conArgs #-}
-- | 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 = (OccursCxt -> UnfoldStrategy)
-> ReaderT OccursCxt (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> UnfoldStrategy
occUnfold ReaderT OccursCxt (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> OccursM a) -> OccursM a
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> (a -> ReaderT OccursCxt (TCMT IO) b)
-> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  UnfoldStrategy
YesUnfold -> OccursM a
m
  UnfoldStrategy
NoUnfold
    | (Elim' Term -> Bool) -> Elims -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\case IApply{} -> Bool
True; Elim' Term
_ -> Bool
False) Elims
es -> OccursM a -> OccursM a
forall a. OccursM a -> OccursM a
flexibly OccursM a
m
    | Bool
otherwise                                   -> OccursM a
m

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

{-# INLINE unfold #-}
unfold :: (Instantiate t, Reduce t) => t -> OccursM t
unfold :: forall t. (Instantiate t, Reduce t) => t -> OccursM t
unfold t
v = (OccursCxt -> UnfoldStrategy)
-> ReaderT OccursCxt (TCMT IO) UnfoldStrategy
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> UnfoldStrategy
occUnfold ReaderT OccursCxt (TCMT IO) UnfoldStrategy
-> (UnfoldStrategy -> ReaderT OccursCxt (TCMT IO) t)
-> ReaderT OccursCxt (TCMT IO) t
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> (a -> ReaderT OccursCxt (TCMT IO) b)
-> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  UnfoldStrategy
NoUnfold  -> t -> ReaderT OccursCxt (TCMT IO) t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate t
v
  UnfoldStrategy
YesUnfold -> t -> ReaderT OccursCxt (TCMT IO) t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce t
v

-- ** Managing rigidity during occurs check.

{-# INLINE weakly #-}
-- | Leave the strongly rigid position.
weakly :: OccursM a -> OccursM a
weakly :: forall a. OccursM a -> OccursM a
weakly = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCxt -> OccursCxt)
 -> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
-> (FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCxt (FlexRig' ())
lensFlexRig ((FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt)
-> (FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt
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

{-# INLINE strongly #-}
strongly :: OccursM a -> OccursM a
strongly :: forall a. OccursM a -> OccursM a
strongly = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCxt -> OccursCxt)
 -> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
-> (FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCxt (FlexRig' ())
lensFlexRig ((FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt)
-> (FlexRig' () -> FlexRig' ()) -> OccursCxt -> OccursCxt
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

{-# INLINE flexibly #-}
flexibly :: OccursM a -> OccursM a
flexibly :: forall a. OccursM a -> OccursM a
flexibly = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCxt -> OccursCxt)
 -> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
-> FlexRig' () -> OccursCxt -> OccursCxt
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter OccursCxt OccursCxt (FlexRig' ()) (FlexRig' ())
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' OccursCxt (FlexRig' ())
lensFlexRig (FlexRig' () -> OccursCxt -> OccursCxt)
-> FlexRig' () -> OccursCxt -> OccursCxt
forall a b. (a -> b) -> a -> b
$ () -> FlexRig' ()
forall a. a -> FlexRig' a
Flexible ()

-- ** Managing modality during occurs check.
-- | Updates both the 'feModality' and the modalities of each variable
-- in the 'occVars'.
{-# INLINE occUnderArgModality #-}
occUnderArgModality :: Modality -> OccursM a -> OccursM a
occUnderArgModality :: forall a. Modality -> OccursM a -> OccursM a
occUnderArgModality Modality
mod = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccursCxt
e -> OccursCxt
e
  { occModality = composeModality mod (occModality e)
  , occVars     = if mod == unitModality then occVars e
                  else mapVarMap (fmap (inverseApplyModalityButNotQuantity mod)) (occVars e)
  }

{-# INLINE debugModalities #-}
debugModalities :: OccursM ()
debugModalities :: OccursM ()
debugModalities = do
  env <- ReaderT OccursCxt (TCMT IO) OccursCxt
forall r (m :: * -> *). MonadReader r m => m r
ask
  reportSDoc "tc.meta.occurs.modal" 60 $ nest 2 (vcat
    [ "ctx:" <+> prettyTCM (getModality env)
    , "var:" <+> prettyTCM (occVars env)
    ])

{-# INLINE patternViolation' #-}
-- ** Error throwing during occurs check.
patternViolation' :: MonadTCM m => Blocker -> Int -> String -> m a
patternViolation' :: forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Int -> String -> m a
patternViolation' Blocker
unblock Int
n String
err = TCM a -> m a
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM a -> m a) -> TCM a -> m a
forall a b. (a -> b) -> a -> b
$ do
  String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.occurs" Int
n String
err
  Blocker -> TCM a
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
unblock

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

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

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

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

{-# INLINE occurs_ #-}
-- GHC flags this as redundant constraint, so we turn off -Wredundant-constraints.
occurs_ :: (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ :: forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ t
t = t -> OccursM t
forall t. Occurs t => t -> OccursM t
occurs t
t

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

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

-- | Going under a binder.
{-# INLINE underBinder #-}
underBinder :: Modality -> OccursM z -> OccursM z
underBinder :: forall a. Modality -> OccursM a -> OccursM a
underBinder Modality
mod = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) z -> ReaderT OccursCxt (TCMT IO) z
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \OccursCxt
e ->
  OccursCxt
e {occLocals = occLocals e + 1, occLocalModalities = mod : occLocalModalities e}

-- | Changing the 'Relevance'.
{-# INLINE underRelevance #-}
underRelevance :: (LensRelevance o) => o -> OccursM z -> OccursM z
underRelevance :: forall o z. LensRelevance o => o -> OccursM z -> OccursM z
underRelevance = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) z -> ReaderT OccursCxt (TCMT IO) z
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCxt -> OccursCxt)
 -> ReaderT OccursCxt (TCMT IO) z -> ReaderT OccursCxt (TCMT IO) z)
-> (o -> OccursCxt -> OccursCxt)
-> o
-> ReaderT OccursCxt (TCMT IO) z
-> ReaderT OccursCxt (TCMT IO) z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Relevance -> Relevance) -> OccursCxt -> OccursCxt
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance ((Relevance -> Relevance) -> OccursCxt -> OccursCxt)
-> (o -> Relevance -> Relevance) -> o -> OccursCxt -> OccursCxt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance (Relevance -> Relevance -> Relevance)
-> (o -> Relevance) -> o -> Relevance -> Relevance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance

-- | In the given computation the 'Quantity' is locally scaled using
-- the 'Quantity' of the first argument.
{-# INLINE underQuantity #-}
underQuantity :: (LensQuantity o) => o -> OccursM a -> OccursM a
underQuantity :: forall o a. LensQuantity o => o -> OccursM a -> OccursM a
underQuantity = (OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a.
(OccursCxt -> OccursCxt)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((OccursCxt -> OccursCxt)
 -> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> (o -> OccursCxt -> OccursCxt)
-> o
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantity -> Quantity) -> OccursCxt -> OccursCxt
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity ((Quantity -> Quantity) -> OccursCxt -> OccursCxt)
-> (o -> Quantity -> Quantity) -> o -> OccursCxt -> OccursCxt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity (Quantity -> Quantity -> Quantity)
-> (o -> Quantity) -> o -> Quantity -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity

-- | Check whether a free variable is allowed in the context as
--   specified by the modality.
variableCheck :: Int -> OccursM Bool
variableCheck :: Int -> ReaderT OccursCxt (TCMT IO) Bool
variableCheck Int
i = do
  locals <- (OccursCxt -> Int) -> ReaderT OccursCxt (TCMT IO) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> Int
occLocals
  -- For bound variables, check if they are usable in current modality
  if i < locals then do
    currentMod <- asks occModality
    localMods <- asks occLocalModalities
    let mod = Modality -> [Modality] -> Int -> Modality
forall a. a -> [a] -> Int -> a
indexWithDefault Modality
forall a. HasCallStack => a
__IMPOSSIBLE__ [Modality]
localMods Int
i
    pure $! mod `moreUsableModality` currentMod
  else do
    vars <- asks occVars
    case lookupVarMap (i - locals) vars of
      -- free vars not listed in @occVars@ are forbidden
      Maybe (VarOcc' MetaSet)
Nothing -> Bool -> ReaderT OccursCxt (TCMT IO) Bool
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      -- otherwise check the usability of modality
      Just VarOcc' MetaSet
o -> do
        currentMod <- (OccursCxt -> Modality) -> ReaderT OccursCxt (TCMT IO) Modality
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> Modality
occModality
        let !mod = VarOcc' MetaSet -> Modality
forall a. LensModality a => a -> Modality
getModality VarOcc' MetaSet
o
        pure $! mod `moreUsableModality` currentMod


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

instance Occurs Term where
  occurs :: Term -> OccursM Term
occurs !Term
v = do
    vb  <- Term -> OccursM (Blocked Term)
forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB Term
v
    let block = Blocked Term -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Term
vb
        -- On a failure, we should retry when any meta that is blocking
        -- the term is solved.
        flexIfBlocked OccursM Term
act = ((OccursM Term -> Result (OccursM Term)) -> Result (OccursM Term))
-> OccursM Term
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \OccursM Term -> Result (OccursM Term)
ret -> if
          -- In the metavariable case we should not yet become flexible
          -- because otherwise pruning won't fire.
          | MetaV{} <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
vb -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
block OccursM Term
act
          | Blocker
block Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocker
neverUnblock -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ 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
$ Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker Blocker
block OccursM Term
act
          -- Re #3594, do not fail hard when Underapplied:
          -- the occurrence could be computed away after eta expansion.
          | NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
blockingStatus = NotBlocked' Term
Underapplied} <- Blocked Term
vb -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly OccursM Term
act
          | Bool
otherwise -> OccursM Term -> Result (OccursM Term)
ret OccursM Term
act
    v <- reduceProjectionLike $ ignoreBlocking vb
    flexIfBlocked $ do
        ctx <- ask
        let m = OccursCxt -> MetaId
occMeta OccursCxt
ctx
        reportSDoc "tc.meta.occurs" 45 $
          text ("occursCheck " ++ prettyShow m ++ " (" ++ show (occFlexRig ctx) ++ ") of ") <+> prettyTCM v
        reportSDoc "tc.meta.occurs" 70 $
          nest 2 $ pretty v
        expand \OccursM Term -> Result (OccursM Term)
ret -> case Term
v of
          Var Int
i Elims
es -> OccursM Term -> Result (OccursM Term)
ret do
            allowed <- Int -> ReaderT OccursCxt (TCMT IO) Bool
variableCheck Int
i

            reportSDoc "tc.meta.occurs.modal" 60 $ vcat
              [ "checking variable" <+> prettyTCM (var i) <+> parens (pretty (var i))
              , nest 2 "allowed:" <+> pretty allowed
              ]
            debugModalities

            if allowed then Var i <$> weakly (occurs es) else do
              -- if the offending variable is of singleton type,
              -- eta-expand it away
              reportSDoc "tc.meta.occurs" 35 $ "offending variable: " <+> prettyTCM (var i)
              t <-  typeOfBV i
              reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "of type " <+> prettyTCM t
              isST <- typeLevelReductions $ isSingletonType t
              reportSDoc "tc.meta.occurs" 35 $ nest 2 $ "(after singleton test)"
              case isST of
                -- not a singleton type
                Maybe Term
Nothing ->
                  -- #4480: Only hard fail if the variable is not in scope. Wrong modality/relevance
                  -- could potentially be salvaged by eta expansion.
                  ReaderT OccursCxt (TCMT IO) Bool
-> OccursM Term -> OccursM Term -> OccursM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (((Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ Int
i) ((Int -> Bool) -> Bool)
-> OccursM (Int -> Bool) -> ReaderT OccursCxt (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccursM (Int -> Bool)
allowedVars) -- vv TODO: neverUnblock is not correct! What could trigger this eta expansion though?
                      (Blocker -> Int -> String -> OccursM Term
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> Int -> String -> m a
patternViolation' Blocker
neverUnblock Int
70 (String -> OccursM Term) -> String -> OccursM Term
forall a b. (a -> b) -> a -> b
$ String
"Disallowed var " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" due to modality/relevance")
                      (OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
strongly (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Blocker -> TypeError -> OccursM Term
forall a. Blocker -> TypeError -> OccursM a
abort Blocker
neverUnblock (TypeError -> OccursM Term) -> TypeError -> OccursM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Term -> Int -> TypeError
MetaCannotDependOn MetaId
m (OccursCxt -> Term
occRHS OccursCxt
ctx) Int
i)
                -- is a singleton type with unique inhabitant sv
                (Just Term
sv) -> Term -> OccursM Term
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> OccursM Term) -> Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term
sv Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
          Lam ArgInfo
h Abs Term
f     -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term)
-> ReaderT OccursCxt (TCMT IO) (Abs Term) -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Modality -> Abs Term -> ReaderT OccursCxt (TCMT IO) (Abs Term)
forall a.
(Occurs a, Subst a) =>
Modality -> Abs a -> OccursM (Abs a)
occursInAbs (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
h) Abs Term
f
          Level Level' Term
l     -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Level' Term -> Term
Level (Level' Term -> Term)
-> ReaderT OccursCxt (TCMT IO) (Level' Term) -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level' Term -> ReaderT OccursCxt (TCMT IO) (Level' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Level' Term
l
          Lit Literal
l       -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Dummy{}     -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          DontCare Term
v  -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term
dontCare (Term -> Term) -> OccursM Term -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            OccursM Term -> OccursM Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Relevance -> OccursM Term -> OccursM Term
forall o z. LensRelevance o => o -> OccursM z -> OccursM 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    -> OccursM Term -> Result (OccursM Term)
ret do
            QName -> OccursM ()
definitionCheck QName
d
            QName -> Elims -> Term
Def QName
d (Elims -> Term)
-> ReaderT OccursCxt (TCMT IO) Elims -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Elims -> ReaderT OccursCxt (TCMT IO) Elims
forall {b}. Occurs b => QName -> b -> ReaderT OccursCxt (TCMT IO) b
occDef QName
d Elims
es
          Con ConHead
c ConInfo
ci Elims
vs -> OccursM Term -> Result (OccursM Term)
ret do
            QName -> OccursM ()
definitionCheck (ConHead -> QName
conName ConHead
c)
            ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term)
-> ReaderT OccursCxt (TCMT IO) Elims -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims
-> ReaderT OccursCxt (TCMT IO) Elims
-> ReaderT OccursCxt (TCMT IO) Elims
forall a. Elims -> OccursM a -> OccursM a
conArgs Elims
vs (Elims -> ReaderT OccursCxt (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'' Term Term)
a Abs (Type'' Term Term)
b      -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
Pi (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term)
-> ReaderT OccursCxt (TCMT IO) (Dom (Type'' Term Term))
-> ReaderT OccursCxt (TCMT IO) (Abs (Type'' Term Term) -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (Type'' Term Term)
-> ReaderT OccursCxt (TCMT IO) (Dom (Type'' Term Term))
forall t. Occurs t => t -> OccursM t
occurs Dom (Type'' Term Term)
a ReaderT OccursCxt (TCMT IO) (Abs (Type'' Term Term) -> Term)
-> ReaderT OccursCxt (TCMT IO) (Abs (Type'' Term Term))
-> OccursM Term
forall a b.
ReaderT OccursCxt (TCMT IO) (a -> b)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Modality
-> Abs (Type'' Term Term)
-> ReaderT OccursCxt (TCMT IO) (Abs (Type'' Term Term))
forall a.
(Occurs a, Subst a) =>
Modality -> Abs a -> OccursM (Abs a)
occursInAbs (Dom (Type'' Term Term) -> Modality
forall a. LensModality a => a -> Modality
getModality Dom (Type'' Term Term)
a) Abs (Type'' Term Term)
b
          Sort Sort' Term
s      -> OccursM Term -> Result (OccursM Term)
ret (OccursM Term -> Result (OccursM Term))
-> OccursM Term -> Result (OccursM Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
Sort (Sort' Term -> Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term) -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Relevance
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall o z. LensRelevance o => o -> OccursM z -> OccursM z
underRelevance Relevance
shapeIrrelevant (ReaderT OccursCxt (TCMT IO) (Sort' Term)
 -> ReaderT OccursCxt (TCMT IO) (Sort' Term))
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort' Term
s
          MetaV MetaId
m' Elims
es -> OccursM Term -> Result (OccursM Term)
ret do
            m' <- MetaId -> OccursM MetaId
metaCheck MetaId
m'
            -- The arguments of a meta are in a flexible position
            (MetaV m' <$> do flexibly $ occurs es) `catchError` \ TCErr
err -> do
                ctx <- ReaderT OccursCxt (TCMT IO) OccursCxt
forall r (m :: * -> *). MonadReader r m => m r
ask
                reportSDoc "tc.meta.kill" 25 $ vcat
                  [ text $ "error during flexible occurs check, we are " ++ show (ctx ^. lensFlexRig)
                  , text $ show err
                  ]
                case err of
                  -- On pattern violations try to remove offending
                  -- flexible occurrences (if not already in a flexible context)
                  PatternErr{} | Bool -> Bool
not (OccursCxt -> Bool
forall o a. LensFlexRig o a => o -> Bool
isFlexible OccursCxt
ctx) -> do
                    String -> Int -> String -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.kill" Int
20 (String -> OccursM ()) -> String -> OccursM ()
forall a b. (a -> b) -> a -> b
$
                      String
"oops, pattern violation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m'
                    -- Andreas, 2014-03-02, see issue 1070:
                    -- Do not prune when meta is projected!
                    Maybe [Arg Term]
-> OccursM Term -> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es) (TCErr -> OccursM Term
forall a. TCErr -> ReaderT OccursCxt (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err) (([Arg Term] -> OccursM Term) -> OccursM Term)
-> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
vs -> do
                      killResult <- TCM PruneResult -> ReaderT OccursCxt (TCMT IO) PruneResult
forall (m :: * -> *) a. Monad m => m a -> ReaderT OccursCxt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM PruneResult -> ReaderT OccursCxt (TCMT IO) PruneResult)
-> ((Int -> Bool) -> TCM PruneResult)
-> (Int -> Bool)
-> ReaderT OccursCxt (TCMT IO) PruneResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> [Arg Term] -> (Int -> Bool) -> TCM PruneResult
prune MetaId
m' [Arg Term]
vs ((Int -> Bool) -> ReaderT OccursCxt (TCMT IO) PruneResult)
-> OccursM (Int -> Bool) -> ReaderT OccursCxt (TCMT IO) PruneResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccursM (Int -> Bool)
allowedVars
                      if (killResult == PrunedEverything) then do
                        -- after successful pruning, restart occurs check
                        reportSDoc "tc.meta.prune" 40 $ "Pruned everything"
                        v' <- instantiate (MetaV m' es)
                        occurs v'
                      else throwError err
                  TCErr
_ -> TCErr -> OccursM Term
forall a. TCErr -> ReaderT OccursCxt (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
          where
            -- a data or record type constructor propagates strong occurrences
            -- since e.g. x = List x is unsolvable
            occDef :: QName -> b -> ReaderT OccursCxt (TCMT IO) b
occDef QName
d b
vs = do
              m   <- (OccursCxt -> MetaId) -> OccursM MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks OccursCxt -> MetaId
occMeta
              lift $ metaOccurs m d
              ifM (liftTCM $ isJust <$> isDataOrRecordType d)
                {-then-} (occurs vs)
                {-else-} (defArgs $ occurs vs)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Occurs Sort where
  occurs :: Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
occurs !Sort' Term
s = do
    Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Instantiate t, Reduce t) => t -> OccursM t
unfold Sort' Term
s ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> (Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term))
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> (a -> ReaderT OccursCxt (TCMT IO) b)
-> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      PiSort Dom' Term Term
a Sort' Term
s1 Abs (Sort' Term)
s2 -> do
        s1' <- ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. OccursM a -> OccursM a
flexibly (ReaderT OccursCxt (TCMT IO) (Sort' Term)
 -> ReaderT OccursCxt (TCMT IO) (Sort' Term))
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort' Term
s1
        a'  <- (a $>) <$> do flexibly $ occurs (unDom a)
        s2' <- mapAbstraction (El s1' <$> a') (flexibly . underBinder (getModality a) . occurs_) s2
        return $ PiSort a' s1' s2'
      FunSort Sort' Term
s1 Sort' Term
s2 -> Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort' Term -> Sort' Term -> Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term -> Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. OccursM a -> OccursM a
flexibly (Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort' Term
s1) ReaderT OccursCxt (TCMT IO) (Sort' Term -> Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a b.
ReaderT OccursCxt (TCMT IO) (a -> b)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. OccursM a -> OccursM a
flexibly (Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort' Term
s2)
      Univ Univ
u Level' Term
a -> do
        -- If --erasure has been turned on, then the argument of
        -- Set/Prop/SSet is erased.
        erasureEnabled <- PragmaOptions -> Bool
optErasure (PragmaOptions -> Bool)
-> ReaderT OccursCxt (TCMT IO) PragmaOptions
-> ReaderT OccursCxt (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT OccursCxt (TCMT IO) PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        Univ u <$>
          (if erasureEnabled then underQuantity zeroQuantity else id)
          (occurs_ a)
      s :: Sort' Term
s@Inf{}    -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
      s :: Sort' Term
s@Sort' Term
SizeUniv -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
      s :: Sort' Term
s@Sort' Term
LockUniv -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
      s :: Sort' Term
s@Sort' Term
LevelUniv -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
      s :: Sort' Term
s@Sort' Term
IntervalUniv -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
      UnivSort Sort' Term
s -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort (Sort' Term -> Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. OccursM a -> OccursM a
flexibly (ReaderT OccursCxt (TCMT IO) (Sort' Term)
 -> ReaderT OccursCxt (TCMT IO) (Sort' Term))
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
-> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall t. (Occurs t, TypeOf t ~ ()) => t -> OccursM t
occurs_ Sort' Term
s
      MetaS MetaId
x Elims
es -> do
        MetaV x es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es)
        return $ MetaS x es
      DefS QName
x Elims
es -> do
        Def x es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (QName -> Elims -> Term
Def QName
x Elims
es)
        return $ DefS x es
      DummyS{}   -> Sort' Term -> ReaderT OccursCxt (TCMT IO) (Sort' Term)
forall a. a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s

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

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

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

occursInAbs :: (Occurs a, Subst a) => Modality -> Abs a -> OccursM (Abs a)
occursInAbs :: forall a.
(Occurs a, Subst a) =>
Modality -> Abs a -> OccursM (Abs a)
occursInAbs Modality
mod (NoAbs String
s a
x) = String -> a -> Abs a
forall a. String -> a -> Abs a
NoAbs String
s (a -> Abs a)
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) (Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReaderT OccursCxt (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs a
x
occursInAbs Modality
mod Abs a
x           = (a -> ReaderT OccursCxt (TCMT IO) a)
-> Abs a -> ReaderT OccursCxt (TCMT IO) (Abs a)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
(a -> m b) -> Abs a -> m (Abs b)
mapAbstraction_ (Modality
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a. Modality -> OccursM a -> OccursM a
underBinder Modality
mod (ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> (a -> ReaderT OccursCxt (TCMT IO) a)
-> a
-> ReaderT OccursCxt (TCMT IO) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReaderT OccursCxt (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs) Abs a
x

metaOccursInAbs :: Occurs a => MetaId -> Abs a -> TCM ()
metaOccursInAbs :: forall a. Occurs a => MetaId -> Abs a -> TCM ()
metaOccursInAbs MetaId
m (Abs String
_ a
x)   = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m a
x
metaOccursInAbs MetaId
m (NoAbs String
_ 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 a
arg = ((OccursM (Arg a) -> Result (OccursM (Arg a)))
 -> Result (OccursM (Arg a)))
-> OccursM (Arg a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \OccursM (Arg a) -> Result (OccursM (Arg a))
ret -> case Arg a
arg of
    Arg ArgInfo
info a
v -> OccursM (Arg a) -> Result (OccursM (Arg a))
ret (OccursM (Arg a) -> Result (OccursM (Arg a)))
-> OccursM (Arg a) -> Result (OccursM (Arg a))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a) -> ReaderT OccursCxt (TCMT IO) a -> OccursM (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      OccursM ()
debugModalities
      String
-> Int
-> String
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall a.
String
-> Int
-> String
-> ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.meta.occurs.arg" Int
70 (String
"going under arg " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Doc -> String
forall a. Show a => a -> String
show (Modality -> Doc
forall a. Pretty a => a -> Doc
P.pretty (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info))) (ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$
        ((ReaderT OccursCxt (TCMT IO) a
  -> Result (ReaderT OccursCxt (TCMT IO) a))
 -> Result (ReaderT OccursCxt (TCMT IO) a))
-> ReaderT OccursCxt (TCMT IO) a
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \ReaderT OccursCxt (TCMT IO) a
-> Result (ReaderT OccursCxt (TCMT IO) a)
ret -> if ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info
          then ReaderT OccursCxt (TCMT IO) a
-> Result (ReaderT OccursCxt (TCMT IO) a)
ret (ReaderT OccursCxt (TCMT IO) a
 -> Result (ReaderT OccursCxt (TCMT IO) a))
-> ReaderT OccursCxt (TCMT IO) a
-> Result (ReaderT OccursCxt (TCMT IO) a)
forall a b. (a -> b) -> a -> b
$ ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
onlyReduceTypes (ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ Modality
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a. Modality -> OccursM a -> OccursM a
occUnderArgModality (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info) (ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ OccursM ()
debugModalities OccursM ()
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) b -> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ReaderT OccursCxt (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs a
v
          else ReaderT OccursCxt (TCMT IO) a
-> Result (ReaderT OccursCxt (TCMT IO) a)
ret (ReaderT OccursCxt (TCMT IO) a
 -> Result (ReaderT OccursCxt (TCMT IO) a))
-> ReaderT OccursCxt (TCMT IO) a
-> Result (ReaderT OccursCxt (TCMT IO) a)
forall a b. (a -> b) -> a -> b
$ Modality
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a. Modality -> OccursM a -> OccursM a
occUnderArgModality (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info) (ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a)
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b. (a -> b) -> a -> b
$ OccursM ()
debugModalities OccursM ()
-> ReaderT OccursCxt (TCMT IO) a -> ReaderT OccursCxt (TCMT IO) a
forall a b.
ReaderT OccursCxt (TCMT IO) a
-> ReaderT OccursCxt (TCMT IO) b -> ReaderT OccursCxt (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> ReaderT OccursCxt (TCMT IO) a
forall t. Occurs t => t -> OccursM t
occurs a
v
  metaOccurs :: MetaId -> Arg a -> TCM ()
metaOccurs MetaId
m = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (a -> TCM ()) -> (Arg a -> a) -> Arg a -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

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

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

-- | @prune m' vs xs@ attempts to remove all arguments from @vs@ whose
--   free variables are not contained in @xs@.
--   If successful, @m'@ is solved by the new, pruned meta variable and we
--   return @True@ else @False@.
--
--   Issue 1147:
--   If any of the meta args @vs@ is matchable, e.g., is a constructor term,
--   we cannot prune, because the offending variables could be removed by
--   reduction for a suitable instantiation of the meta variable.
prune ::
     MetaId         -- ^ Meta to prune.
  -> Args           -- ^ Arguments to meta variable.
  -> (Nat -> Bool)  -- ^ Test for allowed variable (de Bruijn index).
  -> TCM PruneResult
prune :: MetaId -> [Arg Term] -> (Int -> Bool) -> TCM PruneResult
prune MetaId
m' [Arg Term]
vs Int -> Bool
xs = do
  TCMT IO (Either () [Bool])
-> (() -> TCM PruneResult)
-> ([Bool] -> TCM PruneResult)
-> TCM PruneResult
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (ExceptT () (TCMT IO) [Bool] -> TCMT IO (Either () [Bool])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () (TCMT IO) [Bool] -> TCMT IO (Either () [Bool]))
-> ExceptT () (TCMT IO) [Bool] -> TCMT IO (Either () [Bool])
forall a b. (a -> b) -> a -> b
$ (Arg Term -> ExceptT () (TCMT IO) Bool)
-> [Arg Term] -> ExceptT () (TCMT IO) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((Int -> Bool) -> Term -> ExceptT () (TCMT IO) Bool
forall (m :: * -> *).
PureTCM m =>
(Int -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Int -> Bool
xs) (Term -> ExceptT () (TCMT IO) Bool)
-> (Arg Term -> Term) -> Arg Term -> ExceptT () (TCMT IO) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
vs)
    (TCM PruneResult -> () -> TCM PruneResult
forall a b. a -> b -> a
const (TCM PruneResult -> () -> TCM PruneResult)
-> TCM PruneResult -> () -> TCM PruneResult
forall a b. (a -> b) -> a -> b
$ PruneResult -> TCM PruneResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PruneResult
PrunedNothing) (([Bool] -> TCM PruneResult) -> TCM PruneResult)
-> ([Bool] -> TCM PruneResult) -> TCM PruneResult
forall a b. (a -> b) -> a -> b
$ \ [Bool]
kills -> do
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.meta.kill" Int
10 (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
vcat
      [ TCMT IO Doc
"attempting kills"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"m'    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m'
        -- , "xs    =" <+> prettyList (map (prettyTCM . var) xs)  -- no longer printable
        , TCMT IO Doc
"vs    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
        , TCMT IO Doc
"kills =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ([Bool] -> String
forall a. Show a => a -> String
show [Bool]
kills)
        ]
      ]
    [Bool] -> MetaId -> TCM 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 =>
(Int -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Int -> Bool
xs Term
t = do
  -- We fail if we encounter a matchable argument.
  let failure :: ExceptT () m a
failure = () -> ExceptT () m a
forall a. () -> ExceptT () m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ()
  tb <- Term -> ExceptT () m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
t
  let t = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
tb
  case t of
    Var Int
x Elims
_      -> Bool -> ExceptT () m Bool
forall a. a -> ExceptT () m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> ExceptT () m Bool) -> Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Bool
xs Int
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   -> (Int -> Bool) -> Term -> ExceptT () m Bool
forall (m :: * -> *).
PureTCM m =>
(Int -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Int -> Bool
xs Term
v
    -- The following types of arguments cannot be eliminated by a pattern
    -- match: data, record, Pi, levels, sorts
    -- Thus, their offending rigid variables are bad.
    v :: Term
v@(Def QName
f Elims
es) -> ExceptT () m Bool
-> ExceptT () m Bool -> ExceptT () m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (Blocked Term -> QName -> Elims -> ExceptT () m Bool
forall (m :: * -> *) t.
HasConstInfo m =>
Blocked t -> QName -> Elims -> m Bool
isNeutral Blocked Term
tb QName
f Elims
es) ExceptT () m Bool
forall {a}. ExceptT () m a
failure (ExceptT () m Bool -> ExceptT () m Bool)
-> ExceptT () m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ {- else -} do
      m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Elims
es Elims -> (Int -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Int -> Bool) -> m Bool
`rigidVarsNotContainedIn` Int -> 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'' Term Term)
a Abs (Type'' Term Term)
b       -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ (Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b) (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> (Int -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Int -> Bool) -> m Bool
`rigidVarsNotContainedIn` Int -> Bool
xs
    Level Level' Term
v      -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Level' Term
v Level' Term -> (Int -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Int -> Bool) -> m Bool
`rigidVarsNotContainedIn` Int -> Bool
xs
    Sort Sort' Term
s       -> m Bool -> ExceptT () m Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ExceptT () m Bool) -> m Bool -> ExceptT () m Bool
forall a b. (a -> b) -> a -> b
$ Sort' Term
s Sort' Term -> (Int -> Bool) -> m Bool
forall (m :: * -> *) a.
(PureTCM m, AnyRigid a) =>
a -> (Int -> Bool) -> m Bool
`rigidVarsNotContainedIn` Int -> 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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaCon (ConHead -> QName
conName ConHead
c))
        -- in case of a record con, we can in principle prune
        -- (but not this argument; the meta could become a projection!)
        ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> ExceptT () m [Bool] -> ExceptT () m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> ExceptT () m Bool)
-> [Arg Term] -> ExceptT () m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Int -> Bool) -> Term -> ExceptT () m Bool
forall (m :: * -> *).
PureTCM m =>
(Int -> Bool) -> Term -> ExceptT () m Bool
hasBadRigid Int -> Bool
xs (Term -> ExceptT () m Bool)
-> (Arg Term -> Term) -> Arg Term -> ExceptT () m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
args)  -- not andM, we need to force the exceptions!
        ExceptT () m Bool
forall {a}. ExceptT () m a
failure
    Con ConHead
c ConInfo
_ Elims
es | Bool
otherwise -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure
    Lit{}        -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure -- matchable
    MetaV{}      -> ExceptT () m Bool
forall {a}. ExceptT () m a
failure -- potentially matchable
    Dummy{}      -> Bool -> ExceptT () m Bool
forall a. a -> ExceptT () m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

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

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

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

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

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

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

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

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

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

instance (Subst a, AnyRigid a) => AnyRigid (Abs a) where
  anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Int -> tcm Bool) -> Abs a -> tcm Bool
anyRigid Int -> 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
$ (Int -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Int -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Int -> tcm Bool) -> a -> tcm Bool
anyRigid Int -> tcm Bool
f

instance AnyRigid a => AnyRigid (Arg a) where
  anyRigid :: forall (tcm :: * -> *).
PureTCM tcm =>
(Int -> tcm Bool) -> Arg a -> tcm Bool
anyRigid Int -> tcm Bool
f Arg a
a =
      -- Irrelevant arguments are definitionally equal to
      -- values, so the variables there are not considered
      -- "definitely rigid".
    if Arg a -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg a
a then Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else
      (Int -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Int -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Int -> tcm Bool) -> a -> tcm Bool
anyRigid Int -> 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 =>
(Int -> tcm Bool) -> Dom a -> tcm Bool
anyRigid Int -> tcm Bool
f = (Int -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(Int -> tcm Bool) -> a -> tcm Bool
forall (tcm :: * -> *).
PureTCM tcm =>
(Int -> tcm Bool) -> a -> tcm Bool
anyRigid Int -> tcm Bool
f (a -> tcm Bool) -> (Dom a -> a) -> Dom a -> tcm Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom a -> a
forall t e. Dom' t e -> e
unDom

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

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

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


data PruneResult
  = NothingToPrune   -- ^ the kill list is empty or only @False@s
  | PrunedNothing    -- ^ there is no possible kill (because of type dep.)
  | PrunedSomething  -- ^ managed to kill some args in the list
  | PrunedEverything -- ^ all prescribed kills where performed
    deriving (PruneResult -> PruneResult -> Bool
(PruneResult -> PruneResult -> Bool)
-> (PruneResult -> PruneResult -> Bool) -> Eq PruneResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PruneResult -> PruneResult -> Bool
== :: PruneResult -> PruneResult -> Bool
$c/= :: PruneResult -> PruneResult -> Bool
/= :: PruneResult -> PruneResult -> Bool
Eq, Int -> PruneResult -> String -> String
[PruneResult] -> String -> String
PruneResult -> String
(Int -> PruneResult -> String -> String)
-> (PruneResult -> String)
-> ([PruneResult] -> String -> String)
-> Show PruneResult
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> PruneResult -> String -> String
showsPrec :: Int -> PruneResult -> String -> String
$cshow :: PruneResult -> String
show :: PruneResult -> String
$cshowList :: [PruneResult] -> String -> String
showList :: [PruneResult] -> String -> String
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 :: [Bool] -> MetaId -> TCM PruneResult
killArgs :: [Bool] -> MetaId -> TCM PruneResult
killArgs [Bool]
kills MetaId
_
  | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
kills) = PruneResult -> TCM PruneResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PruneResult
NothingToPrune  -- nothing to kill
killArgs [Bool]
kills MetaId
m = do
  mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  allowAssign <- viewTC eAssignMetas
  if mvFrozen mv == Frozen || not allowAssign then return PrunedNothing else do
      -- Andreas 2011-04-26, we allow pruning in MetaV and MetaS
      let a = Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
      TelV tel b <- telView' <$> instantiateFull a
      let args         = [Dom (String, Type'' Term Term)]
-> Infinite Bool -> [(Dom (String, Type'' Term Term), Bool)]
forall a b. [a] -> Infinite b -> [(a, b)]
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a b.
Zip f g h =>
f a -> g b -> h (a, b)
zip (Tele (Dom (Type'' Term Term)) -> [Dom (String, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom (Type'' Term Term))
tel) ([Bool] -> Bool -> Infinite Bool
forall a. [a] -> a -> ListInf a
ListInf.pad [Bool]
kills Bool
False)
      (kills', a') <- killedType args b
      dbg kills' a a'
      -- If there is any prunable argument, perform the pruning
      if not (any unArg kills') then return PrunedNothing else do
        addContext tel $ performKill kills' m a'
        -- Only successful if all occurrences were killed
        -- Andreas, 2011-05-09 more precisely, check that at least
        -- the in 'kills' prescribed kills were carried out
        return $ if (and $ zipWith' implies kills $ map' unArg kills')
                   then PrunedEverything
                   else PrunedSomething
  where
    implies :: Bool -> Bool -> Bool
    implies :: Bool -> Bool -> Bool
implies Bool
False Bool
_ = Bool
True
    implies Bool
True  Bool
x = Bool
x
    dbg :: [Arg Bool] -> Type'' Term Term -> Type'' Term Term -> TCM ()
dbg [Arg Bool]
kills' Type'' Term Term
a Type'' Term Term
a' =
      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.meta.kill" Int
10 (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
vcat
        [ TCMT IO Doc
"after kill analysis"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"metavar =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m
          , TCMT IO Doc
"kills   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ([Bool] -> String
forall a. Show a => a -> String
show [Bool]
kills)
          , TCMT IO Doc
"kills'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Bool -> TCMT IO Doc) -> [Arg Bool] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Bool -> m Doc
prettyTCM [Arg Bool]
kills')
          , TCMT IO Doc
"oldType =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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 (String, Type'' Term Term), Bool)]
-> Type'' Term Term -> m ([Arg Bool], Type'' Term Term)
killedType [(Dom (String, Type'' Term Term), Bool)]
args Type'' Term Term
b = do

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

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

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

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

  -- Turn the VarSet of killed variables into the list of Arg Bool's to return.
  let kills = ((Int, (Dom (String, Type'' Term Term), Bool)) -> Arg Bool)
-> [(Int, (Dom (String, Type'' Term Term), Bool))] -> [Arg Bool]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Int
i, (Dom (String, Type'' Term Term)
dom, Bool
_)) -> ArgInfo -> Bool -> Arg Bool
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> Bool -> Arg Bool) -> ArgInfo -> Bool -> Arg Bool
forall a b. (a -> b) -> a -> b
$$! Dom (String, Type'' Term Term) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom (String, Type'' Term Term)
dom (Bool -> Arg Bool) -> Bool -> Arg Bool
forall a b. (a -> b) -> a -> b
$$! Int -> VarSet -> Bool
VarSet.member Int
i VarSet
killed)
                   [(Int, (Dom (String, Type'' Term Term), Bool))]
iargs
  return (kills, b)
  where
    -- go Δ xs B
    -- Invariants:
    --   - Δ ⊢ B
    --   - Δ is represented as a list in right-to-left order
    --   - xs are deBruijn indices into Δ
    --   - xs ∩ FV(B) = Ø
    -- Result: (ys, Δ' → B')
    --    where Δ' ⊆ Δ  (possibly reduced to remove dependencies, see #3177)
    --          ys ⊆ xs are the variables that were dropped from Δ
    --          B' = strengthen ys B
    go :: (MonadReduce m) => [Dom (ArgName, Type)] -> VarSet -> Type -> m (VarSet, Type)
    go :: forall (m :: * -> *).
MonadReduce m =>
[Dom (String, Type'' Term Term)]
-> VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
go [] VarSet
xs Type'' Term Term
b | VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
xs = (VarSet, Type'' Term Term) -> m (VarSet, Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarSet
xs, Type'' Term Term
b)
               | Bool
otherwise      = m (VarSet, Type'' Term Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
    go (Dom (String, Type'' Term Term)
arg : [Dom (String, Type'' Term Term)]
args) VarSet
xs Type'' Term Term
b  -- go (Δ (x : A)) xs B, (x = deBruijn index 0)
      | Int -> VarSet -> Bool
VarSet.member Int
0 VarSet
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 :: VarSet
ys = Int -> VarSet -> VarSet
VarSet.strengthen Int
1 VarSet
xs
          (ys, b) <- [Dom (String, Type'' Term Term)]
-> VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
forall (m :: * -> *).
MonadReduce m =>
[Dom (String, Type'' Term Term)]
-> VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
go [Dom (String, Type'' Term Term)]
args VarSet
ys (Type'' Term Term -> m (VarSet, Type'' Term Term))
-> Type'' Term Term -> m (VarSet, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Impossible -> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible Type'' Term Term
b
          -- We need to return a set of killed variables relative to Δ (x : A), so
          -- shift ys and add x back in.
          return (VarSet.insert 0 $ VarSet.weaken 1 ys, b)
      | Bool
otherwise = do
          -- Case x ∉ xs. We either can't or don't want to get rid of x. In
          -- this case we have to check A for potential dependencies preventing
          -- us from killing variables in xs.
          let xs' :: VarSet
xs'       = Int -> VarSet -> VarSet
VarSet.strengthen Int
1 VarSet
xs -- Shift to make relative to Δ ⊢ A
              (String
name, Type'' Term Term
a) = Dom (String, Type'' Term Term) -> (String, Type'' Term Term)
forall t e. Dom' t e -> e
unDom Dom (String, Type'' Term Term)
arg
          (ys, a) <- VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
forall (m :: * -> *).
MonadReduce m =>
VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
reallyNotFreeIn VarSet
xs' Type'' Term Term
a
          -- Recurse on Δ, ys, and (x : A') → B, where A reduces to A' and ys ⊆ xs'
          -- not free in A'. We already know ys not free in B.
          (zs, b) <- go args ys $ mkPi ((name, a) <$ arg) b
          -- Shift back up to make it relative to Δ (x : A) again.
          return (VarSet.weaken 1 zs, b)

reallyNotFreeIn :: (MonadReduce m) => VarSet -> Type -> m (VarSet, Type)
reallyNotFreeIn :: forall (m :: * -> *).
MonadReduce m =>
VarSet -> Type'' Term Term -> m (VarSet, Type'' Term Term)
reallyNotFreeIn VarSet
xs Type'' Term Term
a | VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
xs = (VarSet, Type'' Term Term) -> m (VarSet, Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarSet
xs, Type'' Term Term
a) -- Shortcut
reallyNotFreeIn VarSet
xs Type'' Term Term
a = do
  let fvs :: VarMap' MetaSet
fvs      = Type'' Term Term -> VarMap' MetaSet
forall t. Free t => t -> VarMap' MetaSet
freeVarMap Type'' Term Term
a
      anywhere :: VarSet
anywhere = VarMap' MetaSet -> VarSet
allVars VarMap' MetaSet
fvs
      rigid :: VarSet
rigid    = VarSet -> VarSet -> VarSet
VarSet.union (VarMap' MetaSet -> VarSet
stronglyRigidVars VarMap' MetaSet
fvs) (VarMap' MetaSet -> VarSet
unguardedVars VarMap' MetaSet
fvs)
      nonrigid :: VarSet
nonrigid = VarSet -> VarSet -> VarSet
VarSet.difference VarSet
anywhere VarSet
rigid
      hasNo :: VarSet -> Bool
hasNo    = VarSet -> VarSet -> Bool
VarSet.disjoint VarSet
xs
  if VarSet -> Bool
hasNo VarSet
nonrigid
    then
       -- No non-rigid occurrences. We can't do anything about the rigid
       -- occurrences so drop those and leave `a` untouched.
       (VarSet, Type'' Term Term) -> m (VarSet, Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarSet -> VarSet -> VarSet
VarSet.difference VarSet
xs VarSet
rigid, Type'' Term Term
a)
    else do
      -- If there are non-rigid occurrences we need to reduce to see if
      -- we can get rid of them (#3177).
      (fvs, a) <- ReduceM (IntMap IsFree, Type'' Term Term)
-> m (IntMap IsFree, Type'' Term Term)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (IntMap IsFree, Type'' Term Term)
 -> m (IntMap IsFree, Type'' Term Term))
-> ReduceM (IntMap IsFree, Type'' Term Term)
-> m (IntMap IsFree, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ VarSet
-> Type'' Term Term -> ReduceM (IntMap IsFree, Type'' Term Term)
forall a.
(ForceNotFree a, Reduce a) =>
VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree (VarSet -> VarSet -> VarSet
VarSet.difference VarSet
xs VarSet
rigid) Type'' Term Term
a
      let xs = IntMap IsFree -> VarSet
nonFreeVars IntMap IsFree
fvs
      return (xs, a)

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