{-# 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.Data ( checkDataSort )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Empty
import {-# SOURCE #-} Agda.TypeChecking.Lock
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType )

import Agda.Utils.CallStack ( withCurrentCallStack )
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.ProfileOptions as Profile

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    = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraints -> Constraints) -> TCState -> TCState
mapAwakeConstraints
  modifySleepingConstraints :: (Constraints -> Constraints) -> TCM ()
modifySleepingConstraints = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC 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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ TCMT IO Doc
"adding constraint"
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
pids Blocker
unblock forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c
        , TCMT IO Doc
"unblocker: " , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
unblock
        ]
      -- Jesper, 2022-10-22: We should never block on a meta that is
      -- already solved. However, currently this is not always
      -- strictly adhered to. TODO: pull off the band-aid and
      -- uncomment the following line.
      -- whenM (anyM (Set.toList $ allBlockingMetas unblock) isInstantiatedMeta) __IMPOSSIBLE__
      -- Need to reduce to reveal possibly blocking metas
      Constraint
c <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Constraint
c
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Constraint -> TCM (Maybe [Constraint])
simpl Constraint
c) {-no-} (Blocker -> Constraint -> TCM ()
addConstraint' Blocker
unblock Constraint
c) forall a b. (a -> b) -> a -> b
$ {-yes-} \ [Constraint]
cs -> do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.add" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  simplified:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Constraint]
cs)
          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.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constraint -> Bool
isInstanceConstraint Constraint
c) forall a b. (a -> b) -> a -> b
$
         forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' ProblemConstraint -> WakeUp
isWakeableInstanceConstraint
    where
      isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
      isWakeableInstanceConstraint :: ProblemConstraint -> WakeUp
isWakeableInstanceConstraint ProblemConstraint
c =
        case forall a. Closure a -> a
clValue forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c of
          FindInstance{}
            | ProblemConstraint -> Blocker
constraintUnblocker ProblemConstraint
c forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock -> WakeUp
WakeUp
          Constraint
_ -> Maybe Blocker -> WakeUp
DontWakeUp 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 -> TCM (Maybe [Constraint])
simpl Constraint
c
        | Constraint -> Bool
isLvl Constraint
c = do
          -- Get all level constraints.
          [Closure Constraint]
lvlcs <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
            forall a. (a -> Bool) -> [a] -> [a]
List.filter (Constraint -> Bool
isLvl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Closure a -> a
clValue) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Closure Constraint]
lvlcs) forall a b. (a -> b) -> a -> b
$ do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.lvl" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"simplifying level constraint" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"using" Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Closure Constraint]
lvlcs
              ]
          -- Try to simplify @c@ using the other constraints.
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Constraint -> [Constraint] -> Maybe [Constraint]
simplifyLevelConstraint Constraint
c forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Closure a -> a
clValue [Closure Constraint]
lvlcs
        | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

wakeConstraintsTCM :: (ProblemConstraint-> WakeUp) -> TCM ()
wakeConstraintsTCM :: (ProblemConstraint -> WakeUp) -> TCM ()
wakeConstraintsTCM ProblemConstraint -> WakeUp
wake = do
  Constraints
c <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Constraints TCState
stSleepingConstraints
  let (Constraints
wakeup, Constraints
sleepin) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Either ProblemConstraint ProblemConstraint
checkWakeUp Constraints
c
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.constr.wake" Int
50 forall a b. (a -> b) -> a -> b
$
    [Char]
"waking up         " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a b. (a -> b) -> [a] -> [b]
List.map (forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) Constraints
wakeup) forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++
    [Char]
"  still sleeping: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a b. (a -> b) -> [a] -> [b]
List.map (forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Set ProblemId
constraintProblems) Constraints
sleepin)
  forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifySleepingConstraints forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Constraints
sleepin
  forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (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              -> forall a b. a -> Either a b
Left ProblemConstraint
c
      DontWakeUp Maybe Blocker
Nothing  -> forall a b. b -> Either a b
Right ProblemConstraint
c
      DontWakeUp (Just Blocker
u) -> 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 <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.constr.steal" Int
50 forall a b. (a -> b) -> a -> b
$ [Char]
"problem " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Set a -> [a]
Set.toList Set ProblemId
current) forall a. [a] -> [a] -> [a]
++ [Char]
" is stealing problem " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ProblemId
pid forall a. [a] -> [a] -> [a]
++ [Char]
"'s constraints!"
  -- Add current to any constraint in pid.
  let rename :: ProblemConstraint -> ProblemConstraint
rename pc :: ProblemConstraint
pc@(PConstr Set ProblemId
pids Blocker
u Closure Constraint
c) | forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid Set ProblemId
pids = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr (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.
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
pid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems) forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints    forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
List.map ProblemConstraint -> ProblemConstraint
rename
  forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifySleepingConstraints forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
List.map ProblemConstraint -> ProblemConstraint
rename


-- | Don't allow the argument to produce any blocking constraints.
--
-- WARNING: this does not mean that the given computation cannot
-- constrain the solution space further.
-- It can well do so, by solving metas.
noConstraints
  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
  => m a -> m a
noConstraints :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints m a
problem = do
  (ProblemId
pid, a
x) <- forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem m a
problem
  Constraints
cs <- forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Constraints
cs) forall a b. (a -> b) -> a -> b
$ do
    forall b. HasCallStack => (CallStack -> b) -> b
withCurrentCallStack forall a b. (a -> b) -> a -> b
$ \CallStack
loc -> do
      TCWarning
w <- forall (m :: * -> *).
MonadWarning m =>
CallStack -> Warning -> m TCWarning
warning'_ CallStack
loc (Constraints -> Warning
UnsolvedConstraints Constraints
cs)
      forall (m :: * -> *) a.
