Closed
Description
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<...>)
- come from the header of
Trait
- come from each impl
- come from the header of
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.