Skip to content

Instantiate predicate binder without recanonicalizing goal in new solver #136997

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

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
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
17 changes: 1 addition & 16 deletions compiler/rustc_hir_typeck/src/fn_ctxt/inspect_obligations.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ use rustc_span::Span;
use rustc_trait_selection::solve::inspect::{
InspectConfig, InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor,
};
use rustc_type_ir::solve::GoalSource;
use tracing::{debug, instrument, trace};

use crate::FnCtxt;
Expand Down Expand Up @@ -120,21 +119,7 @@ impl<'a, 'tcx> ProofTreeVisitor<'tcx> for NestedObligationsForSelfTy<'a, 'tcx> {
fn visit_goal(&mut self, inspect_goal: &InspectGoal<'_, 'tcx>) {
let tcx = self.fcx.tcx;
let goal = inspect_goal.goal();
if self.fcx.predicate_has_self_ty(goal.predicate, self.self_ty)
// We do not push the instantiated forms of goals as it would cause any
// aliases referencing bound vars to go from having escaping bound vars to
// being able to be normalized to an inference variable.
//
// This is mostly just a hack as arbitrary nested goals could still contain
// such aliases while having a different `GoalSource`. Closure signature inference
// however can't really handle *every* higher ranked `Fn` goal also being present
// in the form of `?c: Fn<(<?x as Trait<'!a>>::Assoc)`.
//
// This also just better matches the behaviour of the old solver where we do not
// encounter instantiated forms of goals, only nested goals that referred to bound
// vars from instantiated goals.
&& !matches!(inspect_goal.source(), GoalSource::InstantiateHigherRanked)
{
if self.fcx.predicate_has_self_ty(goal.predicate, self.self_ty) {
self.obligations_for_self_ty.push(traits::Obligation::new(
tcx,
self.root_cause.clone(),
Expand Down
102 changes: 46 additions & 56 deletions compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -448,63 +448,53 @@ where
fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
let Goal { param_env, predicate } = goal;
let kind = predicate.kind();
if let Some(kind) = kind.no_bound_vars() {
match kind {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
self.compute_trait_goal(Goal { param_env, predicate }).map(|(r, _via)| r)
}
ty::PredicateKind::Clause(ty::ClauseKind::HostEffect(predicate)) => {
self.compute_host_effect_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::Projection(predicate)) => {
self.compute_projection_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(predicate)) => {
self.compute_type_outlives_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(predicate)) => {
self.compute_region_outlives_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {
self.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
}
ty::PredicateKind::Subtype(predicate) => {
self.compute_subtype_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Coerce(predicate) => {
self.compute_coerce_goal(Goal { param_env, predicate })
}
ty::PredicateKind::DynCompatible(trait_def_id) => {
self.compute_dyn_compatible_goal(trait_def_id)
}
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(arg)) => {
self.compute_well_formed_goal(Goal { param_env, predicate: arg })
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(ct)) => {
self.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
}
ty::PredicateKind::ConstEquate(_, _) => {
panic!("ConstEquate should not be emitted when `-Znext-solver` is active")
}
ty::PredicateKind::NormalizesTo(predicate) => {
self.compute_normalizes_to_goal(Goal { param_env, predicate })
}
ty::PredicateKind::AliasRelate(lhs, rhs, direction) => self
.compute_alias_relate_goal(Goal {
param_env,
predicate: (lhs, rhs, direction),
}),
ty::PredicateKind::Ambiguous => {
self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
self.enter_forall(kind, |ecx, kind| match kind {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(predicate)) => {
ecx.compute_trait_goal(Goal { param_env, predicate }).map(|(r, _via)| r)
}
} else {
self.enter_forall(kind, |ecx, kind| {
let goal = goal.with(ecx.cx(), ty::Binder::dummy(kind));
ecx.add_goal(GoalSource::InstantiateHigherRanked, goal);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
ty::PredicateKind::Clause(ty::ClauseKind::HostEffect(predicate)) => {
ecx.compute_host_effect_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::Projection(predicate)) => {
ecx.compute_projection_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(predicate)) => {
ecx.compute_type_outlives_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::RegionOutlives(predicate)) => {
ecx.compute_region_outlives_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstArgHasType(ct, ty)) => {
ecx.compute_const_arg_has_type_goal(Goal { param_env, predicate: (ct, ty) })
}
ty::PredicateKind::Subtype(predicate) => {
ecx.compute_subtype_goal(Goal { param_env, predicate })
}
ty::PredicateKind::Coerce(predicate) => {
ecx.compute_coerce_goal(Goal { param_env, predicate })
}
ty::PredicateKind::DynCompatible(trait_def_id) => {
ecx.compute_dyn_compatible_goal(trait_def_id)
}
ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(arg)) => {
ecx.compute_well_formed_goal(Goal { param_env, predicate: arg })
}
ty::PredicateKind::Clause(ty::ClauseKind::ConstEvaluatable(ct)) => {
ecx.compute_const_evaluatable_goal(Goal { param_env, predicate: ct })
}
ty::PredicateKind::ConstEquate(_, _) => {
panic!("ConstEquate should not be emitted when `-Znext-solver` is active")
}
ty::PredicateKind::NormalizesTo(predicate) => {
ecx.compute_normalizes_to_goal(Goal { param_env, predicate })
}
ty::PredicateKind::AliasRelate(lhs, rhs, direction) => {
ecx.compute_alias_relate_goal(Goal { param_env, predicate: (lhs, rhs, direction) })
}
ty::PredicateKind::Ambiguous => {
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
}
})
}

// Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,6 @@ impl<'tcx> BestObligation<'tcx> {
nested_goal.source(),
GoalSource::ImplWhereBound
| GoalSource::AliasBoundConstCondition
| GoalSource::InstantiateHigherRanked
| GoalSource::AliasWellFormed
) && match (self.consider_ambiguities, nested_goal.result()) {
(true, Ok(Certainty::Maybe(MaybeCause::Ambiguity)))
Expand Down Expand Up @@ -380,10 +379,6 @@ impl<'tcx> ProofTreeVisitor<'tcx> for BestObligation<'tcx> {
));
impl_where_bound_count += 1;
}
// Skip over a higher-ranked predicate.
(_, GoalSource::InstantiateHigherRanked) => {
obligation = self.obligation.clone();
}
(ChildMode::PassThrough, _)
| (_, GoalSource::AliasWellFormed | GoalSource::AliasBoundConstCondition) => {
obligation = make_obligation(self.obligation.cause.clone());
Expand Down
7 changes: 4 additions & 3 deletions compiler/rustc_trait_selection/src/traits/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -660,9 +660,10 @@ impl<'a, 'tcx> ProofTreeVisitor<'tcx> for AmbiguityCausesVisitor<'a, 'tcx> {
// For bound predicates we simply call `infcx.enter_forall`
// and then prove the resulting predicate as a nested goal.
let Goal { param_env, predicate } = goal.goal();
let trait_ref = match predicate.kind().no_bound_vars() {
Some(ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr))) => tr.trait_ref,
Some(ty::PredicateKind::Clause(ty::ClauseKind::Projection(proj)))
let predicate_kind = goal.infcx().enter_forall_and_leak_universe(predicate.kind());
let trait_ref = match predicate_kind {
ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr)) => tr.trait_ref,
ty::PredicateKind::Clause(ty::ClauseKind::Projection(proj))
if matches!(
infcx.tcx.def_kind(proj.projection_term.def_id),
DefKind::AssocTy | DefKind::AssocConst
Expand Down
2 changes: 0 additions & 2 deletions compiler/rustc_type_ir/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,6 @@ pub enum GoalSource {
///
/// FIXME(-Znext-solver=coinductive): Are these even coinductive?
AliasBoundConstCondition,
/// Instantiating a higher-ranked goal and re-proving it.
InstantiateHigherRanked,
/// Predicate required for an alias projection to be well-formed.
/// This is used in two places: projecting to an opaque whose hidden type
/// is already registered in the opaque type storage, and for rigid projections.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ LL | impl<T> Trait for Box<T> {}
| ^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `Box<_>`
|
= note: downstream crates may implement trait `WithAssoc<'a>` for type `std::boxed::Box<_>`
= note: downstream crates may implement trait `WhereBound` for type `std::boxed::Box<_>`
= note: downstream crates may implement trait `WhereBound` for type `std::boxed::Box<<std::boxed::Box<_> as WithAssoc<'a>>::Assoc>`

error: aborting due to 1 previous error

Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//@ revisions: old next
//@[next] compile-flags: -Znext-solver
//@[old] check-pass
//@ check-pass

// cc #119820

Expand All @@ -25,7 +25,6 @@ where
// the leak check both candidates may apply and we prefer the
// `param_env` candidate in winnowing.
hr_bound::<&T>();
//[next]~^ ERROR the trait bound `for<'a> &'a &T: Trait` is not satisfied
}

fn main() {}

This file was deleted.

Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//@ revisions: current next
//@[next] compile-flags: -Znext-solver
//@[current] check-pass
//@ check-pass

// cc #119820

Expand All @@ -13,7 +13,6 @@ fn impl_hr<'b, T: for<'a> Trait<'a, 'b>>() {}

fn not_hr<'a, T: for<'b> Trait<'a, 'b> + OtherTrait<'static>>() {
impl_hr::<T>();
//[next]~^ ERROR the trait bound `for<'a> T: Trait<'a, '_>` is not satisfied
}

fn main() {}
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
error[E0308]: mismatched types
--> $DIR/candidate-from-env-universe-err-project.rs:38:5
--> $DIR/candidate-from-env-universe-err-project.rs:37:5
|
LL | projection_bound::<T>();
| ^^^^^^^^^^^^^^^^^^^^^^^ one type is more general than the other
Expand All @@ -13,7 +13,7 @@ LL | fn projection_bound<T: for<'a> Trait<'a, Assoc = usize>>() {}
| ^^^^^^^^^^^^^

error[E0308]: mismatched types
--> $DIR/candidate-from-env-universe-err-project.rs:53:30
--> $DIR/candidate-from-env-universe-err-project.rs:51:30
|
LL | let _higher_ranked_norm: for<'a> fn(<T as Trait<'a>>::Assoc) = |_| ();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ one type is more general than the other
Expand All @@ -22,7 +22,7 @@ LL | let _higher_ranked_norm: for<'a> fn(<T as Trait<'a>>::Assoc) = |_| ();
found associated type `<T as Trait<'a>>::Assoc`

error[E0308]: mismatched types
--> $DIR/candidate-from-env-universe-err-project.rs:53:30
--> $DIR/candidate-from-env-universe-err-project.rs:51:30
|
LL | let _higher_ranked_norm: for<'a> fn(<T as Trait<'a>>::Assoc) = |_| ();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ one type is more general than the other
Expand Down
Original file line number Diff line number Diff line change
@@ -1,29 +1,5 @@
error[E0277]: the trait bound `for<'a> T: Trait<'a>` is not satisfied
--> $DIR/candidate-from-env-universe-err-project.rs:28:19
|
LL | trait_bound::<T>();
| ^ the trait `for<'a> Trait<'a>` is not implemented for `T`
|
note: required by a bound in `trait_bound`
--> $DIR/candidate-from-env-universe-err-project.rs:17:19
|
LL | fn trait_bound<T: for<'a> Trait<'a>>() {}
| ^^^^^^^^^^^^^^^^^ required by this bound in `trait_bound`

