# Lesson XIII
The brush meets the ink. Holding opens the way; unknown remains open; running closes the stroke.
## Try
```prolog
?- E = kernel, infer(E, [dup, add], Scheme).
Scheme = scheme([requires(numeric, A)], effect([A|S], [A|S])).
?- E = kernel, infer(E, [push(int(1)), dup, add], Scheme).
Scheme = scheme([], effect(S, [int|S])).
?- E = kernel, infer(E, [push(bool(true)), dup, add], Scheme).
ERROR: forth_error(constraint, unsatisfied, requires(numeric, bool)).
```
## Lesson
We could collect constraints, but runtime used `holds/1` as a local yes/no check and public inference returned constraints without normalization. Remove that split by making `solve/2` the single constraint boundary.
Supported concrete obligations disappear, open obligations are preserved, and unsatisfied obligations throw in one place. `apply` and `infer` are modified to share that policy.
> [!info]- Change
> ```diff
> - apply(Env, Word, Stack0, Stack) :-
> - find(Env, Word, InPattern -- OutPattern, Constraints, Goal),
> - bind(InPattern, Stack0),
> - holds(Constraints),
> - call(Goal),
> - build(OutPattern, Stack).
> -
> - infer(Env, Words, scheme(Constraints, effect(In, Out))) :-
> - infer(Env, Words, effect(In, Out), Constraints, []).
> -
> - holds([]).
> - holds([requires(Name, Type)|Constraints]) :-
> - nonvar(Type),
> - supports(Type, Name),
> - holds(Constraints).
> ```
```prolog
apply(Env, Word, Stack0, Stack) :-
find(Env, Word, InPattern -- OutPattern, Constraints, Goal),
bind(InPattern, Stack0),
solve(Constraints, []),
call(Goal),
build(OutPattern, Stack).
infer(Env, Words, scheme(Constraints, effect(In, Out))) :-
infer(Env, Words, effect(In, Out), RawConstraints, []),
solve(RawConstraints, Constraints).
```
`solve/2` performs one local reduction at a time.
* `requires(numeric, A)` stays open when `A` is a variable.
* `requires(numeric, int)` disappears because `int` is numeric.
* `requires(numeric, bool)` throws because `bool` has no numeric support.
```prolog
solve([], []).
solve([Constraint|Constraints0], Constraints) :-
reduce1(Constraint, More),
solve(Constraints0, Rest),
append(More, Rest, Constraints).
reduce1(requires(Name, Type), [requires(Name, Type)]) :-
var(Type),
supports(_, Name),
!.
reduce1(requires(Name, Type), []) :-
supports(Type, Name),
!.
reduce1(Constraint, _) :-
throw(error(forth_error(constraint, unsatisfied, Constraint), _)).
```
[[12_lesson|Prev]] | [[14_lesson|Next]]