{-# 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
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.add" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ TCM Doc
"adding constraint"
        , ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ProblemConstraint -> TCM Doc)
-> (Closure Constraint -> ProblemConstraint)
-> Closure Constraint
-> TCM 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 -> TCM Doc)
-> TCMT IO (Closure Constraint) -> TCM 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
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.add" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"  simplified:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Constraint -> TCM Doc) -> [Constraint] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> TCM 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
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.lvl" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCM Doc
"simplifying level constraint" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> VerboseLevel -> m Doc -> m Doc
hang TCM Doc
"using" VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Closure Constraint] -> TCM 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
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.constr.wake" VerboseLevel
50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
    VerboseKey
"waking up         " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[ProblemId]] -> VerboseKey
forall a. Show a => a -> VerboseKey
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) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
    VerboseKey
"  still sleeping: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[ProblemId]] -> VerboseKey
forall a. Show a => a -> VerboseKey
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
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.constr.steal" VerboseLevel
50 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
current) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" is stealing problem " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ProblemId -> VerboseKey
forall a. Show a => a -> VerboseKey
show ProblemId
pid VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"'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 :: 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 :: 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 :: 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_ :: 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 :: 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_ :: 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 :: m ()
solveAwakeConstraints = Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
False

solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
solveAwakeConstraints' :: 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
    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"profile.constraints" VerboseLevel
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
$ VerboseKey -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
VerboseKey -> Integer -> m ()
tickMax VerboseKey
"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
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.solve" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCM Doc
"Solving awake constraints."
                                             , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Constraints -> VerboseKey) -> Constraints -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> VerboseKey)
-> (Constraints -> VerboseLevel) -> Constraints -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Constraints -> TCM Doc) -> TCMT IO Constraints -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints
                                             , TCM 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
    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"profile.constraints" VerboseLevel
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
$ VerboseKey -> TCM ()
forall (m :: * -> *). MonadStatistics m => VerboseKey -> m ()
tick VerboseKey
"attempted-constraints"
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.constr.solve" VerboseLevel
20 VerboseKey
"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
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.solve.constr" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text ([ProblemId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([ProblemId] -> VerboseKey) -> [ProblemId] -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Constraint -> TCM 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
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.unblock" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCM Doc
"not unblocking", MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m, TCM Doc
"because",
                                                  TCMT IO Bool -> TCM Doc -> TCM Doc -> TCM 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) TCM Doc
"it's frozen" TCM 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
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.unblock" VerboseLevel
65 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"unblocking a metavar yields the constraint: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaInstantiation -> VerboseKey
forall a. Show a => a -> VerboseKey
show MetaInstantiation
inst)
    case MetaInstantiation
inst of
      BlockedConst Term
t -> do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr.blocked" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"blocked const " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ MetaId -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow MetaId
m VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" :=") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
        MetaId -> [Arg VerboseKey] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> 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 VerboseKey] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m (Telescope -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
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 TCM => 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 VerboseLevel
k Term
v0 Type
pt PrincipalArgTypeMetas
patm ->
    Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> VerboseLevel
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Type
t VerboseLevel
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 = VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.constr" VerboseLevel
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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.constr" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"Current constraints"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"awake " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((ProblemConstraint -> TCM Doc) -> Constraints -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraints
awake)
                    , TCM Doc
"asleep" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((ProblemConstraint -> TCM Doc) -> Constraints -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraints
sleeping) ] ]