oops! new unsoundness

Bless tests and show an introduced unsoundness related to
exits<'a> { forall<'b> { 'a == 'b } }.
We now resolve the var ?a in U0 to the placeholder !b in U1.
This commit is contained in:
Ali MJ Al-Nasrawy 2023-03-05 12:05:04 +03:00
parent 79dca7b7ba
commit eea560494c
7 changed files with 21 additions and 41 deletions

View File

@ -2,6 +2,9 @@
// //
// In particular, we test this pattern in trait solving, where it is not connected // In particular, we test this pattern in trait solving, where it is not connected
// to any part of the source code. // to any part of the source code.
//
// check-pass
// Oops!
use std::cell::Cell; use std::cell::Cell;
@ -25,5 +28,5 @@ fn main() {
// yielding `fn(&!b u32)`, in a fresh universe U1 // yielding `fn(&!b u32)`, in a fresh universe U1
// - So we get `?a = !b` but the universe U0 assigned to `?a` cannot name `!b`. // - So we get `?a = !b` but the universe U0 assigned to `?a` cannot name `!b`.
foo::<()>(); //~ ERROR implementation of `Trait` is not general enough foo::<()>();
} }

View File

@ -1,11 +0,0 @@
error: implementation of `Trait` is not general enough
--> $DIR/hrtb-exists-forall-trait-invariant.rs:28:5
|
LL | foo::<()>();
| ^^^^^^^^^^^ implementation of `Trait` is not general enough
|
= note: `()` must implement `Trait<for<'b> fn(Cell<&'b u32>)>`
= note: ...but it actually implements `Trait<fn(Cell<&'0 u32>)>`, for some specific lifetime `'0`
error: aborting due to previous error

View File

@ -14,12 +14,6 @@ LL | fn give_some<'a>() {
| -- lifetime `'a` defined here | -- lifetime `'a` defined here
LL | want_hrtb::<&'a u32>() LL | want_hrtb::<&'a u32>()
| ^^^^^^^^^^^^^^^^^^^^ requires that `'a` must outlive `'static` | ^^^^^^^^^^^^^^^^^^^^ requires that `'a` must outlive `'static`
|
note: due to current limitations in the borrow checker, this implies a `'static` lifetime
--> $DIR/hrtb-just-for-static.rs:9:15
|
LL | where T : for<'a> Foo<&'a isize>
| ^^^^^^^^^^^^^^^^^^^^^^
error: implementation of `Foo` is not general enough error: implementation of `Foo` is not general enough
--> $DIR/hrtb-just-for-static.rs:30:5 --> $DIR/hrtb-just-for-static.rs:30:5

View File

@ -15,9 +15,9 @@ impl<'a> Y for C<'a> {
struct C<'a>(&'a ()); struct C<'a>(&'a ());
struct X<T: Y>(T::P); struct X<T: Y>(T::P);
impl<T: NotAuto> NotAuto for Box<T> {} //~ NOTE: required impl<T: NotAuto> NotAuto for Box<T> {}
impl<T: Y> NotAuto for X<T> where T::P: NotAuto {} //~ NOTE: required
//~^ NOTE unsatisfied trait bound introduced here //~^ NOTE unsatisfied trait bound introduced here
impl<T: Y> NotAuto for X<T> where T::P: NotAuto {}
impl<'a> NotAuto for C<'a> {} impl<'a> NotAuto for C<'a> {}
fn is_send<S: NotAuto>() {} fn is_send<S: NotAuto>() {}
@ -28,6 +28,4 @@ fn main() {
// Should only be a few notes. // Should only be a few notes.
is_send::<X<C<'static>>>(); is_send::<X<C<'static>>>();
//~^ ERROR overflow evaluating //~^ ERROR overflow evaluating
//~| 3 redundant requirements hidden
//~| required for
} }

View File

