    module Agda.TypeChecking.Monad.Constraints where

    import Control.Arrow ((&&&))
    import Control.Monad.Except
    import Control.Monad.Reader

    import qualified Data.Foldable as Fold
    import qualified Data.List as List
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Semigroup ((<>))

    import Agda.Interaction.Options.Base
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Closure
    import Agda.TypeChecking.Monad.Debug

    import Agda.Utils.Lens
    import Agda.Utils.Monad

    solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
    solvingProblem :: forall (m :: * -> *) a.
    MonadConstraint m =>
    ProblemId -> m a -> m a
    solvingProblem ProblemId
    pid = Set ProblemId -> m a -> m a
    forall (m :: * -> *) a.
    MonadConstraint m =>
    Set ProblemId -> m a -> m a
    solvingProblems (ProblemId -> Set ProblemId
    forall a. a -> Set a
    Set.singleton ProblemId
    pid)

    solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
    solvingProblems :: forall (m :: * -> *) a.
    MonadConstraint m =>
    Set ProblemId -> m a -> m a
    solvingProblems Set ProblemId
    pids m a
    m = [Char] -> VerboseLevel -> [Char] -> m a -> m a
    forall a. [Char] -> VerboseLevel -> [Char] -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.constr.solve" VerboseLevel
    50 ([Char]
    "working on problems " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemId] -> [Char]
    forall a. Show a => a -> [Char]
    show (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList Set ProblemId
    pids)) (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
      x <- (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envActiveProblems = pids `Set.union` envActiveProblems e }) m a
    m
      Fold.forM_ pids $ \ ProblemId
    pid -> do
        m Bool -> m () -> m () -> m ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (ProblemId -> m Bool
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemSolved ProblemId
    pid)
            ([Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.constr.solve" VerboseLevel
    50 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "problem " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ProblemId -> [Char]
    forall a. Show a => a -> [Char]
    show ProblemId
    pid [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " was not solved.")
          (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
            [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.constr.solve" VerboseLevel
    50 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "problem " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ProblemId -> [Char]
    forall a. Show a => a -> [Char]
    show ProblemId
    pid [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " was solved!"
            (ProblemConstraint -> WakeUp) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints (ProblemId -> Blocker -> WakeUp
    wakeIfBlockedOnProblem ProblemId
    pid (Blocker -> WakeUp)
    -> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker)
      return x

    isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
    isProblemSolved :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemSolved = Bool -> ProblemId -> m Bool
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Bool -> ProblemId -> m Bool
    isProblemSolved' Bool
    False

    isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
    isProblemCompletelySolved :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemCompletelySolved = Bool -> ProblemId -> m Bool
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Bool -> ProblemId -> m Bool
    isProblemSolved' Bool
    True

    isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool
    isProblemSolved' :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Bool -> ProblemId -> m Bool
    isProblemSolved' Bool
    completely ProblemId
    pid =
      m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M (Bool -> Bool
    not (Bool -> Bool) -> (Set ProblemId -> Bool) -> Set ProblemId -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ProblemId
    pid (Set ProblemId -> Bool) -> m (Set ProblemId) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Set ProblemId) -> m (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems)
            (Bool -> Bool
    not (Bool -> Bool)
    -> ([ProblemConstraint] -> Bool) -> [ProblemConstraint] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ProblemConstraint -> Bool
    belongsToUs ([ProblemConstraint] -> Bool) -> m [ProblemConstraint] -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [ProblemConstraint]
    forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAllConstraints)
      where
        belongsToUs :: ProblemConstraint -> Bool
    belongsToUs ProblemConstraint
    c
          | ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.notMember ProblemId
    pid (ProblemConstraint -> Set ProblemId
    constraintProblems ProblemConstraint
    c)         = Bool
    False
          | Constraint -> Bool
    isBlockingConstraint (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) = Bool
    True
          | Bool
    otherwise                                        = Bool
    completely -- Ignore non-blocking unless `completely`

    {-# SPECIALIZE getConstraintsForProblem :: ProblemId -> TCM Constraints #-}
    getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
    getConstraintsForProblem :: forall (m :: * -> *).
    ReadTCState m =>
    ProblemId -> m [ProblemConstraint]
    getConstraintsForProblem ProblemId
    pid = (ProblemConstraint -> Bool)
    -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. (a -> Bool) -> [a] -> [a]
    List.filter (ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ProblemId
    pid (Set ProblemId -> Bool)
    -> (ProblemConstraint -> Set ProblemId)
    -> ProblemConstraint
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Set ProblemId
    constraintProblems) ([ProblemConstraint] -> [ProblemConstraint])
    -> m [ProblemConstraint] -> m [ProblemConstraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [ProblemConstraint]
    forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAllConstraints

    -- | Get the awake constraints
    getAwakeConstraints :: ReadTCState m => m Constraints
    getAwakeConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAwakeConstraints = Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints

    -- danger...
    dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
    dropConstraints :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m ()
    dropConstraints ProblemConstraint -> Bool
    crit = do
      let filt :: [ProblemConstraint] -> [ProblemConstraint]
    filt = (ProblemConstraint -> Bool)
    -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. (a -> Bool) -> [a] -> [a]
    List.filter ((ProblemConstraint -> Bool)
     -> [ProblemConstraint] -> [ProblemConstraint])
    -> (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> [ProblemConstraint]
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool)
    -> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Bool
    crit
      ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifySleepingConstraints [ProblemConstraint] -> [ProblemConstraint]
    filt
      ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifyAwakeConstraints    [ProblemConstraint] -> [ProblemConstraint]
    filt

    -- | Takes out all constraints matching given filter.
    --   Danger!  The taken constraints need to be solved or put back at some point.
    takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints
    takeConstraints :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m [ProblemConstraint]
    takeConstraints ProblemConstraint -> Bool
    f = do
      (takeAwake , keepAwake ) <- (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> ([ProblemConstraint], [ProblemConstraint])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition ProblemConstraint -> Bool
    f ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
    -> m [ProblemConstraint]
    -> m ([ProblemConstraint], [ProblemConstraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints
      (takeAsleep, keepAsleep) <- List.partition f <$> useTC stSleepingConstraints
      modifyAwakeConstraints    $ const keepAwake
      modifySleepingConstraints $ const keepAsleep
      return $ takeAwake ++ takeAsleep

    putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
    putConstraintsToSleep :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m ()
    putConstraintsToSleep ProblemConstraint -> Bool
    sleepy = do
      awakeOnes <- Lens' TCState [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints
      let (gotoSleep, stayAwake) = List.partition sleepy awakeOnes
      modifySleepingConstraints $ (++ gotoSleep)
      modifyAwakeConstraints    $ const stayAwake

    putAllConstraintsToSleep :: MonadConstraint m => m ()
    putAllConstraintsToSleep :: forall (m :: * -> *). MonadConstraint m => m ()
    putAllConstraintsToSleep = (ProblemConstraint -> Bool) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m ()
    putConstraintsToSleep (Bool -> ProblemConstraint -> Bool
    forall a b. a -> b -> a
    const Bool
    True)

    data ConstraintStatus = AwakeConstraint | SleepingConstraint
      deriving (ConstraintStatus -> ConstraintStatus -> Bool
    (ConstraintStatus -> ConstraintStatus -> Bool)
    -> (ConstraintStatus -> ConstraintStatus -> Bool)
    -> Eq ConstraintStatus
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ConstraintStatus -> ConstraintStatus -> Bool
    == :: ConstraintStatus -> ConstraintStatus -> Bool
    $c/= :: ConstraintStatus -> ConstraintStatus -> Bool
    /= :: ConstraintStatus -> ConstraintStatus -> Bool
    Eq, VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
    [ConstraintStatus] -> [Char] -> [Char]
    ConstraintStatus -> [Char]
    (VerboseLevel -> ConstraintStatus -> [Char] -> [Char])
    -> (ConstraintStatus -> [Char])
    -> ([ConstraintStatus] -> [Char] -> [Char])
    -> Show ConstraintStatus
    forall a.
    (VerboseLevel -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
    showsPrec :: VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
    $cshow :: ConstraintStatus -> [Char]
    show :: ConstraintStatus -> [Char]
    $cshowList :: [ConstraintStatus] -> [Char] -> [Char]
    showList :: [ConstraintStatus] -> [Char] -> [Char]
    Show)

    -- | Suspend constraints matching the predicate during the execution of the
    --   second argument. Caution: held sleeping constraints will not be woken up
    --   by events that would normally trigger a wakeup call.
    holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
    holdConstraints :: forall a.
    (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
    holdConstraints ConstraintStatus -> ProblemConstraint -> Bool
    p TCM a
    m = do
      (holdAwake, stillAwake)   <- (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> ([ProblemConstraint], [ProblemConstraint])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (ConstraintStatus -> ProblemConstraint -> Bool
    p ConstraintStatus
    AwakeConstraint)    ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
    -> TCMT IO [ProblemConstraint]
    -> TCMT IO ([ProblemConstraint], [ProblemConstraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState [ProblemConstraint] -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints
      (holdAsleep, stillAsleep) <- List.partition (p SleepingConstraint) <$> useTC stSleepingConstraints
      stAwakeConstraints    `setTCLens` stillAwake
      stSleepingConstraints `setTCLens` stillAsleep
      let restore = do
            ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints    Lens' TCState [ProblemConstraint]
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` ([ProblemConstraint]
    holdAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++)
            ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stSleepingConstraints Lens' TCState [ProblemConstraint]
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` ([ProblemConstraint]
    holdAsleep [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++)
      catchError (m <* restore) (\ TCErr
    err -> TCMT IO ()
    restore TCMT IO () -> TCM a -> TCM a
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> TCErr -> TCM a
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err)

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

    takeAwakeConstraint'
      :: MonadConstraint m
      => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
    takeAwakeConstraint' :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
    takeAwakeConstraint' ProblemConstraint -> Bool
    p = do
      cs <- m [ProblemConstraint]
    forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAwakeConstraints
      case break p cs of
        ([ProblemConstraint]
    _, [])       -> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ProblemConstraint
    forall a. Maybe a
    Nothing
        ([ProblemConstraint]
    cs0, ProblemConstraint
    c : [ProblemConstraint]
    cs) -> do
          ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifyAwakeConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a b. a -> b -> a
    const ([ProblemConstraint]
    cs0 [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemConstraint]
    cs)
          Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ProblemConstraint -> m (Maybe ProblemConstraint))
    -> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
    forall a b. (a -> b) -> a -> b
    $ ProblemConstraint -> Maybe ProblemConstraint
    forall a. a -> Maybe a
    Just ProblemConstraint
    c

    getAllConstraints :: ReadTCState m => m Constraints
    getAllConstraints :: forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAllConstraints = do
      s <- m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      return $ s ^. stAwakeConstraints ++ s ^. stSleepingConstraints

    withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint :: forall (m :: * -> *) a.
    MonadConstraint m =>
    (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint Constraint -> m a
    f (PConstr Set ProblemId
    pids Blocker
    _ Closure Constraint
    c) = do
      -- We should preserve the problem stack and the isSolvingConstraint flag
      (pids', isSolving) <- (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC ((TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool))
    -> (TCEnv -> (Set ProblemId, Bool)) -> m (Set ProblemId, Bool)
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> Set ProblemId
    envActiveProblems (TCEnv -> Set ProblemId)
    -> (TCEnv -> Bool) -> TCEnv -> (Set ProblemId, Bool)
    forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& TCEnv -> Bool
    envSolvingConstraints
      enterClosure c $ \Constraint
    c ->
        (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envActiveProblems = pids', envSolvingConstraints = isSolving }) (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $
        Set ProblemId -> m a -> m a
    forall (m :: * -> *) a.
    MonadConstraint m =>
    Set ProblemId -> m a -> m a
    solvingProblems Set ProblemId
    pids (Constraint -> m a
    f Constraint
    c)

    buildProblemConstraint
      :: (MonadTCEnv m, ReadTCState m)
      => Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint Set ProblemId
    pids Blocker
    unblock Constraint
    c = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr Set ProblemId
    pids Blocker
    unblock (Closure Constraint -> ProblemConstraint)
    -> m (Closure Constraint) -> m ProblemConstraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Constraint -> m (Closure Constraint)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Constraint
    c

    buildProblemConstraint_
      :: (MonadTCEnv m, ReadTCState m)
      => Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint_ :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint_ = Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint Set ProblemId
    forall a. Set a
    Set.empty

    buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
    buildConstraint :: Blocker -> Constraint -> TCM ProblemConstraint
    buildConstraint Blocker
    unblock Constraint
    c = do
      pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
      buildProblemConstraint pids unblock c

    -- | Monad service class containing methods for adding and solving
    --   constraints
    class ( MonadTCEnv m
          , ReadTCState m
          , MonadError TCErr m
          , MonadBlock m
          , HasOptions m
          , MonadDebug m
          ) => MonadConstraint m where
      -- | Unconditionally add the constraint.
      addConstraint :: Blocker -> Constraint -> m ()

      -- | Add constraint as awake constraint.
      addAwakeConstraint :: Blocker -> Constraint -> m ()

      solveConstraint :: Constraint -> m ()

      -- | Solve awake constraints matching the predicate. If the second argument is
      --   True solve constraints even if already 'isSolvingConstraints'.
      solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()

      wakeConstraints :: (ProblemConstraint-> WakeUp) -> m ()

      stealConstraints :: ProblemId -> m ()

      modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()

      modifySleepingConstraints  :: (Constraints -> Constraints) -> m ()

    instance MonadConstraint m => MonadConstraint (ReaderT e m) where
      addConstraint :: Blocker -> Constraint -> ReaderT e m ()
    addConstraint             = (m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((Constraint -> m ()) -> Constraint -> ReaderT e m ())
    -> (Blocker -> Constraint -> m ())
    -> Blocker
    -> Constraint
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint
      addAwakeConstraint :: Blocker -> Constraint -> ReaderT e m ()
    addAwakeConstraint        = (m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((Constraint -> m ()) -> Constraint -> ReaderT e m ())
    -> (Blocker -> Constraint -> m ())
    -> Blocker
    -> Constraint
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addAwakeConstraint
      solveConstraint :: Constraint -> ReaderT e m ()
    solveConstraint           = m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (Constraint -> m ()) -> Constraint -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraint -> m ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint
      solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> ReaderT e m ()
    solveSomeAwakeConstraints = (m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (Bool -> m ()) -> Bool -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((Bool -> m ()) -> Bool -> ReaderT e m ())
    -> ((ProblemConstraint -> Bool) -> Bool -> m ())
    -> (ProblemConstraint -> Bool)
    -> Bool
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> Bool) -> Bool -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> Bool -> m ()
    solveSomeAwakeConstraints
      stealConstraints :: ProblemId -> ReaderT e m ()
    stealConstraints          = m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (ProblemId -> m ()) -> ProblemId -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemId -> m ()
    forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
    stealConstraints
      modifyAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
    modifyAwakeConstraints    = m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
    -> ([ProblemConstraint] -> [ProblemConstraint])
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifyAwakeConstraints
      modifySleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> ReaderT e m ()
    modifySleepingConstraints = m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
    -> ([ProblemConstraint] -> [ProblemConstraint])
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifySleepingConstraints
      wakeConstraints :: (ProblemConstraint -> WakeUp) -> ReaderT e m ()
    wakeConstraints = m () -> ReaderT e m ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT e m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ReaderT e m ())
    -> ((ProblemConstraint -> WakeUp) -> m ())
    -> (ProblemConstraint -> WakeUp)
    -> ReaderT e m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> WakeUp) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints

    -- | Add new a constraint
    addConstraint' :: Blocker -> Constraint -> TCM ()
    addConstraint' :: Blocker -> Constraint -> TCMT IO ()
    addConstraint' = Lens' TCState [ProblemConstraint]
    -> Blocker -> Constraint -> TCMT IO ()
    addConstraintTo ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stSleepingConstraints

    addAwakeConstraint' :: Blocker -> Constraint -> TCM ()
    addAwakeConstraint' :: Blocker -> Constraint -> TCMT IO ()
    addAwakeConstraint' = Lens' TCState [ProblemConstraint]
    -> Blocker -> Constraint -> TCMT IO ()
    addConstraintTo ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints

    addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM ()
    addConstraintTo :: Lens' TCState [ProblemConstraint]
    -> Blocker -> Constraint -> TCMT IO ()
    addConstraintTo Lens' TCState [ProblemConstraint]
    bucket Blocker
    unblock Constraint
    c = do
        pc <- Blocker -> Constraint -> TCM ProblemConstraint
    buildConstraint Blocker
    unblock Constraint
    c
        stDirty `setTCLens` True
        bucket `modifyTCLens` (pc :)

    -- | A problem is considered solved if there are no unsolved blocking constraints belonging to it.
    --   There's no really good principle for what constraints are blocking and which are not, but the
    --   general idea is that nothing bad should happen if you assume a non-blocking constraint is
    --   solvable, but it turns out it isn't. For instance, assuming an equality constraint between two
    --   types that turns out to be false can lead to ill typed terms in places where we don't expect
    --   them.
    isBlockingConstraint :: Constraint -> Bool
    isBlockingConstraint :: Constraint -> Bool
    isBlockingConstraint = \case
      SortCmp{}             -> Bool
    False
      LevelCmp{}            -> Bool
    False
      FindInstance{}        -> Bool
    False
      ResolveInstanceHead{} -> Bool
    False
      HasBiggerSort{}       -> Bool
    False
      HasPTSRule{}          -> Bool
    False
      CheckDataSort{}       -> Bool
    False
      ValueCmp{}            -> Bool
    True
      ValueCmpOnFace{}      -> Bool
    True
      ElimCmp{}             -> Bool
    True
      UnBlock{}             -> Bool
    True
      IsEmpty{}             -> Bool
    True
      CheckSizeLtSat{}      -> Bool
    True
      CheckFunDef{}         -> Bool
    True
      UnquoteTactic{}       -> Bool
    True
      CheckMetaInst{}       -> Bool
    True
      CheckType{}           -> Bool
    True
      CheckLockedVars{}     -> Bool
    True
      UsableAtModality{}    -> Bool
    True

    -- | Start solving constraints
    nowSolvingConstraints :: MonadTCEnv m => m a -> m a
    nowSolvingConstraints :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    nowSolvingConstraints = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envSolvingConstraints = True }

    isSolvingConstraints :: MonadTCEnv m => m Bool
    isSolvingConstraints :: forall (m :: * -> *). MonadTCEnv m => m Bool
    isSolvingConstraints = (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envSolvingConstraints

    -- | Add constraint if the action raises a pattern violation
    catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
    catchConstraint :: forall (m :: * -> *).
    MonadConstraint m =>
    Constraint -> m () -> m ()
    catchConstraint Constraint
    c = (Blocker -> m ()) -> m () -> m ()
    forall a. (Blocker -> m a) -> m a -> m a
    forall (m :: * -> *) a.
    MonadBlock m =>
    (Blocker -> m a) -> m a -> m a
    catchPatternErr ((Blocker -> m ()) -> m () -> m ())
    -> (Blocker -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Blocker
    unblock -> Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    unblock Constraint
    c

    isInstanceConstraint :: Constraint -> Bool
    isInstanceConstraint :: Constraint -> Bool
    isInstanceConstraint FindInstance{} = Bool
    True
    isInstanceConstraint Constraint
    _              = Bool
    False

    canDropRecursiveInstance :: (ReadTCState m, HasOptions m) => m Bool
    canDropRecursiveInstance :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    canDropRecursiveInstance =
      m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M ((TCState -> Lens' TCState Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stConsideringInstance) (TCState -> Bool) -> m TCState -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState)
            (Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optBacktrackingInstances (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)

    shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch :: forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch = m Bool
    forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    canDropRecursiveInstance m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` ((TCState -> Lens' TCState Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stPostponeInstanceSearch) (TCState -> Bool) -> m TCState -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState)

    -- | Wake constraints matching the given predicate (and aren't instance
    --   constraints if 'shouldPostponeInstanceSearch').
    wakeConstraints' :: MonadConstraint m => (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints' :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints' ProblemConstraint -> WakeUp
    p = do
      skipInstance <- m Bool
    forall (m :: * -> *). (ReadTCState m, HasOptions m) => m Bool
    shouldPostponeInstanceSearch
      let skip ProblemConstraint
    c = Bool
    skipInstance Bool -> Bool -> Bool
    && Constraint -> Bool
    isInstanceConstraint (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)
      wakeConstraints $ wakeUpWhen (not . skip) p

    ---------------------------------------------------------------------------
    -- * Lenses
    ---------------------------------------------------------------------------

    mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
    mapAwakeConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
    mapAwakeConstraints = Lens' TCState [ProblemConstraint]
    -> ([ProblemConstraint] -> [ProblemConstraint])
    -> TCState
    -> TCState
    forall o i. Lens' o i -> LensMap o i
    over ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stAwakeConstraints

    mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState
    mapSleepingConstraints :: ([ProblemConstraint] -> [ProblemConstraint]) -> TCState -> TCState
    mapSleepingConstraints = Lens' TCState [ProblemConstraint]
    -> ([ProblemConstraint] -> [ProblemConstraint])
    -> TCState
    -> TCState
    forall o i. Lens' o i -> LensMap o i
    over ([ProblemConstraint] -> f [ProblemConstraint])
    -> TCState -> f TCState
    Lens' TCState [ProblemConstraint]
    stSleepingConstraints