One of the key parts of the interface between the Chalk Solver and rustc is when the solver requests the program clauses to solve a given goal:
/// Returns the set of program clauses that might apply to
/// `goal`. (This set can be over-approximated, naturally.)
fn program_clauses(
&self,
environment: &I::Environment,
goal: &I::DomainGoal,
) -> Vec<I::ProgramClause>;
In Rustc, this is our chance to do some queries and figure out the full set of clauses. This is building on the work in #49177, where we create the lowering rules for a trait, item, etc (see also the rustc guide coverage).
The set of clauses is somewhat specific to the domain goal:
Implemented(P0: Trait<...>)
FromEnv(P0: Trait<..>)
- these come -- ultimately -- from the param environment
- but because of implied bounds rules we need to combine with the rules from traits
- we need to compute transitive closure of traits reachable from the env and combine their program clauses, or else iterate over "all traits" (which is actually not easy)
- I have some code working towards this on my WIP branch for this issue
- ... the rest have to be written out :)
I'll probably keep iterating on this, but if somebody is keen to hack on it, I'd love to collaborate.
One of the key parts of the interface between the Chalk Solver and rustc is when the solver requests the program clauses to solve a given goal:
In Rustc, this is our chance to do some queries and figure out the full set of clauses. This is building on the work in #49177, where we create the lowering rules for a trait, item, etc (see also the rustc guide coverage).
The set of clauses is somewhat specific to the domain goal:
Implemented(P0: Trait<...>)TraitFromEnv(P0: Trait<..>)I'll probably keep iterating on this, but if somebody is keen to hack on it, I'd love to collaborate.