use implied bounds from impl header when comparing trait and impl methods

[aliemjay]

Fixes #105495.

I pulled it out of #105483.

r? @compiler-errors

[compiler-errors]

r? @lcnr because they're the one who's most aware of the current state of the issue w/ implied bounds and unnormalized types.

[bors]

☔ The latest upstream changes (presumably #106129) made this pull request unmergeable. Please resolve the merge conflicts.

[lcnr]

Unless there's another reason apart from consistency for adding this, I think this should wait until we're able to add explicit implied bounds in the trait solver. I think we should block this on coinductive trait predicates.

What does this PR do

When we check that the where-bounds of the impl are weaker than the where-bounds of the trait, we now add the implied bounds of the impl header to our assumptions, allowing where-bounds which rely on these implied bounds.

Does this agree with our long term plan for implied bounds

Definitely yes. We pretty much want to get to a point where we add WellFormed predicates for types in the impl signature to the predicates_of and then use these bounds as assumptions while inside of the item.

This means that any place which uses the param_env of the impl should also be able to use the implied bounds of the impl.

Is this currently sound

Sadly not completely. It would allow for a slightly different variant of #100051. Instead of now only relying on this unchecked implied bounds when checking that the signature has weaker requirements, we also rely on them when checking the where-bounds.

This causes the following unsound test to compile:

(pretty much #100051)

trait Trait {
    type Type;
}

impl<T> Trait for T {
    type Type = ();
}

trait Extend<'a, 'b> {
    fn extend(s: &'a str) -> &'b str;
}

impl<'a, 'b> Extend<'a, 'b> for <&'b &'a () as Trait>::Type
where
    for<'what, 'ever> &'what &'ever (): Trait,
{
    // instead of getting the implied bound from the self type
    // we get it through an explicit bound on the impl method instead.
    //
    // This explicit bound is accepted because it's implied by the
    // impl header.
    fn extend(s: &'a str) -> &'b str
    where
        'a: 'b
    {
        s
    }
}

fn main() {
    let y = <() as Extend<'_, '_>>::extend(&String::from("Hello World"));
    println!("{}", y);
}

I don't think this unsoundness will ever get triggered by accident and if someone wants to use it, they can already use the #100051. So I don't think that this is a hard blocker to landing this PR if there were practical applications.

Is it useful

I don't think it's too useful. If bounds on the impl method rely on the implied bounds from the impl header to be correct, then why add these as bounds at all if they're already implied by the impl header.

borrowck also doesn't use implied bounds from the impl header right now, only from its signature, so this PR would allow circumventing that issue. That would be pretty inconsistent though. Allowing borrowck to use implied bounds from impl headers would allow the above unsoundness in a more implicit way so I fear that it might actually be possible to rely on that by accident.

---

I guess let's go with:

@rust-lang/types I believe we should delay adding implied bounds to compare_predicate_entailment until we're correctly dealing with implied bounds from unnormalized projections in the impl header.

@rfcbot fcp close

[rfcbot]

Team member @lcnr has proposed to close this. The next step is review by the rest of the tagged team members:

• @Aaron1011
• @cjgillot
• @compiler-errors
• @davidtwco
• @eddyb
• @estebank
• @jackh726
• @lcnr
• @matthewjasper
• @michaelwoerister
• @nagisa
• @nikomatsakis
• @oli-obk
• @petrochenkov
• @pnkfelix
• @spastorino
• @wesleywiser

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[lcnr]

@rfcbot fcp cancel

sorry for the ping 😅

[rfcbot]

@lcnr proposal cancelled.

[lcnr]

@rfcbot fcp close

[rfcbot]

Team member @lcnr has proposed to close this. The next step is review by the rest of the tagged team members:

• @compiler-errors
• @jackh726
• @lcnr
• @nikomatsakis
• @oli-obk
• @spastorino

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period, with a disposition to close, as per the review above, is now complete.

As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed.