Agda.TypeChecking.Constraints

Documentation

catchConstraint :: Constraint -> TCM () -> TCM ()

Catches pattern violation errors and adds a constraint.

addConstraint :: Constraint -> TCM ()

noConstraints :: TCM a -> TCM a

Don't allow the argument to produce any blocking constraints.

newProblem :: TCM a -> TCM (ProblemId, a)

Create a fresh problem for the given action.

newProblem_ :: TCM () -> TCM ProblemId

ifNoConstraints :: TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b

ifNoConstraints_ :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a

guardConstraint :: Constraint -> TCM () -> TCM ()

guardConstraint c blocker tries to solve blocker first. If successful without constraints, it moves on to solve c, otherwise it adds a Guarded c cs constraint to the blocker-generated constraints cs.

whenConstraints :: TCM () -> TCM () -> TCM ()

wakeConstraints' :: (ProblemConstraint -> TCM Bool) -> TCM ()

Wake constraints matching the given predicate (and aren't instance constraints if isConsideringInstance).

wakeupConstraints :: MetaId -> TCM ()

Wake up the constraints depending on the given meta.

wakeupConstraints_ :: TCM ()

Wake up all constraints.

solveAwakeConstraints :: TCM ()

solveAwakeConstraints' :: Bool -> TCM ()

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

solveConstraint :: Constraint -> TCM ()

solveConstraint_ :: Constraint -> TCM ()

checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term

debugConstraints :: TCM ()