Skip to content

Commit

Permalink
elaborate unknowable goals
Browse files Browse the repository at this point in the history
if a trait is unknowable, but its super trait
is definitely not implemented, then the trait
itself is definitely also not implemented.
  • Loading branch information
lcnr committed Jul 10, 2024
1 parent 0fdfb61 commit ef4bf0e
Show file tree
Hide file tree
Showing 11 changed files with 124 additions and 2 deletions.
12 changes: 12 additions & 0 deletions compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -699,6 +699,18 @@ where
if ecx.trait_ref_is_knowable(goal.param_env, trait_ref)? {
Err(NoSolution)
} else {
// While the trait bound itself may be unknowable, we may be able to
// prove that a super trait is not implemented. For this, we recursively
// prove the super trait bounds of the current goal.
//
// We skip the goal itself as that one would cycle.
let predicate: I::Predicate = trait_ref.upcast(cx);
ecx.add_goals(
GoalSource::Misc,
elaborate::elaborate(cx, [predicate])
.skip(1)
.map(|predicate| goal.with(cx, predicate)),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
},
Expand Down
1 change: 1 addition & 0 deletions compiler/rustc_type_ir/src/inherent.rs
Original file line number Diff line number Diff line change
Expand Up @@ -433,6 +433,7 @@ pub trait Predicate<I: Interner<Predicate = Self>>:
+ UpcastFrom<I, ty::OutlivesPredicate<I, I::Ty>>
+ UpcastFrom<I, ty::OutlivesPredicate<I, I::Region>>
+ IntoKind<Kind = ty::Binder<I, ty::PredicateKind<I>>>
+ Elaboratable<I>
{
fn as_clause(self) -> Option<I::Clause>;

Expand Down
1 change: 1 addition & 0 deletions tests/ui/coherence/normalize-for-errors.next.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ LL |
LL | impl<S: Iterator> MyTrait<S> for (Box<<(MyType,) as Mirror>::Assoc>, S::Item) {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `(Box<(MyType,)>, <_ as Iterator>::Item)`
|
= note: upstream crates may add a new impl of trait `std::clone::Clone` for type `(MyType,)` in future versions
= note: upstream crates may add a new impl of trait `std::marker::Copy` for type `std::boxed::Box<(MyType,)>` in future versions

error: aborting due to 1 previous error
Expand Down
1 change: 1 addition & 0 deletions tests/ui/coherence/normalize-for-errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,5 +18,6 @@ impl<S: Iterator> MyTrait<S> for (Box<<(MyType,) as Mirror>::Assoc>, S::Item) {}
//~^ ERROR conflicting implementations of trait `MyTrait<_>` for type `(Box<(MyType,)>,
//~| NOTE conflicting implementation for `(Box<(MyType,)>,
//~| NOTE upstream crates may add a new impl of trait `std::marker::Copy` for type `std::boxed::Box<(MyType,)>` in future versions
//[next]~| NOTE upstream crates may add a new impl of trait `std::clone::Clone` for type `(MyType,)` in future versions

fn main() {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
error[E0119]: conflicting implementations of trait `Overlap<_>` for type `()`
--> $DIR/super-trait-knowable-1.rs:16:1
|
LL | impl<T, U: Sub<T>> Overlap<T> for U {}
| ----------------------------------- first implementation here
LL | impl<T> Overlap<T> for () {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `()`
|
= note: downstream crates may implement trait `Sub<_>` for type `()`

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0119`.
19 changes: 19 additions & 0 deletions tests/ui/coherence/super-traits/super-trait-knowable-1.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Added in #124532. While `(): Super` is knowable, `(): Sub<?t>` is not.
//
// We therefore elaborate super trait bounds in the implicit negative
// overlap check.

//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@[next] check-pass

trait Super {}
trait Sub<T>: Super {}

trait Overlap<T> {}
impl<T, U: Sub<T>> Overlap<T> for U {}
impl<T> Overlap<T> for () {}
//[current]~^ ERROR conflicting implementations

fn main() {}
33 changes: 33 additions & 0 deletions tests/ui/coherence/super-traits/super-trait-knowable-2.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// A regression test for pyella-0.1.5 which broke when
// enabling the new solver in coherence.
//
// `Tensor: TensorValue` is knowable while `Tensor: TensorOp<?t2>`
// may be implemented downstream. We previously didn't check the
// super trait bound in coherence, causing these impls to overlap.
//
// However, we did fail to normalize `<Tensor as TensorValue::Unmasked`
// which caused the old solver to emit a `Tensor: TensorValue` goal in
// `fn normalize_to_error` which then failed, causing this test to pass.

//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@ check-pass

pub trait TensorValue {
type Unmasked;
}

trait TensorCompare<T> {}
pub trait TensorOp<T>: TensorValue {}

pub struct Tensor;
impl<T2> TensorCompare<T2> for Tensor {}
impl<T1, T2> TensorCompare<T2> for T1
where
T1: TensorOp<T2>,
T1::Unmasked: Sized,
{}


fn main() {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
error[E0119]: conflicting implementations of trait `Overlap<_>` for type `()`
--> $DIR/super-trait-knowable-3.rs:21:1
|
LL | impl<T, U: Bound<W<T>>> Overlap<T> for U {}
| ---------------------------------------- first implementation here
LL | impl<T> Overlap<T> for () {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `()`
|
= note: downstream crates may implement trait `Sub<_>` for type `()`

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0119`.
24 changes: 24 additions & 0 deletions tests/ui/coherence/super-traits/super-trait-knowable-3.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
// Unlike in `super-trait-knowable-1.rs`, the knowable
// super trait bound is in a nested goal and we currently
// only elaborate in the root. This can, and should, be#
// changed in the future.

//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@[next] check-pass

trait Super {}
trait Sub<T>: Super {}

trait Bound<T> {}

impl<T: Sub<U>, U> Bound<W<U>> for T {}

struct W<T>(T);
trait Overlap<T> {}
impl<T, U: Bound<W<T>>> Overlap<T> for U {}
impl<T> Overlap<T> for () {}
//[current]~^ ERROR conflicting implementations of trait `Overlap<_>` for type `()`

fn main() {}
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
error[E0119]: conflicting implementations of trait `Clone` for type `Node<[_]>`
--> $DIR/issue-48728.rs:4:10
--> $DIR/issue-48728.rs:9:10
|
LL | #[derive(Clone)]
| ^^^^^ conflicting implementation for `Node<[_]>`
Expand Down
7 changes: 6 additions & 1 deletion tests/ui/issues/issue-48728.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
// Regression test for #48728, an ICE that occurred computing
// coherence "help" information.

#[derive(Clone)] //~ ERROR conflicting implementations of trait `Clone`
//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@[next] check-pass

#[derive(Clone)] //[current]~ ERROR conflicting implementations of trait `Clone`
struct Node<T: ?Sized>(Box<T>);

impl<T: Clone + ?Sized> Clone for Node<[T]> {
Expand Down

0 comments on commit ef4bf0e

Please sign in to comment.