error[E0277]: the trait bound `for<'a> T: Trait<'a>` is not satisfied
--> $DIR/candidate-from-env-universe-err-project.rs:38:24
|
LL | projection_bound::<T>();
| ^ the trait `for<'a> Trait<'a>` is not implemented for `T`
|
note: required by a bound in `projection_bound`
--> $DIR/candidate-from-env-universe-err-project.rs:18:24
|
LL | fn projection_bound<T: for<'a> Trait<'a, Assoc = usize>>() {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `projection_bound`

error[E0271]: type mismatch resolving `<T as Trait<'a>>::Assoc == usize`
--> $DIR/candidate-from-env-universe-err-project.rs:38:24
--> $DIR/candidate-from-env-universe-err-project.rs:37:24
|
LL | projection_bound::<T>();
| ^ type mismatch resolving `<T as Trait<'a>>::Assoc == usize`
Expand All @@ -40,20 +16,19 @@ LL | fn projection_bound<T: for<'a> Trait<'a, Assoc = usize>>() {}
| ^^^^^^^^^^^^^ required by this bound in `projection_bound`

error: higher-ranked subtype error
--> $DIR/candidate-from-env-universe-err-project.rs:53:30
--> $DIR/candidate-from-env-universe-err-project.rs:51:30
|
LL | let _higher_ranked_norm: for<'a> fn(<T as Trait<'a>>::Assoc) = |_| ();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: higher-ranked subtype error
--> $DIR/candidate-from-env-universe-err-project.rs:53:30
--> $DIR/candidate-from-env-universe-err-project.rs:51:30
|
LL | let _higher_ranked_norm: for<'a> fn(<T as Trait<'a>>::Assoc) = |_| ();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: duplicate diagnostic emitted due to `-Z deduplicate-diagnostics=no`

error: aborting due to 5 previous errors
error: aborting due to 3 previous errors

Some errors have detailed explanations: E0271, E0277.
For more information about an error, try `rustc --explain E0271`.
For more information about this error, try `rustc --explain E0271`.
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,12 @@ fn projection_bound<T: for<'a> Trait<'a, Assoc = usize>>() {}
// We use a function with a trivial where-bound which is more
// restrictive than the impl.
fn function1<T: Trait<'static>>() {
// err
// ok
//
// Proving `for<'a> T: Trait<'a>` using the where-bound does not
// result in a leak check failure even though it does not apply.
// We prefer env candidates over impl candidatescausing this to succeed.
trait_bound::<T>();
//[next]~^ ERROR the trait bound `for<'a> T: Trait<'a>` is not satisfied
}

fn function2<T: Trait<'static, Assoc = usize>>() {
Expand All @@ -37,8 +36,7 @@ fn function2<T: Trait<'static, Assoc = usize>>() {
// to prefer it over the impl, resulting in a placeholder error.
projection_bound::<T>();
//[next]~^ ERROR type mismatch resolving `<T as Trait<'a>>::Assoc == usize`
//[next]~| ERROR the trait bound `for<'a> T: Trait<'a>` is not satisfied
//[current]~^^^ ERROR mismatched types
//[current]~^^ ERROR mismatched types
}

fn function3<T: Trait<'static, Assoc = usize>>() {
Expand Down

This file was deleted.

Loading
Loading