    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Monad.MetaVars where

    import Prelude hiding (null)

    import Control.DeepSeq

    import Control.Monad                ( (<=<), guard )
    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.Trans.Identity ( IdentityT )
    import Control.Monad.Reader
    import Control.Monad.Writer
    -- Control.Monad.Fail import is redundant since GHC 8.8.1
    import Control.Monad.Fail (MonadFail)

    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Foldable as Fold

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    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)
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Signature (HasConstInfo)
    import Agda.TypeChecking.Substitute
    import {-# SOURCE #-} Agda.TypeChecking.Telescope

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

    import Agda.Utils.Impossible

    -- | Various kinds of metavariables.

    data MetaKind =
        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 (MetaKind -> MetaKind -> Bool
    (MetaKind -> MetaKind -> Bool)
    -> (MetaKind -> MetaKind -> Bool) -> Eq MetaKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: MetaKind -> MetaKind -> Bool
    $c/= :: MetaKind -> MetaKind -> Bool
    == :: MetaKind -> MetaKind -> Bool
    $c== :: MetaKind -> MetaKind -> Bool
    Eq, Int -> MetaKind
    MetaKind -> Int
    MetaKind -> [MetaKind]
    MetaKind -> MetaKind
    MetaKind -> MetaKind -> [MetaKind]
    MetaKind -> MetaKind -> MetaKind -> [MetaKind]
    (MetaKind -> MetaKind)
    -> (MetaKind -> MetaKind)
    -> (Int -> MetaKind)
    -> (MetaKind -> Int)
    -> (MetaKind -> [MetaKind])
    -> (MetaKind -> MetaKind -> [MetaKind])
    -> (MetaKind -> MetaKind -> [MetaKind])
    -> (MetaKind -> MetaKind -> MetaKind -> [MetaKind])
    -> Enum MetaKind
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
    $cenumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
    enumFromTo :: MetaKind -> MetaKind -> [MetaKind]
    $cenumFromTo :: MetaKind -> MetaKind -> [MetaKind]
    enumFromThen :: MetaKind -> MetaKind -> [MetaKind]
    $cenumFromThen :: MetaKind -> MetaKind -> [MetaKind]
    enumFrom :: MetaKind -> [MetaKind]
    $cenumFrom :: MetaKind -> [MetaKind]
    fromEnum :: MetaKind -> Int
    $cfromEnum :: MetaKind -> Int
    toEnum :: Int -> MetaKind
    $ctoEnum :: Int -> MetaKind
    pred :: MetaKind -> MetaKind
    $cpred :: MetaKind -> MetaKind
    succ :: MetaKind -> MetaKind
    $csucc :: MetaKind -> MetaKind
    Enum, MetaKind
    MetaKind -> MetaKind -> Bounded MetaKind
    forall a. a -> a -> Bounded a
    maxBound :: MetaKind
    $cmaxBound :: MetaKind
    minBound :: MetaKind
    $cminBound :: MetaKind
    Bounded, Int -> MetaKind -> ShowS
    [MetaKind] -> ShowS
    MetaKind -> [Char]
    (Int -> MetaKind -> ShowS)
    -> (MetaKind -> [Char]) -> ([MetaKind] -> ShowS) -> Show MetaKind
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    showList :: [MetaKind] -> ShowS
    $cshowList :: [MetaKind] -> ShowS
    show :: MetaKind -> [Char]
    $cshow :: MetaKind -> [Char]
    showsPrec :: Int -> MetaKind -> ShowS
    $cshowsPrec :: Int -> MetaKind -> ShowS
    Show)

    -- | All possible metavariable kinds.

    allMetaKinds :: [MetaKind]
    allMetaKinds :: [MetaKind]
    allMetaKinds = [MetaKind
    forall a. Bounded a => a
    minBound .. MetaKind
    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 metavariable, if it is of the specified kind.
      --   Don't do anything if the metavariable is a blocked term.
      etaExpandMeta :: [MetaKind] -> 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 ()

    -- | 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 (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    env -> TCEnv
    env { envAssignMetas :: Bool
    envAssignMetas = Bool
    False }) m a
    cont

    -- | Get the meta store.
    getMetaStore :: (ReadTCState m) => m MetaStore
    getMetaStore :: forall (m :: * -> *). ReadTCState m => m MetaStore
    getMetaStore = Lens' MetaStore TCState -> m MetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' MetaStore TCState
    stMetaStore

    modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
    modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
    modifyMetaStore MetaStore -> MetaStore
    f = Lens' MetaStore TCState
    stMetaStore Lens' MetaStore TCState -> (MetaStore -> MetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` MetaStore -> MetaStore
    f

    -- | Run a computation and record which new metas it created.
    metasCreatedBy :: ReadTCState m => m a -> m (a, MetaStore)
    metasCreatedBy :: forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
    metasCreatedBy m a
    m = do
      -- Compute largestMeta strictly to avoid leaking memory.
      !Maybe Int
    largestMeta <- Maybe Int -> Maybe Int
    forall a. NFData a => a -> a
    force (Maybe Int -> Maybe Int)
    -> (MetaStore -> Maybe Int) -> MetaStore -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, MetaVariable) -> Int)
    -> Maybe (Int, MetaVariable) -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int, MetaVariable) -> Int
    forall a b. (a, b) -> a
    fst (Maybe (Int, MetaVariable) -> Maybe Int)
    -> (MetaStore -> Maybe (Int, MetaVariable))
    -> MetaStore
    -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaStore -> Maybe (Int, MetaVariable)
    forall a. IntMap a -> Maybe (Int, a)
    IntMap.lookupMax (MetaStore -> Maybe Int) -> m MetaStore -> m (Maybe Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                        Lens' MetaStore TCState -> m MetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' MetaStore TCState
    stMetaStore
      a
    a            <- m a
    m
      MetaStore
    ms           <- Lens' MetaStore TCState -> m MetaStore
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' MetaStore TCState
    stMetaStore
      let createdMetas :: MetaStore
    createdMetas = case Maybe Int
    largestMeta of
            Maybe Int
    Nothing          -> MetaStore
    ms
            Just Int
    largestMeta -> (MetaStore, MetaStore) -> MetaStore
    forall a b. (a, b) -> b
    snd ((MetaStore, MetaStore) -> MetaStore)
    -> (MetaStore, MetaStore) -> MetaStore
    forall a b. (a -> b) -> a -> b
    $ Int -> MetaStore -> (MetaStore, MetaStore)
    forall a. Int -> IntMap a -> (IntMap a, IntMap a)
    IntMap.split Int
    largestMeta MetaStore
    ms
      (a, MetaStore) -> m (a, MetaStore)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    a, MetaStore
    createdMetas)

    -- | Lookup a meta variable.
    lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
    lookupMeta' :: forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupMeta' MetaId
    m = Int -> MetaStore -> Maybe MetaVariable
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup (MetaId -> Int
    metaId MetaId
    m) (MetaStore -> Maybe MetaVariable)
    -> m MetaStore -> m (Maybe MetaVariable)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m MetaStore
    forall (m :: * -> *). ReadTCState m => m MetaStore
    getMetaStore

    lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
    lookupMeta :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m = m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM m MetaVariable
    failure (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)
    lookupMeta' MetaId
    m
      where failure :: m MetaVariable
    failure = [Char] -> m MetaVariable
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail ([Char] -> m MetaVariable) -> [Char] -> m MetaVariable
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "no such meta variable " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m

    -- | Type of a term or sort meta.
    metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
    metaType :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type)
    -> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> Judgement MetaId
    mvJudgement (MetaVariable -> Type) -> m MetaVariable -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x

    -- | Update the information associated with a meta variable.
    updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM MetaId
    m MetaVariable -> MetaVariable
    f = (MetaStore -> MetaStore) -> TCM ()
    modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
    -> (MetaStore -> MetaStore) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (MetaVariable -> MetaVariable) -> Int -> MetaStore -> MetaStore
    forall a. (a -> a) -> Int -> IntMap a -> IntMap a
    IntMap.adjust MetaVariable -> MetaVariable
    f (Int -> MetaStore -> MetaStore) -> Int -> MetaStore -> MetaStore
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Int
    metaId MetaId
    m

    -- | Insert a new meta variable with associated information into the meta store.
    insertMetaVar :: MetaId -> MetaVariable -> TCM ()
    insertMetaVar :: MetaId -> MetaVariable -> TCM ()
    insertMetaVar MetaId
    m MetaVariable
    mv = (MetaStore -> MetaStore) -> TCM ()
    modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
    -> (MetaStore -> MetaStore) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> MetaVariable -> MetaStore -> MetaStore
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert (MetaId -> Int
    metaId MetaId
    m) MetaVariable
    mv

    getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
    getMetaPriority :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta

    isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
    isSortMeta :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isSortMeta MetaId
    m = MetaVariable -> Bool
    isSortMeta_ (MetaVariable -> Bool) -> m MetaVariable -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m

    isSortMeta_ :: MetaVariable -> Bool
    isSortMeta_ :: MetaVariable -> Bool
    isSortMeta_ MetaVariable
    mv = case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
        HasType{} -> Bool
    False
        IsSort{}  -> Bool
    True

    getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
    getMetaType :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    getMetaType MetaId
    m = do
      MetaVariable
    mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      Type -> m Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv of
        HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } -> Type
    t
        IsSort{}  -> Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Compute the context variables that a meta 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
    args <- m Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
      Args -> m Args
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Args -> m Args) -> Args -> m Args
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Args -> Args
    forall a. Permutation -> [a] -> [a]
    permute (Int -> Permutation -> Permutation
    takeP (Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) Permutation
    p) Args
    args

    -- | Given a meta, return the type applied to the current context.
    getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m, HasBuiltins m)
                         => MetaId -> m Type
    getMetaTypeInContext :: forall (m :: * -> *).
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
     HasBuiltins m) =>
    MetaId -> m Type
    getMetaTypeInContext MetaId
    m = do
      mv :: MetaVariable
    mv@MetaVar{ mvJudgement :: MetaVariable -> Judgement MetaId
    mvJudgement = Judgement MetaId
    j } <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      case Judgement MetaId
    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
    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__

    -- | Is it a meta that might be generalized?
    isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
    isGeneralizableMeta :: forall (m :: * -> *).
    (ReadTCState m, MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta 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 :: (MonadFail m, ReadTCState m) => a -> m Bool

    instance IsInstantiatedMeta MetaId where
      isInstantiatedMeta :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    m

    instance IsInstantiatedMeta Term where
      isInstantiatedMeta :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    Term -> m Bool
    isInstantiatedMeta = Term -> m Bool
    forall (m :: * -> *).
    (MonadFail 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, MonadFail m, ReadTCState m) =>
    a -> 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, MonadFail m, ReadTCState m) =>
    a -> m Bool
    isInstantiatedMeta Level
    l
          Lam ArgInfo
    _ Abs Term
    b    -> Abs Term -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
    a -> 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, MonadFail m, ReadTCState m) =>
    a -> m Bool
    isInstantiatedMeta Args
    vs
          Term
    _          -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta Level where
      isInstantiatedMeta :: forall (m :: * -> *).
    (MonadFail 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, MonadFail m, ReadTCState m) =>
    a -> m Bool
    isInstantiatedMeta [PlusLevel' Term]
    ls
      isInstantiatedMeta Level
    _ = m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta PlusLevel where
      isInstantiatedMeta :: forall (m :: * -> *).
    (MonadFail 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, MonadFail m, ReadTCState m) =>
    a -> m Bool
    isInstantiatedMeta Term
    l
      isInstantiatedMeta PlusLevel' Term
    _ = m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
      isInstantiatedMeta :: forall (m :: * -> *). (MonadFail 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, MonadFail m, ReadTCState m) =>
    a -> m Bool
    isInstantiatedMeta

    instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
      isInstantiatedMeta :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    Maybe a -> m Bool
    isInstantiatedMeta = [a] -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    Arg a -> m Bool
    isInstantiatedMeta = a -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    Abs a -> m Bool
    isInstantiatedMeta = a -> m Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, MonadFail 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

    isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
    isInstantiatedMeta' :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    m = do
      MetaVariable
    mv <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
      Maybe Term -> m (Maybe Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term -> m (Maybe Term)) -> Maybe Term -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ case MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    mv of
        InstV [Arg [Char]]
    tel Term
    v -> 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 (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Arg [Char] -> Term -> Term
    mkLam Term
    v [Arg [Char]]
    tel
        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 (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 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 (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 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 (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 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 (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 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 (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 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 (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 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)
    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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m [Listener]
    getMetaListeners MetaId
    x)
          FindInstance 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m (Maybe Term)
    isInstantiatedMeta' MetaId
    x) (Set MetaId -> TCM (Set MetaId)
    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 (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 t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton
          IsEmpty{}                -> Set MetaId -> TCM (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckFunDef{}            -> Set MetaId -> TCM (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          CheckSizeLtSat{}         -> Set MetaId -> TCM (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          HasBiggerSort{}          -> Set MetaId -> TCM (Set MetaId)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set MetaId
    forall a. Monoid a => a
    mempty
          HasPTSRule{}             -> Set MetaId -> TCM (Set MetaId)
    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 (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 (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 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 (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 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 (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 (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
      Range
    r        <- m Range
    forall (m :: * -> *). MonadTCEnv m => m Range
    getCurrentRange
      Closure Range
    cl       <- Range -> m (Closure Range)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Range
    r
      DoGeneralize
    gen      <- Lens' DoGeneralize TCEnv -> m DoGeneralize
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' DoGeneralize TCEnv
    eGeneralizeMetas
      Modality
    modality <- Lens' Modality TCEnv -> m Modality
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Modality TCEnv
    eModality
      MetaInfo -> m MetaInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaInfo :: Closure Range
    -> Modality
    -> RunMetaOccursCheck
    -> [Char]
    -> Arg DoGeneralize
    -> MetaInfo
    MetaInfo
        { miClosRange :: Closure Range
    miClosRange       = Closure Range
    cl
        , miModality :: Modality
    miModality        = Modality
    modality
        , miMetaOccursCheck :: RunMetaOccursCheck
    miMetaOccursCheck = RunMetaOccursCheck
    b
        , miNameSuggestion :: [Char]
    miNameSuggestion  = [Char]
    ""
        , miGeneralizable :: Arg DoGeneralize
    miGeneralizable   = DoGeneralize -> Arg DoGeneralize
    forall a. a -> Arg a
    defaultArg DoGeneralize
    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] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    u
          () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
    getMetaNameSuggestion :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    mi [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to " [Char] -> ShowS
    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 :: MetaInfo
    mvInfo = (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mvar) { miNameSuggestion :: [Char]
    miNameSuggestion = [Char]
    s }}

    -- | Change the ArgInfo that will be used when generalizing over this meta.
    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 :: MetaInfo
    mvInfo = (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv)
            { miGeneralizable :: Arg DoGeneralize
    miGeneralizable = ArgInfo -> Arg DoGeneralize -> Arg DoGeneralize
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    i (MetaInfo -> Arg DoGeneralize
    miGeneralizable (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    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 :: MetaInfo
    mvInfo = (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mvar) { miMetaOccursCheck :: RunMetaOccursCheck
    miMetaOccursCheck = RunMetaOccursCheck
    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 (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 () -> t n ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> t n ())
    -> ((InteractionPoints -> InteractionPoints) -> n ())
    -> (InteractionPoints -> InteractionPoints)
    -> t n ()
    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 (IdentityT m)
    instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)
    instance MonadInteractionPoints m => MonadInteractionPoints (StateT s 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 = Lens' InteractionPoints TCState
    stInteractionPoints Lens' InteractionPoints TCState
    -> (InteractionPoints -> InteractionPoints) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (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
      InteractionPoints
    m <- Lens' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    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 Bool -> Bool
    not Bool
    preciseRange Bool -> Bool -> Bool
    || Maybe Int -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe Int
    maybeId then InteractionPoints -> m InteractionId
    continue InteractionPoints
    m else do
        -- If the range does not come from a file, it is not
        -- precise, so ignore it.
        Maybe AbsolutePath
    -> m InteractionId
    -> (AbsolutePath -> m InteractionId)
    -> m InteractionId
    forall a b. Maybe a -> b -> (a -> b) -> b
    Strict.caseMaybe (Range -> Maybe AbsolutePath
    rangeFile Range
    r) (InteractionPoints -> m InteractionId
    continue InteractionPoints
    m) ((AbsolutePath -> m InteractionId) -> m InteractionId)
    -> (AbsolutePath -> m InteractionId) -> m InteractionId
    forall a b. (a -> b) -> a -> b
    $ \ AbsolutePath
    _ -> 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 (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!
      InteractionId
    ii <- case Maybe Int
    maybeId of
        Just Int
    i  -> InteractionId -> m InteractionId
    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
    ip = InteractionPoint :: Range -> Maybe MetaId -> Bool -> IPClause -> InteractionPoint
    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 }
      case (InteractionId
     -> InteractionPoint -> InteractionPoint -> InteractionPoint)
    -> InteractionId
    -> InteractionPoint
    -> InteractionPoints
    -> (Maybe InteractionPoint, InteractionPoints)
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
    BiMap.insertLookupWithKey (\ InteractionId
    key InteractionPoint
    new InteractionPoint
    old -> InteractionPoint
    old) InteractionId
    ii InteractionPoint
    ip InteractionPoints
    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 (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 (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 (f :: * -> *). Alternative f => Bool -> f ()
    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
    _) | 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

    -- | Hook up meta variable to interaction point.
    connectInteractionPoint
      :: MonadInteractionPoints m
      => InteractionId -> MetaId -> m ()
    connectInteractionPoint :: forall (m :: * -> *).
    MonadInteractionPoints m =>
    InteractionId -> MetaId -> m ()
    connectInteractionPoint InteractionId
    ii MetaId
    mi = do
      IPClause
    ipCl <- (TCEnv -> IPClause) -> m IPClause
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> IPClause
    envClause
      InteractionPoints
    m <- Lens' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    stInteractionPoints
      let ip :: InteractionPoint
    ip = InteractionPoint :: Range -> Maybe MetaId -> Bool -> IPClause -> InteractionPoint
    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 }
      -- The interaction point needs to be present already, we just set the meta.
      case (InteractionId
     -> InteractionPoint -> InteractionPoint -> InteractionPoint)
    -> InteractionId
    -> InteractionPoint
    -> InteractionPoints
    -> (Maybe InteractionPoint, InteractionPoints)
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
    BiMap.insertLookupWithKey (\ InteractionId
    key InteractionPoint
    new InteractionPoint
    old -> InteractionPoint
    new { ipRange :: Range
    ipRange = InteractionPoint -> Range
    ipRange InteractionPoint
    old }) InteractionId
    ii InteractionPoint
    ip InteractionPoints
    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 :: Bool
    ipSolved = Bool
    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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    stInteractionPoints

    getUniqueMetasRanges :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range]
    getUniqueMetasRanges :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    [MetaId] -> m [Range]
    getUniqueMetasRanges = ([Range] -> [Range]) -> m [Range] -> m [Range]
    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)
    mapM MetaId -> m Range
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Range
    getMetaRange

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

    getUnsolvedInteractionMetas :: (MonadFail m, ReadTCState m) => m [Range]
    getUnsolvedInteractionMetas :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => m [Range]
    getUnsolvedInteractionMetas = [MetaId] -> m [Range]
    forall (m :: * -> *).
    (MonadFail 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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    stInteractionPoints

    -- | Get the information associated to an interaction point.
    {-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
    lookupInteractionPoint
      :: (MonadFail m, ReadTCState m, MonadError TCErr m)
      => InteractionId -> m InteractionPoint
    lookupInteractionPoint :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr 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 m InteractionPoint
    err (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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    stInteractionPoints
      where
        err :: m InteractionPoint
    err  = [Char] -> m InteractionPoint
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail ([Char] -> m InteractionPoint) -> [Char] -> m InteractionPoint
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "no such interaction point: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Show a => a -> [Char]
    show InteractionId
    ii

    -- | Get 'MetaId' for an interaction point.
    --   Precondition: interaction point is connected.
    lookupInteractionId
      :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
      => InteractionId -> m MetaId
    lookupInteractionId :: forall (m :: * -> *).
    (MonadFail 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 m MetaId
    err2 (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 :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii
      where
        err2 :: m MetaId
    err2 = TypeError -> m MetaId
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m MetaId) -> TypeError -> m MetaId
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "No type nor action available for hole " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ InteractionId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow InteractionId
    ii [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ". Possible cause: the hole has not been reached during type checking (do you see yellow?)"

    -- | 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' InteractionPoints TCState -> m InteractionPoints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' InteractionPoints TCState
    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 (m :: * -> *) a.
    MonadMetaSolver m =>
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> m MetaId
    newMeta' MetaInstantiation
    Open

    -- | 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
      MetaId
    x <- TCM MetaId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      let j' :: Judgement MetaId
    j' = Judgement a
    j { jMetaId :: MetaId
    jMetaId = MetaId
    x }  -- fill the identifier part of the judgement
          mv :: MetaVariable
    mv = MetaVar :: MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement MetaId
    -> MetaInstantiation
    -> Set Listener
    -> Frozen
    -> Maybe MetaId
    -> MetaVariable
    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'
      MetaId -> MetaVariable -> TCM ()
    insertMetaVar MetaId
    x MetaVariable
    mv
      MetaId -> TCM MetaId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MetaId
    x

    -- | Get the 'Range' for an interaction point.
    {-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
    getInteractionRange
      :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m)
      => InteractionId -> m Range
    getInteractionRange :: forall (m :: * -> *).
    (MonadInteractionPoints m, MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint

    -- | Get the 'Range' for a meta variable.
    getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range
    getMetaRange :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta

    getInteractionScope
      :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
      => InteractionId -> m ScopeInfo
    getInteractionScope :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta (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 :: * -> *).
    (MonadFail 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 :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    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
      :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m)
      => InteractionId -> m a -> m a
    withInteractionId :: forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    i m a
    ret = do
      MetaId
    m <- InteractionId -> m MetaId
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    i
      MetaId -> m a -> m a
    forall (m :: * -> *) a.
    (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    MetaId -> m a -> m a
    withMetaId MetaId
    m m a
    ret

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

    getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
    getMetaVariables :: forall (m :: * -> *).
    ReadTCState m =>
    (MetaVariable -> Bool) -> m [MetaId]
    getMetaVariables MetaVariable -> Bool
    p = do
      MetaStore
    store <- m MetaStore
    forall (m :: * -> *). ReadTCState m => m MetaStore
    getMetaStore
      [MetaId] -> m [MetaId]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Int -> MetaId
    MetaId Int
    i | (Int
    i, MetaVariable
    mv) <- MetaStore -> [(Int, MetaVariable)]
    forall a. IntMap a -> [(Int, a)]
    IntMap.assocs MetaStore
    store, MetaVariable -> Bool
    p MetaVariable
    mv ]

    getOpenMetas :: ReadTCState m => m [MetaId]
    getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas = (MetaVariable -> Bool) -> m [MetaId]
    forall (m :: * -> *).
    ReadTCState m =>
    (MetaVariable -> Bool) -> m [MetaId]
    getMetaVariables (MetaInstantiation -> Bool
    isOpenMeta (MetaInstantiation -> Bool)
    -> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> MetaInstantiation
    mvInstantiation)

    isOpenMeta :: MetaInstantiation -> Bool
    isOpenMeta :: MetaInstantiation -> Bool
    isOpenMeta MetaInstantiation
    Open                           = Bool
    True
    isOpenMeta MetaInstantiation
    OpenInstance                   = 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 Listener
    mvListeners = Listener -> Set Listener -> Set Listener
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Listener
    l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Set Listener
    mvListeners MetaVariable
    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 Listener
    mvListeners = Listener -> Set Listener -> Set Listener
    forall a. Ord a => a -> Set a -> Set a
    Set.delete Listener
    l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Set Listener
    mvListeners MetaVariable
    mv }

    -- | Get the listeners to a meta.
    getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
    getMetaListeners :: forall (m :: * -> *).
    (MonadFail 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta 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 Listener
    mvListeners = Set Listener
    forall a. Set a
    Set.empty }

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

    -- | Freeze the given meta-variables and return those that were not
    --   already frozen.
    freezeMetas :: MetaStore -> TCM IntSet
    freezeMetas :: MetaStore -> TCM IntSet
    freezeMetas MetaStore
    ms =
      WriterT IntSet (TCMT IO) () -> TCM IntSet
    forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
    execWriterT (WriterT IntSet (TCMT IO) () -> TCM IntSet)
    -> WriterT IntSet (TCMT IO) () -> TCM IntSet
    forall a b. (a -> b) -> a -> b
    $
      Lens' MetaStore TCState
    -> (MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
    -> WriterT IntSet (TCMT IO) ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> m a) -> m ()
    modifyTCLensM Lens' MetaStore TCState
    stMetaStore ((MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
     -> WriterT IntSet (TCMT IO) ())
    -> (MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
    -> WriterT IntSet (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
      StateT MetaStore (WriterT IntSet (TCMT IO)) ()
    -> MetaStore -> WriterT IntSet (TCMT IO) MetaStore
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    execStateT ((Int -> StateT MetaStore (WriterT IntSet (TCMT IO)) ())
    -> [Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Int -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
    forall (m :: * -> *).
    Monad m =>
    Int -> StateT MetaStore (WriterT IntSet m) ()
    freeze ([Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ())
    -> [Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys MetaStore
    ms)
      where
      freeze :: Monad m => Int -> StateT MetaStore (WriterT IntSet m) ()
      freeze :: forall (m :: * -> *).
    Monad m =>
    Int -> StateT MetaStore (WriterT IntSet m) ()
    freeze Int
    m = do
        MetaStore
    store <- StateT MetaStore (WriterT IntSet m) MetaStore
    forall s (m :: * -> *). MonadState s m => m s
    get
        case Int -> MetaStore -> Maybe MetaVariable
    forall a. Int -> IntMap a -> Maybe a
    IntMap.lookup Int
    m MetaStore
    store of
          Just MetaVariable
    mvar
            | MetaVariable -> Frozen
    mvFrozen MetaVariable
    mvar Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Frozen
    Frozen -> do
              WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ())
    -> WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ()
    forall a b. (a -> b) -> a -> b
    $ IntSet -> WriterT IntSet m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Int -> IntSet
    IntSet.singleton Int
    m)
              MetaStore -> StateT MetaStore (WriterT IntSet m) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (MetaStore -> StateT MetaStore (WriterT IntSet m) ())
    -> MetaStore -> StateT MetaStore (WriterT IntSet m) ()
    forall a b. (a -> b) -> a -> b
    $ Int -> MetaVariable -> MetaStore -> MetaStore
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert Int
    m (MetaVariable
    mvar { mvFrozen :: Frozen
    mvFrozen = Frozen
    Frozen }) MetaStore
    store
            | Bool
    otherwise -> () -> StateT MetaStore (WriterT IntSet m) ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Maybe MetaVariable
    Nothing -> StateT MetaStore (WriterT IntSet m) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Thaw all meta variables.
    unfreezeMetas :: TCM ()
    unfreezeMetas :: TCM ()
    unfreezeMetas = (MetaStore -> MetaStore) -> TCM ()
    modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
    -> (MetaStore -> MetaStore) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (MetaVariable -> MetaVariable) -> MetaStore -> MetaStore
    forall a b. (a -> b) -> IntMap a -> IntMap b
    IntMap.map MetaVariable -> MetaVariable
    unfreeze
      where
      unfreeze :: MetaVariable -> MetaVariable
      unfreeze :: MetaVariable -> MetaVariable
    unfreeze MetaVariable
    mvar = MetaVariable
    mvar { mvFrozen :: Frozen
    mvFrozen = Frozen
    Instantiable }

    isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
    isFrozen :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x = do
      MetaVariable
    mvar <- MetaId -> m MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
      Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Frozen
    mvFrozen MetaVariable
    mvar Frozen -> Frozen -> Bool
    forall a. Eq a => a -> a -> Bool
    == Frozen
    Frozen

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

    instance UnFreezeMeta MetaId where
      unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    unfreezeMeta MetaId
    x = 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 :: Frozen
    mvFrozen = Frozen
    Instantiable }
        Type -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> 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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Type
    metaType MetaId
    x

    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 ()
    unfreezeMeta Sort
    s m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> 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 ()
    unfreezeMeta MetaId
    x
      unfreezeMeta (Sort Sort
    s)      = Sort -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    unfreezeMeta Sort
    s
      unfreezeMeta (Level Level
    l)     = Level -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    unfreezeMeta Level
    l
      unfreezeMeta (DontCare Term
    t)  = Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    unfreezeMeta Term
    t
      unfreezeMeta (Lam ArgInfo
    _ Abs Term
    v)     = Abs Term -> m ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    unfreezeMeta Abs Term
    v
      unfreezeMeta Term
    _             = () -> m ()
    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 ()
    unfreezeMeta MetaId
    x
      unfreezeMeta Sort
    _             = () -> m ()
    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 ()
    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 ()
    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 ()
    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 ()
    unfreezeMeta