    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.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 (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
      a
    x <- (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envActiveProblems :: Set ProblemId
    envActiveProblems = Set ProblemId
    pids Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` TCEnv -> Set ProblemId
    envActiveProblems TCEnv
    e }) m a
    m
      Set ProblemId -> (ProblemId -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    Fold.forM_ Set ProblemId
    pids ((ProblemId -> m ()) -> m ()) -> (ProblemId -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ 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)
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
    isProblemSolved :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemSolved 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 (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] -> 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)

    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' [ProblemConstraint] TCState -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' [ProblemConstraint] TCState
    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
      ([ProblemConstraint]
    takeAwake , [ProblemConstraint]
    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' [ProblemConstraint] TCState -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stAwakeConstraints
      ([ProblemConstraint]
    takeAsleep, [ProblemConstraint]
    keepAsleep) <- (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' [ProblemConstraint] TCState -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stSleepingConstraints
      ([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]
    keepAwake
      ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifySleepingConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a b. a -> b -> a
    const [ProblemConstraint]
    keepAsleep
      [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ProblemConstraint] -> m [ProblemConstraint])
    -> [ProblemConstraint] -> m [ProblemConstraint]
    forall a b. (a -> b) -> a -> b
    $ [ProblemConstraint]
    takeAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemConstraint]
    takeAsleep

    putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
    putConstraintsToSleep :: forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m ()
    putConstraintsToSleep ProblemConstraint -> Bool
    sleepy = do
      [ProblemConstraint]
    awakeOnes <- Lens' [ProblemConstraint] TCState -> m [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' [ProblemConstraint] TCState
    stAwakeConstraints
      let ([ProblemConstraint]
    gotoSleep, [ProblemConstraint]
    stayAwake) = (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> ([ProblemConstraint], [ProblemConstraint])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition ProblemConstraint -> Bool
    sleepy [ProblemConstraint]
    awakeOnes
      ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    modifySleepingConstraints (([ProblemConstraint] -> [ProblemConstraint]) -> m ())
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ ([ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemConstraint]
    gotoSleep)
      ([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]
    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
    /= :: ConstraintStatus -> ConstraintStatus -> Bool
    $c/= :: ConstraintStatus -> ConstraintStatus -> Bool
    == :: ConstraintStatus -> ConstraintStatus -> Bool
    $c== :: 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
    showList :: [ConstraintStatus] -> [Char] -> [Char]
    $cshowList :: [ConstraintStatus] -> [Char] -> [Char]
    show :: ConstraintStatus -> [Char]
    $cshow :: ConstraintStatus -> [Char]
    showsPrec :: VerboseLevel -> ConstraintStatus -> [Char] -> [Char]
    $cshowsPrec :: VerboseLevel -> 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
      ([ProblemConstraint]
    holdAwake, [ProblemConstraint]
    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' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stAwakeConstraints
      ([ProblemConstraint]
    holdAsleep, [ProblemConstraint]
    stillAsleep) <- (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> ([ProblemConstraint], [ProblemConstraint])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (ConstraintStatus -> ProblemConstraint -> Bool
    p ConstraintStatus
    SleepingConstraint) ([ProblemConstraint] -> ([ProblemConstraint], [ProblemConstraint]))
    -> TCMT IO [ProblemConstraint]
    -> TCMT IO ([ProblemConstraint], [ProblemConstraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [ProblemConstraint] TCState
    stSleepingConstraints
      Lens' [ProblemConstraint] TCState
    stAwakeConstraints    Lens' [ProblemConstraint] TCState
    -> [ProblemConstraint] -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` [ProblemConstraint]
    stillAwake
      Lens' [ProblemConstraint] TCState
    stSleepingConstraints Lens' [ProblemConstraint] TCState
    -> [ProblemConstraint] -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` [ProblemConstraint]
    stillAsleep
      let restore :: TCMT IO ()
    restore = do
            Lens' [ProblemConstraint] TCState
    stAwakeConstraints    Lens' [ProblemConstraint] TCState
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` ([ProblemConstraint]
    holdAwake [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++)
            Lens' [ProblemConstraint] TCState
    stSleepingConstraints Lens' [ProblemConstraint] TCState
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` ([ProblemConstraint]
    holdAsleep [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++)
      TCM a -> (TCErr -> TCM a) -> TCM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError (TCM a
    m TCM a -> TCMT IO () -> TCM a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* TCMT IO ()
    restore) (\ TCErr
    err -> TCMT IO ()
    restore TCMT IO () -> TCM a -> TCM a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> TCErr -> TCM 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
      [ProblemConstraint]
    cs <- m [ProblemConstraint]
    forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
    getAwakeConstraints
      case (ProblemConstraint -> Bool)
    -> [ProblemConstraint]
    -> ([ProblemConstraint], [ProblemConstraint])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break ProblemConstraint -> Bool
    p [ProblemConstraint]
    cs of
        ([ProblemConstraint]
    _, [])       -> Maybe ProblemConstraint -> m (Maybe ProblemConstraint)
    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 (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
      TCState
    s <- m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      [ProblemConstraint] -> m [ProblemConstraint]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ProblemConstraint] -> m [ProblemConstraint])
    -> [ProblemConstraint] -> m [ProblemConstraint]
    forall a b. (a -> b) -> a -> b
    $ TCState
    sTCState -> Lens' [ProblemConstraint] TCState -> [ProblemConstraint]
    forall o i. o -> Lens' i o -> i
    ^.Lens' [ProblemConstraint] TCState
    stAwakeConstraints [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. [a] -> [a] -> [a]
    ++ TCState
    sTCState -> Lens' [ProblemConstraint] TCState -> [ProblemConstraint]
    forall o i. o -> Lens' i o -> i
    ^.Lens' [ProblemConstraint] TCState
    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
      (Set ProblemId
    pids', Bool
    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 (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& TCEnv -> Bool
    envSolvingConstraints
      Closure Constraint -> (Constraint -> m a) -> m a
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Constraint
    c ((Constraint -> m a) -> m a) -> (Constraint -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $ \Constraint
    c ->
        (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envActiveProblems :: Set ProblemId
    envActiveProblems = Set ProblemId
    pids', envSolvingConstraints :: Bool
    envSolvingConstraints = Bool
    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
      Set ProblemId
    pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
      Set ProblemId -> Blocker -> Constraint -> TCM ProblemConstraint
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Set ProblemId -> Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint Set ProblemId
    pids Blocker
    unblock Constraint
    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 (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 (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 (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 (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 (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 (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 (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 (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

    addAndUnblocker :: MonadBlock m => Blocker -> m a -> m a
    addAndUnblocker :: forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
    addAndUnblocker Blocker
    u
      | Blocker
    u Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock = m a -> m a
    forall a. a -> a
    id
      | Bool
    otherwise          = (Blocker -> m a) -> m a -> m a
    forall (m :: * -> *) a.
    MonadBlock m =>
    (Blocker -> m a) -> m a -> m a
    catchPatternErr ((Blocker -> m a) -> m a -> m a) -> (Blocker -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ Blocker
    u' -> Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker
    u Blocker -> Blocker -> Blocker
    forall a. Semigroup a => a -> a -> a
    <> Blocker
    u')

    addOrUnblocker :: MonadBlock m => Blocker -> m a -> m a
    addOrUnblocker :: forall (m :: * -> *) a. MonadBlock m => Blocker -> m a -> m a
    addOrUnblocker Blocker
    u
      | Blocker
    u Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    neverUnblock = m a -> m a
    forall a. a -> a
    id
      | Bool
    otherwise         = (Blocker -> m a) -> m a -> m a
    forall (m :: * -> *) a.
    MonadBlock m =>
    (Blocker -> m a) -> m a -> m a
    catchPatternErr ((Blocker -> m a) -> m a -> m a) -> (Blocker -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \ Blocker
    u' -> Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> Blocker -> Blocker
    unblockOnEither Blocker
    u Blocker
    u')

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

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

    addConstraintTo :: Lens' Constraints TCState -> Blocker -> Constraint -> TCM ()
    addConstraintTo :: Lens' [ProblemConstraint] TCState
    -> Blocker -> Constraint -> TCMT IO ()
    addConstraintTo Lens' [ProblemConstraint] TCState
    bucket Blocker
    unblock Constraint
    c = do
        ProblemConstraint
    pc <- TCM ProblemConstraint
    build
        Lens' Bool TCState
    stDirty Lens' Bool TCState -> Bool -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Bool
    True
        Lens' [ProblemConstraint] TCState
    bucket Lens' [ProblemConstraint] TCState
    -> ([ProblemConstraint] -> [ProblemConstraint]) -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` (ProblemConstraint
    pc ProblemConstraint -> [ProblemConstraint] -> [ProblemConstraint]
    forall a. a -> [a] -> [a]
    :)
      where
        build :: TCM ProblemConstraint
    build | Constraint -> Bool
    isBlocking Constraint
    c = Blocker -> Constraint -> TCM ProblemConstraint
    buildConstraint Blocker
    unblock Constraint
    c
              | Bool
    otherwise    = Blocker -> Constraint -> TCM ProblemConstraint
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    Blocker -> Constraint -> m ProblemConstraint
    buildProblemConstraint_ Blocker
    unblock Constraint
    c
        isBlocking :: Constraint -> Bool
    isBlocking = \case
          SortCmp{}        -> Bool
    False
          LevelCmp{}       -> Bool
    False
          FindInstance{}   -> Bool
    False
          HasBiggerSort{}  -> Bool
    False
          HasPTSRule{}     -> 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 (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 :: Bool
    envSolvingConstraints = Bool
    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 (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

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

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

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