1
Fork 0

Recurse on GAT where clauses in fulfillment error proof tree visitor

This commit is contained in:
Michael Goulet 2024-12-23 20:17:53 +00:00
parent 2be9ffc1af
commit ebdf19a8bb
11 changed files with 29 additions and 25 deletions

View file

@ -103,7 +103,7 @@ where
|ecx| { |ecx| {
// Const conditions must hold for the implied const bound to hold. // Const conditions must hold for the implied const bound to hold.
ecx.add_goals( ecx.add_goals(
GoalSource::Misc, GoalSource::AliasBoundConstCondition,
cx.const_conditions(alias_ty.def_id) cx.const_conditions(alias_ty.def_id)
.iter_instantiated(cx, alias_ty.args) .iter_instantiated(cx, alias_ty.args)
.map(|trait_ref| { .map(|trait_ref| {
@ -353,7 +353,7 @@ where
ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| { ecx.probe_builtin_trait_candidate(BuiltinImplSource::Misc).enter(|ecx| {
ecx.add_goals( ecx.add_goals(
GoalSource::ImplWhereBound, GoalSource::AliasBoundConstCondition,
const_conditions.into_iter().map(|trait_ref| { const_conditions.into_iter().map(|trait_ref| {
goal.with( goal.with(
cx, cx,

View file

@ -413,6 +413,7 @@ impl<'tcx> BestObligation<'tcx> {
matches!( matches!(
nested_goal.source(), nested_goal.source(),
GoalSource::ImplWhereBound GoalSource::ImplWhereBound
| GoalSource::AliasBoundConstCondition
| GoalSource::InstantiateHigherRanked | GoalSource::InstantiateHigherRanked
| GoalSource::AliasWellFormed | GoalSource::AliasWellFormed
) && match self.consider_ambiguities { ) && match self.consider_ambiguities {
@ -495,7 +496,6 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
}; };
let mut impl_where_bound_count = 0; let mut impl_where_bound_count = 0;
let mut impl_const_condition_bound_count = 0;
for nested_goal in candidate.instantiate_nested_goals(self.span()) { for nested_goal in candidate.instantiate_nested_goals(self.span()) {
trace!(nested_goal = ?(nested_goal.goal(), nested_goal.source(), nested_goal.result())); trace!(nested_goal = ?(nested_goal.goal(), nested_goal.source(), nested_goal.result()));
@ -521,21 +521,25 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
)); ));
impl_where_bound_count += 1; impl_where_bound_count += 1;
} }
(ChildMode::Host(parent_host_pred), GoalSource::ImplWhereBound) => { (
ChildMode::Host(parent_host_pred),
GoalSource::ImplWhereBound | GoalSource::AliasBoundConstCondition,
) => {
obligation = make_obligation(derive_host_cause( obligation = make_obligation(derive_host_cause(
tcx, tcx,
candidate.kind(), candidate.kind(),
self.obligation.cause.clone(), self.obligation.cause.clone(),
impl_const_condition_bound_count, impl_where_bound_count,
parent_host_pred, parent_host_pred,
)); ));
impl_const_condition_bound_count += 1; impl_where_bound_count += 1;
} }
// Skip over a higher-ranked predicate. // Skip over a higher-ranked predicate.
(_, GoalSource::InstantiateHigherRanked) => { (_, GoalSource::InstantiateHigherRanked) => {
obligation = self.obligation.clone(); obligation = self.obligation.clone();
} }
(ChildMode::PassThrough, _) | (_, GoalSource::AliasWellFormed) => { (ChildMode::PassThrough, _)
| (_, GoalSource::AliasWellFormed | GoalSource::AliasBoundConstCondition) => {
obligation = make_obligation(self.obligation.cause.clone()); obligation = make_obligation(self.obligation.cause.clone());
} }
} }

View file

@ -68,6 +68,10 @@ pub enum GoalSource {
/// FIXME(-Znext-solver=coinductive): Explain how and why this /// FIXME(-Znext-solver=coinductive): Explain how and why this
/// changes whether cycles are coinductive. /// changes whether cycles are coinductive.
ImplWhereBound, ImplWhereBound,
/// Const conditions that need to hold for `~const` alias bounds to hold.
///
/// FIXME(-Znext-solver=coinductive): Are these even coinductive?
AliasBoundConstCondition,
/// Instantiating a higher-ranked goal and re-proving it. /// Instantiating a higher-ranked goal and re-proving it.
InstantiateHigherRanked, InstantiateHigherRanked,
/// Predicate required for an alias projection to be well-formed. /// Predicate required for an alias projection to be well-formed.

View file

@ -5,7 +5,7 @@ LL | T::Assoc::<U>::func();
| ^^^^^^^^^^^^^ | ^^^^^^^^^^^^^
error[E0277]: the trait bound `U: ~const Other` is not satisfied error[E0277]: the trait bound `U: ~const Other` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail-2.rs:27:5 --> $DIR/assoc-type-const-bound-usage-fail-2.rs:26:5
| |
LL | <T as Trait>::Assoc::<U>::func(); LL | <T as Trait>::Assoc::<U>::func();
| ^^^^^^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^^^^^^

View file

@ -1,11 +1,11 @@
error[E0277]: the trait bound `<T as Trait>::Assoc<U>: ~const Trait` is not satisfied error[E0277]: the trait bound `U: ~const Other` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail-2.rs:24:5 --> $DIR/assoc-type-const-bound-usage-fail-2.rs:24:5
| |
LL | T::Assoc::<U>::func(); LL | T::Assoc::<U>::func();
| ^^^^^^^^^^^^^ | ^^^^^^^^^^^^^
error[E0277]: the trait bound `<T as Trait>::Assoc<U>: ~const Trait` is not satisfied error[E0277]: the trait bound `U: ~const Other` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail-2.rs:27:5 --> $DIR/assoc-type-const-bound-usage-fail-2.rs:26:5
| |
LL | <T as Trait>::Assoc::<U>::func(); LL | <T as Trait>::Assoc::<U>::func();
| ^^^^^^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^^^^^^

View file

@ -22,11 +22,9 @@ trait Other {}
const fn fails<T: ~const Trait, U: Other>() { const fn fails<T: ~const Trait, U: Other>() {
T::Assoc::<U>::func(); T::Assoc::<U>::func();
//[current]~^ ERROR the trait bound `U: ~const Other` is not satisfied //~^ ERROR the trait bound `U: ~const Other` is not satisfied
//[next]~^^ ERROR the trait bound `<T as Trait>::Assoc<U>: ~const Trait` is not satisfied
<T as Trait>::Assoc::<U>::func(); <T as Trait>::Assoc::<U>::func();
//[current]~^ ERROR the trait bound `U: ~const Other` is not satisfied //~^ ERROR the trait bound `U: ~const Other` is not satisfied
//[next]~^^ ERROR the trait bound `<T as Trait>::Assoc<U>: ~const Trait` is not satisfied
} }
const fn works<T: ~const Trait, U: ~const Other>() { const fn works<T: ~const Trait, U: ~const Other>() {

View file

@ -5,7 +5,7 @@ LL | T::Assoc::func();
| ^^^^^^^^ | ^^^^^^^^
error[E0277]: the trait bound `T: ~const Trait` is not satisfied error[E0277]: the trait bound `T: ~const Trait` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail.rs:20:5 --> $DIR/assoc-type-const-bound-usage-fail.rs:19:5
| |
LL | <T as Trait>::Assoc::func(); LL | <T as Trait>::Assoc::func();
| ^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^

View file

@ -1,11 +1,11 @@
error[E0277]: the trait bound `<T as Trait>::Assoc: ~const Trait` is not satisfied error[E0277]: the trait bound `T: ~const Trait` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail.rs:17:5 --> $DIR/assoc-type-const-bound-usage-fail.rs:17:5
| |
LL | T::Assoc::func(); LL | T::Assoc::func();
| ^^^^^^^^ | ^^^^^^^^
error[E0277]: the trait bound `<T as Trait>::Assoc: ~const Trait` is not satisfied error[E0277]: the trait bound `T: ~const Trait` is not satisfied
--> $DIR/assoc-type-const-bound-usage-fail.rs:20:5 --> $DIR/assoc-type-const-bound-usage-fail.rs:19:5
| |
LL | <T as Trait>::Assoc::func(); LL | <T as Trait>::Assoc::func();
| ^^^^^^^^^^^^^^^^^^^ | ^^^^^^^^^^^^^^^^^^^

View file

@ -15,11 +15,9 @@ trait Trait {
const fn unqualified<T: Trait>() { const fn unqualified<T: Trait>() {
T::Assoc::func(); T::Assoc::func();
//[current]~^ ERROR the trait bound `T: ~const Trait` is not satisfied //~^ ERROR the trait bound `T: ~const Trait` is not satisfied
//[next]~^^ ERROR the trait bound `<T as Trait>::Assoc: ~const Trait` is not satisfied
<T as Trait>::Assoc::func(); <T as Trait>::Assoc::func();
//[current]~^ ERROR the trait bound `T: ~const Trait` is not satisfied //~^ ERROR the trait bound `T: ~const Trait` is not satisfied
//[next]~^^ ERROR the trait bound `<T as Trait>::Assoc: ~const Trait` is not satisfied
} }
const fn works<T: ~const Trait>() { const fn works<T: ~const Trait>() {

View file

@ -12,7 +12,7 @@ note: required by a bound in `bar`
LL | const fn bar<T: ~const Foo>(t: T) -> impl ~const Foo { LL | const fn bar<T: ~const Foo>(t: T) -> impl ~const Foo {
| ^^^^^^ required by this bound in `bar` | ^^^^^^ required by this bound in `bar`
error[E0277]: the trait bound `impl Foo: const Foo` is not satisfied error[E0277]: the trait bound `(): const Foo` is not satisfied
--> $DIR/const-opaque.rs:33:12 --> $DIR/const-opaque.rs:33:12
| |
LL | opaque.method(); LL | opaque.method();

View file

@ -31,7 +31,7 @@ const _: () = {
let opaque = bar(()); let opaque = bar(());
//[no]~^ ERROR the trait bound `(): const Foo` is not satisfied //[no]~^ ERROR the trait bound `(): const Foo` is not satisfied
opaque.method(); opaque.method();
//[no]~^ ERROR the trait bound `impl Foo: const Foo` is not satisfied //[no]~^ ERROR the trait bound `(): const Foo` is not satisfied
std::mem::forget(opaque); std::mem::forget(opaque);
}; };