Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -465,6 +465,15 @@ where
// `PathKind::Inductive`. Keeping them as unknown until we're confident
// about this and have an example where it is necessary.
GoalSource::AliasBoundConstCondition | GoalSource::AliasWellFormed => PathKind::Unknown,
// While normalizing an opaque, its provisional hidden type is registered
// before we check the goals required by its item bounds. Proving one of
// these bounds may normalize the same opaque again, forming a cycle back
// to that provisional normalization.
//
// Treat crossing this edge as coinductive so that recursive normalization
// can reuse the provisional hidden type. This does not make cycles wholly
// contained in the bound proof coinductive.
GoalSource::OpaqueTypeBound => PathKind::Coinductive,
}
}

Expand Down Expand Up @@ -1399,7 +1408,7 @@ where
hidden_ty,
&mut goals,
);
self.add_goals(GoalSource::AliasWellFormed, goals)?;
self.add_goals(GoalSource::OpaqueTypeBound, goals)?;
Ok(())
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,7 @@ impl<'tcx> BestObligation<'tcx> {
GoalSource::ImplWhereBound
| GoalSource::AliasBoundConstCondition
| GoalSource::AliasWellFormed
| GoalSource::OpaqueTypeBound
) && nested_goal.result().is_err()
},
)
Expand Down Expand Up @@ -538,7 +539,12 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
impl_where_bound_count += 1;
}
(ChildMode::PassThrough, _)
| (_, GoalSource::AliasWellFormed | GoalSource::AliasBoundConstCondition) => {
| (
_,
GoalSource::AliasWellFormed
| GoalSource::AliasBoundConstCondition
| GoalSource::OpaqueTypeBound,
) => {
obligation = make_obligation(self.obligation.cause.clone());
}
}
Expand Down
2 changes: 2 additions & 0 deletions compiler/rustc_type_ir/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -438,6 +438,8 @@ pub enum GoalSource {
/// 2. for rigid projections's trait goal,
/// 3. for GAT where clauses.
AliasWellFormed,
/// Predicate required while proving the item bounds of an opaque's hidden type.
OpaqueTypeBound,
/// In case normalizing aliases in nested goals cycles, eagerly normalizing these
/// aliases in the context of the parent may incorrectly change the cycle kind.
/// Normalizing aliases in goals therefore tracks the original path kind for this
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
//@ compile-flags: -Znext-solver
//@ check-fail

trait Bound {}

trait Needs {}

impl Needs for () {}

trait Trait {
type Assoc<T>
where
T: Bound;
}

impl Trait for () {
type Assoc<T>
= ()
where
T: Bound;
}

// Normalizing `Assoc<()>` also requires its own `(): Bound` clause.
// Treating `AliasWellFormed` as coinductive would incorrectly make
// this cycle productive.
impl Bound for ()
//~^ ERROR overflow evaluating the requirement `<() as Trait>::Assoc<()> == _`
where
<() as Trait>::Assoc<()>: Needs,
{}

fn require_bound<T: Bound>() {}

fn main() {
require_bound::<()>();
//~^ ERROR overflow evaluating the requirement `(): Bound`
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
error[E0275]: overflow evaluating the requirement `<() as Trait>::Assoc<()> == _`
--> $DIR/alias-well-formed-not-coinductive.rs:26:1
|
LL | / impl Bound for ()
LL | |
LL | | where
LL | | <() as Trait>::Assoc<()>: Needs,
| |____________________________________^

error[E0275]: overflow evaluating the requirement `(): Bound`
--> $DIR/alias-well-formed-not-coinductive.rs:35:21
|
LL | require_bound::<()>();
| ^^
|
note: required by a bound in `require_bound`
--> $DIR/alias-well-formed-not-coinductive.rs:32:21
|
LL | fn require_bound<T: Bound>() {}
| ^^^^^ required by this bound in `require_bound`

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0275`.
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@ check-pass

#![feature(type_alias_impl_trait)]

pub type Foo<T> = impl PartialEq<(Foo<T>, T)>;

struct Bar<T>(T);

impl<T> PartialEq<(Foo<T>, T)> for Bar<T> {
fn eq(&self, _: &(Foo<T>, T)) -> bool {
true
}
}

#[define_opaque(Foo)]
fn foo<T>(value: T) -> Foo<T> {
Bar(value)
}

fn main() {}
26 changes: 26 additions & 0 deletions tests/ui/traits/next-solver/opaques/recursive-tait-bound-reveal.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//@ compile-flags: -Znext-solver
//@ check-pass

#![feature(type_alias_impl_trait)]

// Checking the opaque's recursive item bound requires normalizing `Foo`
// to its provisional hidden type while selecting the `PartialEq` impl.
// This ensures we do not handle recursive TAIT bounds by suppressing
// normalization of the recursive opaque.

pub type Foo = impl PartialEq<(Foo, i32)>;

#[define_opaque(Foo)]
fn foo() -> Foo {
Bar
}

struct Bar;

impl PartialEq<(Bar, i32)> for Bar {
fn eq(&self, _: &(Bar, i32)) -> bool {
true
}
}

fn main() {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
//@ compile-flags: -Znext-solver
//@ check-fail

#![feature(type_alias_impl_trait)]

trait Trait {}

type Foo = impl Trait;

struct Bar<T>(T);

// This cycle is entirely inside the proof of the opaque's item bound.
// Crossing `OpaqueTypeBound` must not make this recursive impl productive.
impl<T> Trait for Bar<T>
where
Bar<T>: Trait,
{}

#[define_opaque(Foo)]
fn foo() -> Foo {
//~^ ERROR overflow evaluating the requirement `Foo == Bar<()>`
Bar(())
}

fn main() {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
error[E0275]: overflow evaluating the requirement `Foo == Bar<()>`
--> $DIR/recursive-tait-bound-unproductive.rs:20:13
|
LL | fn foo() -> Foo {
| ^^^

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0275`.
23 changes: 23 additions & 0 deletions tests/ui/traits/next-solver/opaques/recursive-tait-bound.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver
//@ check-pass

#![feature(type_alias_impl_trait)]

pub type Foo = impl PartialEq<(Foo, i32)>;

#[define_opaque(Foo)]
fn foo() -> Foo {
Bar
}

struct Bar;

impl PartialEq<(Foo, i32)> for Bar {
fn eq(&self, _: &(Foo, i32)) -> bool {
true
}
}

fn main() {}
Loading