    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Constraints where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Monad.Except

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

    import Agda.Syntax.Common
    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.MetaVars.Mention
    import Agda.TypeChecking.Warnings

    import Agda.TypeChecking.Irrelevance
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
    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 Agda.Utils.Functor
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (prettyShow)

    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
          Set ProblemId
    pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
          [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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
            [ TCMT IO Doc
    "adding constraint"
            , ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (ProblemConstraint -> TCMT IO Doc)
    -> (Closure Constraint -> ProblemConstraint)
    -> Closure Constraint
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr Set ProblemId
    pids Blocker
    unblock (Closure Constraint -> TCMT IO Doc)
    -> TCMT IO (Closure Constraint) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Constraint -> TCMT IO (Closure Constraint)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Constraint
    c ]
          -- Need to reduce to reveal possibly blocking metas
          Constraint
    c <- Constraint -> TCMT IO Constraint
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Constraint -> TCMT IO Constraint)
    -> TCMT IO Constraint -> TCMT IO Constraint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Constraint -> TCMT IO Constraint
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Constraint
    c
          TCMT IO (Maybe [Constraint])
    -> TCM () -> ([Constraint] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Constraint -> TCMT IO (Maybe [Constraint])
    simpl Constraint
    c) {-no-} (Blocker -> Constraint -> TCM ()
    addConstraint' Blocker
    unblock Constraint
    c) (([Constraint] -> TCM ()) -> TCM ())
    -> ([Constraint] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ {-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, Semigroup (m Doc), 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
    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.
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Constraint -> Bool
    isInstanceConstraint Constraint
    c) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
             (ProblemConstraint -> WakeUp) -> TCM ()
    wakeConstraints' ProblemConstraint -> WakeUp
    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.
              [Closure Constraint]
    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
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Closure Constraint] -> Bool
    forall a. Null a => a -> Bool
    null [Closure Constraint]
    lvlcs) (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.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
    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
    $ [Closure Constraint] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Closure Constraint]
    lvlcs
                  ]
              -- Try to simplify @c@ using the other constraints.
              Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
    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 -> [Constraint] -> Maybe [Constraint]
    simplifyLevelConstraint Constraint
    c ([Constraint] -> Maybe [Constraint])
    -> [Constraint] -> Maybe [Constraint]
    forall a b. (a -> b) -> a -> b
    $ (Closure Constraint -> Constraint)
    -> [Closure Constraint] -> [Constraint]
    forall a b. (a -> b) -> [a] -> [b]
    map Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue [Closure Constraint]
    lvlcs
            | Bool
    otherwise = Maybe [Constraint] -> TCMT IO (Maybe [Constraint])
    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
      Constraints
    c <- Lens' Constraints TCState -> TCMT IO Constraints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' Constraints TCState
    stSleepingConstraints
      let (Constraints
    wakeup, Constraints
    sleepin) = [Either ProblemConstraint ProblemConstraint]
    -> (Constraints, Constraints)
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either ProblemConstraint ProblemConstraint]
     -> (Constraints, Constraints))
    -> [Either ProblemConstraint ProblemConstraint]
    -> (Constraints, Constraints)
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> Either ProblemConstraint ProblemConstraint)
    -> Constraints -> [Either ProblemConstraint ProblemConstraint]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> Either ProblemConstraint ProblemConstraint
    checkWakeUp Constraints
    c
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.constr.wake" Int
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "waking up         " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[ProblemId]] -> [Char]
    forall a. Show a => a -> [Char]
    show ((ProblemConstraint -> [ProblemId]) -> Constraints -> [[ProblemId]]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList (Set ProblemId -> [ProblemId])
    -> (ProblemConstraint -> Set ProblemId)
    -> ProblemConstraint
    -> [ProblemId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Set ProblemId
    constraintProblems) Constraints
    wakeup) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
        [Char]
    "  still sleeping: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[ProblemId]] -> [Char]
    forall a. Show a => a -> [Char]
    show ((ProblemConstraint -> [ProblemId]) -> Constraints -> [[ProblemId]]
    forall a b. (a -> b) -> [a] -> [b]
    List.map (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList (Set ProblemId -> [ProblemId])
    -> (ProblemConstraint -> Set ProblemId)
    -> ProblemConstraint
    -> [ProblemId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ProblemConstraint -> Set ProblemId
    constraintProblems) Constraints
    sleepin)
      (Constraints -> Constraints) -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (Constraints -> Constraints) -> m ()
    modifySleepingConstraints ((Constraints -> Constraints) -> TCM ())
    -> (Constraints -> Constraints) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Constraints -> Constraints -> Constraints
    forall a b. a -> b -> a
    const Constraints
    sleepin
      (Constraints -> Constraints) -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (Constraints -> Constraints) -> m ()
    modifyAwakeConstraints (Constraints -> Constraints -> Constraints
    forall a. [a] -> [a] -> [a]
    ++ Constraints
    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 :: Blocker
    constraintUnblocker = Blocker
    u }

    -- | Add all constraints belonging to the given problem to the current problem(s).
    stealConstraintsTCM :: ProblemId -> TCM ()
    stealConstraintsTCM :: ProblemId -> TCM ()
    stealConstraintsTCM ProblemId
    pid = do
      Set ProblemId
    current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.constr.steal" Int
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    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 (Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList Set ProblemId
    current) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is stealing 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]
    "'s constraints!"
      -- Add current to any constraint in pid.
      let rename :: ProblemConstraint -> ProblemConstraint
    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.
      TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ProblemId
    pid (Set ProblemId -> Bool) -> TCMT IO (Set ProblemId) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      (Constraints -> Constraints) -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (Constraints -> Constraints) -> m ()
    modifyAwakeConstraints    ((Constraints -> Constraints) -> TCM ())
    -> (Constraints -> Constraints) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> ProblemConstraint)
    -> Constraints -> Constraints
    forall a b. (a -> b) -> [a] -> [b]
    List.map ProblemConstraint -> ProblemConstraint
    rename
      (Constraints -> Constraints) -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    (Constraints -> Constraints) -> m ()
    modifySleepingConstraints ((Constraints -> Constraints) -> TCM ())
    -> (Constraints -> Constraints) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (ProblemConstraint -> ProblemConstraint)
    -> Constraints -> Constraints
    forall a b. (a -> b) -> [a] -> [b]
    List.map ProblemConstraint -> ProblemConstraint
    rename

    -- | 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 m a
    problem = do
      (ProblemId
    pid, a
    x) <- m a -> m (ProblemId, a)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem m a
    problem
      Constraints
    cs <- ProblemId -> m Constraints
    forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
    getConstraintsForProblem ProblemId
    pid
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Constraints -> Bool
    forall a. Null a => a -> Bool
    null Constraints
    cs) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        (CallStack -> m ()) -> m ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCurrentCallStack ((CallStack -> m ()) -> m ()) -> (CallStack -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \CallStack
    loc -> do
          TCWarning
    w <- CallStack -> Warning -> m TCWarning
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m TCWarning
    warning'_ CallStack
    loc (Constraints -> Warning
    UnsolvedConstraints Constraints
    cs)
          CallStack -> TypeError -> m ()
    forall (m :: * -> *) a.
    MonadTCError m =>
    CallStack -> TypeError -> m a
    typeError' CallStack
    loc (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> TypeError
    NonFatalErrors [ TCWarning
    w ]
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    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

    -- | 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
      ProblemId
    pid <- m ProblemId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      -- Don't get distracted by other constraints while working on the problem
      a
    x <- m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    nowSolvingConstraints (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ ProblemId -> m a -> m a
    forall (m :: * -> *) a.
    MonadConstraint m =>
    ProblemId -> m a -> m a
    solvingProblem ProblemId
    pid m a
    action
      -- Now we can check any woken constraints
      m ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints
      (ProblemId, a) -> m (ProblemId, a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProblemId
    pid, a
    x)

    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
      (ProblemId
    pid, a
    x) <- TCM a -> TCMT IO (ProblemId, a)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem TCM a
    check
      TCMT IO Bool -> TCM b -> TCM b -> TCM b
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ProblemId -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemSolved ProblemId
    pid) (a -> TCM b
    ifNo a
    x) (ProblemId -> a -> TCM b
    ifCs ProblemId
    pid a
    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 (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

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

    -- | Wake up the constraints depending on the given meta.
    wakeupConstraints :: MetaId -> TCM ()
    wakeupConstraints :: MetaId -> TCM ()
    wakeupConstraints MetaId
    x = do
      (ProblemConstraint -> WakeUp) -> TCM ()
    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)
      TCM ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints

    -- | Wake up all constraints not blocked on a problem.
    wakeupConstraints_ :: TCM ()
    wakeupConstraints_ :: TCM ()
    wakeupConstraints_ = do
      (ProblemConstraint -> WakeUp) -> TCM ()
    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

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

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

    -- | 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
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "profile.constraints" Int
    10 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    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' (Set ProblemId) TCEnv
    -> (Set ProblemId -> Set ProblemId) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' (Set ProblemId) TCEnv
    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 (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
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "profile.constraints" Int
    10 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    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 (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
          Set ProblemId
    pids <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.solve.constr" Int
    20 (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 ([ProblemId] -> [Char]
    forall a. Show a => a -> [Char]
    show ([ProblemId] -> [Char]) -> [ProblemId] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Set ProblemId -> [ProblemId]
    forall a. Set a -> [a]
    Set.toList Set ProblemId
    pids) 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
    prettyTCM Constraint
    c
          Constraint -> TCM ()
    solveConstraint_ Constraint
    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 :: * -> *).
    (MonadFail 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
    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 :: * -> *).
    (MonadFail 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
        MetaInstantiation
    inst <- MetaVariable -> MetaInstantiation
    mvInstantiation (MetaVariable -> MetaInstantiation)
    -> TCMT IO MetaVariable -> TCMT IO MetaInstantiation
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    m
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr.unblock" Int
    65 (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]
    "unblocking a metavar yields the constraint: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaInstantiation -> [Char]
    forall a. Show a => a -> [Char]
    show MetaInstantiation
    inst)
        case MetaInstantiation
    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
    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 :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    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
              Telescope
    tel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
              Term
    v   <- TCM Term -> TCM Term
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ TypeCheckingProblem -> TCM Term
    checkTypeCheckingProblem TypeCheckingProblem
    prob
              MetaId -> [Arg [Char]] -> Term -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m (Telescope -> [Arg [Char]]
    forall a. TelToArgs a => a -> [Arg [Char]]
    telToArgs Telescope
    tel) Term
    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__
          -- Open (whatever that means)
          MetaInstantiation
    Open -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          MetaInstantiation
    OpenInstance -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    solveConstraint_ (FindInstance MetaId
    m Maybe [Candidate]
    cands) = MetaId -> Maybe [Candidate] -> TCM ()
    findInstance MetaId
    m Maybe [Candidate]
    cands
    solveConstraint_ (CheckFunDef Delayed
    d 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.
      Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
    checkFunDef Delayed
    d 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_ (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 Modality
    mod Term
    t) = Modality -> Term -> TCM ()
    MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
    usableAtModality 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 Range
    r [NamedArg Expr]
    args Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    k -> Comparison
    -> ExpandHidden
    -> Range
    -> [NamedArg Expr]
    -> Type
    -> Type
    -> (ArgsCheckState CheckedTarget -> TCM Term)
    -> TCM Term
    checkArguments Comparison
    cmp ExpandHidden
    eh Range
    r [NamedArg Expr]
    args Type
    t0 Type
    t1 ArgsCheckState CheckedTarget -> TCM Term
    k
      CheckProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    o List1 QName
    ds [NamedArg Expr]
    args Type
    t Int
    k Term
    v0 Type
    pt PrincipalArgTypeMetas
    patm ->
        Comparison
    -> Expr
    -> ProjOrigin
    -> List1 QName
    -> [NamedArg Expr]
    -> Type
    -> Int
    -> Term
    -> Type
    -> PrincipalArgTypeMetas
    -> TCM Term
    checkProjAppToKnownPrincipalArg Comparison
    cmp Expr
    e ProjOrigin
    o List1 QName
    ds [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

    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
      Constraints
    awake    <- Lens' Constraints TCState -> TCMT IO Constraints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' Constraints TCState
    stAwakeConstraints
      Constraints
    sleeping <- Lens' Constraints TCState -> TCMT IO Constraints
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' Constraints TCState
    stSleepingConstraints
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.constr" Int
    50 (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
    "Current constraints"
        , 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ TCMT IO Doc
    "awake " 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
    vcat ((ProblemConstraint -> TCMT IO Doc) -> Constraints -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Constraints
    awake)
                        , TCMT IO Doc
    "asleep" 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
    vcat ((ProblemConstraint -> TCMT IO Doc) -> Constraints -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemConstraint -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Constraints
    sleeping) ] ]