RustcContributor::explore @lcnr session: walkthrough of -Ztrait-solver=next

RustContributor walks through the workings of -Ztrait-solver=next, showcasing how it handles ambiguity, cycles, and complex type proofs.

Key takeaways
  • The solver works by walking over the type of a goal, replacing placeholders with inference variables, and then checking whether each goal is proven by a candidate.
  • When a goal is proven, the solver checks whether the proof is ambiguous, and if it is, it returns ambiguity with no constraints.
  • The solver uses caching to speed up the process of proving goals.
  • The solver can detect and handle cycles, which occur when a goal is dependent on another goal that is still being proven.
  • The solver uses the concept of canonicalization to standardize the type of a goal, which makes it easier to prove.
  • The solver can also use the concept of conduction to simplify the process of proving goals.
  • The solver has a step called “evaluate canonical goal” which is responsible for evaluating the type of a goal and determining whether it is proven or not.
  • The solver uses the concept of “existential” to prove goals that have conditions that depend on the existence of a type.
  • The solver can also use the concept of “co-inductive” to prove goals that have conditions that depend on the existence of a type and also have existential bounds.
  • The solver has a step called “assemble candidates” which is responsible for creating a list of candidates that can be used to prove a goal.
  • The solver has a step called “merge trade candidates” which is responsible for merging candidates with the same constraints.
  • The solver has a step called “compute goal” which is responsible for proving a goal by using a candidate.
  • The solver has a step called “evaluate projection goal” which is responsible for evaluating a goal that involves a projection.
  • The solver has a step called “evaluate trait goal” which is responsible for evaluating a goal that involves a trait.
  • The solver has a step called “assemble input candidates” which is responsible for creating a list of input candidates that can be used to prove a goal.
  • The solver has a step called “merge input candidates” which is responsible for merging input candidates with the same constraints.
  • The solver has a step called “compute input goal” which is responsible for proving an input goal by using an input candidate.