    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Constraints where

    import Prelude hiding (null)

    import Control.Monad.Except ( MonadError )

    import qualified Data.List as List
    import qualified Data.Set as Set
    import Data.Either

    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty ( prettyShow )
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.InstanceArguments
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.LevelConstraints
    import Agda.TypeChecking.SizedTypes
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Warnings

    import Agda.TypeChecking.Irrelevance
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Data ( checkDataSort )
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Def
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
    import {-# SOURCE #-} Agda.TypeChecking.Conversion
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import {-# SOURCE #-} Agda.TypeChecking.Empty
    import {-# SOURCE #-} Agda.TypeChecking.Lock
    import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType )

    import Agda.Utils.CallStack ( withCurrentCallStack )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null ()
    import qualified Agda.Utils.ProfileOptions as Profile
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    instance MonadConstraint TCM where
      addConstraint :: Blocker -> Constraint -> TCM ()
    addConstraint             = Blocker -> Constraint -> TCM ()
    addConstraintTCM
      addAwakeConstraint :: Blocker -> Constraint -> TCM ()
    addAwakeConstraint        = Blocker -> Constraint -> TCM ()
    addAwakeConstraint'
      solveConstraint :: Constraint -> TCM ()
    solveConstraint           = Constraint -> TCM ()
    solveConstraintTCM
      solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
    solveSomeAwakeConstraints = (ProblemConstraint -> Bool) -> Bool -> TCM ()
    solveSomeAwakeConstraintsTCM
      wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM ()
    wakeConstraints           = (ProblemConstraint -> WakeUp) -> TCM ()
    wakeConstraintsTCM
      stealConstraints :: ProblemId -> TCM ()
    stealConstraints          = ProblemId -> TCM ()
    stealConstraintsTCM
      modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM ()
    modifyAwakeConstraints    = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((Constraints -> Constraints) -> TCState -> TCState)
    -> (Constraints -> Constraints)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraints -> Constraints) -> TCState -> TCState
    mapAwakeConstraints
      modifySleepingConstraints :: (Constraints -> Constraints) -> TCM ()
    modifySleepingConstraints = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((Constraints -> Constraints) -> TCState -> TCState)
    -> (Constraints -> Constraints)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraints -> Constraints) -> TCState -> TCState
    mapSleepingConstraints

    addConstraintTCM :: Blocker -> Constraint -> TCM ()
    addConstraintTCM :: Blocker -> Constraint -> TCM ()
    addConstraintTCM 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
          reportSDoc "tc.constr.add" 20 $ hsep
            [ "adding constraint"
            , prettyTCM . PConstr pids unblock =<< buildClosure c
            , "unblocker: " , prettyTCM unblock
            ]
          -- Jesper, 2022-10-22: We should never block on a meta that is
          -- already solved.
          forM_ (allBlockingMetas unblock) $ \ MetaId
    m ->
            TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (MetaId -> TCMT IO Bool
    forall a (m :: * -> *).
    (IsInstantiatedMeta a, ReadTCState m) =>
    a -> m Bool
    forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
    isInstantiatedMeta MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.add" Int
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Attempted to block on solved meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m
              TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- Need to reduce to reveal possibly blocking metas
          c <- reduce =<< instantiateFull c
          caseMaybeM (simpl c) {-no-} (addConstraint' unblock c) $ {-yes-} \ [Constraint]
    cs -> do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.add" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  simplified:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Constraint -> TCMT IO Doc) -> [Constraint] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
    prettyTCM [Constraint]
    cs)
              (Constraint -> TCM ()) -> [Constraint] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Constraint -> TCM ()
    solveConstraint_ [Constraint]
    cs
          -- The added constraint can cause instance constraints to be solved,
          -- but only the constraints which aren’t blocked on an uninstantiated meta.
          unless (isInstanceConstraint c) $
             wakeConstraints' isWakeableInstanceConstraint
        where
          isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
          isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
    isWakeableInstanceConstraint ProblemConstraint
    c =
            case 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 of
              FindInstance{}
                | ProblemConstraint -> Blocker
    constraintUnblocker ProblemConstraint
    c Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock -> WakeUp
    WakeUp
              Constraint
    _ -> Maybe Blocker -> WakeUp
    DontWakeUp Maybe Blocker
    forall a. Maybe a
    Nothing

          isLvl :: Constraint -> Bool
    isLvl LevelCmp{} = Bool
    True
          isLvl Constraint
    _          = Bool
    False

          -- Try to simplify a level constraint
          simpl :: Constraint -> TCM (Maybe [Constraint])
          simpl :: Constraint -> TCMT IO (Maybe [Constraint])
    simpl Constraint
    c
            | Constraint -> Bool
    isLvl Constraint
    c = do
              -- Get all level constraints.
              lvlcs <- [Closure Constraint] -> TCMT IO [Closure Constraint]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ([Closure Constraint] -> TCMT IO [Closure Constraint])
    -> TCMT IO [Closure Constraint] -> TCMT IO [Closure Constraint]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
                (Closure Constraint -> Bool)
    -> [Closure Constraint] -> [Closure Constraint]
    forall a. (a -> Bool) -> [a] -> [a]
    List.filter (Constraint -> Bool
    isLvl (Constraint -> Bool)
    -> (Closure Constraint -> Constraint) -> Closure Constraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue) ([Closure Constraint] -> [Closure Constraint])
    -> (Constraints -> [Closure Constraint])
    -> Constraints
    -> [Closure Constraint]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProblemConstraint -> Closure Constraint)
    -> Constraints -> [Closure Constraint]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> Closure Constraint
    theConstraint (Constraints -> [Closure Constraint])
    -> TCMT IO Constraints -> TCMT IO [Closure Constraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    getAllConstraints
              List1.ifNull lvlcs (return Nothing) $ {-else-} \ List1 (Closure Constraint)
    lvlcs -> do
                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.lvl" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "simplifying level constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Constraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
    prettyTCM Constraint
    c
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang TCMT IO Doc
    "using" Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ List1 (Closure Constraint) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    List1 (Closure Constraint) -> m Doc
    prettyTCM List1 (Closure Constraint)
    lvlcs
                  ]
                -- Try to simplify @c@ using the other constraints.
                Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Constraint] -> TCMT IO (Maybe [Constraint]))
    -> Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
    forall a b. (a -> b) -> a -> b
    $ Constraint -> List1 Constraint -> Maybe [Constraint]
    simplifyLevelConstraint Constraint
    c (List1 Constraint -> Maybe [Constraint])
    -> List1 Constraint -> Maybe [Constraint]
    forall a b. (a -> b) -> a -> b
    $ (Closure Constraint -> Constraint)
    -> List1 (Closure Constraint) -> List1 Constraint
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue List1 (Closure Constraint)
    lvlcs
            | Bool
    otherwise = Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [Constraint]
    forall a. Maybe a
    Nothing

    wakeConstraintsTCM :: (ProblemConstraint-> WakeUp) -> TCM ()
    wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
    wakeConstraintsTCM ProblemConstraint -> WakeUp
    wake = do
      c <- Lens' TCState Constraints -> TCMT IO Constraints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Constraints -> f Constraints) -> TCState -> f TCState
    Lens' TCState Constraints
    stSleepingConstraints
      let (wakeup, sleepin) = partitionEithers $ map checkWakeUp c
      reportSLn "tc.constr.wake" 50 $
        "waking up         " ++ show (List.map (Set.toList . constraintProblems) wakeup) ++ "\n" ++
        "  still sleeping: " ++ show (List.map (Set.toList . constraintProblems) sleepin)
      modifySleepingConstraints $ const sleepin
      modifyAwakeConstraints (++ wakeup)
      where
        checkWakeUp :: ProblemConstraint -> Either ProblemConstraint ProblemConstraint
    checkWakeUp ProblemConstraint
    c = case ProblemConstraint -> WakeUp
    wake ProblemConstraint
    c of
          WakeUp
    WakeUp              -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
    forall a b. a -> Either a b
    Left ProblemConstraint
    c
          DontWakeUp Maybe Blocker
    Nothing  -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
    forall a b. b -> Either a b
    Right ProblemConstraint
    c
          DontWakeUp (Just Blocker
    u) -> ProblemConstraint -> Either ProblemConstraint ProblemConstraint
    forall a b. b -> Either a b
    Right ProblemConstraint
    c{ constraintUnblocker = u }

    -- | Add all constraints belonging to the given problem to the current problem(s).
    stealConstraintsTCM :: ProblemId -> TCM ()
    stealConstraintsTCM :: ProblemId -> TCM ()
    stealConstraintsTCM ProblemId
    pid = do
      current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
      reportSLn "tc.constr.steal" 50 $ "problem " ++ show (Set.toList current) ++ " is stealing problem " ++ show pid ++ "'s constraints!"
      -- Add current to any constraint in pid.
      let rename pc :: ProblemConstraint
    pc@(PConstr Set ProblemId
    pids Blocker
    u Closure Constraint
    c) | ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ProblemId
    pid Set ProblemId
    pids = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set ProblemId
    current Set ProblemId
    pids) Blocker
    u Closure Constraint
    c
                                       | Bool
    otherwise           = ProblemConstraint
    pc
      -- We should never steal from an active problem.
      whenM (Set.member pid <$> asksTC envActiveProblems) __IMPOSSIBLE__
      modifyAwakeConstraints    $ List.map rename
      modifySleepingConstraints $ List.map rename

    {-# SPECIALIZE noConstraints :: TCM a -> TCM a #-}
    -- | Don't allow the argument to produce any blocking constraints.
    --
    -- WARNING: this does not mean that the given computation cannot
    -- constrain the solution space further.
    -- It can well do so, by solving metas.
    noConstraints
      :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
      => m a -> m a
    noConstraints :: forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints = Bool -> m a -> m a
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    Bool -> m a -> m a
    noConstraints' Bool
    False

    -- | As noConstraints but also fail for non-blocking constraints.
    reallyNoConstraints
      :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
      => m a -> m a
    reallyNoConstraints :: forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    reallyNoConstraints = Bool -> m a -> m a
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    Bool -> m a -> m a
    noConstraints' Bool
    True

    noConstraints'
      :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
      => Bool -> m a -> m a
    noConstraints' :: forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    Bool -> m a -> m a
    noConstraints' Bool
    includingNonBlocking m a
    problem = do
      (pid, x) <- m a -> m (ProblemId, a)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem m a
    problem
      let counts | Bool
    includingNonBlocking = Bool -> ProblemConstraint -> Bool
    forall a b. a -> b -> a
    const Bool
    True
                 | Bool
    otherwise            = Constraint -> Bool
    isBlockingConstraint (Constraint -> Bool)
    -> (ProblemConstraint -> Constraint) -> ProblemConstraint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (Closure Constraint -> Constraint)
    -> (ProblemConstraint -> Closure Constraint)
    -> ProblemConstraint
    -> Constraint
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Closure Constraint
    theConstraint
      cs <- List.filter counts <$> getConstraintsForProblem pid
      List1.ifNull cs (pure ()) \ List1 ProblemConstraint
    cs -> do
        (CallStack -> m ()) -> m ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCurrentCallStack \ CallStack
    loc -> do
          w <- CallStack -> Warning -> m TCWarning
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_ CallStack
    loc (Warning -> m TCWarning) -> Warning -> m TCWarning
    forall a b. (a -> b) -> a -> b
    $ List1 ProblemConstraint -> Warning
    UnsolvedConstraints List1 ProblemConstraint
    cs
          typeError' loc $ NonFatalErrors $ singleton w
      return x

    -- | Run a computation that should succeeds without constraining
    --   the solution space, i.e., not add any information about meta-variables.
    nonConstraining ::
      ( HasOptions m
      , MonadConstraint m
      , MonadDebug m
      , MonadError TCErr m
      , MonadFresh ProblemId m
      , MonadTCEnv m
      , MonadWarning m
      ) => m a -> m a
    nonConstraining :: forall (m :: * -> *) a.
    (HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m,
     MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) =>
    m a -> m a
    nonConstraining = m a -> m a
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (m a -> m a) -> (m a -> m a) -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m a -> m a
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints

    {-# SPECIALIZE newProblem :: TCM a -> TCM (ProblemId, a) #-}
    -- | Create a fresh problem for the given action.
    newProblem
      :: (MonadFresh ProblemId m, MonadConstraint m)
      => m a -> m (ProblemId, a)
    newProblem :: forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem m a
    action = do
      pid <- m ProblemId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      -- Don't get distracted by other constraints while working on the problem
      x <- nowSolvingConstraints $ solvingProblem pid action
      -- Now we can check any woken constraints
      solveAwakeConstraints
      return (pid, x)

    {-# SPECIALIZE newProblem_ :: TCM a -> TCM ProblemId #-}
    newProblem_
      :: (MonadFresh ProblemId m, MonadConstraint m)
      => m a -> m ProblemId
    newProblem_ :: forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m ProblemId
    newProblem_ m a
    action = (ProblemId, a) -> ProblemId
    forall a b. (a, b) -> a
    fst ((ProblemId, a) -> ProblemId) -> m (ProblemId, a) -> m ProblemId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m a -> m (ProblemId, a)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem m a
    action

    ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
    ifNoConstraints :: forall a b.
    TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
    ifNoConstraints TCM a
    check a -> TCM b
    ifNo ProblemId -> a -> TCM b
    ifCs = do
      (pid, x) <- TCM a -> TCMT IO (ProblemId, a)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem TCM a
    check
      ifM (isProblemSolved pid) (ifNo x) (ifCs pid x)

    ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
    ifNoConstraints_ :: forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
    ifNoConstraints_ TCM ()
    check TCM a
    ifNo ProblemId -> TCM a
    ifCs = TCM () -> (() -> TCM a) -> (ProblemId -> () -> TCM a) -> TCM a
    forall a b.
    TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
    ifNoConstraints TCM ()
    check (TCM a -> () -> TCM a
    forall a b. a -> b -> a
    const TCM a
    ifNo) (\ProblemId
    pid ()
    _ -> ProblemId -> TCM a
    ifCs ProblemId
    pid)

    -- | @guardConstraint c blocker@ tries to solve @blocker@ first.
    --   If successful without constraints, it moves on to solve @c@, otherwise it
    --   adds a @c@ to the constraint pool, blocked by the problem generated by @blocker@.
    guardConstraint :: Constraint -> TCM () -> TCM ()
    guardConstraint :: Constraint -> TCM () -> TCM ()
    guardConstraint Constraint
    c TCM ()
    blocker =
      TCM () -> TCM () -> (ProblemId -> TCM ()) -> TCM ()
    forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
    ifNoConstraints_ TCM ()
    blocker (Constraint -> TCM ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint Constraint
    c) (\ ProblemId
    pid -> Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint (ProblemId -> Blocker
    unblockOnProblem ProblemId
    pid) Constraint
    c)

    whenConstraints :: TCM () -> TCM () -> TCM ()
    whenConstraints :: TCM () -> TCM () -> TCM ()
    whenConstraints TCM ()
    action TCM ()
    handler =
      TCM () -> TCM () -> (ProblemId -> TCM ()) -> TCM ()
    forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
    ifNoConstraints_ TCM ()
    action (() -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((ProblemId -> TCM ()) -> TCM ())
    -> (ProblemId -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ProblemId
    pid -> do
        ProblemId -> TCM ()
    forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
    stealConstraints ProblemId
    pid
        TCM ()
    handler

    {-# SPECIALIZE wakeupConstraints :: MetaId -> TCM () #-}
    -- | Wake up the constraints depending on the given meta.
    wakeupConstraints :: MonadMetaSolver m => MetaId -> m ()
    wakeupConstraints :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    wakeupConstraints MetaId
    x = do
      (ProblemConstraint -> WakeUp) -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints' (MetaId -> Blocker -> WakeUp
    wakeIfBlockedOnMeta MetaId
    x (Blocker -> WakeUp)
    -> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker)
      m ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints

    -- | Wake up all constraints not blocked on a problem.
    wakeupConstraints_ :: TCM ()
    wakeupConstraints_ :: TCM ()
    wakeupConstraints_ = do
      (ProblemConstraint -> WakeUp) -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> WakeUp) -> m ()
    wakeConstraints' (Blocker -> WakeUp
    wakeup (Blocker -> WakeUp)
    -> (ProblemConstraint -> Blocker) -> ProblemConstraint -> WakeUp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Blocker
    constraintUnblocker)
      TCM ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints
      where
        wakeup :: Blocker -> WakeUp
    wakeup Blocker
    u | Set ProblemId -> Bool
    forall a. Set a -> Bool
    Set.null (Set ProblemId -> Bool) -> Set ProblemId -> Bool
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Set ProblemId
    allBlockingProblems Blocker
    u = WakeUp
    WakeUp
                 | Bool
    otherwise                        = Maybe Blocker -> WakeUp
    DontWakeUp Maybe Blocker
    forall a. Maybe a
    Nothing

    -- | Solve awake constraints matching the predicate. If the second argument is
    --   True solve constraints even if already 'isSolvingConstraints'.
    solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
    solveSomeAwakeConstraintsTCM :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
    solveSomeAwakeConstraintsTCM ProblemConstraint -> Bool
    solveThis Bool
    force = do
        ProfileOption -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Constraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Integer -> TCM ()
    forall (m :: * -> *).
    MonadStatistics m =>
    [Char] -> Integer -> m ()
    tickMax [Char]
    "max-open-constraints" (Integer -> TCM ())
    -> (Constraints -> Integer) -> Constraints -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraints -> Integer
    forall i a. Num i => [a] -> i
    List.genericLength (Constraints -> TCM ()) -> TCMT IO Constraints -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    getAllConstraints
        TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ((Bool
    force Bool -> Bool -> Bool
    ||) (Bool -> Bool) -> (Bool -> Bool) -> Bool -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isSolvingConstraints) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    nowSolvingConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
         -- solveSizeConstraints -- Andreas, 2012-09-27 attacks size constrs too early
         -- Ulf, 2016-12-06: Don't inherit problems here! Stored constraints
         -- already contain all their dependencies.
         Lens' TCEnv (Set ProblemId)
    -> (Set ProblemId -> Set ProblemId) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
    Lens' TCEnv (Set ProblemId)
    eActiveProblems (Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a b. a -> b -> a
    const Set ProblemId
    forall a. Set a
    Set.empty) TCM ()
    solve
      where
        solve :: TCM ()
    solve = do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.solve" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ TCMT IO Doc
    "Solving awake constraints."
                                                 , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Constraints -> [Char]) -> Constraints -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [Char]
    forall a. Show a => a -> [Char]
    show (Int -> [Char]) -> (Constraints -> Int) -> Constraints -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraints -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Constraints -> TCMT IO Doc) -> TCMT IO Constraints -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => m Constraints
    getAwakeConstraints
                                                 , TCMT IO Doc
    "remaining." ]
          TCMT IO (Maybe ProblemConstraint)
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM ((ProblemConstraint -> Bool) -> TCMT IO (Maybe ProblemConstraint)
    forall (m :: * -> *).
    MonadConstraint m =>
    (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
    takeAwakeConstraint' ProblemConstraint -> Bool
    solveThis) ((ProblemConstraint -> TCM ()) -> TCM ())
    -> (ProblemConstraint -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ ProblemConstraint
    c -> do
            (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
    forall (m :: * -> *) a.
    MonadConstraint m =>
    (Constraint -> m a) -> ProblemConstraint -> m a
    withConstraint Constraint -> TCM ()
    forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
    solveConstraint ProblemConstraint
    c
            TCM ()
    solve

    solveConstraintTCM :: Constraint -> TCM ()
    solveConstraintTCM :: Constraint -> TCM ()
    solveConstraintTCM Constraint
    c = do
        ProfileOption -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Constraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCM ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "attempted-constraints"
        [Char] -> Int -> [Char] -> TCM () -> TCM ()
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.constr.solve" Int
    20 [Char]
    "solving constraint" (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
          reportSDoc "tc.constr.solve.constr" 20 $ text (show $ Set.toList pids) <+> prettyTCM c
          solveConstraint_ c

    solveConstraint_ :: Constraint -> TCM ()
    solveConstraint_ :: Constraint -> TCM ()
    solveConstraint_ (ValueCmp Comparison
    cmp CompareAs
    a Term
    u Term
    v)       = Comparison -> CompareAs -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> CompareAs -> Term -> Term -> m ()
    compareAs Comparison
    cmp CompareAs
    a Term
    u Term
    v
    solveConstraint_ (ValueCmpOnFace Comparison
    cmp Term
    p Type
    a Term
    u Term
    v) = Comparison -> Term -> Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Term -> Type -> Term -> Term -> m ()
    compareTermOnFace Comparison
    cmp Term
    p Type
    a Term
    u Term
    v
    solveConstraint_ (ElimCmp [Polarity]
    cmp [IsForced]
    fs Type
    a Term
    e [Elim]
    u [Elim]
    v)   = [Polarity]
    -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity]
    -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m ()
    compareElims [Polarity]
    cmp [IsForced]
    fs Type
    a Term
    e [Elim]
    u [Elim]
    v
    solveConstraint_ (SortCmp Comparison
    cmp Sort
    s1 Sort
    s2)        = Comparison -> Sort -> Sort -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Sort -> Sort -> m ()
    compareSort Comparison
    cmp Sort
    s1 Sort
    s2
    solveConstraint_ (LevelCmp Comparison
    cmp Level
    a Level
    b)         = Comparison -> Level -> Level -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> Level -> Level -> m ()
    compareLevel Comparison
    cmp Level
    a Level
    b
    solveConstraint_ (IsEmpty Range
    r Type
    t)              = Range -> Type -> TCM ()
    ensureEmptyType Range
    r Type
    t
    solveConstraint_ (CheckSizeLtSat Term
    t)         = Term -> TCM ()
    checkSizeLtSat Term
    t
    solveConstraint_ (UnquoteTactic Term
    tac Term
    hole Type
    goal) = Term -> Term -> Type -> TCM ()
    unquoteTactic Term
    tac Term
    hole Type
    goal
    solveConstraint_ (UnBlock MetaId
    m)                =   -- alwaysUnblock since these have their own unblocking logic (for now)
      TCMT IO Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` (Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas)) (do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.unblock" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [TCMT IO Doc
    "not unblocking", MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m, TCMT IO Doc
    "because",
                                                      TCMT IO Bool -> TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) TCMT IO Doc
    "it's frozen" TCMT IO Doc
    "meta assignments are turned off"]
            Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    alwaysUnblock (Constraint -> TCM ()) -> Constraint -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Constraint
    UnBlock MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        inst <- MetaId -> TCMT IO MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    m
        reportSDoc "tc.constr.unblock" 65 $ "unblocking a metavar yields the constraint:" <+> pretty inst
        case inst of
          BlockedConst Term
    t -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.blocked" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "blocked const " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " :=") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t
            MetaId -> [Arg [Char]] -> Term -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m [] Term
    t
          PostponedTypeCheckingProblem Closure TypeCheckingProblem
    cl -> Closure TypeCheckingProblem
    -> (TypeCheckingProblem -> TCM ()) -> TCM ()
    forall (m :: * -> *) c a b.
    (MonadTCEnv m, ReadTCState m, LensClosure c a) =>
    c -> (a -> m b) -> m b
    enterClosure Closure TypeCheckingProblem
    cl ((TypeCheckingProblem -> TCM ()) -> TCM ())
    -> (TypeCheckingProblem -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TypeCheckingProblem
    prob -> do
              tel <- TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
              v   <- liftTCM $ checkTypeCheckingProblem prob
              assignTerm m (telToArgs tel) v
          -- Andreas, 2009-02-09, the following were IMPOSSIBLE cases
          -- somehow they pop up in the context of sized types
          --
          -- already solved metavariables: should only happen for size
          -- metas (not sure why it does, Andreas?)
          -- Andreas, 2017-07-11:
          -- I think this is because the size solver instantiates
          -- some metas with infinity but does not clean up the UnBlock constraints.
          -- See also issue #2637.
          -- Ulf, 2018-04-30: The size solver shouldn't touch blocked terms! They have
          -- a twin meta that it's safe to solve.
          InstV{} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          OpenMeta{} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    solveConstraint_ (FindInstance Range
    _ MetaId
    m Maybe [Candidate]
    cands) = MetaId -> Maybe [Candidate] -> TCM ()
    findInstance MetaId
    m Maybe [Candidate]
    cands
    solveConstraint_ (ResolveInstanceHead QName
    q) = QName -> TCM ()
    resolveInstanceHead QName
    q
    solveConstraint_ (CheckFunDef DefInfo
    i QName
    q [Clause]
    cs TCErr
    _err) = TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    withoutCache (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
      -- re #3498: checking a fundef would normally be cached, but here it's
      -- happening out of order so it would only corrupt the caching log.
      DefInfo -> QName -> [Clause] -> TCM ()
    checkFunDef DefInfo
    i QName
    q [Clause]
    cs
    solveConstraint_ (CheckLockedVars Term
    a Type
    b Arg Term
    c Type
    d)   = Term -> Type -> Arg Term -> Type -> TCM ()
    checkLockedVars Term
    a Type
    b Arg Term
    c Type
    d
    solveConstraint_ (HasBiggerSort Sort
    a)      = Sort -> TCM ()
    hasBiggerSort Sort
    a
    solveConstraint_ (HasPTSRule Dom Type
    a Abs Sort
    b)       = Dom Type -> Abs Sort -> TCM ()
    hasPTSRule Dom Type
    a Abs Sort
    b
    solveConstraint_ (CheckDataSort QName
    q Sort
    s)    = QName -> Sort -> TCM ()
    checkDataSort QName
    q Sort
    s
    solveConstraint_ (CheckMetaInst MetaId
    m)      = MetaId -> TCM ()
    checkMetaInst MetaId
    m
    solveConstraint_ (CheckType Type
    t)          = Type -> TCM ()
    forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
    checkType Type
    t
    solveConstraint_ (UsableAtModality WhyCheckModality
    cc Maybe Sort
    ms Modality
    mod Term
    t) = Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    MonadConstraint (TCMT IO) =>
    Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
    usableAtModality' Maybe Sort
    ms WhyCheckModality
    cc Modality
    mod Term
    t

    checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
    checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
    checkTypeCheckingProblem = \case
      CheckExpr Comparison
    cmp Expr
    e Type
    t              -> Comparison -> Expr -> Type -> TCM Term
    checkExpr' Comparison
    cmp Expr
    e Type
    t
      CheckArgs Comparison
    cmp ExpandHidden
    eh Expr
    hd [NamedArg Expr]
    args Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    k -> Comparison
    -> ExpandHidden
    -> Expr
    -> [NamedArg Expr]
    -> Type
    -> Type
    -> (ArgsCheckState CheckedTarget -> TCM Term)
    -> TCM Term
    checkArguments Comparison
    cmp ExpandHidden
    eh Expr
    hd [NamedArg Expr]
    args Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    k
      CheckProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    o List1 QName
    ds Expr
    hd [NamedArg Expr]
    args Type
    t Int
    k Term
    v0 Type
    pt PrincipalArgTypeMetas
    patm ->
        Comparison
    -> Expr
    -> ProjOrigin
    -> List1 QName
    -> Expr
    -> [NamedArg Expr]
    -> Type
    -> Int
    -> Term
    -> Type
    -> PrincipalArgTypeMetas
    -> TCM Term
    checkProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    o List1 QName
    ds Expr
    hd [NamedArg Expr]
    args Type
    t Int
    k Term
    v0 Type
    pt PrincipalArgTypeMetas
    patm
      CheckLambda Comparison
    cmp Arg (List1 (WithHiding Name), Maybe Type)
    args Expr
    body Type
    target -> Comparison
    -> Arg (List1 (WithHiding Name), Maybe Type)
    -> Expr
    -> Type
    -> TCM Term
    checkPostponedLambda Comparison
    cmp Arg (List1 (WithHiding Name), Maybe Type)
    args Expr
    body Type
    target
      DoQuoteTerm Comparison
    cmp Term
    et Type
    t           -> Comparison -> Term -> Type -> TCM Term
    doQuoteTerm Comparison
    cmp Term
    et Type
    t
      DisambiguateConstructor ConstructorDisambiguationData
    bcd ConHead -> TCM Term
    k  -> ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
    disambiguateConstructor' ConstructorDisambiguationData
    bcd ConHead -> TCM Term
    k

    debugConstraints :: TCM ()
    debugConstraints :: TCM ()
    debugConstraints = [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.constr" Int
    50 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      awake    <- Lens' TCState Constraints -> TCMT IO Constraints
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Constraints -> f Constraints) -> TCState -> f TCState
    Lens' TCState Constraints
    stAwakeConstraints
      sleeping <- useTC stSleepingConstraints
      reportSDoc "tc.constr" 50 $ vcat
        [ "Current constraints"
        , nest 2 $ vcat [ "awake " <+> vcat (map prettyTCM awake)
                        , "asleep" <+> vcat (map prettyTCM sleeping) ] ]

    -- Update the blocker after some instantiation or pruning might have happened.
    updateBlocker :: (PureTCM m) => Blocker -> m Blocker
    updateBlocker :: forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker = Blocker -> m Blocker
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate

    addAndUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a
    addAndUnblocker :: forall (m :: * -> *) a.
    (PureTCM m, 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 a. (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' -> do
          u <- Blocker -> m Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker Blocker
    u
          patternViolation (unblockOnBoth u u')

    addOrUnblocker :: (PureTCM m, MonadBlock m) => Blocker -> m a -> m a
    addOrUnblocker :: forall (m :: * -> *) a.
    (PureTCM m, 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 a. (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' -> do
          u <- Blocker -> m Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker Blocker
    u
          patternViolation (unblockOnEither u u')

    -- Reduce a term and call the continuation. If the continuation is
    -- blocked, the whole call is blocked either on what blocked the reduction
    -- or on what blocked the continuation (using `blockedOnEither`).
    withReduced
      :: (Reduce a, IsMeta a, PureTCM m, MonadBlock m)
      => a -> (a -> m b) -> m b
    withReduced :: forall a (m :: * -> *) b.
    (Reduce a, IsMeta a, PureTCM m, MonadBlock m) =>
    a -> (a -> m b) -> m b
    withReduced a
    a a -> m b
    cont = a -> (Blocker -> a -> m b) -> (NotBlocked -> a -> m b) -> m b
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked a
    a (\Blocker
    b a
    a' -> Blocker -> m b -> m b
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker Blocker
    b (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ a -> m b
    cont a
    a') (\NotBlocked
    _ a
    a' -> a -> m b
    cont a
    a')