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

Associated type bounds can be used to prove themselves with trivial where-clauses #62

Closed
compiler-errors opened this issue Sep 20, 2023 · 5 comments

Comments

@compiler-errors
Copy link
Member

compiler-errors commented Sep 20, 2023

trait Foo {
    type Assoc: Bar
        where Self: Foo;
}

trait Bar {}

impl Foo for () {
    type Assoc = ()
        where Self: Foo;
}

This side-steps the check that associated type bounds may only be used if we have a param-env predicate that "roots" the associated type. See the doc comment on validate_alias_bound_self_from_param_env.

Turns out this is not a complete solution.

@compiler-errors compiler-errors changed the title Associated type bounds are still unsound Associated type bounds can be used to prove themselves with trivial where-clauses Sep 20, 2023
@compiler-errors
Copy link
Member Author

#46 is the same problem as this, and #59 is related but for type-outlives obligations

@compiler-errors
Copy link
Member Author

Unsound :(

trait Foo {
    type Assoc<'a>: Static
        where Self: Foo;
}

trait Static {
    fn uwu(self) -> &'static str;
}
impl Static for &'static str {
    fn uwu(self) -> &'static str { self }
}

impl Foo for () {
    type Assoc<'a> = &'a str
        where Self: Foo;
}

fn hello<T: Foo>(x: T::Assoc<'_>) -> &'static str {
    T::Assoc::uwu(x)
}


fn main() {
    let x = String::new();
    let x: &'static str = hello::<()>(&x);
}

@compiler-errors
Copy link
Member Author

The correct fix here:

  • Prove item bounds when normalizes-to being proven via impl (or built-impl, anything that requires its bounds to hold for it to be WF; i.e. not a param-env normalizes-to candidate)
  • Prove concrete-ty alias-eq associated type in compare_type_predicate_entailment or whatever it's called (check_type_items_bounds?)

@compiler-errors
Copy link
Member Author

But the hacky fix:

  • Eagerly fold item bounds to replace with T::Alias with ConcreteTy before proving item bounds in check_type_item_bounds.

fmease added a commit to fmease/rust that referenced this issue May 30, 2024
…r=lcnr

Fold item bounds before proving them in `check_type_bounds` in new solver

Vaguely confident that this is sufficient to prevent rust-lang/trait-system-refactor-initiative#46 and rust-lang/trait-system-refactor-initiative#62.

This is not the "correct" solution, but will probably suffice until coinduction, at which point we implement the right solution (`check_type_bounds` must prove `Assoc<...> alias-eq ConcreteType`, normalizing requires proving item bounds).

r? lcnr
bors added a commit to rust-lang-ci/rust that referenced this issue May 31, 2024
…lcnr

Fold item bounds before proving them in `check_type_bounds` in new solver

Vaguely confident that this is sufficient to prevent rust-lang/trait-system-refactor-initiative#46 and rust-lang/trait-system-refactor-initiative#62.

This is not the "correct" solution, but will probably suffice until coinduction, at which point we implement the right solution (`check_type_bounds` must prove `Assoc<...> alias-eq ConcreteType`, normalizing requires proving item bounds).

r? lcnr
matthiaskrgr added a commit to matthiaskrgr/rust that referenced this issue May 31, 2024
…r=lcnr

Fold item bounds before proving them in `check_type_bounds` in new solver

Vaguely confident that this is sufficient to prevent rust-lang/trait-system-refactor-initiative#46 and rust-lang/trait-system-refactor-initiative#62.

This is not the "correct" solution, but will probably suffice until coinduction, at which point we implement the right solution (`check_type_bounds` must prove `Assoc<...> alias-eq ConcreteType`, normalizing requires proving item bounds).

r? lcnr
rust-timer added a commit to rust-lang-ci/rust that referenced this issue May 31, 2024
Rollup merge of rust-lang#125786 - compiler-errors:fold-item-bounds, r=lcnr

Fold item bounds before proving them in `check_type_bounds` in new solver

Vaguely confident that this is sufficient to prevent rust-lang/trait-system-refactor-initiative#46 and rust-lang/trait-system-refactor-initiative#62.

This is not the "correct" solution, but will probably suffice until coinduction, at which point we implement the right solution (`check_type_bounds` must prove `Assoc<...> alias-eq ConcreteType`, normalizing requires proving item bounds).

r? lcnr
flip1995 pushed a commit to flip1995/rust-clippy that referenced this issue Jun 28, 2024
Fold item bounds before proving them in `check_type_bounds` in new solver

Vaguely confident that this is sufficient to prevent rust-lang/trait-system-refactor-initiative#46 and rust-lang/trait-system-refactor-initiative#62.

This is not the "correct" solution, but will probably suffice until coinduction, at which point we implement the right solution (`check_type_bounds` must prove `Assoc<...> alias-eq ConcreteType`, normalizing requires proving item bounds).

r? lcnr
@compiler-errors
Copy link
Member Author

This got fixed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant