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

old solver incompletely prefers projection and object candidates #27

Open
lcnr opened this issue May 31, 2023 · 3 comments
Open

old solver incompletely prefers projection and object candidates #27

lcnr opened this issue May 31, 2023 · 3 comments
Labels
A-incomplete incorrectly return `NoSolution`, unsound during coherence

Comments

@lcnr
Copy link
Contributor

lcnr commented May 31, 2023

the following example compiles in the old solver and errors in the new solver. This happens because the old solver makes an arbitrary choice here https://github.com/rust-lang/rust/blob/617d3d6d722c432cdcbf210e6db55c3bdeafe381/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1967-L1972

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

fn foo<'x, 'y>() -> impl Trait<'x> + Trait<'y> {}

fn impls_trait<'x, T: Trait<'x>>(_: T) {}

fn bar<'x, 'y>() {
    impls_trait::<'y, _>(foo::<'_, '_>());
}

fn main() {}

changing this example a bit we get a MIR typeck ICE with the new solver

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

fn foo<'x, 'y>() -> impl Trait<'x> + Trait<'y> {}

fn impls_trait<'x, T: Trait<'x>>(_: T) {}

fn bar<'x, 'y>() {
    impls_trait::<'y, _>(foo::<'x, 'y>());
}

fn main() {}
error: internal compiler error: errors selecting obligation during MIR typeck: [FulfillmentError(Obligation(predicate=Binder(TraitPredicate(<Opaque(DefId(0:17 ~ main[db48]::foo::{opaque#0}), ['?16, '?17, '?18, '?19]) as Trait<ReFree(DefId(0:13 ~ main[db48]::bar), BrNamed(DefId(0:15 ~ main[db48]::bar::'y), 'y))>>, polarity:Positive), []), cause=ObligationCause { span: src/main.rs:6:23: 6:32 (#0), body_id: DefId(0:0 ~ main[db48]), code: AscribeUserTypeProvePredicate(src/main.rs:6:23: 6:32 (#0)) }, param_env=ParamEnv { caller_bounds: [], reveal: UserFacing, constness: NotConst }, depth=0),Ambiguity), FulfillmentError(Obligation(predicate=Binder(WellFormed(fn(?0t) {impls_trait::<ReFree(DefId(0:13 ~ main[db48]::bar), BrNamed(DefId(0:15 ~ main[db48]::bar::'y), 'y)), ?0t>}), []), cause=ObligationCause { span: no-location (#0), body_id: DefId(0:0 ~ main[db48]), code: MiscObligation }, param_env=ParamEnv { caller_bounds: [], reveal: UserFacing, constness: NotConst }, depth=0),Ambiguity)]

This feels like it may be caused by the theoretical issue discussed in https://rust-lang.zulipchat.com/#narrow/stream/364551-t-types.2Ftrait-system-refactor/topic/mir.20typeck.20and.20relying.20on.20region.20equality

@lcnr
Copy link
Contributor Author

lcnr commented May 31, 2023

the same using projection candidates
ambig in new solver:

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

trait Proj<'x, 'y> {
    type Assoc: Trait<'x> + Trait<'y>;
}

fn foo<'x, 'y, T: Proj<'x, 'y>>() -> T::Assoc { todo!() }

fn impls_trait<'x, T: Trait<'x>>(_: T) {}

fn bar<'x, 'y, T: Proj<'x, 'y>>() {
    impls_trait::<'y, _>(foo::<'_, '_, T>());
}

fn main() {}

ICE in new solver

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

trait Proj<'x, 'y> {
    type Assoc: Trait<'x> + Trait<'y>;
}

fn foo<'x, 'y, T: Proj<'x, 'y>>() -> T::Assoc { todo!() }

fn impls_trait<'x, T: Trait<'x>>(_: T) {}

fn bar<'x, 'y, T: Proj<'x, 'y>>() {
    impls_trait::<'y, _>(foo::<'x, 'y, T>());
}

fn main() {}

@lcnr
Copy link
Contributor Author

lcnr commented May 31, 2023

and using object bounds

ambig

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

trait Object<'x, 'y>: Trait<'x> + Trait<'y> {}

fn foo<'x, 'y>() -> Box<dyn Object<'x, 'y>> { todo!() }

fn impls_trait<'x, T: Trait<'x> + ?Sized>(_: Box<T>) {}

fn bar<'x, 'y>() {
    impls_trait::<'y, _>(foo::<'_, '_>());
}

fn main() {}

mir ICE:

trait Trait<'t> {}
impl<'t> Trait<'t> for () {}

trait Object<'x, 'y>: Trait<'x> + Trait<'y> {}

fn foo<'x, 'y>() -> Box<dyn Object<'x, 'y>> { todo!() }

fn impls_trait<'x, T: Trait<'x> + ?Sized>(_: Box<T>) {}

fn bar<'x, 'y>() {
    impls_trait::<'y, _>(foo::<'x, 'y>());
}

fn main() {}

@lcnr lcnr added the A-incomplete incorrectly return `NoSolution`, unsound during coherence label Jul 7, 2023
@lcnr
Copy link
Contributor Author

lcnr commented Jul 11, 2024

this issue may be fixed by supporting OR bounds in query outputs instead. This means we'd rely on no region based incompleteness existing

bors added a commit to rust-lang-ci/rust that referenced this issue Sep 25, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [ ] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 26, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [x] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 27, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [x] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 27, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [x] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 27, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [x] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 27, 2024
caching? CACHING!

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but would like to provide an easily verifiable abstraction for caching visitors if possible. Don't think I can extend that one to `TypeRelating` however.

The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

- [x] add test of the new nalgebra minimization, it's different from this
- [ ] add an abstraction for caching type visitors

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 30, 2024
add caching to most type folders

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but it definitely adds some non-local complexity in places. The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Sep 30, 2024
add caching to most type folders

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but it definitely adds some non-local complexity in places. The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

r? `@compiler-errors`
bors added a commit to rust-lang-ci/rust that referenced this issue Oct 2, 2024
add caching to most type folders, rm region uniquification

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but it definitely adds some non-local complexity in places. The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

r? `@compiler-errors`
RalfJung pushed a commit to RalfJung/miri that referenced this issue Oct 3, 2024
add caching to most type folders, rm region uniquification

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but it definitely adds some non-local complexity in places. The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

r? `@compiler-errors`
lnicola pushed a commit to lnicola/rust-analyzer that referenced this issue Oct 8, 2024
add caching to most type folders, rm region uniquification

Fixes the new minimization of the hang in nalgebra and nalgebra itself :3

this is a bit iffy, especially the cache in `TypeRelating`. I believe all the caches are correct, but it definitely adds some non-local complexity in places. The first commit removes region uniquification, reintroducing the ICE from rust-lang/trait-system-refactor-initiative#27. This does not affect coherence and I would like to fix this by introducing OR-region constraints

r? `@compiler-errors`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-incomplete incorrectly return `NoSolution`, unsound during coherence
Projects
None yet
Development

No branches or pull requests

1 participant