    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Monad.MetaVars where

    import Prelude hiding (null)

    import Control.Monad.Except         ( ExceptT, MonadError )
    import Control.Monad.State          ( StateT, execStateT, get, put )
    import Control.Monad.Trans          ( MonadTrans, lift )
    import Control.Monad.Trans.Identity ( IdentityT )
    import Control.Monad.Trans.Maybe    ( MaybeT )
    import Control.Monad.Reader         ( ReaderT(ReaderT), runReaderT )
    import Control.Monad.Writer         ( WriterT, execWriterT, tell )

    import qualified Data.HashMap.Strict as HMap
    import qualified Data.List as List
    import qualified Data.Map.Strict as MapS
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Foldable as Fold

    import GHC.Stack (HasCallStack)

    import Agda.Syntax.Common
    import Agda.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta), MetaNameSuggestion )
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Common.Pretty (prettyShow)

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin (HasBuiltins)
    import Agda.TypeChecking.Monad.Trace
    import Agda.TypeChecking.Monad.Closure
    import Agda.TypeChecking.Monad.Constraints (MonadConstraint(..))
    import Agda.TypeChecking.Monad.Debug
      (MonadDebug, reportSLn, __IMPOSSIBLE_VERBOSE__)
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Signature (HasConstInfo)
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Substitute
    import {-# SOURCE #-} Agda.TypeChecking.Telescope

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Functor ((<.>))
    import Agda.Utils.Lens
    import Agda.Utils.List (nubOn)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Tuple
    import qualified Agda.Utils.Maybe.Strict as Strict

    import Agda.Utils.Impossible

    -- | Various classes of metavariables.

    data MetaClass =
        Records
        -- ^ Meta variables of record type.
      | SingletonRecords
        -- ^ Meta variables of \"hereditarily singleton\" record type.
      | Levels
        -- ^ Meta variables of level type, if type-in-type is activated.
      deriving (MetaClass -> MetaClass -> Bool
    (MetaClass -> MetaClass -> Bool)
    -> (MetaClass -> MetaClass -> Bool) -> Eq MetaClass
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: MetaClass -> MetaClass -> Bool
    == :: MetaClass -> MetaClass -> Bool
    $c/= :: MetaClass -> MetaClass -> Bool
    /= :: MetaClass -> MetaClass -> Bool
    Eq, Int -> MetaClass
    MetaClass -> Int
    MetaClass -> [MetaClass]
    MetaClass -> MetaClass
    MetaClass -> MetaClass -> [MetaClass]
    MetaClass -> MetaClass -> MetaClass -> [MetaClass]
    (MetaClass -> MetaClass)
    -> (MetaClass -> MetaClass)
    -> (Int -> MetaClass)
    -> (MetaClass -> Int)
    -> (MetaClass -> [MetaClass])
    -> (MetaClass -> MetaClass -> [MetaClass])
    -> (MetaClass -> MetaClass -> [MetaClass])
    -> (MetaClass -> MetaClass -> MetaClass -> [MetaClass])
    -> Enum MetaClass
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: MetaClass -> MetaClass
    succ :: MetaClass -> MetaClass
    $cpred :: MetaClass -> MetaClass
    pred :: MetaClass -> MetaClass
    $ctoEnum :: Int -> MetaClass
    toEnum :: Int -> MetaClass
    $cfromEnum :: MetaClass -> Int
    fromEnum :: MetaClass -> Int
    $cenumFrom :: MetaClass -> [MetaClass]
    enumFrom :: MetaClass -> [MetaClass]
    $cenumFromThen :: MetaClass -> MetaClass -> [MetaClass]
    enumFromThen :: MetaClass -> MetaClass -> [MetaClass]
    $cenumFromTo :: MetaClass -> MetaClass -> [MetaClass]
    enumFromTo :: MetaClass -> MetaClass -> [MetaClass]
    $cenumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
    enumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
    Enum, MetaClass
    MetaClass -> MetaClass -> Bounded MetaClass
    forall a. a -> a -> Bounded a
    $cminBound :: MetaClass
    minBound :: MetaClass
    $cmaxBound :: MetaClass
    maxBound :: MetaClass
    Bounded, Int -> MetaClass -> [Char] -> [Char]
    [MetaClass] -> [Char] -> [Char]
    MetaClass -> [Char]
    (Int -> MetaClass -> [Char] -> [Char])
    -> (MetaClass -> [Char])
    -> ([MetaClass] -> [Char] -> [Char])
    -> Show MetaClass
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> MetaClass -> [Char] -> [Char]
    showsPrec :: Int -> MetaClass -> [Char] -> [Char]
    $cshow :: MetaClass -> [Char]
    show :: MetaClass -> [Char]
    $cshowList :: [MetaClass] -> [Char] -> [Char]
    showList :: [MetaClass] -> [Char] -> [Char]
    Show)

    -- | All possible metavariable classes.

    allMetaClasses :: [MetaClass]
    allMetaClasses :: [MetaClass]
    allMetaClasses = [MetaClass
    forall a. Bounded a => a
    minBound .. MetaClass
    forall a. Bounded a => a
    maxBound]

    data KeepMetas = KeepMetas | RollBackMetas

    -- | Monad service class for creating, solving and eta-expanding of
    --   metavariables.
    class ( MonadConstraint m
          , MonadReduce m
          , MonadAddContext m
          , MonadTCEnv m
          , ReadTCState m
          , HasBuiltins m
          , HasConstInfo m
          , MonadDebug m
          ) => MonadMetaSolver m where
      -- | Generate a new meta variable with some instantiation given.
      --   For instance, the instantiation could be a 'PostponedTypeCheckingProblem'.
      newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
                  Judgement a -> m MetaId

      -- * Solve constraint @x vs = v@.

      -- | Assign to an open metavar which may not be frozen.
      --   First check that metavar args are in pattern fragment.
      --     Then do extended occurs check on given thing.
      --
      --   Assignment is aborted by throwing a @PatternErr@ via a call to
      --   @patternViolation@.  This error is caught by @catchConstraint@
      --   during equality checking (@compareAtom@) and leads to
      --   restoration of the original constraints.
      assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()

      -- | Directly instantiate the metavariable. Skip pattern check,
      -- occurs check and frozen check. Used for eta expanding frozen
      -- metas.
      assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()

      -- | Eta-expand a local meta-variable, if it is of the specified
      -- class. Don't do anything if the meta-variable is a blocked term.
      etaExpandMeta :: [MetaClass] -> MetaId -> m ()

      -- | Update the status of the metavariable
      updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()

      -- | 'speculateMetas fallback m' speculatively runs 'm', but if the
      --    result is 'RollBackMetas' any changes to metavariables are
      --    rolled back and 'fallback' is run instead.
      speculateMetas :: m () -> m KeepMetas -> m ()

    instance MonadMetaSolver m => MonadMetaSolver (ReaderT r m) where
      newMeta' :: forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> ReaderT r m MetaId
    newMeta' MetaInstantiation
    inst Frozen
    f MetaInfo
    i MetaPriority
    p Permutation
    perm Judgement a
    j = m MetaId -> ReaderT r m MetaId
    forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m MetaId -> ReaderT r m MetaId) -> m MetaId -> ReaderT r m MetaId
    forall a b. (a -> b) -> a -> b
    $ MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    forall (m :: * -> *) a.
    MonadMetaSolver m =>
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta' MetaInstantiation
    inst Frozen
    f MetaInfo
    i MetaPriority
    p Permutation
    perm Judgement a
    j
      assignV :: CompareDirection
    -> MetaId -> Args -> Term -> CompareAs -> ReaderT r m ()
    assignV CompareDirection
    dir MetaId
    m Args
    us Term
    v CompareAs
    cmp = m () -> ReaderT r m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
    forall a b. (a -> b) -> a -> b
    $ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
    assignV CompareDirection
    dir MetaId
    m Args
    us Term
    v CompareAs
    cmp
      assignTerm' :: MonadMetaSolver (ReaderT r m) =>
    MetaId -> [Arg [Char]] -> Term -> ReaderT r m ()
    assignTerm' MetaId
    m [Arg [Char]]
    us Term
    v = m () -> ReaderT r m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> [Arg [Char]] -> Term -> m ()
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadMetaSolver m) =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm' MetaId
    m [Arg [Char]]
    us Term
    v
      etaExpandMeta :: [MetaClass] -> MetaId -> ReaderT r m ()
    etaExpandMeta [MetaClass]
    k MetaId
    m = m () -> ReaderT r m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
    forall a b. (a -> b) -> a -> b
    $ [MetaClass] -> MetaId -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [MetaClass] -> MetaId -> m ()
    etaExpandMeta [MetaClass]
    k MetaId
    m
      updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> ReaderT r m ()
    updateMetaVar MetaId
    m MetaVariable -> MetaVariable
    f = m () -> ReaderT r m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m MetaVariable -> MetaVariable
    f
      speculateMetas :: ReaderT r m () -> ReaderT r m KeepMetas -> ReaderT r m ()
    speculateMetas ReaderT r m ()
    fallback ReaderT r m KeepMetas
    m = (r -> m ()) -> ReaderT r m ()
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((r -> m ()) -> ReaderT r m ()) -> (r -> m ()) -> ReaderT r m ()
    forall a b. (a -> b) -> a -> b
    $ \r
    x -> m () -> m KeepMetas -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    m () -> m KeepMetas -> m ()
    speculateMetas (ReaderT r m () -> r -> m ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT r m ()
    fallback r
    x) (ReaderT r m KeepMetas -> r -> m KeepMetas
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT r m KeepMetas
    m r
    x)

    -- | Switch off assignment of metas.
    dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
    dontAssignMetas :: forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas m a
    cont = do
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta" Int
    45 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "don't assign metas"
      (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    env -> TCEnv
    env { envAssignMetas = False }) m a
    cont

    -- | Is the meta-variable from another top-level module?

    isRemoteMeta :: ReadTCState m => m (MetaId -> Bool)
    isRemoteMeta :: forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
    isRemoteMeta = do
      h <- m ModuleNameHash
    forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash
      return (\MetaId
    m -> ModuleNameHash
    h ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    /= MetaId -> ModuleNameHash
    metaModule MetaId
    m)

    -- | If another meta-variable is created, then it will get this
    -- 'MetaId' (unless the state is changed too much, for instance by
    -- 'setTopLevelModule').

    nextLocalMeta :: ReadTCState m => m MetaId
    nextLocalMeta :: forall (m :: * -> *). ReadTCState m => m MetaId
    nextLocalMeta = Lens' TCState MetaId -> m MetaId
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (MetaId -> f MetaId) -> TCState -> f TCState
    Lens' TCState MetaId
    stFreshMetaId

    -- | Pairs of local meta-stores.

    data LocalMetaStores = LocalMetaStores
      { LocalMetaStores -> LocalMetaStore
    openMetas :: LocalMetaStore
        -- ^ A 'MetaStore' containing open meta-variables.
      , LocalMetaStores -> LocalMetaStore
    solvedMetas :: LocalMetaStore
        -- ^ A 'MetaStore' containing instantiated meta-variables.
      }

    -- | Run a computation and record which new metas it created.
    metasCreatedBy ::
      forall m a. ReadTCState m => m a -> m (a, LocalMetaStores)
    metasCreatedBy :: forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy m a
    m = do
      !nextMeta <- m MetaId
    forall (m :: * -> *). ReadTCState m => m MetaId
    nextLocalMeta
      a         <- m
      os        <- created stOpenMetaStore   nextMeta
      ss        <- created stSolvedMetaStore nextMeta
      return (a, LocalMetaStores { openMetas = os, solvedMetas = ss })
      where
      created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
      created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
    created Lens' TCState LocalMetaStore
    store MetaId
    next = do
        ms <- Lens' TCState LocalMetaStore -> m LocalMetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    store
        return $ case MapS.splitLookup next ms of
          (LocalMetaStore
    _, Maybe MetaVariable
    Nothing, LocalMetaStore
    ms) -> LocalMetaStore
    ms
          (LocalMetaStore
    _, Just MetaVariable
    m,  LocalMetaStore
    ms) -> MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert MetaId
    next MetaVariable
    m LocalMetaStore
    ms

    -- | Find information about the given local meta-variable, if any.

    lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' MetaId
    m = do
      mv <- LocalMetaStore -> Maybe MetaVariable
    lkup (LocalMetaStore -> Maybe MetaVariable)
    -> m LocalMetaStore -> m (Maybe MetaVariable)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState LocalMetaStore -> m LocalMetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stSolvedMetaStore
      case mv of
        mv :: Maybe MetaVariable
    mv@Just{} -> Maybe MetaVariable -> m (Maybe MetaVariable)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe MetaVariable
    mv
        Maybe MetaVariable
    Nothing   -> LocalMetaStore -> Maybe MetaVariable
    lkup (LocalMetaStore -> Maybe MetaVariable)
    -> m LocalMetaStore -> m (Maybe MetaVariable)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState LocalMetaStore -> m LocalMetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore
      where
      lkup :: LocalMetaStore -> Maybe MetaVariable
    lkup = MetaId -> LocalMetaStore -> Maybe MetaVariable
    forall k a. Ord k => k -> Map k a -> Maybe a
    MapS.lookup MetaId
    m

    -- | Find information about the given local meta-variable.

    lookupLocalMeta ::
      (HasCallStack, MonadDebug m, ReadTCState m) =>
      MetaId -> m MetaVariable
    lookupLocalMeta :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m =
      m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM ([Char] -> m MetaVariable
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    err) (m (Maybe MetaVariable) -> m MetaVariable)
    -> m (Maybe MetaVariable) -> m MetaVariable
    forall a b. (a -> b) -> a -> b
    $ MetaId -> m (Maybe MetaVariable)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' MetaId
    m
      where
      err :: [Char]
    err = [Char]
    "no such local meta-variable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m

    -- | Find information about the (local or remote) meta-variable, if
    -- any.
    --
    -- If no meta-variable is found, then the reason could be that the
    -- dead-code elimination
    -- ('Agda.TypeChecking.DeadCode.eliminateDeadCode') failed to find the
    -- meta-variable, perhaps because some 'NamesIn' instance is
    -- incorrectly defined.

    {-# SPECIALIZE lookupMeta :: MetaId -> TCM (Maybe (Either RemoteMetaVariable MetaVariable)) #-}
    lookupMeta ::
      ReadTCState m =>
      MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m = do
      mv <- MetaId -> m (Maybe MetaVariable)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' MetaId
    m
      case mv of
        Just MetaVariable
    mv -> Maybe (Either RemoteMetaVariable MetaVariable)
    -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either RemoteMetaVariable MetaVariable
    -> Maybe (Either RemoteMetaVariable MetaVariable)
    forall a. a -> Maybe a
    Just (MetaVariable -> Either RemoteMetaVariable MetaVariable
    forall a b. b -> Either a b
    Right MetaVariable
    mv))
        Maybe MetaVariable
    Nothing -> (RemoteMetaVariable -> Either RemoteMetaVariable MetaVariable)
    -> Maybe RemoteMetaVariable
    -> Maybe (Either RemoteMetaVariable MetaVariable)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RemoteMetaVariable -> Either RemoteMetaVariable MetaVariable
    forall a b. a -> Either a b
    Left (Maybe RemoteMetaVariable
     -> Maybe (Either RemoteMetaVariable MetaVariable))
    -> (HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable)
    -> HashMap MetaId RemoteMetaVariable
    -> Maybe (Either RemoteMetaVariable MetaVariable)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId
    -> HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup MetaId
    m (HashMap MetaId RemoteMetaVariable
     -> Maybe (Either RemoteMetaVariable MetaVariable))
    -> m (HashMap MetaId RemoteMetaVariable)
    -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (HashMap MetaId RemoteMetaVariable)
    -> m (HashMap MetaId RemoteMetaVariable)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (HashMap MetaId RemoteMetaVariable
     -> f (HashMap MetaId RemoteMetaVariable))
    -> TCState -> f TCState
    Lens' TCState (HashMap MetaId RemoteMetaVariable)
    stImportedMetaStore

    -- | Find the meta-variable's instantiation.

    {-# SPECIALIZE lookupMetaInstantiation :: MetaId -> TCM MetaInstantiation #-}
    lookupMetaInstantiation ::
      ReadTCState m => MetaId -> m MetaInstantiation
    lookupMetaInstantiation :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m = do
      mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m
      case mi of
        Just (Left RemoteMetaVariable
    mv)  -> MetaInstantiation -> m MetaInstantiation
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Instantiation -> MetaInstantiation
    InstV (Instantiation -> MetaInstantiation)
    -> Instantiation -> MetaInstantiation
    forall a b. (a -> b) -> a -> b
    $ RemoteMetaVariable -> Instantiation
    rmvInstantiation RemoteMetaVariable
    mv)
        Just (Right MetaVariable
    mv) -> MetaInstantiation -> m MetaInstantiation
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv)
        Maybe (Either RemoteMetaVariable MetaVariable)
    Nothing         -> m MetaInstantiation
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Find the meta-variable's judgement.

    lookupMetaJudgement :: ReadTCState m => MetaId -> m (Judgement MetaId)
    lookupMetaJudgement :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Judgement MetaId)
    lookupMetaJudgement MetaId
    m = do
      mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m
      case mi of
        Just (Left RemoteMetaVariable
    mv)  -> Judgement MetaId -> m (Judgement MetaId)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RemoteMetaVariable -> Judgement MetaId
    rmvJudgement RemoteMetaVariable
    mv)
        Just (Right MetaVariable
    mv) -> Judgement MetaId -> m (Judgement MetaId)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv)
        Maybe (Either RemoteMetaVariable MetaVariable)
    Nothing         -> m (Judgement MetaId)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Find the meta-variable's modality.

    lookupMetaModality :: ReadTCState m => MetaId -> m Modality
    lookupMetaModality :: forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
    lookupMetaModality MetaId
    m = do
      mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m
      case mi of
        Just (Left RemoteMetaVariable
    mv)  -> Modality -> m Modality
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RemoteMetaVariable -> Modality
    rmvModality RemoteMetaVariable
    mv)
        Just (Right MetaVariable
    mv) -> Modality -> m Modality
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MetaVariable -> Modality
    forall a. LensModality a => a -> Modality
    getModality MetaVariable
    mv)
        Maybe (Either RemoteMetaVariable MetaVariable)
    Nothing         -> m Modality
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# INLINE metaType #-}
    -- | The type of a term or sort meta-variable.
    metaType :: ReadTCState m => MetaId -> m Type
    metaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> m (Judgement MetaId) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m (Judgement MetaId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Judgement MetaId)
    lookupMetaJudgement MetaId
    x

    -- | Update the information associated with a local meta-variable.
    updateMetaVarTCM ::
      HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM :: HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM MetaId
    m MetaVariable -> MetaVariable
    f = do
      mv <- MetaId -> TCMT IO (Maybe MetaVariable)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' MetaId
    m
      case mv of
        Maybe MetaVariable
    Nothing -> do
          mv <- MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
    lookupMeta MetaId
    m
          case mv of
            Maybe (Either RemoteMetaVariable MetaVariable)
    Nothing -> [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__
                         ([Char]
    "Meta-variable not found: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m)
            Just{}  -> [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__
                         ([Char]
    "Attempt to update remote meta-variable: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                          MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m)
        Just MetaVariable
    mv -> do
          let mv' :: MetaVariable
    mv'    = MetaVariable -> MetaVariable
    f MetaVariable
    mv
              insert :: Lens' TCState LocalMetaStore -> TCM ()
    insert = (Lens' TCState LocalMetaStore
    -> (LocalMetaStore -> LocalMetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert MetaId
    m MetaVariable
    mv')
              delete :: Lens' TCState LocalMetaStore -> TCM ()
    delete = (Lens' TCState LocalMetaStore
    -> (LocalMetaStore -> LocalMetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` MetaId -> LocalMetaStore -> LocalMetaStore
    forall k a. Ord k => k -> Map k a -> Map k a
    MapS.delete MetaId
    m)
          case ( MetaInstantiation -> Bool
    isOpenMeta (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv)
               , MetaInstantiation -> Bool
    isOpenMeta (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv')
               ) of
            (Bool
    True,  Bool
    True)  -> Lens' TCState LocalMetaStore -> TCM ()
    insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore
            (Bool
    False, Bool
    False) -> Lens' TCState LocalMetaStore -> TCM ()
    insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stSolvedMetaStore
            (Bool
    True,  Bool
    False) -> do
              Lens' TCState LocalMetaStore -> TCM ()
    delete (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore
              Lens' TCState LocalMetaStore -> TCM ()
    insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stSolvedMetaStore
            (Bool
    False, Bool
    True)  -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Insert a new meta-variable with associated information into the
    -- local meta store.
    insertMetaVar :: MetaId -> MetaVariable -> TCM ()
    insertMetaVar :: MetaId -> MetaVariable -> TCM ()
    insertMetaVar MetaId
    m MetaVariable
    mv
      | MetaInstantiation -> Bool
    isOpenMeta (MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv) = Lens' TCState LocalMetaStore -> TCM ()
    insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore
      | Bool
    otherwise                       = Lens' TCState LocalMetaStore -> TCM ()
    insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stSolvedMetaStore
      where
      insert :: Lens' TCState LocalMetaStore -> TCM ()
    insert = (Lens' TCState LocalMetaStore
    -> (LocalMetaStore -> LocalMetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert MetaId
    m MetaVariable
    mv)

    {-# INLINE getMetaPriority #-}
    -- | Returns the 'MetaPriority' of the given local meta-variable.
    getMetaPriority ::
      (HasCallStack, MonadDebug m, ReadTCState m) =>
      MetaId -> m MetaPriority
    getMetaPriority :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaPriority
    getMetaPriority = MetaVariable -> MetaPriority
    mvPriority (MetaVariable -> MetaPriority)
    -> (MetaId -> m MetaVariable) -> MetaId -> m MetaPriority
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta

    isSortMeta :: ReadTCState m => MetaId -> m Bool
    isSortMeta :: forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
    isSortMeta MetaId
    m = Judgement MetaId -> Bool
    forall a. Judgement a -> Bool
    isSortJudgement (Judgement MetaId -> Bool) -> m (Judgement MetaId) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m (Judgement MetaId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Judgement MetaId)
    lookupMetaJudgement MetaId
    m

    isSortMeta_ :: MetaVariable -> Bool
    isSortMeta_ :: MetaVariable -> Bool
    isSortMeta_ MetaVariable
    mv = Judgement MetaId -> Bool
    forall a. Judgement a -> Bool
    isSortJudgement (MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv)

    isSortJudgement :: Judgement a -> Bool
    isSortJudgement :: forall a. Judgement a -> Bool
    isSortJudgement HasType{} = Bool
    False
    isSortJudgement IsSort{}  = Bool
    True

    -- | If a meta variable is still open, what is its kind?
    --
    metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
    metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
    metaInstantiationToMetaKind = \case
      OpenMeta MetaKind
    k                     -> MetaKind
    k
      InstV{}                        -> MetaKind
    forall a. Null a => a
    empty
      BlockedConst{}                 -> MetaKind
    forall a. Null a => a
    empty
      PostponedTypeCheckingProblem{} -> MetaKind
    forall a. Null a => a
    empty

    {-# SPECIALIZE getMetaType :: MetaId -> TCM Type #-}
    getMetaType :: ReadTCState m => MetaId -> m Type
    getMetaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType MetaId
    m = do
      j <- MetaId -> m (Judgement MetaId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Judgement MetaId)
    lookupMetaJudgement MetaId
    m
      return $ case j of
        HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } -> Type
    t
        IsSort{}  -> Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# SPECIALIZE getMetaContextArgs :: MetaVariable -> TCM Args #-}
    -- | Compute the context variables that a local meta-variable should
    -- be applied to, accounting for pruning.
    getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs :: forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVar{ mvPermutation :: MetaVariable -> Permutation
    mvPermutation = Permutation
    p } = do
      args <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      return $ permute (takeP (length args) p) args

    {-# SPECIALIZE getMetaTypeInContext :: MetaId -> TCM Type #-}
    -- | Given a local meta-variable, return the type applied to the
    -- current context.
    getMetaTypeInContext ::
      (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
       MonadTCEnv m, ReadTCState m) =>
      MetaId -> m Type
    getMetaTypeInContext :: forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m = do
      mv@MetaVar{ mvJudgement = j } <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      case j of
        HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } -> Type -> Args -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    Type -> Args -> m Type
    piApplyM Type
    t (Args -> m Type) -> m Args -> m Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaVariable -> m Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    mv
        IsSort{}                 -> m Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-# SPECIALIZE isGeneralizableMeta :: MetaId -> TCM DoGeneralize #-}
    -- | Is it a local meta-variable that might be generalized?
    isGeneralizableMeta ::
      (HasCallStack, MonadDebug m, ReadTCState m) =>
      MetaId -> m DoGeneralize
    isGeneralizableMeta :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m DoGeneralize
    isGeneralizableMeta MetaId
    x =
      Arg DoGeneralize -> DoGeneralize
    forall e. Arg e -> e
    unArg (Arg DoGeneralize -> DoGeneralize)
    -> (MetaVariable -> Arg DoGeneralize)
    -> MetaVariable
    -> DoGeneralize
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaInfo -> Arg DoGeneralize
    miGeneralizable (MetaInfo -> Arg DoGeneralize)
    -> (MetaVariable -> MetaInfo) -> MetaVariable -> Arg DoGeneralize
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> MetaInfo
    mvInfo (MetaVariable -> DoGeneralize) -> m MetaVariable -> m DoGeneralize
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x

    -- | Check whether all metas are instantiated.
    --   Precondition: argument is a meta (in some form) or a list of metas.
    class IsInstantiatedMeta a where
      isInstantiatedMeta :: (ReadTCState m) => a -> m Bool

    {-# SPECIALIZE isInstantiatedMeta :: Term -> TCM Bool #-}
    {-# SPECIALIZE isInstantiatedMeta :: Type -> TCM Bool #-}

    instance IsInstantiatedMeta MetaId where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
    isInstantiatedMeta MetaId
    m = Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m (Maybe Term)
    forall (m :: * -> *). ReadTCState m => MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    m

    instance IsInstantiatedMeta Term where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => Term -> m Bool
    isInstantiatedMeta = Term -> m Bool
    forall (m :: * -> *). ReadTCState m => Term -> m Bool
    loop where
       loop :: Term -> m Bool
    loop Term
    v =
        case Term
    v of
          MetaV MetaId
    x [Elim]
    _  -> MetaId -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
    isInstantiatedMeta MetaId
    x
          DontCare Term
    v -> Term -> m Bool
    loop Term
    v
          Level Level
    l    -> Level -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => Level -> m Bool
    isInstantiatedMeta Level
    l
          Lam ArgInfo
    _ Abs Term
    b    -> Abs Term -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => Abs Term -> m Bool
    isInstantiatedMeta Abs Term
    b
          Con ConHead
    _ ConInfo
    _ [Elim]
    es | Just Args
    vs <- [Elim] -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    es -> Args -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => Args -> m Bool
    isInstantiatedMeta Args
    vs
          Term
    _          -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta Level where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => Level -> m Bool
    isInstantiatedMeta (Max Integer
    n [PlusLevel' Term]
    ls) | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = [PlusLevel' Term] -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => [PlusLevel' Term] -> m Bool
    isInstantiatedMeta [PlusLevel' Term]
    ls
      isInstantiatedMeta Level
    _ = m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta PlusLevel where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => PlusLevel' Term -> m Bool
    isInstantiatedMeta (Plus Integer
    n Term
    l) | Integer
    n Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = Term -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => Term -> m Bool
    isInstantiatedMeta Term
    l
      isInstantiatedMeta PlusLevel' Term
    _ = m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => [a] -> m Bool
    isInstantiatedMeta = [m Bool] -> m Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m Bool) -> [a] -> [m Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => a -> m Bool
    isInstantiatedMeta

    instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => Maybe a -> m Bool
    isInstantiatedMeta = [a] -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => [a] -> m Bool
    isInstantiatedMeta ([a] -> m Bool) -> (Maybe a -> [a]) -> Maybe a -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe a -> [a]
    forall a. Maybe a -> [a]
    maybeToList

    instance IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => Arg a -> m Bool
    isInstantiatedMeta = a -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => a -> m Bool
    isInstantiatedMeta (a -> m Bool) -> (Arg a -> a) -> Arg a -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg a -> a
    forall e. Arg e -> e
    unArg

    -- | Does not worry about raising.
    instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where
      isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => Abs a -> m Bool
    isInstantiatedMeta = a -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => a -> m Bool
    isInstantiatedMeta (a -> m Bool) -> (Abs a -> a) -> Abs a -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Abs a -> a
    forall a. Abs a -> a
    unAbs

    {-# SPECIALIZE isInstantiatedMeta' :: MetaId -> TCM (Maybe Term) #-}
    isInstantiatedMeta' :: (ReadTCState m) => MetaId -> m (Maybe Term)
    isInstantiatedMeta' :: forall (m :: * -> *). ReadTCState m => MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    m = do
      inst <- MetaId -> m MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m
      return $ case inst of
        InstV Instantiation
    inst -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Arg [Char] -> Term -> Term
    mkLam (Instantiation -> Term
    instBody Instantiation
    inst) (Instantiation -> [Arg [Char]]
    instTel Instantiation
    inst)
        MetaInstantiation
    _          -> Maybe Term
    forall a. Maybe a
    Nothing

    -- | Returns all metavariables in a constraint. Slightly complicated by the
    --   fact that blocked terms are represented by two meta variables. To find the
    --   second one we need to look up the meta listeners for the one in the
    --   UnBlock constraint.
    --   This is used for the purpose of deciding if a metavariable is constrained or if it can be
    --   generalized over (see Agda.TypeChecking.Generalize).
    constraintMetas :: Constraint -> TCM (Set MetaId)
    constraintMetas :: Constraint -> TCM (Set MetaId)
    constraintMetas = \case
        -- We don't use allMetas here since some constraints should not stop us from generalizing. For
        -- instance CheckSizeLtSat (see #3694). We also have to check meta listeners to get metas of
        -- UnBlock constraints.
        -- #5147: Don't count metas in the type of a constraint. For instance the constraint u = v : t
        -- should not stop us from generalize metas in t, since we could never solve those metas based
        -- on that constraint alone.
          ValueCmp Comparison
    _ CompareAs
    _ Term
    u Term
    v         -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Term
    u, Term
    v)
          ValueCmpOnFace Comparison
    _ Term
    p Type
    _ Term
    u Term
    v -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Term, Term, Term) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> (Term, Term, Term) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Term
    p, Term
    u, Term
    v)
          ElimCmp [Polarity]
    _ [IsForced]
    _ Type
    _ Term
    _ [Elim]
    es [Elim]
    es'   -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> ([Elim], [Elim]) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> ([Elim], [Elim]) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton ([Elim]
    es, [Elim]
    es')
          LevelCmp Comparison
    _ Level
    l Level
    l'          -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Level -> Term
    Level Level
    l, Level -> Term
    Level Level
    l')
          UnquoteTactic Term
    t Term
    h Type
    g      -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Term, Term, Type) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> (Term, Term, Type) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Term
    t, Term
    h, Type
    g)
          SortCmp Comparison
    _ Sort
    s1 Sort
    s2          -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Sort -> Term
    Sort Sort
    s1, Sort -> Term
    Sort Sort
    s2)
          UnBlock MetaId
    x                -> MetaId -> Set MetaId -> Set MetaId
    forall a. Ord a => a -> Set a -> Set a
    Set.insert MetaId
    x (Set MetaId -> Set MetaId)
    -> ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Set MetaId] -> Set MetaId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set MetaId] -> Set MetaId)
    -> TCMT IO [Set MetaId] -> TCM (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Listener -> TCM (Set MetaId))
    -> [Listener] -> TCMT IO [Set MetaId]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Listener -> TCM (Set MetaId)
    listenerMetas ([Listener] -> TCMT IO [Set MetaId])
    -> TCMT IO [Listener] -> TCMT IO [Set MetaId]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> TCMT IO [Listener]
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m [Listener]
    getMetaListeners MetaId
    x)
          FindInstance Range
    _ MetaId
    x Maybe [Candidate]
    _       ->
            -- #5093: We should not generalize over metas bound by instance constraints.
            -- We keep instance constraints even if the meta is solved, to check that it could indeed
            -- be filled by instance search. If it's solved, look in the solution.
            TCMT IO (Maybe Term)
    -> TCM (Set MetaId)
    -> (Term -> TCM (Set MetaId))
    -> TCM (Set MetaId)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (MetaId -> TCMT IO (Maybe Term)
    forall (m :: * -> *). ReadTCState m => MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    x) (Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton MetaId
    x) ((Term -> TCM (Set MetaId)) -> TCM (Set MetaId))
    -> (Term -> TCM (Set MetaId)) -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId))
    -> (Term -> Set MetaId) -> Term -> TCM (Set MetaId)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Set MetaId) -> Term -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> Term -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton
          ResolveInstanceHead{}    -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          IsEmpty{}                -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckFunDef{}            -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckSizeLtSat{}         -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          HasBiggerSort{}          -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          HasPTSRule{}             -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckDataSort{}          -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckMetaInst MetaId
    x          -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckType Type
    t              -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> Type -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> Type -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton Type
    t
          CheckLockedVars Term
    a Type
    b Arg Term
    c Type
    d  -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId)
    -> (Term, Type, Arg Term, Type) -> Set MetaId
    forall m.
    Monoid m =>
    (MetaId -> m) -> (Term, Type, Arg Term, Type) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton (Term
    a, Type
    b, Arg Term
    c, Type
    d)
          UsableAtModality{}       -> Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
      where
        -- For blocked constant twin variables
        listenerMetas :: Listener -> TCM (Set MetaId)
    listenerMetas EtaExpand{}           = Set MetaId -> TCM (Set MetaId)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Set a
    Set.empty
        listenerMetas (CheckConstraint Int
    _ ProblemConstraint
    c) = Constraint -> TCM (Set MetaId)
    constraintMetas (Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> Closure Constraint -> Constraint
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c)

    -- | Create 'MetaInfo' in the current environment.
    createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
    createMetaInfo :: forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
    createMetaInfo = RunMetaOccursCheck -> m MetaInfo
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' RunMetaOccursCheck
    RunMetaOccursCheck

    createMetaInfo'
      :: (MonadTCEnv m, ReadTCState m)
      => RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' RunMetaOccursCheck
    b = do
      r        <- m Range
    forall (m :: * -> *). MonadTCEnv m => m Range
    getCurrentRange
      cl       <- buildClosure r
      gen      <- viewTC eGeneralizeMetas
      modality <- currentModality
      return MetaInfo
        { miClosRange       = cl
        , miModality        = modality
        , miMetaOccursCheck = b
        , miNameSuggestion  = ""
        , miGeneralizable   = defaultArg gen
                              -- The ArgInfo is set to the right value in
                              -- the newArgsMetaCtx' function.
        }

    setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
    setValueMetaName :: forall (m :: * -> *). MonadMetaSolver m => Term -> [Char] -> m ()
    setValueMetaName Term
    v [Char]
    s = do
      case Term
    v of
        MetaV MetaId
    mi [Elim]
    _ -> MetaId -> [Char] -> m ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
    setMetaNameSuggestion MetaId
    mi [Char]
    s
        Term
    u          -> do
          [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.name" Int
    70 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "cannot set meta name; newMeta returns " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    u
          () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    getMetaNameSuggestion ::
      (HasCallStack, MonadDebug m, ReadTCState m) =>
      MetaId -> m MetaNameSuggestion
    getMetaNameSuggestion :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m [Char]
    getMetaNameSuggestion MetaId
    mi =
      MetaInfo -> [Char]
    miNameSuggestion (MetaInfo -> [Char])
    -> (MetaVariable -> MetaInfo) -> MetaVariable -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> MetaInfo
    mvInfo (MetaVariable -> [Char]) -> m MetaVariable -> m [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    mi

    setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
    setMetaNameSuggestion :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
    setMetaNameSuggestion MetaId
    mi [Char]
    s = Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Char] -> Bool
    forall a. Null a => a -> Bool
    null [Char]
    s Bool -> Bool -> Bool
    || [Char] -> Bool
    forall a. Underscore a => a -> Bool
    isUnderscore [Char]
    s) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.name" Int
    20 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "setting name of meta " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    mi [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s
      MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    mi ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mvar ->
        MetaVariable
    mvar { mvInfo = (mvInfo mvar) { miNameSuggestion = s }}

    -- | Change the ArgInfo that will be used when generalizing over this
    -- local meta-variable.
    setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
    setMetaGeneralizableArgInfo :: forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> ArgInfo -> m ()
    setMetaGeneralizableArgInfo MetaId
    m ArgInfo
    i = MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mv ->
      MetaVariable
    mv { mvInfo = (mvInfo mv)
            { miGeneralizable = setArgInfo i (miGeneralizable (mvInfo mv)) } }

    updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
    updateMetaVarRange :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
    updateMetaVarRange MetaId
    mi Range
    r = MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    mi (Range -> MetaVariable -> MetaVariable
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r)

    setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
    setMetaOccursCheck :: forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> RunMetaOccursCheck -> m ()
    setMetaOccursCheck MetaId
    mi RunMetaOccursCheck
    b = MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    mi ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mvar ->
      MetaVariable
    mvar { mvInfo = (mvInfo mvar) { miMetaOccursCheck = b } }

    -- * Query and manipulate interaction points.

    class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
      freshInteractionId :: m InteractionId
      default freshInteractionId
        :: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
        => m InteractionId
      freshInteractionId = n InteractionId -> t n InteractionId
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift n InteractionId
    forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
    freshInteractionId

      modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
      default modifyInteractionPoints
        :: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
        => (InteractionPoints -> InteractionPoints) -> m ()
      modifyInteractionPoints = n () -> m ()
    n () -> t n ()
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> m ())
    -> ((InteractionPoints -> InteractionPoints) -> n ())
    -> (InteractionPoints -> InteractionPoints)
    -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionPoints -> InteractionPoints) -> n ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints

    instance MonadInteractionPoints m => MonadInteractionPoints (ExceptT e m)
    instance MonadInteractionPoints m => MonadInteractionPoints (MaybeT m)
    instance MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)
    instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)
    instance MonadInteractionPoints m => MonadInteractionPoints (StateT s m)
    instance (MonadInteractionPoints m, Monoid w) => MonadInteractionPoints (WriterT w m)

    instance MonadInteractionPoints TCM where
      freshInteractionId :: TCM InteractionId
    freshInteractionId = TCM InteractionId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
    modifyInteractionPoints InteractionPoints -> InteractionPoints
    f = (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints Lens' TCState InteractionPoints
    -> (InteractionPoints -> InteractionPoints) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` InteractionPoints -> InteractionPoints
    f

    -- | Register an interaction point during scope checking.
    --   If there is no interaction id yet, create one.
    registerInteractionPoint
      :: forall m. MonadInteractionPoints m
      => Bool -> Range -> Maybe Nat -> m InteractionId
    registerInteractionPoint :: forall (m :: * -> *).
    MonadInteractionPoints m =>
    Bool -> Range -> Maybe Int -> m InteractionId
    registerInteractionPoint Bool
    preciseRange Range
    r Maybe Int
    maybeId = do
      m <- Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints
      -- If we're given an interaction id we shouldn't look up by range.
      -- This is important when doing 'refine', since all interaction points
      -- created by the refine gets the same range.
      if not preciseRange || isJust maybeId then continue m else do
        -- If the range does not come from a file, it is not
        -- precise, so ignore it.
        Strict.caseMaybe (rangeFile r) (continue m) $ \ RangeFile
    _ -> do
        -- First, try to find the interaction point by Range.
        Maybe InteractionId
    -> m InteractionId
    -> (InteractionId -> m InteractionId)
    -> m InteractionId
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Range -> InteractionPoints -> Maybe InteractionId
    findInteractionPoint_ Range
    r InteractionPoints
    m) (InteractionPoints -> m InteractionId
    continue InteractionPoints
    m) {-else-} InteractionId -> m InteractionId
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
     where
     continue :: InteractionPoints -> m InteractionId
     continue :: InteractionPoints -> m InteractionId
    continue InteractionPoints
    m = do
      -- We did not find an interaction id with the same Range, so let's create one!
      ii <- case Maybe Int
    maybeId of
        Just Int
    i  -> InteractionId -> m InteractionId
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InteractionId -> m InteractionId)
    -> InteractionId -> m InteractionId
    forall a b. (a -> b) -> a -> b
    $ Int -> InteractionId
    InteractionId Int
    i
        Maybe Int
    Nothing -> m InteractionId
    forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
    freshInteractionId
      let ip = InteractionPoint { ipRange :: Range
    ipRange = Range
    r, ipMeta :: Maybe MetaId
    ipMeta = Maybe MetaId
    forall a. Maybe a
    Nothing, ipSolved :: Bool
    ipSolved = Bool
    False, ipClause :: IPClause
    ipClause = IPClause
    IPNoClause, ipBoundary :: IPBoundary
    ipBoundary = Map (IntMap Bool) Term -> IPBoundary
    forall t. Map (IntMap Bool) t -> IPBoundary' t
    IPBoundary Map (IntMap Bool) Term
    forall a. Monoid a => a
    mempty }
      case BiMap.insertLookupWithKey (\ InteractionId
    key InteractionPoint
    new InteractionPoint
    old -> InteractionPoint
    old) ii ip m of
        -- If the interaction point is already present, we keep the old ip.
        -- However, it needs to be at the same range as the new one.
        (Just InteractionPoint
    ip0, InteractionPoints
    _)
           | InteractionPoint -> Range
    ipRange InteractionPoint
    ip Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    /= InteractionPoint -> Range
    ipRange InteractionPoint
    ip0 -> m InteractionId
    forall a. HasCallStack => a
    __IMPOSSIBLE__
           | Bool
    otherwise                 -> InteractionId -> m InteractionId
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return InteractionId
    ii
        (Maybe InteractionPoint
    Nothing, InteractionPoints
    m') -> do
          (InteractionPoints -> InteractionPoints) -> m ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints (InteractionPoints -> InteractionPoints -> InteractionPoints
    forall a b. a -> b -> a
    const InteractionPoints
    m')
          InteractionId -> m InteractionId
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return InteractionId
    ii

    -- | Find an interaction point by 'Range' by searching the whole map.
    --   Issue 3000: Don't consider solved interaction points.
    --
    --   O(n): linear in the number of registered interaction points.

    findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
    findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
    findInteractionPoint_ Range
    r InteractionPoints
    m = do
      Bool -> Maybe ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r
      [InteractionId] -> Maybe InteractionId
    forall a. [a] -> Maybe a
    listToMaybe ([InteractionId] -> Maybe InteractionId)
    -> [InteractionId] -> Maybe InteractionId
    forall a b. (a -> b) -> a -> b
    $ ((InteractionId, InteractionPoint) -> Maybe InteractionId)
    -> [(InteractionId, InteractionPoint)] -> [InteractionId]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (InteractionId, InteractionPoint) -> Maybe InteractionId
    sameRange ([(InteractionId, InteractionPoint)] -> [InteractionId])
    -> [(InteractionId, InteractionPoint)] -> [InteractionId]
    forall a b. (a -> b) -> a -> b
    $ InteractionPoints -> [(InteractionId, InteractionPoint)]
    forall k v. BiMap k v -> [(k, v)]
    BiMap.toList InteractionPoints
    m
      where
        sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
        sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
    sameRange (InteractionId
    ii, InteractionPoint Range
    r' Maybe MetaId
    _ Bool
    False IPClause
    _ IPBoundary
    _) | Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    r' = InteractionId -> Maybe InteractionId
    forall a. a -> Maybe a
    Just InteractionId
    ii
        sameRange (InteractionId, InteractionPoint)
    _ = Maybe InteractionId
    forall a. Maybe a
    Nothing

    {-# INLINABLE connectInteractionPoint #-}
    -- | Hook up a local meta-variable to an interaction point.
    connectInteractionPoint
      :: MonadInteractionPoints m
      => InteractionId -> MetaId -> m ()
    connectInteractionPoint :: forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> MetaId -> m ()
    connectInteractionPoint InteractionId
    ii MetaId
    mi = do
      ipCl <- (TCEnv -> IPClause) -> m IPClause
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> IPClause
    envClause
      m <- useR stInteractionPoints
      let ip = InteractionPoint { ipRange :: Range
    ipRange = Range
    forall a. HasCallStack => a
    __IMPOSSIBLE__, ipMeta :: Maybe MetaId
    ipMeta = MetaId -> Maybe MetaId
    forall a. a -> Maybe a
    Just MetaId
    mi, ipSolved :: Bool
    ipSolved = Bool
    False, ipClause :: IPClause
    ipClause = IPClause
    ipCl, ipBoundary :: IPBoundary
    ipBoundary = Map (IntMap Bool) Term -> IPBoundary
    forall t. Map (IntMap Bool) t -> IPBoundary' t
    IPBoundary Map (IntMap Bool) Term
    forall a. Monoid a => a
    mempty }
      -- The interaction point needs to be present already, we just set the meta.
      case BiMap.insertLookupWithKey (\ InteractionId
    key InteractionPoint
    new InteractionPoint
    old -> InteractionPoint
    new { ipRange = ipRange old }) ii ip m of
        (Maybe InteractionPoint
    Nothing, InteractionPoints
    _) -> m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Just InteractionPoint
    _, InteractionPoints
    m') -> (InteractionPoints -> InteractionPoints) -> m ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
    -> (InteractionPoints -> InteractionPoints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ InteractionPoints -> InteractionPoints -> InteractionPoints
    forall a b. a -> b -> a
    const InteractionPoints
    m'

    -- | Mark an interaction point as solved.
    removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
    removeInteractionPoint :: forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> m ()
    removeInteractionPoint InteractionId
    ii =
      (InteractionPoints -> InteractionPoints) -> m ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
    -> (InteractionPoints -> InteractionPoints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (InteractionPoint -> Maybe InteractionPoint)
    -> InteractionId -> InteractionPoints -> InteractionPoints
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> Maybe v) -> k -> BiMap k v -> BiMap k v
    BiMap.update (\ InteractionPoint
    ip -> InteractionPoint -> Maybe InteractionPoint
    forall a. a -> Maybe a
    Just InteractionPoint
    ip{ ipSolved = True }) InteractionId
    ii

    -- | Get a list of interaction ids.
    {-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
    getInteractionPoints :: ReadTCState m => m [InteractionId]
    getInteractionPoints :: forall (m :: * -> *). ReadTCState m => m [InteractionId]
    getInteractionPoints = InteractionPoints -> [InteractionId]
    forall k v. BiMap k v -> [k]
    BiMap.keys (InteractionPoints -> [InteractionId])
    -> m InteractionPoints -> m [InteractionId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints

    -- | Get all metas that correspond to unsolved interaction ids.
    getInteractionMetas :: ReadTCState m => m [MetaId]
    getInteractionMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
    getInteractionMetas =
      (InteractionPoint -> Maybe MetaId)
    -> [InteractionPoint] -> [MetaId]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe InteractionPoint -> Maybe MetaId
    ipMeta ([InteractionPoint] -> [MetaId])
    -> (InteractionPoints -> [InteractionPoint])
    -> InteractionPoints
    -> [MetaId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionPoint -> Bool)
    -> [InteractionPoint] -> [InteractionPoint]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool)
    -> (InteractionPoint -> Bool) -> InteractionPoint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoint -> Bool
    ipSolved) ([InteractionPoint] -> [InteractionPoint])
    -> (InteractionPoints -> [InteractionPoint])
    -> InteractionPoints
    -> [InteractionPoint]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoints -> [InteractionPoint]
    forall k v. BiMap k v -> [v]
    BiMap.elems (InteractionPoints -> [MetaId])
    -> m InteractionPoints -> m [MetaId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints

    getUniqueMetasRanges ::
      (HasCallStack, MonadDebug m, ReadTCState m) => [MetaId] -> m [Range]
    getUniqueMetasRanges :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    [MetaId] -> m [Range]
    getUniqueMetasRanges = ([Range] -> [Range]) -> m [Range] -> m [Range]
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Range -> Range) -> [Range] -> [Range]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn Range -> Range
    forall a. a -> a
    id) (m [Range] -> m [Range])
    -> ([MetaId] -> m [Range]) -> [MetaId] -> m [Range]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> m Range) -> [MetaId] -> m [Range]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM MetaId -> m Range
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange

    getUnsolvedMetas ::
      (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
    getUnsolvedMetas :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    m [Range]
    getUnsolvedMetas = do
      openMetas            <- m [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas
      interactionMetas     <- getInteractionMetas
      getUniqueMetasRanges (openMetas List.\\ interactionMetas)

    getUnsolvedInteractionMetas ::
      (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
    getUnsolvedInteractionMetas :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    m [Range]
    getUnsolvedInteractionMetas = [MetaId] -> m [Range]
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    [MetaId] -> m [Range]
    getUniqueMetasRanges ([MetaId] -> m [Range]) -> m [MetaId] -> m [Range]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getInteractionMetas

    -- | Get all metas that correspond to unsolved interaction ids.
    getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
    getInteractionIdsAndMetas :: forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
    getInteractionIdsAndMetas =
      ((InteractionId, InteractionPoint)
     -> Maybe (InteractionId, MetaId))
    -> [(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (InteractionId, InteractionPoint) -> Maybe (InteractionId, MetaId)
    forall {t}. (t, InteractionPoint) -> Maybe (t, MetaId)
    f ([(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)])
    -> (InteractionPoints -> [(InteractionId, InteractionPoint)])
    -> InteractionPoints
    -> [(InteractionId, MetaId)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((InteractionId, InteractionPoint) -> Bool)
    -> [(InteractionId, InteractionPoint)]
    -> [(InteractionId, InteractionPoint)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool)
    -> ((InteractionId, InteractionPoint) -> Bool)
    -> (InteractionId, InteractionPoint)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoint -> Bool
    ipSolved (InteractionPoint -> Bool)
    -> ((InteractionId, InteractionPoint) -> InteractionPoint)
    -> (InteractionId, InteractionPoint)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (InteractionId, InteractionPoint) -> InteractionPoint
    forall a b. (a, b) -> b
    snd) ([(InteractionId, InteractionPoint)]
     -> [(InteractionId, InteractionPoint)])
    -> (InteractionPoints -> [(InteractionId, InteractionPoint)])
    -> InteractionPoints
    -> [(InteractionId, InteractionPoint)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoints -> [(InteractionId, InteractionPoint)]
    forall k v. BiMap k v -> [(k, v)]
    BiMap.toList (InteractionPoints -> [(InteractionId, MetaId)])
    -> m InteractionPoints -> m [(InteractionId, MetaId)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints
      where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
    f (t
    ii, InteractionPoint
    ip) = (t
    ii,) (MetaId -> (t, MetaId)) -> Maybe MetaId -> Maybe (t, MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionPoint -> Maybe MetaId
    ipMeta InteractionPoint
    ip

    -- | Does the meta variable correspond to an interaction point?
    --
    --   Time: @O(log n)@ where @n@ is the number of interaction metas.
    isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
    isInteractionMeta :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    x = Tag InteractionPoint -> InteractionPoints -> Maybe InteractionId
    forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
    BiMap.invLookup Tag InteractionPoint
    MetaId
    x (InteractionPoints -> Maybe InteractionId)
    -> m InteractionPoints -> m (Maybe InteractionId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints

    -- | Get the information associated to an interaction point.
    {-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
    lookupInteractionPoint
      :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m)
      => InteractionId -> m InteractionPoint
    lookupInteractionPoint :: forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii =
      m InteractionPoint
    -> m (Maybe InteractionPoint) -> m InteractionPoint
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (InteractionError -> m InteractionPoint
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m InteractionPoint)
    -> InteractionError -> m InteractionPoint
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> InteractionError
    NoSuchInteractionPoint InteractionId
    ii) (m (Maybe InteractionPoint) -> m InteractionPoint)
    -> m (Maybe InteractionPoint) -> m InteractionPoint
    forall a b. (a -> b) -> a -> b
    $
        InteractionId -> InteractionPoints -> Maybe InteractionPoint
    forall k v. Ord k => k -> BiMap k v -> Maybe v
    BiMap.lookup InteractionId
    ii (InteractionPoints -> Maybe InteractionPoint)
    -> m InteractionPoints -> m (Maybe InteractionPoint)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints

    {-# SPECIALIZE lookupInteractionId :: InteractionId -> TCM MetaId #-}
    -- | Get 'MetaId' for an interaction point.
    --   Precondition: interaction point is connected.
    lookupInteractionId
      :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m)
      => InteractionId -> m MetaId
    lookupInteractionId :: forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii =
      m MetaId -> m (Maybe MetaId) -> m MetaId
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM (InteractionError -> m MetaId
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m MetaId) -> InteractionError -> m MetaId
    forall a b. (a -> b) -> a -> b
    $ InteractionId -> InteractionError
    NoActionForInteractionPoint InteractionId
    ii) (m (Maybe MetaId) -> m MetaId) -> m (Maybe MetaId) -> m MetaId
    forall a b. (a -> b) -> a -> b
    $
        InteractionPoint -> Maybe MetaId
    ipMeta (InteractionPoint -> Maybe MetaId)
    -> m InteractionPoint -> m (Maybe MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> m InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii

    -- | Check whether an interaction id is already associated with a meta variable.
    lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
    lookupInteractionMeta :: forall (m :: * -> *).
    ReadTCState m =>
    InteractionId -> m (Maybe MetaId)
    lookupInteractionMeta InteractionId
    ii = InteractionId -> InteractionPoints -> Maybe MetaId
    lookupInteractionMeta_ InteractionId
    ii (InteractionPoints -> Maybe MetaId)
    -> m InteractionPoints -> m (Maybe MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState InteractionPoints -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints

    lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
    lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
    lookupInteractionMeta_ InteractionId
    ii InteractionPoints
    m = InteractionPoint -> Maybe MetaId
    ipMeta (InteractionPoint -> Maybe MetaId)
    -> Maybe InteractionPoint -> Maybe MetaId
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InteractionId -> InteractionPoints -> Maybe InteractionPoint
    forall k v. Ord k => k -> BiMap k v -> Maybe v
    BiMap.lookup InteractionId
    ii InteractionPoints
    m

    -- | Generate new meta variable.
    newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
    newMeta :: forall (m :: * -> *) a.
    MonadMetaSolver m =>
    Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta = MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    forall (m :: * -> *) a.
    MonadMetaSolver m =>
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta' (MetaKind -> MetaInstantiation
    OpenMeta MetaKind
    UnificationMeta)

    -- | Generate a new meta variable with some instantiation given.
    --   For instance, the instantiation could be a 'PostponedTypeCheckingProblem'.
    newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
                   Judgement a -> TCM MetaId
    newMetaTCM' :: forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> TCM MetaId
    newMetaTCM' MetaInstantiation
    inst Frozen
    frozen MetaInfo
    mi MetaPriority
    p Permutation
    perm Judgement a
    j = do
      x <- TCM MetaId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      let j' = Judgement a
    j { jMetaId = x }  -- fill the identifier part of the judgement
          mv = MetaVar{ mvInfo :: MetaInfo
    mvInfo             = MetaInfo
    mi
                      , mvPriority :: MetaPriority
    mvPriority         = MetaPriority
    p
                      , mvPermutation :: Permutation
    mvPermutation      = Permutation
    perm
                      , mvJudgement :: Judgement MetaId
    mvJudgement        = Judgement MetaId
    j'
                      , mvInstantiation :: MetaInstantiation
    mvInstantiation    = MetaInstantiation
    inst
                      , mvListeners :: Set Listener
    mvListeners        = Set Listener
    forall a. Set a
    Set.empty
                      , mvFrozen :: Frozen
    mvFrozen           = Frozen
    frozen
                      , mvTwin :: Maybe MetaId
    mvTwin             = Maybe MetaId
    forall a. Maybe a
    Nothing
                      }
      -- printing not available (import cycle)
      -- reportSDoc "tc.meta.new" 50 $ "new meta" <+> prettyTCM j'
      insertMetaVar x mv
      return x

    -- | Get the 'Range' for an interaction point.
    {-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
    getInteractionRange
      :: (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m)
      => InteractionId -> m Range
    getInteractionRange :: forall (m :: * -> *).
    (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) =>
    InteractionId -> m Range
    getInteractionRange = InteractionPoint -> Range
    ipRange (InteractionPoint -> Range)
    -> (InteractionId -> m InteractionPoint)
    -> InteractionId
    -> m Range
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> InteractionId -> m InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint

    -- | Get the 'Range' for a local meta-variable.
    getMetaRange ::
      (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Range
    getMetaRange :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange = MetaVariable -> Range
    forall a. HasRange a => a -> Range
    getRange (MetaVariable -> Range)
    -> (MetaId -> m MetaVariable) -> MetaId -> m Range
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta

    getInteractionScope ::
      (MonadDebug m, ReadTCState m, MonadError TCErr m,
       MonadTCEnv m) =>
      InteractionId -> m ScopeInfo
    getInteractionScope :: forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m ScopeInfo
    getInteractionScope =
      MetaVariable -> ScopeInfo
    getMetaScope (MetaVariable -> ScopeInfo)
    -> (MetaId -> m MetaVariable) -> MetaId -> m ScopeInfo
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta (MetaId -> m ScopeInfo)
    -> (InteractionId -> m MetaId) -> InteractionId -> m ScopeInfo
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< InteractionId -> m MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId

    withMetaInfo' :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => MetaVariable -> m a -> m a
    withMetaInfo' :: forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    MetaVariable -> m a -> m a
    withMetaInfo' MetaVariable
    mv = Closure Range -> m a -> m a
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    Closure Range -> m a -> m a
    withMetaInfo (MetaInfo -> Closure Range
    miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv)

    withMetaInfo :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => Closure Range -> m a -> m a
    withMetaInfo :: forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    Closure Range -> m a -> m a
    withMetaInfo Closure Range
    mI m a
    cont = Closure Range -> (Range -> m a) -> m a
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Range
    mI ((Range -> m a) -> m a) -> (Range -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \ Range
    r ->
      Range -> m a -> m a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r m a
    cont

    withInteractionId ::
      (MonadDebug m, ReadTCState m, MonadError TCErr m,
       MonadTCEnv m, MonadTrace m) =>
      InteractionId -> m a -> m a
    withInteractionId :: forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    i m a
    ret = do
      m <- InteractionId -> m MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    i
      withMetaId m ret

    withMetaId ::
      (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
       ReadTCState m) =>
      MetaId -> m a -> m a
    withMetaId :: forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
     ReadTCState m) =>
    MetaId -> m a -> m a
    withMetaId MetaId
    m m a
    ret = do
      mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
      withMetaInfo' mv ret

    getOpenMetas :: ReadTCState m => m [MetaId]
    getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas = LocalMetaStore -> [MetaId]
    forall k a. Map k a -> [k]
    MapS.keys (LocalMetaStore -> [MetaId]) -> m LocalMetaStore -> m [MetaId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState LocalMetaStore -> m LocalMetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore

    isOpenMeta :: MetaInstantiation -> Bool
    isOpenMeta :: MetaInstantiation -> Bool
    isOpenMeta OpenMeta{}                     = Bool
    True
    isOpenMeta BlockedConst{}                 = Bool
    True
    isOpenMeta PostponedTypeCheckingProblem{} = Bool
    True
    isOpenMeta InstV{}                        = Bool
    False

    -- | @listenToMeta l m@: register @l@ as a listener to @m@. This is done
    --   when the type of l is blocked by @m@.
    listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
    listenToMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Listener -> MetaId -> m ()
    listenToMeta Listener
    l MetaId
    m =
      MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \MetaVariable
    mv -> MetaVariable
    mv { mvListeners = Set.insert l $ mvListeners mv }

    -- | Unregister a listener.
    unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
    unlistenToMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Listener -> MetaId -> m ()
    unlistenToMeta Listener
    l MetaId
    m =
      MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \MetaVariable
    mv -> MetaVariable
    mv { mvListeners = Set.delete l $ mvListeners mv }

    -- | Get the listeners for a local meta-variable.
    getMetaListeners ::
      (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m [Listener]
    getMetaListeners :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m [Listener]
    getMetaListeners MetaId
    m = Set Listener -> [Listener]
    forall a. Set a -> [a]
    Set.toList (Set Listener -> [Listener])
    -> (MetaVariable -> Set Listener) -> MetaVariable -> [Listener]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> Set Listener
    mvListeners (MetaVariable -> [Listener]) -> m MetaVariable -> m [Listener]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m

    clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
    clearMetaListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    clearMetaListeners MetaId
    m =
      MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \MetaVariable
    mv -> MetaVariable
    mv { mvListeners = Set.empty }

    -- | Do safe eta-expansions for meta (@SingletonRecords,Levels@).
    etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m ()
    etaExpandMetaSafe :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    etaExpandMetaSafe = [MetaClass] -> MetaId -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [MetaClass] -> MetaId -> m ()
    etaExpandMeta [MetaClass
    SingletonRecords,MetaClass
    Levels]

    -- | Eta expand metavariables listening on the current meta.
    etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()
    etaExpandListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    etaExpandListeners MetaId
    m = do
      ls <- MetaId -> m [Listener]
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m [Listener]
    getMetaListeners MetaId
    m
      clearMetaListeners m  -- we don't really have to do this
      mapM_ wakeupListener ls

    -- | Wake up a meta listener and let it do its thing
    wakeupListener :: MonadMetaSolver m => Listener -> m ()
      -- Andreas 2010-10-15: do not expand record mvars, lazyness needed for irrelevance
    wakeupListener :: forall (m :: * -> *). MonadMetaSolver m => Listener -> m ()
    wakeupListener (EtaExpand MetaId
    x)         = MetaId -> m ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    etaExpandMetaSafe MetaId
    x
    wakeupListener (CheckConstraint Int
    _ ProblemConstraint
    c) = do
      --reportSDoc "tc.meta.blocked" 20 $ "waking boxed constraint" <+> prettyTCM c
      (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (Constraints -> Constraints) -> m ()
    modifyAwakeConstraints (ProblemConstraint
    cProblemConstraint -> Constraints -> Constraints
    forall a. a -> [a] -> [a]
    :)
      m ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints

    solveAwakeConstraints :: (MonadConstraint m) => m ()
    solveAwakeConstraints :: forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints = Bool -> m ()
    forall (m :: * -> *). MonadConstraint m => Bool -> m ()
    solveAwakeConstraints' Bool
    False

    solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
    solveAwakeConstraints' :: forall (m :: * -> *). MonadConstraint m => Bool -> m ()
    solveAwakeConstraints' = (ProblemConstraint -> Bool) -> Bool -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> Bool -> m ()
    solveSomeAwakeConstraints (Bool -> ProblemConstraint -> Bool
    forall a b. a -> b -> a
    const Bool
    True)

    ---------------------------------------------------------------------------
    -- * Freezing and unfreezing metas.
    ---------------------------------------------------------------------------

    {-# SPECIALIZE freezeMetas :: LocalMetaStore -> TCM (Set MetaId) #-}
    -- | Freeze the given meta-variables (but only if they are open) and
    -- return those that were not already frozen.
    freezeMetas :: forall m. (MonadTCState m, ReadTCState m) => LocalMetaStore -> m (Set MetaId)
    freezeMetas :: forall (m :: * -> *).
    (MonadTCState m, ReadTCState m) =>
    LocalMetaStore -> m (Set MetaId)
    freezeMetas LocalMetaStore
    ms =
      WriterT (Set MetaId) m () -> m (Set MetaId)
    forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
    execWriterT (WriterT (Set MetaId) m () -> m (Set MetaId))
    -> WriterT (Set MetaId) m () -> m (Set MetaId)
    forall a b. (a -> b) -> a -> b
    $
      Lens' TCState LocalMetaStore
    -> (LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
    -> WriterT (Set MetaId) m ()
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    Lens' TCState a -> (a -> m a) -> m ()
    modifyTCLensM (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore ((LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
     -> WriterT (Set MetaId) m ())
    -> (LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
    -> WriterT (Set MetaId) m ()
    forall a b. (a -> b) -> a -> b
    $
      StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    -> LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    execStateT ((MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
    -> [MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    freeze ([MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
    -> [MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall a b. (a -> b) -> a -> b
    $ LocalMetaStore -> [MetaId]
    forall k a. Map k a -> [k]
    MapS.keys LocalMetaStore
    ms)
      where
      freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
      freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    freeze MetaId
    m = do
        store <- StateT LocalMetaStore (WriterT (Set MetaId) m) LocalMetaStore
    forall s (m :: * -> *). MonadState s m => m s
    get
        case MapS.lookup m store of
          Just MetaVariable
    mvar
            | MetaVariable -> Frozen
    mvFrozen MetaVariable
    mvar Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Frozen
    Frozen -> do
              WriterT (Set MetaId) m ()
    -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall (m :: * -> *) a. Monad m => m a -> StateT LocalMetaStore m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT (Set MetaId) m ()
     -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
    -> WriterT (Set MetaId) m ()
    -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall a b. (a -> b) -> a -> b
    $ Set MetaId -> WriterT (Set MetaId) m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton MetaId
    m)
              LocalMetaStore -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (LocalMetaStore
     -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
    -> LocalMetaStore
    -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert MetaId
    m (MetaVariable
    mvar { mvFrozen = Frozen }) LocalMetaStore
    store
            | Bool
    otherwise -> () -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall a. a -> StateT LocalMetaStore (WriterT (Set MetaId) m) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Maybe MetaVariable
    Nothing -> () -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
    forall a. a -> StateT LocalMetaStore (WriterT (Set MetaId) m) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Thaw all open meta variables.
    unfreezeMetas :: TCM ()
    unfreezeMetas :: TCM ()
    unfreezeMetas = (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore Lens' TCState LocalMetaStore
    -> (LocalMetaStore -> LocalMetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` (MetaVariable -> MetaVariable) -> LocalMetaStore -> LocalMetaStore
    forall a b k. (a -> b) -> Map k a -> Map k b
    MapS.map MetaVariable -> MetaVariable
    unfreeze
      where
      unfreeze :: MetaVariable -> MetaVariable
      unfreeze :: MetaVariable -> MetaVariable
    unfreeze MetaVariable
    mvar = MetaVariable
    mvar { mvFrozen = Instantiable }

    {-# SPECIALIZE isFrozen :: MetaId -> TCM Bool #-}
    isFrozen ::
      (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool
    isFrozen :: forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x = do
      mvar <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
      return $ mvFrozen mvar == Frozen

    withFrozenMetas ::
        (MonadMetaSolver m, MonadTCState m)
      => m a -> m a
    withFrozenMetas :: forall (m :: * -> *) a.
    (MonadMetaSolver m, MonadTCState m) =>
    m a -> m a
    withFrozenMetas m a
    act = do
      openMetas <- Lens' TCState LocalMetaStore -> m LocalMetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
    Lens' TCState LocalMetaStore
    stOpenMetaStore
      frozenMetas <- freezeMetas openMetas
      result <- act
      forM_ frozenMetas $ \MetaId
    m ->
        MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    m ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mv -> MetaVariable
    mv { mvFrozen = Instantiable }
      return result

    -- | Unfreeze a meta and its type if this is a meta again.
    --   Does not unfreeze deep occurrences of meta-variables or remote
    --   meta-variables.
    class UnFreezeMeta a where
      unfreezeMeta :: MonadMetaSolver m => a -> m ()

    instance UnFreezeMeta MetaId where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    unfreezeMeta MetaId
    x = m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (((MetaId -> Bool) -> MetaId -> Bool
    forall a b. (a -> b) -> a -> b
    $ MetaId
    x) ((MetaId -> Bool) -> Bool) -> m (MetaId -> Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (MetaId -> Bool)
    forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
    isRemoteMeta) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        MetaId -> (MetaVariable -> MetaVariable) -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
    updateMetaVar MetaId
    x ((MetaVariable -> MetaVariable) -> m ())
    -> (MetaVariable -> MetaVariable) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mv -> MetaVariable
    mv { mvFrozen = Instantiable }
        Type -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
    unfreezeMeta (Type -> m ()) -> m Type -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
    {-# SPECIALIZE unfreezeMeta :: MetaId -> TCM () #-}

    instance UnFreezeMeta Type where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
    unfreezeMeta (El Sort
    s Term
    t) = Sort -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
    unfreezeMeta Sort
    s m () -> m () -> m ()
    forall a b. m a -> m b -> m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
    unfreezeMeta Term
    t

    instance UnFreezeMeta Term where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
    unfreezeMeta (MetaV MetaId
    x [Elim]
    _)   = MetaId -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    unfreezeMeta MetaId
    x
      unfreezeMeta (Sort Sort
    s)      = Sort -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
    unfreezeMeta Sort
    s
      unfreezeMeta (Level Level
    l)     = Level -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
    unfreezeMeta Level
    l
      unfreezeMeta (DontCare Term
    t)  = Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
    unfreezeMeta Term
    t
      unfreezeMeta (Lam ArgInfo
    _ Abs Term
    v)     = Abs Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Abs Term -> m ()
    unfreezeMeta Abs Term
    v
      unfreezeMeta Term
    _             = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance UnFreezeMeta Sort where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
    unfreezeMeta (MetaS MetaId
    x [Elim]
    _)   = MetaId -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    unfreezeMeta MetaId
    x
      unfreezeMeta Sort
    _             = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance UnFreezeMeta Level where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
    unfreezeMeta (Max Integer
    _ [PlusLevel' Term]
    ls)      = [PlusLevel' Term] -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [PlusLevel' Term] -> m ()
    unfreezeMeta [PlusLevel' Term]
    ls

    instance UnFreezeMeta PlusLevel where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => PlusLevel' Term -> m ()
    unfreezeMeta (Plus Integer
    _ Term
    a)    = Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
    unfreezeMeta Term
    a

    instance UnFreezeMeta a => UnFreezeMeta [a] where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => [a] -> m ()
    unfreezeMeta = (a -> m ()) -> [a] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ a -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => a -> m ()
    unfreezeMeta

    instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Abs a -> m ()
    unfreezeMeta = (a -> m ()) -> Abs a -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    Fold.mapM_ a -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    forall (m :: * -> *). MonadMetaSolver m => a -> m ()
    unfreezeMeta