MonadTCError m =>
CallStack -> TypeError -> m a
typeError' CallStack
loc forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [ TCWarning
w ]
  forall (m :: * -> *) a. Monad m => a -> m a
return a
x

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

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

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

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

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ :: forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
check TCM a
ifNo ProblemId -> TCM a
ifCs = forall a b.
TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
ifNoConstraints TCM ()
check (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 =
  forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
blocker (forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint Constraint
c) (\ ProblemId
pid -> 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 =
  forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ TCM ()
action (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \ProblemId
pid -> do
    forall (m :: * -> *). MonadConstraint m => ProblemId -> m ()
stealConstraints ProblemId
pid
    TCM ()
handler

-- | 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
  forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' (MetaId -> Blocker -> WakeUp
wakeIfBlockedOnMeta MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker)
  forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

-- | Wake up all constraints not blocked on a problem.
wakeupConstraints_ :: TCM ()
wakeupConstraints_ :: TCM ()
wakeupConstraints_ = do
  forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> WakeUp) -> m ()
wakeConstraints' (Blocker -> WakeUp
wakeup forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker)
  forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
  where
    wakeup :: Blocker -> WakeUp
wakeup Blocker
u | forall a. Set a -> Bool
Set.null forall a b. (a -> b) -> a -> b
$ Blocker -> Set ProblemId
allBlockingProblems Blocker
u = WakeUp
WakeUp
             | Bool
otherwise                        = Maybe Blocker -> WakeUp
DontWakeUp 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
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Constraints forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadStatistics m =>
[Char] -> Integer -> m ()
tickMax [Char]
"max-open-constraints" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i a. Num i => [a] -> i
List.genericLength forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool
force Bool -> Bool -> Bool
||) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Bool
isSolvingConstraints) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints 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.
     forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Set ProblemId) TCEnv
eActiveProblems (forall a b. a -> b -> a
const forall a. Set a
Set.empty) TCM ()
solve
  where
    solve :: TCM ()
solve = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.solve" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"Solving awake constraints."
                                             , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m Constraints
getAwakeConstraints
                                             , TCMT IO Doc
"remaining." ]
      forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
takeAwakeConstraint' ProblemConstraint -> Bool
solveThis) forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
c -> do
        forall (m :: * -> *) a.
MonadConstraint m =>
(Constraint -> m a) -> ProblemConstraint -> m a
withConstraint forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint ProblemConstraint
c
        TCM ()
solve

solveConstraintTCM :: Constraint -> TCM ()
solveConstraintTCM :: Constraint -> TCM ()
solveConstraintTCM Constraint
c = do
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Constraints forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"attempted-constraints"
    forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.constr.solve" Int
20 [Char]
"solving constraint" forall a b. (a -> b) -> a -> b
$ do
      Set ProblemId
pids <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.solve.constr" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set ProblemId
pids) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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)       = 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) = 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)   = 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)        = forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s1 Sort
s2
solveConstraint_ (LevelCmp Comparison
cmp Level
a Level
b)         = 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)
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)) (do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.unblock" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [TCMT IO Doc
"not unblocking", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m, TCMT IO Doc
"because",
                                                  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (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"]
        forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
alwaysUnblock forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
UnBlock MetaId
m) forall a b. (a -> b) -> a -> b
$ do
    MetaInstantiation
inst <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.unblock" Int
65 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unblocking a metavar yields the constraint:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaInstantiation
inst
    case MetaInstantiation
inst of
      BlockedConst Term
t -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.constr.blocked" Int
15 forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"blocked const " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m forall a. [a] -> [a] -> [a]
++ [Char]
" :=") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
        forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m [] Term
t
      PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl forall a b. (a -> b) -> a -> b
$ \TypeCheckingProblem
prob -> do
          Telescope
tel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          Term
v   <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ TypeCheckingProblem -> TCMT IO Term
checkTypeCheckingProblem TypeCheckingProblem
prob
          forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m (forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Telescope
tel) Term
v
      -- Andreas, 2009-02-09, the following were IMPOSSIBLE cases
      -- somehow they pop up in the context of sized types
      --
      -- already solved metavariables: should only happen for size
      -- metas (not sure why it does, Andreas?)
      -- Andreas, 2017-07-11:
      -- I think this is because the size solver instantiates
      -- some metas with infinity but does not clean up the UnBlock constraints.
      -- See also issue #2637.
      -- Ulf, 2018-04-30: The size solver shouldn't touch blocked terms! They have
      -- a twin meta that it's safe to solve.
      InstV{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Open (whatever that means)
      MetaInstantiation
Open -> forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaInstantiation
OpenInstance -> 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) = forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache 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_ (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)          = forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
t
solveConstraint_ (UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
t) = MonadConstraint (TCMT IO) =>
Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
usableAtModality' Maybe Sort
ms WhyCheckModality
cc Modality
mod Term
t

checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
checkTypeCheckingProblem :: TypeCheckingProblem -> TCMT IO Term
checkTypeCheckingProblem = \case
  CheckExpr Comparison
cmp Expr
e Type
t              -> Comparison -> Expr -> Type -> TCMT IO Term
checkExpr' Comparison
cmp Expr
e Type
t
  CheckArgs Comparison
cmp ExpandHidden
eh Range
r [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCMT IO Term
k -> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCMT IO Term)
-> TCMT IO Term
checkArguments Comparison
cmp ExpandHidden
eh Range
r [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCMT IO Term
k
  CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm ->
    Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> Int
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCMT IO Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm
  CheckLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe Type)
args Expr
body Type
target -> Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TCMT IO 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 -> TCMT IO Term
doQuoteTerm Comparison
cmp Term
et Type
t

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