{-# LANGUAGE NondecreasingIndentation  #-}

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

  When hitting a meta variable:

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

module Agda.TypeChecking.MetaVars.Occurs where

import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader

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

import qualified Agda.Benchmarking as Bench

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

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

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

import Agda.Utils.Impossible

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

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

data B : Set where
  inn : A -> B

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

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

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

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

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

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

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

-}

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

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


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

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

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

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

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

-- ** Modality handling.

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

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

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

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

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

  -- Check for loop
  --   don't fail hard on this, since we might still be on the top-level
  --   after some killing (Issue 442)
  --
  -- Andreas, 2013-02-18  Issue 795 demonstrates that a recursive
  -- occurrence of a meta could be solved by the identity.
  --   ? (Q A) = Q (? A)
  -- So, do not throw an error.
  -- I guess the error was there from times when occurrence check
  -- was done after the "lhs=linear variables" check, but now
  -- occurrence check comes first.
  -- WAS:
  -- when (m == m') $ if ctx == Top then patternViolation else
  --   abort ctx $ MetaOccursInItself m'
  Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m0) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> VerboseLevel -> VerboseKey -> OccursM ()
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> VerboseLevel -> VerboseKey -> m a
patternViolation' Blocker
neverUnblock VerboseLevel
50 (VerboseKey -> OccursM ()) -> VerboseKey -> OccursM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"occursCheck failed: Found " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m

  MetaVariable
mv <- MetaId
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  let mmod :: Modality
mmod = MetaVariable -> Modality
getMetaModality MetaVariable
mv
      mmod' :: Modality
mmod' = Relevance -> Modality -> Modality
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Quantity -> Modality -> Modality
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
qnt (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Modality
mmod
  if (Modality
mmod Modality -> Modality -> Bool
`moreUsableModality` Modality
mmod') then MetaId -> OccursM MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
m else do
    VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
35 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
      [ TCM Doc
"occursCheck: meta variable"
      , MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m
      , TCM Doc
"has relevance"
      , Relevance -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mmod)
      , TCM Doc
"and quantity"
      , Quantity -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mmod)
      ]
    Bool
allowAssign <- (TCEnv -> Bool)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas
    -- Jesper, 2020-11-10: if we encounter a metavariable that is
    -- unusable because of its modality (e.g. irrelevant or erased) we
    -- try to *promote* the meta to the required modality, by creating
    -- a new meta with that modality and solving the old one with
    -- it. Don't do this if the meta occurs in a flexible or unguarded
    -- position:
    -- - If it is in a flexible position, it could disappear when
    --   another meta is solved, so promotion is maybe not necessary.
    -- - If it is in a top-level position, we can instead solve the
    --   equation by instantiating the other way around, so promotion
    --   is not necessary.
    let fail :: TCM Doc -> OccursM ()
fail TCM Doc
reason = do
          VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
20 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Meta occurs check found bad relevance"
          VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
20 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"aborting because" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
reason
          Blocker -> OccursM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> OccursM ()) -> Blocker -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MetaVariable -> Frozen
