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 InferCtxtEvalExt::evaluate_root_goal
. This function sets up the root EvalCtxt
and then calls EvalCtxt::evaluate_goal
, 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 separate local 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 Vec<T>: Clone
, EvalCtxt::compute_trait_goal
has 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 EvalCtxt::merge_candidates
.
EvalCtxt::add_goal
To prove nested goals, we don't directly call EvalCtxt::compute_goal
, but instead add the goal to the EvalCtxt
with EvalCtxt::all_goal
. We then prove all nested goals together in either EvalCtxt::try_evaluate_added_goals
or 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, then proving ?x: Debug
is initially ambiguous, but after proving (): ConstrainToU8<?x>
we constrain ?x
to u8
and proving u8: Debug
succeeds.
TyKind
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 be incorrect.
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 ())
, EvalCtxt::compute_goal
eagerly instantiates '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 EvalCtxt::try_merge_responses
fails.
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.