{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Constraints where

import Prelude hiding (null)

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

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 {-# SOURCE #-} Agda.TypeChecking.Rewriting

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

import Agda.Utils.Impossible
import Agda.Utils.Function (applyUnless)

instance MonadConstraint TCM where
  addConstraint :: Blocker -> Constraint -> TCM ()
addConstraint Blocker
u Constraint
c = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Blocker -> Constraint -> TCM ()
addConstraintTCM Blocker
u Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u
  addAwakeConstraint :: Blocker -> Constraint -> TCM ()
addAwakeConstraint Blocker
u Constraint
c  = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Blocker -> Constraint -> TCM ()
addAwakeConstraint' Blocker
u Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
u

  solveConstraint :: Constraint -> TCM ()
solveConstraint Constraint
c = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (Constraint -> TCM ()
solveConstraintTCM Constraint
c) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock -- TODO: does this happen?

  solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraints ProblemConstraint -> Bool
s Bool
f = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ((ProblemConstraint -> Bool) -> Bool -> TCM ()
solveSomeAwakeConstraintsTCM ProblemConstraint -> Bool
s Bool
f) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE wakeConstraints #-}
  wakeConstraints :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraints ProblemConstraint -> WakeUp
w             = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ((ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
w)  (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE stealConstraints #-}
  stealConstraints :: ProblemId -> TCM ()
stealConstraints ProblemId
w            = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (ProblemId -> TCM ()
stealConstraintsTCM ProblemId
w) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  {-# INLINE modifyConstraints #-}
  modifyConstraints :: (Constraints -> Constraints)
-> (Constraints -> Constraints) -> TCM ()
modifyConstraints Constraints -> Constraints
f Constraints -> Constraints
g = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv
    ((TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints Constraints -> Constraints
f (TCState -> TCState) -> (TCState -> TCState) -> TCState -> TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints Constraints -> Constraints
g))
    (Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock) -- TODO: does this happen?


addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM :: Blocker -> Constraint -> TCM ()
addConstraintTCM Blocker
unblock Constraint
c = do
  pids <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  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

{-# INLINE wakeConstraintsTCM #-}
wakeConstraintsTCM :: (ProblemConstraint-> WakeUp) -> TCM ()
wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
wake = do
  tc <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  let c = TCState
tc TCState -> Getting Constraints TCState Constraints -> Constraints
forall s a. s -> Getting a s a -> a
^. Getting Constraints TCState Constraints
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)
  putTC $!
    mapAwakeConstraints (++! wakeup) $ -- TODO: quadratic append!!
      mapSleepingConstraints (const sleepin) tc
  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 <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
  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 <$> viewTC eActiveProblems) __IMPOSSIBLE__
  modifyTC $   mapAwakeConstraints    (map' rename)
             . mapSleepingConstraints (map' rename)

{-# SPECIALIZE noConstraints :: TCM a -> TCM a #-}
-- | Error out with @'NonFatalErrors' 'UnsolvedConstraints'@
-- if the computation produced 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, MonadFresh ProblemId m)
  => m a -> m a
noConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadFresh ProblemId m) =>
m a -> m a
noConstraints = Bool -> m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning 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, MonadFresh ProblemId m)
  => m a -> m a
reallyNoConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadFresh ProblemId m) =>
m a -> m a
reallyNoConstraints = Bool -> m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadFresh ProblemId m) =>
Bool -> m a -> m a
noConstraints' Bool
True

-- | Error out with @'NonFatalErrors' 'UnsolvedConstraints'@
--   when given computation produced constraints ('True') or blocking constraints ('False').
noConstraints' ::
     (MonadConstraint m, MonadWarning m, MonadFresh ProblemId m)
  => Bool -> m a -> m a
noConstraints' :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning 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
  -- Consider only blocking constraints unless @includingNonBlocking@.
  let isBlocking = 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 <- applyUnless includingNonBlocking (List.filter isBlocking) <$> getConstraintsForProblem pid
  List1.unlessNull cs \ 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 ::
  ( MonadConstraint m
  , MonadFresh ProblemId m
  , MonadWarning m
  ) => m a -> m a
nonConstraining :: forall (m :: * -> *) a.
(MonadConstraint m, MonadFresh ProblemId m, MonadWarning m) =>
m a -> m a
nonConstraining = m a -> m a
forall (m :: * -> *) a. (MonadTCEnv 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, MonadFresh ProblemId m) =>
m a -> m a
noConstraints

{-# INLINE newProblem #-}
-- | 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)

{-# INLINE newProblem_ #-}
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

{-# INLINE newProblemDontWake_ #-}
-- | Create a fresh problem for the given action. Don't wake problems after the action finishes.
newProblemDontWake_
  :: (MonadFresh ProblemId m, MonadConstraint m)
  => m a -> m ProblemId
newProblemDontWake_ :: forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblemDontWake_ 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
  _ <- nowSolvingConstraints $
         verboseBracket "tc.constr.solve" 50 ("working on problem " ++ show pid) $
           localTC (over eActiveProblems (Set.insert pid)) action
  pure pid

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] -> Word64 -> TCM ()
forall (m :: * -> *). MonadStatistics m => [Char] -> Word64 -> m ()
tickMax [Char]
"max-open-constraints" (Word64 -> TCM ())
-> (Constraints -> Word64) -> Constraints -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> Word64
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 -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.constr.solve" Int
10 do
        TCMT IO Constraints -> (Constraints -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
m a -> (a -> m ()) -> m ()
unlessNullM TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints \ Constraints
cs ->
          [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) -> (Int -> [Char]) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> TCMT IO Doc) -> Int -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Constraints -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Constraints
cs, 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
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 <- Lens' TCEnv (Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Set ProblemId -> f (Set ProblemId)) -> TCEnv -> f TCEnv
Lens' TCEnv (Set ProblemId)
eActiveProblems
      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 ()
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 ()
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 ()
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 ()
compareSort Comparison
cmp Sort
s1 Sort
s2
solveConstraint_ (LevelCmp Comparison
cmp Level
a Level
b)         = Comparison -> Level -> Level -> TCM ()
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
<$> Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas)) (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 ()
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 KwRange
kwr QName
q) = KwRange -> QName -> TCM ()
resolveInstanceHead KwRange
kwr 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 ()
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
solveConstraint_ (RewConstraint LocalEquation
eq)     = LocalEquation -> TCM ()
checkRewConstraint LocalEquation
eq

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 AmbiguousQName
ds Expr
hd [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm ->
    Comparison
-> Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> Type
-> Int
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
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')