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_defaults are unsound in the new solver #46

Open
compiler-errors opened this issue Jul 7, 2023 · 7 comments
Open

associated_type_defaults are unsound in the new solver #46

compiler-errors opened this issue Jul 7, 2023 · 7 comments

Comments

@compiler-errors
Copy link
Member

compiler-errors commented Jul 7, 2023

rust-lang/rust#110673 attempted to make alias bounds sound in the new solver by only assembling alias bounds for a projection (such as <A as B>::C) when the trait that the projection comes from (<A as B>) can be satisfied via a param-env candidate.

This is problematic when checking whether an associated type default is well-formed, because we assume within the trait that Self: Trait<..> holds.

// compile-flags: -Ztrait-solver=next
#![feature(associated_type_defaults)]

trait Tr {
    type Ty: Copy = String;

    fn clone(x: &Self::Ty) -> Self::Ty {
        *x
    }
}

impl Tr for () {}

fn main() {
    let x = String::from("hello, world");
    let y = <() as Tr>::clone(&x);
    drop(x);
    println!("{y}");
    // ^^
}

During check_type_bounds in the above program, we must prove:

[
    Obligation(predicate=Binder { value: TraitPredicate(<<Self as Tr>::Ty as std::marker::Sized>, polarity:Positive), bound_vars: [] }, depth=0),
    Obligation(predicate=Binder { value: TraitPredicate(<<Self as Tr>::Ty as std::marker::Copy>, polarity:Positive), bound_vars: [] }, depth=0),
]

given the caller bounds of:

[
    Binder { value: TraitPredicate(<Self as Tr>, polarity:Positive), bound_vars: [] },
]

Which means that the check implemented in EvalCtxt::validate_alias_bound_self_from_param_env succeeds.

@lcnr
Copy link
Contributor

lcnr commented Jul 20, 2023

This feels somewhat unsolvable until we fully enable coinductive trait goals and check impl where clauses instead of the current hack which disables alias bounds candidates for stuff proven via impls

@TroyKomodo

This comment was marked as outdated.

@compiler-errors

This comment was marked as outdated.

@TroyKomodo

This comment was marked as outdated.

@pitaj

This comment was marked as off-topic.

@compiler-errors

This comment was marked as off-topic.

@pitaj

This comment was marked as off-topic.

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
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

4 participants