mvFrozen MetaVariable
mv Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
== Frozen
Frozen)             (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> OccursM ()
fail TCM Doc
"meta is frozen"
    Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> MetaInstantiation -> Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv) (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> OccursM ()
fail TCM Doc
"meta is already solved"
    Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowAssign                       (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> OccursM ()
fail TCM Doc
"assigning metas is not allowed here"
    Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FreeEnv' () OccursExtra AllowedVar -> Bool
forall a o. LensFlexRig a o => o -> Bool
isFlexible FreeEnv' () OccursExtra AllowedVar
cxt)                    (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> OccursM ()
fail TCM Doc
"occurrence is flexible"
    Bool -> OccursM () -> OccursM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FreeEnv' () OccursExtra AllowedVar -> Bool
forall a o. LensFlexRig a o => o -> Bool
isUnguarded FreeEnv' () OccursExtra AllowedVar
cxt)                   (OccursM () -> OccursM ()) -> OccursM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc -> OccursM ()
fail TCM Doc
"occurrence is unguarded"

    VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
20 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Promoting meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"to modality" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Modality -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mmod'
    let info' :: MetaInfo
info' = Modality -> MetaInfo -> MetaInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mmod' (MetaInfo -> MetaInfo) -> MetaInfo -> MetaInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
    MetaId
m' <- TCM MetaId -> OccursM MetaId
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM MetaId -> OccursM MetaId) -> TCM MetaId -> OccursM MetaId
forall a b. (a -> b) -> a -> b
$ Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement MetaId
-> TCM MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta Frozen
Instantiable MetaInfo
info' (MetaVariable -> MetaPriority
mvPriority MetaVariable
mv) (MetaVariable -> Permutation
mvPermutation MetaVariable
mv) (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
    VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs.qnt" VerboseLevel
20 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
       [ TCM Doc
"occursCheck: new meta variable"
       , MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m'
       ]
    TCM () -> OccursM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> OccursM ()) -> TCM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg VerboseKey] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m [] (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m' []
    VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
35 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"New name for" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"is" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m'
    MetaId -> OccursM MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
m'

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

-- ** Unfolding during occurs check.

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

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

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

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

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

-- ** Managing rigidiy during occurs check.

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

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

flexibly :: OccursM a -> OccursM a
flexibly :: OccursM a -> OccursM a
flexibly = (FreeEnv' () OccursExtra AllowedVar
 -> FreeEnv' () OccursExtra AllowedVar)
-> OccursM a -> OccursM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((FreeEnv' () OccursExtra AllowedVar
  -> FreeEnv' () OccursExtra AllowedVar)
 -> OccursM a -> OccursM a)
-> (FreeEnv' () OccursExtra AllowedVar
    -> FreeEnv' () OccursExtra AllowedVar)
-> OccursM a
-> OccursM a
forall a b. (a -> b) -> a -> b
$ Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
-> LensSet (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
forall i o. Lens' i o -> LensSet i o
set forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
lensFlexRig LensSet (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
-> LensSet (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
forall a b. (a -> b) -> a -> b
$ () -> FlexRig' ()
forall a. a -> FlexRig' a
Flexible ()

-- ** Error throwing during occurs check.

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

abort :: Blocker -> TypeError -> OccursM a
abort :: Blocker -> TypeError -> OccursM a
abort Blocker
unblock TypeError
err = do
  FreeEnv' () OccursExtra AllowedVar
ctx <- ReaderT
  (FreeEnv' () OccursExtra AllowedVar)
  TCM
  (FreeEnv' () OccursExtra AllowedVar)
forall r (m :: * -> *). MonadReader r m => m r
ask
  TCM a -> OccursM a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM a -> OccursM a) -> TCM a -> OccursM a
forall a b. (a -> b) -> a -> b
$ do
    if | FreeEnv' () OccursExtra AllowedVar -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant FreeEnv' () OccursExtra AllowedVar
ctx                    -> TCM a
soft
       | FlexRig' ()
StronglyRigid <- FreeEnv' () OccursExtra AllowedVar
ctx FreeEnv' () OccursExtra AllowedVar
-> Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
-> FlexRig' ()
forall o i. o -> Lens' i o -> i
^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
lensFlexRig -> TCM a
hard
       | Bool
otherwise -> TCM a
soft
  where
  hard :: TCM a
hard = TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
err -- here, throw an uncatchable error (unsolvable constraint)
  soft :: TCM a
soft = Blocker -> VerboseLevel -> VerboseKey -> TCM a
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> VerboseLevel -> VerboseKey -> m a
patternViolation' Blocker
unblock VerboseLevel
70 (TypeError -> VerboseKey
forall a. Show a => a -> VerboseKey
show TypeError
err) -- throws a PatternErr, which leads to delayed constraint

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

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

  default occurs :: (Traversable f, Occurs a, f a ~ t) => t -> OccursM t
  occurs = (a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a)
-> f a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (f a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall t. Occurs t => t -> OccursM t
occurs

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

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

  where
    -- Produce nicer error messages
    nicerErrorMessage :: TCM a -> TCM a
    nicerErrorMessage :: TCM a -> TCM a
nicerErrorMessage TCM a
f = TCM a
f TCM a -> (TCErr -> TCM a) -> TCM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> case TCErr
err of
      TypeError CallStack
_ TCState
_ Closure TypeError
cl -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl of
        MetaOccursInItself{} ->
          TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Refuse to construct infinite term by instantiating " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to")
                 , a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (a -> TCM Doc) -> TCM a -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> TCM a
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull a
v
                 ]
        MetaCannotDependOn MetaId
_ VerboseLevel
i ->
          TCM Bool -> TCM a -> TCM a -> TCM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCM Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isSortMeta MetaId
m TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism))
          ( TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Cannot instantiate the metavariable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to")
                 , a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
                 , TCM Doc
"since universe polymorphism is disabled"
                 ]
          ) {- else -}
          ( TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Cannot instantiate the metavariable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to solution")
                   , a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
                   , TCM Doc
"since it contains the variable"
                   , Closure TypeError -> (TypeError -> TCM Doc) -> TCM Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
cl ((TypeError -> TCM Doc) -> TCM Doc)
-> (TypeError -> TCM Doc) -> TCM Doc
forall a b. (a -> b) -> a -> b
$ \TypeError
_ -> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Elims -> Term
Var VerboseLevel
i [])
                   , TCM Doc
"which is not in scope of the metavariable"
                   ]
            )
        MetaIrrelevantSolution MetaId
_ Term
_ ->
          TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Cannot instantiate the metavariable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to solution")
                 , a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
                 , TCM Doc
"since (part of) the solution was created in an irrelevant context"
                 ]
        MetaErasedSolution MetaId
_ Term
_ ->
          TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"Cannot instantiate the metavariable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" to solution")
                 , a -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
                 , TCM Doc
"since (part of) the solution was created in an erased context"
                 ]
        TypeError
_ -> TCErr -> TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
      TCErr
_ -> TCErr -> TCM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

instance Occurs Term where
  occurs :: Term -> OccursM Term
occurs Term
v = do
    Blocked Term
vb  <- Term -> OccursM (Blocked Term)
forall t. (Instantiate t, Reduce t) => t -> OccursM (Blocked t)
unfoldB Term
v
    -- occurs' ctx $ ignoreBlocking v  -- fails test/succeed/DontPruneBlocked
    let flexIfBlocked :: OccursM Term -> OccursM Term
flexIfBlocked = case Blocked Term
vb of
          -- Don't fail on blocked terms or metas
          Blocked Blocker
_ MetaV{} -> OccursM Term -> OccursM Term
forall a. a -> a
id
          Blocked Blocker
b Term
_ -> OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly (OccursM Term -> OccursM Term)
-> (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker Blocker
b
          -- Re #3594, do not fail hard when Underapplied:
          -- the occurrence could be computed away after eta expansion.
          NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
blockingStatus = NotBlocked' Term
Underapplied} -> OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly
          NotBlocked{} -> OccursM Term -> OccursM Term
forall a. a -> a
id
    let v :: Term
v = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
vb
    OccursM Term -> OccursM Term
flexIfBlocked (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ do
        FreeEnv' () OccursExtra AllowedVar
ctx <- ReaderT
  (FreeEnv' () OccursExtra AllowedVar)
  TCM
  (FreeEnv' () OccursExtra AllowedVar)
forall r (m :: * -> *). MonadReader r m => m r
ask
        let m :: MetaId
m = OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId)
-> (FreeEnv' () OccursExtra AllowedVar -> OccursExtra)
-> FreeEnv' () OccursExtra AllowedVar
-> MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeEnv' () OccursExtra AllowedVar -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra (FreeEnv' () OccursExtra AllowedVar -> MetaId)
-> FreeEnv' () OccursExtra AllowedVar -> MetaId
forall a b. (a -> b) -> a -> b
$ FreeEnv' () OccursExtra AllowedVar
ctx
        VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
45 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$
          VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"occursCheck " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" (" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ FlexRig' () -> VerboseKey
forall a. Show a => a -> VerboseKey
show (FreeEnv' () OccursExtra AllowedVar -> FlexRig' ()
forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig FreeEnv' () OccursExtra AllowedVar
ctx) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
") of ") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
70 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$
          VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
        case Term
v of
          Var VerboseLevel
i Elims
es   -> do
            Bool
allowed <- All -> Bool
getAll (All -> Bool) -> (AllowedVar -> All) -> AllowedVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AllowedVar -> AllowedVar
forall a b. (a -> b) -> a -> b
$ Modality
unitModality) (AllowedVar -> Bool)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM AllowedVar
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseLevel
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM AllowedVar
forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
VerboseLevel -> FreeT a b m c
variable VerboseLevel
i
            if Bool
allowed then VerboseLevel -> Elims -> Term
Var VerboseLevel
i (Elims -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall a. OccursM a -> OccursM a
weakly (Elims -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall t. Occurs t => t -> OccursM t
occurs Elims
es) else do
              -- if the offending variable is of singleton type,
              -- eta-expand it away
              VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
35 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"offending variable: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i)
              Type
t <-  VerboseLevel
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
              VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
35 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
              Maybe Term
isST <- Type
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Maybe Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> m (Maybe Term)
isSingletonType Type
t
              VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.occurs" VerboseLevel
35 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"(after singleton test)"
              case Maybe Term
isST of
                -- not a singleton type
                Maybe Term
Nothing ->
                  -- #4480: Only hard fail if the variable is not in scope. Wrong modality/relevance
                  -- could potentially be salvaged by eta expansion.
                  ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
-> OccursM Term -> OccursM Term -> OccursM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (((VerboseLevel -> Bool) -> VerboseLevel -> Bool
forall a b. (a -> b) -> a -> b
$ VerboseLevel
i) ((VerboseLevel -> Bool) -> Bool)
-> OccursM (VerboseLevel -> Bool)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccursM (VerboseLevel -> Bool)
allowedVars) -- vv TODO: neverUnblock is not correct! What could trigger this eta expansion though?
                      (Blocker -> VerboseLevel -> VerboseKey -> OccursM Term
forall (m :: * -> *) a.
MonadTCM m =>
Blocker -> VerboseLevel -> VerboseKey -> m a
patternViolation' Blocker
neverUnblock VerboseLevel
70 (VerboseKey -> OccursM Term) -> VerboseKey -> OccursM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Disallowed var " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
i VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" 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 -> VerboseLevel -> TypeError
MetaCannotDependOn MetaId
m VerboseLevel
i)
                -- is a singleton type with unique inhabitant sv
                (Just Term
sv) -> Term -> OccursM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> OccursM Term) -> Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term
sv Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
          Lam ArgInfo
h Abs Term
f     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Abs Term)
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Term
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Abs Term)
forall t. Occurs t => t -> OccursM t
occurs Abs Term
f
          Level Level