@ -1,18 +1,14 @@
error[E0275]: overflow evaluating the requirement `X<C<'_>>: NotAuto` error[E0275]: overflow evaluating the requirement `Box<X<C<'static>>>: NotAuto`
--> $DIR/lifetime.rs:29:5 --> $DIR/lifetime.rs:29:5
| |
LL | is_send::<X<C<'static>>>(); LL | is_send::<X<C<'static>>>();
| ^^^^^^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^^^^^^
| |
note: required for `Box<X<C<'_>>>` to implement `NotAuto` note: required for `X<C<'static>>` to implement `NotAuto`
--> $DIR/lifetime.rs:18:18 --> $DIR/lifetime.rs:19:12
| |
LL | impl<T: NotAuto> NotAuto for Box<T> {} LL | impl<T: Y> NotAuto for X<T> where T::P: NotAuto {}
| ------- ^^^^^^^ ^^^^^^ | ^^^^^^^ ^^^^ ------- unsatisfied trait bound introduced here
| |
| unsatisfied trait bound introduced here
= note: 3 redundant requirements hidden
= note: required for `X<C<'static>>` to implement `NotAuto`
note: required by a bound in `is_send` note: required by a bound in `is_send`
--> $DIR/lifetime.rs:23:15 --> $DIR/lifetime.rs:23:15
| |

View File

@ -4,10 +4,10 @@
pub struct Table<T, const N: usize>([Option<T>; N]); pub struct Table<T, const N: usize>([Option<T>; N]);
impl<'a, T, const N: usize> IntoIterator for &'a Table<T, N> { impl<'a, T, const N: usize> IntoIterator for &'a Table<T, N> {
type IntoIter = std::iter::Flatten<std::slice::Iter<'a, T>>; //~ ERROR `&T` is not an iterator type IntoIter = std::iter::Flatten<std::slice::Iter<'a, T>>; //~ ERROR `&'a T` is not an iterator
type Item = &'a T; type Item = &'a T;
fn into_iter(self) -> Self::IntoIter { //~ ERROR `&T` is not an iterator fn into_iter(self) -> Self::IntoIter { //~ ERROR `&'a T` is not an iterator
unimplemented!() unimplemented!()
} }
} }

View File

@ -1,24 +1,24 @@
error[E0277]: `&T` is not an iterator error[E0277]: `&'a T` is not an iterator
--> $DIR/hir-wf-check-erase-regions.rs:7:21 --> $DIR/hir-wf-check-erase-regions.rs:7:21
| |
LL | type IntoIter = std::iter::Flatten<std::slice::Iter<'a, T>>; LL | type IntoIter = std::iter::Flatten<std::slice::Iter<'a, T>>;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `&T` is not an iterator | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `&'a T` is not an iterator
| |
= help: the trait `Iterator` is not implemented for `&T` = help: the trait `Iterator` is not implemented for `&'a T`
= help: the trait `Iterator` is implemented for `&mut I` = help: the trait `Iterator` is implemented for `&mut I`
= note: required for `&T` to implement `IntoIterator` = note: required for `&'a T` to implement `IntoIterator`
note: required by a bound in `Flatten` note: required by a bound in `Flatten`
--> $SRC_DIR/core/src/iter/adapters/flatten.rs:LL:COL --> $SRC_DIR/core/src/iter/adapters/flatten.rs:LL:COL
error[E0277]: `&T` is not an iterator error[E0277]: `&'a T` is not an iterator
--> $DIR/hir-wf-check-erase-regions.rs:10:27 --> $DIR/hir-wf-check-erase-regions.rs:10:27
| |
LL | fn into_iter(self) -> Self::IntoIter { LL | fn into_iter(self) -> Self::IntoIter {
| ^^^^^^^^^^^^^^ `&T` is not an iterator | ^^^^^^^^^^^^^^ `&'a T` is not an iterator
| |
= help: the trait `Iterator` is not implemented for `&T` = help: the trait `Iterator` is not implemented for `&'a T`
= help: the trait `Iterator` is implemented for `&mut I` = help: the trait `Iterator` is implemented for `&mut I`
= note: required for `&T` to implement `IntoIterator` = note: required for `&'a T` to implement `IntoIterator`
note: required by a bound in `Flatten` note: required by a bound in `Flatten`
--> $SRC_DIR/core/src/iter/adapters/flatten.rs:LL:COL --> $SRC_DIR/core/src/iter/adapters/flatten.rs:LL:COL