Also consider reading the documentation for the recursive solver in chalk as it is very similar to this implementation and also talks about limitations of this approach.
The entry-point of the solver is
function sets up the root
EvalCtxt and then calls
to actually enter the trait solver.
EvalCtxt::evaluate_goal handles canonicalization, caching,
overflow, and solver cycles. Once that is done, it creates a nested
EvalCtxt with a
InferCtxt and calls
EvalCtxt::compute_goal, which is responsible for the
'actual solver behavior'. We match on the
PredicateKind, delegating to a separate function
for each one.
For trait goals, such a
to collect all the possible ways this goal can be proven via
EvalCtxt::assemble_and_evaluate_candidates. Each candidate is handled in
a separate "probe", to not leak inference constraints to the other candidates.
We then try to merge the assembled candidates via
To prove nested goals, we don't directly call
EvalCtxt::compute_goal, but instead
add the goal to the
EvalCtxt::all_goal. We then prove all nested
goals together in either
EvalCtxt::evaluate_added_goals_and_make_canonical_response. This allows us to handle
inference constraints from later goals.
E.g. if we have both
?x: Debug and
(): ConstrainToU8<?x> as nested goals,
?x: Debug is initially ambiguous, but after proving
u8 and proving
u8: Debug succeeds.
We lazily normalize types in the solver, so we always have to assume that any types
and constants are potentially unnormalized. This means that matching on
TyKind can easily
We handle normalization in two different ways. When proving
Trait goals when normalizing
associated types, we separately assemble candidates depending on whether they structurally
match the self type. Candidates which match on the self type are handled in
EvalCtxt::assemble_candidates_via_self_ty which recurses via
EvalCtxt::assemble_candidates_after_normalizing_self_ty, which normalizes the self type
by one level. In all other cases we have to match on a
TyKind we first use
EvalCtxt::try_normalize_ty to normalize the type as much as possible.
In case the goal is higher-ranked, e.g.
for<'a> F: FnOnce(&'a ()),
'a with a placeholder and then recursively proves
F: FnOnce(&'!a ()) as a nested goal.
Some goals can be proven in multiple ways. In these cases we try each option in
a separate "probe" and then attempt to merge the resulting responses by using
EvalCtxt::try_merge_responses. If merging the responses fails, we use
EvalCtxt::flounder instead, returning ambiguity. For some goals, we try
incompletely prefer some choices over others in case
The solver should be fairly self-contained. I hope that the above information provides a good foundation when looking at the code itself. Please reach out on zulip if you get stuck while doing so or there are some quirks and design decisions which were unclear and deserve better comments or should be mentioned here.