l     -> Level -> Term
Level (Level -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
forall t. Occurs t => t -> OccursM t
occurs Level
l
          Lit Literal
l       -> Term -> OccursM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Dummy{}     -> Term -> OccursM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          DontCare Term
v  -> Term -> Term
dontCare (Term -> Term) -> OccursM Term -> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Relevance -> OccursM Term -> OccursM Term
forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance Relevance
Irrelevant (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs Term
v
          Def QName
d Elims
es    -> do
            QName -> OccursM ()
definitionCheck QName
d
            QName -> Elims -> Term
Def QName
d (Elims -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> Elims -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall b.
Occurs b =>
QName -> b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
occDef QName
d Elims
es
          Con ConHead
c ConInfo
ci Elims
vs -> do
            QName -> OccursM ()
definitionCheck (ConHead -> QName
conName ConHead
c)
            ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elims
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall a. Elims -> OccursM a -> OccursM a
conArgs Elims
vs (Elims -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall t. Occurs t => t -> OccursM t
occurs Elims
vs)  -- if strongly rigid, remain so, except with unreduced IApply arguments.
          Pi Dom Type
a Abs Type
b      -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi ((Dom Type, Abs Type) -> Term)
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM (Dom Type, Abs Type)
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Dom Type, Abs Type)
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM (Dom Type, Abs Type)
forall t. Occurs t => t -> OccursM t
occurs (Dom Type
a,Abs Type
b)
          Sort Sort
s      -> Sort -> Term
Sort (Sort -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Relevance
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance Relevance
NonStrict (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs Sort
s
          MetaV MetaId
m' Elims
es -> do
            MetaId
m' <- MetaId -> OccursM MetaId
metaCheck MetaId
m'

            Blocker -> OccursM Term -> OccursM Term
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
m') (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ do
                         -- If getting stuck here, we need to trigger wakeup if this meta is
                         -- solved.
              -- The arguments of a meta are in a flexible position
              (MetaId -> Elims -> Term
MetaV MetaId
m' (Elims -> Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> OccursM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall a. OccursM a -> OccursM a
flexibly (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall a b. (a -> b) -> a -> b
$ Elims -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Elims
forall t. Occurs t => t -> OccursM t
occurs Elims
es) OccursM Term -> (TCErr -> OccursM Term) -> OccursM Term
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do
                FreeEnv' () OccursExtra AllowedVar
ctx <- ReaderT
  (FreeEnv' () OccursExtra AllowedVar)
  TCM
  (FreeEnv' () OccursExtra AllowedVar)
forall r (m :: * -> *). MonadReader r m => m r
ask
                VerboseKey -> VerboseLevel -> TCM Doc -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.kill" VerboseLevel
25 (TCM Doc -> OccursM ()) -> TCM Doc -> OccursM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                  [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"error during flexible occurs check, we are " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ FlexRig' () -> VerboseKey
forall a. Show a => a -> VerboseKey
show (FreeEnv' () OccursExtra AllowedVar
ctx FreeEnv' () OccursExtra AllowedVar
-> Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
-> FlexRig' ()
forall o i. o -> Lens' i o -> i
^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
Lens' (FlexRig' ()) (FreeEnv' () OccursExtra AllowedVar)
lensFlexRig)
                  , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> VerboseKey
forall a. Show a => a -> VerboseKey
show TCErr
err
                  ]
                case TCErr
err of
                  -- On pattern violations try to remove offending
                  -- flexible occurrences (if not already in a flexible context)
                  PatternErr{} | Bool -> Bool
not (FreeEnv' () OccursExtra AllowedVar -> Bool
forall a o. LensFlexRig a o => o -> Bool
isFlexible FreeEnv' () OccursExtra AllowedVar
ctx) -> do
                    VerboseKey -> VerboseLevel -> VerboseKey -> OccursM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.meta.kill" VerboseLevel
20 (VerboseKey -> OccursM ()) -> VerboseKey -> OccursM ()
forall a b. (a -> b) -> a -> b
$
                      VerboseKey
"oops, pattern violation for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m'
                    -- Andreas, 2014-03-02, see issue 1070:
                    -- Do not prune when meta is projected!
                    Maybe [Arg Term]
-> OccursM Term -> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es) (TCErr -> OccursM Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err) (([Arg Term] -> OccursM Term) -> OccursM Term)
-> ([Arg Term] -> OccursM Term) -> OccursM Term
forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
vs -> do
                      PruneResult
killResult <- TCM PruneResult
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM PruneResult
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM PruneResult
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM PruneResult)
-> ((VerboseLevel -> Bool) -> TCM PruneResult)
-> (VerboseLevel -> Bool)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM PruneResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> [Arg Term] -> (VerboseLevel -> Bool) -> TCM PruneResult
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
MetaId -> [Arg Term] -> (VerboseLevel -> Bool) -> m PruneResult
prune MetaId
m' [Arg Term]
vs ((VerboseLevel -> Bool)
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM PruneResult)
-> OccursM (VerboseLevel -> Bool)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM PruneResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccursM (VerboseLevel -> Bool)
allowedVars
                      if (PruneResult
killResult PruneResult -> PruneResult -> Bool
forall a. Eq a => a -> a -> Bool
== PruneResult
PrunedEverything)
                        -- after successful pruning, restart occurs check
                        then Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> OccursM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (MetaId -> Elims -> Term
MetaV MetaId
m' Elims
es)
                        else TCErr -> OccursM Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
                  TCErr
_ -> TCErr -> OccursM Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
          where
            -- a data or record type constructor propagates strong occurrences
            -- since e.g. x = List x is unsolvable
            occDef :: QName -> b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
occDef QName
d b
vs = do
              MetaId
m   <- (FreeEnv' () OccursExtra AllowedVar -> MetaId) -> OccursM MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OccursExtra -> MetaId
occMeta (OccursExtra -> MetaId)
-> (FreeEnv' () OccursExtra AllowedVar -> OccursExtra)
-> FreeEnv' () OccursExtra AllowedVar
-> MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeEnv' () OccursExtra AllowedVar -> OccursExtra
forall a b c. FreeEnv' a b c -> b
feExtra)
              TCM () -> OccursM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> OccursM ()) -> TCM () -> OccursM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m QName
d
              ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool)
-> TCM Bool
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Bool
forall a b. (a -> b) -> a -> b
$ Maybe DataOrRecord -> Bool
forall a. Maybe a -> Bool
isJust (Maybe DataOrRecord -> Bool)
-> TCMT IO (Maybe DataOrRecord) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe DataOrRecord)
isDataOrRecordType QName
d)
                {-then-} (b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall t. Occurs t => t -> OccursM t
occurs b
vs)
                {-else-} (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall a. OccursM a -> OccursM a
defArgs (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall a b. (a -> b) -> a -> b
$ b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall t. Occurs t => t -> OccursM t
occurs b
vs)

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

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

  metaOccurs :: MetaId -> QName -> TCM ()
metaOccurs MetaId
m QName
d = TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (QName -> TCM Bool
defNeedsChecking QName
d) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    QName -> TCM ()
tallyDef QName
d
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.meta.occurs" VerboseLevel
30 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Checking for occurrences in " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Show a => a -> VerboseKey
show QName
d
    MetaId -> QName -> TCM ()
metaOccursQName MetaId
m QName
d

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

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

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

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

  metaOccurs :: MetaId -> Clause -> TCM ()
metaOccurs MetaId
m = MetaId -> Maybe Term -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (Maybe Term -> TCM ())
-> (Clause -> Maybe Term) -> Clause -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody

instance Occurs Level where
  occurs :: Level -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
occurs (Max Integer
n [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level)
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM [PlusLevel' Term]
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term]
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM [PlusLevel' Term]
forall t. Occurs t => t -> OccursM t
occurs [PlusLevel' Term]
as

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

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

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

instance Occurs Type where
  occurs :: Type -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Type
occurs (El Sort
s Term
v) = (Sort -> Term -> Type) -> (Sort, Term) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El ((Sort, Term) -> Type)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Sort, Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sort, Term)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Sort, Term)
forall t. Occurs t => t -> OccursM t
occurs (Sort
s,Term
v)

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

instance Occurs Sort where
  occurs :: Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
occurs Sort
s = do
    Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. (Instantiate t, Reduce t) => t -> OccursM t
unfold Sort
s ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
        Sort
s1' <- ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a. OccursM a -> OccursM a
flexibly (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs Sort
s1
        Dom' Term Term
a'  <- (Dom' Term Term
a Dom' Term Term -> Term -> Dom' Term Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) (Term -> Dom' Term Term)
-> OccursM Term
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM (Dom' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do OccursM Term -> OccursM Term
forall a. OccursM a -> OccursM a
flexibly (OccursM Term -> OccursM Term) -> OccursM Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (Term -> OccursM Term) -> Term -> OccursM Term
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
a
        Abs Sort
s2' <- Dom Type
-> (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Abs Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Abs Sort)
forall a b (m :: * -> *).
(Subst a, Subst b, MonadAddContext m) =>
Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
mapAbstraction (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s1' (Term -> Type) -> Dom' Term Term -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term
a') (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a. OccursM a -> OccursM a
flexibly (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs) Abs Sort
s2
        Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom' Term Term
a' Sort
s1' Abs Sort
s2'
      FunSort Sort
s1 Sort
s2 -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a. OccursM a -> OccursM a
flexibly (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs Sort
s1) ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (Sort -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a. OccursM a -> OccursM a
flexibly (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs Sort
s2)
      Type Level
a     -> Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
forall t. Occurs t => t -> OccursM t
occurs Level
a
      Prop Level
a     -> Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
forall t. Occurs t => t -> OccursM t
occurs Level
a
      s :: Sort
s@Inf{}    -> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
      SSet Level
a     -> Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Level
forall t. Occurs t => t -> OccursM t
occurs Level
a
      s :: Sort
s@Sort
SizeUniv -> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
      s :: Sort
s@Sort
LockUniv -> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
      UnivSort Sort
s -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a. OccursM a -> OccursM a
flexibly (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall t. Occurs t => t -> OccursM t
occurs Sort
s
      MetaS MetaId
x Elims
es -> do
        MetaV MetaId
x Elims
es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es)
        Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x Elims
es
      DefS QName
x Elims
es -> do
        Def QName
x Elims
es <- Term -> OccursM Term
forall t. Occurs t => t -> OccursM t
occurs (QName -> Elims -> Term
Def QName
x Elims
es)
        Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort)
-> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
x Elims
es
      DummyS{}   -> Sort -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s

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

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

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

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

  metaOccurs :: MetaId -> Abs a -> TCM ()
metaOccurs MetaId
m (Abs   VerboseKey
_ a
x) = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m a
x
  metaOccurs MetaId
m (NoAbs VerboseKey
_ a
x) = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m a
x

instance Occurs a => Occurs (Arg a) where
  occurs :: Arg a -> OccursM (Arg a)
occurs (Arg ArgInfo
info a
v) = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (a -> Arg a)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
-> OccursM (Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do ArgInfo
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality ArgInfo
info (ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
 -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a)
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall a b. (a -> b) -> a -> b
$ a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall t. Occurs t => t -> OccursM t
occurs a
v
  metaOccurs :: MetaId -> Arg a -> TCM ()
metaOccurs MetaId
m = MetaId -> a -> TCM ()
forall t. Occurs t => MetaId -> t -> TCM ()
metaOccurs MetaId
m (a -> TCM ()) -> (Arg a -> a) -> Arg a -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance Occurs a => Occurs (Dom a) where
instance Occurs a => Occurs [a] where
instance Occurs a => Occurs (Maybe a) where

instance (Occurs a, Occurs b) => Occurs (a,b) where
  occurs :: (a, b) -> OccursM (a, b)
occurs (a
x,b
y) = (,) (a -> b -> (a, b))
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall t. Occurs t => t -> OccursM t
occurs a
x ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (b -> (a, b))
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> OccursM (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall t. Occurs t => t -> OccursM t
occurs b
y

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

instance (Occurs a, Occurs b, Occurs c) => Occurs (a,b,c) where
  occurs :: (a, b, c) -> OccursM (a, b, c)
occurs (a
x,b
y,c
z) = (,,) (a -> b -> c -> (a, b, c))
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM a
forall t. Occurs t => t -> OccursM t
occurs a
x ReaderT
  (FreeEnv' () OccursExtra AllowedVar) TCM (b -> c -> (a, b, c))
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
-> ReaderT
     (FreeEnv' () OccursExtra AllowedVar) TCM (c -> (a, b, c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM b
forall t. Occurs t => t -> OccursM t
occurs b
y ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM (c -> (a, b, c))
-> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM c
-> OccursM (a, b, c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> ReaderT (FreeEnv' () OccursExtra AllowedVar) TCM c
forall t. Occurs t => t -> OccursM t
occurs c
z

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance AnyRigid a => AnyRigid (Arg a) where
  anyRigid :: (VerboseLevel -> tcm Bool) -> Arg a -> tcm Bool
anyRigid VerboseLevel -> tcm Bool
f Arg a
a =
    case Arg a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
a of
      -- Irrelevant arguments are definitionally equal to
      -- values, so the variables there are not considered
      -- "definitely rigid".
      Relevance
Irrelevant -> Bool -> tcm Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Relevance
_          -> (VerboseLevel -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(VerboseLevel -> tcm Bool) -> a -> tcm Bool
anyRigid VerboseLevel -> 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 :: (VerboseLevel -> tcm Bool) -> Dom a -> tcm Bool
anyRigid VerboseLevel -> tcm Bool
f Dom a
dom = (VerboseLevel -> tcm Bool) -> a -> tcm Bool
forall a (tcm :: * -> *).
(AnyRigid a, PureTCM tcm) =>
(VerboseLevel -> tcm Bool) -> a -> tcm Bool
anyRigid VerboseLevel -> tcm Bool
f (a -> tcm Bool) -> a -> tcm Bool
forall a b. (a -> b) -> a -> b
$ Dom a -> a
forall t e. Dom' t e -> e
unDom Dom a
dom

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

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

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


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

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

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

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

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

  -- Then recurse over the telescope (right-to-left), building up the final type.
  (IntSet
killed, Type
b) <- [Dom (VerboseKey, Type)] -> IntSet -> Type -> m (IntSet, Type)
forall (m :: * -> *).
MonadReduce m =>
[Dom (VerboseKey, Type)] -> IntSet -> Type -> m (IntSet, Type)
go ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a. [a] -> [a]
reverse ([Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)])
-> [Dom (VerboseKey, Type)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> a -> b
$ ((Dom (VerboseKey, Type), Bool) -> Dom (VerboseKey, Type))
-> [(Dom (VerboseKey, Type), Bool)] -> [Dom (VerboseKey, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Dom (VerboseKey, Type), Bool) -> Dom (VerboseKey, Type)
forall a b. (a, b) -> a
fst [(Dom (VerboseKey, Type), Bool)]
args) IntSet
tokill Type
b

  -- Turn the IntSet of killed variables into the list of Arg Bool's to return.
  let kills :: [Arg Bool]
kills = [ ArgInfo -> Bool -> Arg Bool
forall e. ArgInfo -> e -> Arg e
Arg (Dom (VerboseKey, Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom (VerboseKey, Type)
dom) (VerboseLevel -> IntSet -> Bool
IntSet.member VerboseLevel
i IntSet
killed)
              | (VerboseLevel
i, (Dom (VerboseKey, Type)
dom, Bool
_)) <- [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
-> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
forall a. [a] -> [a]
reverse ([(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
 -> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))])
-> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
-> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
forall a b. (a -> b) -> a -> b
$ [VerboseLevel]
-> [(Dom (VerboseKey, Type), Bool)]
-> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] ([(Dom (VerboseKey, Type), Bool)]
 -> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))])
-> [(Dom (VerboseKey, Type), Bool)]
-> [(VerboseLevel, (Dom (VerboseKey, Type), Bool))]
forall a b. (a -> b) -> a -> b
$ [(Dom (VerboseKey, Type), Bool)]
-> [(Dom (VerboseKey, Type), Bool)]
forall a. [a] -> [a]
reverse [(Dom (VerboseKey, Type), Bool)]
args ]
  ([Arg Bool], Type) -> m ([Arg Bool], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Bool]
kills, Type
b)
  where
    down :: IntSet -> IntSet
down = (VerboseLevel -> VerboseLevel) -> IntSet -> IntSet
IntSet.map VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
pred
    up :: IntSet -> IntSet
up   = (VerboseLevel -> VerboseLevel) -> IntSet -> IntSet
IntSet.map VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
succ

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

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

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