rust-lang / chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver
https://rust-lang.github.io/chalk/book/
Other
1.81k stars 179 forks source link

Generate `Normalize` clauses for dyn and opaque types #780

Closed lowr closed 1 year ago

lowr commented 1 year ago

When a trait Trait has a transitive supertrait defined like trait SuperTrait: AnotherTrait<Assoc = Ty>, we've been generating impl AnotherTrait for dyn Trait and opaque type T: Trait but without accounting for the associated type bound. This patch adds Normalize clauses that correspond to such bounds.

For example, given the following definition

trait SuperTrait where WC {
   type Assoc where AssocWC;
}
trait Trait: SuperTrait<Assoc = Ty> {}

we generate the following clauses

// for dyn Trait
Implemented(dyn Trait: SuperTrait) :- WC
Normalize(<dyn Trait as SuperTrait>::Assoc -> Ty) :- WC, AssocWC // this patch adds this
// for placeholder !T for opaque type T: Trait
Implemented(!T: SuperTrait) :- WC
Normalize(<!T as SuperTrait>::Assoc -> Ty) :- WC, AssocWC // this patch adds this

I think this doesn't contradict #203 as "we may legitimately assume that all things talking directly about ?Self are true", but I'm not really sure if this is the right direction. One caveat is that this patch exacerbates "wastefulness" as in this comment as it adds the Normalize clauses even when we're trying to prove other kinds of goals.

Fixes #777

jackh726 commented 1 year ago

@bors r+

bors commented 1 year ago

:pushpin: Commit 1346728050928f5ed800dea034603af9d38bcb0d has been approved by jackh726

It is now in the queue for this repository.

bors commented 1 year ago

:hourglass: Testing commit 1346728050928f5ed800dea034603af9d38bcb0d with merge 1635ed5da8e1eb6aceb9d11b4ebcd2ff732d653b...

bors commented 1 year ago

:sunny: Test successful - checks-actions Approved by: jackh726 Pushing 1635ed5da8e1eb6aceb9d11b4ebcd2ff732d653b to master...