Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't check GAT bounds in normalization #117682

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

aliemjay
Copy link
Member

@aliemjay aliemjay commented Nov 7, 2023

This should fix most of GAT bugs related to where Self: 'a. See the ui tests for examples.

The core idea is that we don't check associated type bounds when normalizing them, but rather rely on the them being well-formed. This is similar to how we deal with other rigid types. This should, for example, eliminate the strange inconsistent behavior in this snippet:

trait Trait { type Gat<'a> where Self: 'a; }
impl<T> Trait for T { type Gat<'a> = &'a T where Self: 'a; }

type Raw<'a, T> = &'a T; // requires T: 'a
type Gat<'a, T> = <T as Trait>::Gat::<'a>; // requires T: 'a as well

fn test<T, U: Trait>() {
    let _: fn(Raw<'_, T>); // Ok
    let _: fn(Gat<'_, T>); // Error now; Ok with this PR
    let _: fn(Gat<'_, U>); // Ok (normalized to a rigid projection)
}

The main problem with this approach is that we currently don't check the well-formedness of projection types before normalizing them. See #100041 and #104764. This causes us to accept the following invalid code (from tests/ui/generic-associated-types/unsatisfied-{body,item}-lifetime-bound.rs)

trait Trait { type Gat<'a> where Self: 'a; }
impl<T> Trait for T { type Gat<'a> = () where Self: 'a; }

struct MyTy<T> {
    f: <T as Trait>::Gat::<'static>, // error now (as expected); passes with this PR!
    g: T,
}

but I believe both issues are relatively straightforward to fix given the previous attempts in #100046 and #104746.

Another problem is that of tests/ui/generic-associated-types/projection-bound-cycle{,-generic}.rs, but that's hopefully fixable in some kind of analysis. (I can see it in compare_predicate_entailement).

So, my question to @rust-lang/types is that, assuming that we have a satisfactory solution to both problems above, do you have other concerns about this approach?

r? @ghost

@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. labels Nov 7, 2023
@aliemjay aliemjay added T-types Relevant to the types team, which will review and decide on the PR/issue. S-blocked Status: Marked as blocked ❌ on something else such as an RFC or other implementation work. and removed T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Nov 7, 2023
@jackh726
Copy link
Member

jackh726 commented Nov 8, 2023

Niko tried this same thing in #98742. Can't remember that we actually discussed this much then, though.

My biggest thought is that, in theory, the bounds we prove for projections is the same that we prove when normalizing that projection. So, if we start actually proving that projections are WF correctly, we're going to end up proving these bounds still.

@jackh726
Copy link
Member

jackh726 commented Nov 8, 2023

I'm curious: Does this variation of your example above pass or fail under this PR?

trait Trait { type Gat<'a> where Self: 'a; }
impl<T> Trait for T { type Gat<'a> = &'a T where Self: 'a; }

type Raw<'a, T> = &'a T; // requires T: 'a
type Gat<'a, T> = <T as Trait>::Gat::<'a>; // requires T: 'a as well

fn test<T, U: Trait>() {
    let _: fn(Gat<'static, T>);
}

@aliemjay
Copy link
Member Author

aliemjay commented Nov 8, 2023

Niko tried this same thing in #98742. Can't remember that we actually discussed this much then, though.

This PR accepts more code because it applies to impl candidates as well (vs. Niko's PR which applies to param env candidates only). The snippet above, for example, does not pass under Niko's PR

// ...
fn test<T, U: Trait>() {
    let _: fn(Gat<'_, T>); // Error always
}

I'm curious: Does this variation of your example above pass or fail under this PR?

It fails beacause it is normalized to &'static T which in turn enforces T: 'static, only because #54940 got fixed.

@BoxyUwU
Copy link
Member

BoxyUwU commented Nov 8, 2023

Removing well formedness checks that are evidently required for soundness makes me pretty nervous, regardless of the fact that normalization being where we end up actually checking the bounds hold for soundness reasons is weird. This kind of compounds with the fact that the motivation here to me doesn't feel very good, this doesn't directly fix the issue it just works around it by avoiding proving bounds that we should be able to prove.

Is it particularly urgent to solve this? It was acceptable to stabilize gats with these bugs in mind so I would assume we are not in any kind of rush. with that in mind i'd prefer us to wait until the new solver is done to tackle this (and do so by tracking implied bounds properly so that we can check wfness of types under binders properly)

@bors
Copy link
Contributor

bors commented Nov 25, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
S-blocked Status: Marked as blocked ❌ on something else such as an RFC or other implementation work. T-types Relevant to the types team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants