-
-
Notifications
You must be signed in to change notification settings - Fork 14.4k
Closed
Labels
A-trait-systemArea: Trait systemArea: Trait systemC-enhancementCategory: An issue proposing an enhancement or a PR with one.Category: An issue proposing an enhancement or a PR with one.T-langRelevant to the language teamRelevant to the language team
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.
Metadata
Metadata
Assignees
Labels
A-trait-systemArea: Trait systemArea: Trait systemC-enhancementCategory: An issue proposing an enhancement or a PR with one.Category: An issue proposing an enhancement or a PR with one.T-langRelevant to the language teamRelevant to the language team