Skip to content

🚀 create a query for the program clauses needed to solve a given goal #49600

Closed
@nikomatsakis

Description

@nikomatsakis

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.

Metadata

Metadata

Assignees

Labels

A-trait-systemArea: Trait systemC-enhancementCategory: An issue proposing an enhancement or a PR with one.T-langRelevant to the language team, which will review and decide on the PR/issue.WG-traitsWorking group: Traits, https://internals.rust-lang.org/t/announcing-traits-working-group/6804

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions