Skip to content

Use the new solver in the impossible_predicates #136988

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.

Sign up for GitHub

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+43 −9
Open

Use the new solver in the impossible_predicates #136988

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 5 additions & 9 deletions compiler/rustc_trait_selection/src/traits/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -690,8 +690,11 @@ fn replace_param_and_infer_args_with_placeholder<'tcx>(
/// used during analysis.
pub fn impossible_predicates<'tcx>(tcx: TyCtxt<'tcx>, predicates: Vec<ty::Clause<'tcx>>) -> bool {
debug!("impossible_predicates(predicates={:?})", predicates);
let (infcx, param_env) =
tcx.infer_ctxt().build_with_typing_env(ty::TypingEnv::fully_monomorphized());
let (infcx, param_env) = tcx
.infer_ctxt()
.with_next_trait_solver(true)
.build_with_typing_env(ty::TypingEnv::fully_monomorphized());
Comment on lines +693 to +696
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It feels kind of weird to be using the new trait solver "because its more complete" while also using a typing mode that is allowed to be incomplete (unlike coherence mode). I guess it is also true that the not-required-to-be-complete solver modes in the new solver should less incomplete than the not-required-to-be-complete-solver-modes in the old solver. So still a good change and it being weird is kind of pre-existing.

Do we expect the trait solver to always be complete even outside of coherence in some specific circumstances? What are those circumstances?

Copy link
Contributor

@lcnr lcnr May 7, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we expect the trait solver to always be complete even outside of coherence in some specific circumstances? What are those circumstances?

I think the following is required in all TypingMode

  • goal holds without infer vars in a generic context -> goal holds in an empty env after instantiating this context (otherwise we'd have to recheck all goals during monomorphization)
  • goal holds with infer vars, constraining the infer vars to some concrete type also means the goal holds (otherwise we'd need to keep goals around until they have no infer vars, even if they hold. This would result in a MIR typeck ICE if it goes wrong)

So we'd have "for<T: Clone> Foo<T>: Clone implies Foo<u32>: Clone" and "Foo<?x>: Clone implies Foo<Vec<u32>>: Clone".

I am not totally sure whether Foo<?x>: Clone implies Foo<Vec<?x>>: Clone and think that not doing so wouldn't be unsound, just questionable.


let ocx = ObligationCtxt::new(&infcx);
let predicates = ocx.normalize(&ObligationCause::dummy(), param_env, predicates);
for predicate in predicates {
Expand All @@ -704,13 +707,6 @@ pub fn impossible_predicates<'tcx>(tcx: TyCtxt<'tcx>, predicates: Vec<ty::Clause
return true;
}

// Leak check for any higher-ranked trait mismatches.
// We only need to do this in the old solver, since the new solver already
// leak-checks.
if !infcx.next_trait_solver() && infcx.leak_check(ty::UniverseIndex::ROOT, None).is_err() {
return true;
}

false
}

Expand Down
38 changes: 38 additions & 0 deletions tests/ui/traits/vtable/impossible-method.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
//@ run-pass
//@ revisions: current next
//@ ignore-compare-mode-next-solver (explicit revisions)
//@[next] compile-flags: -Znext-solver

trait Id {
type This<'a>;
}
impl<T> Id for T {
type This<'a> = T;
}

trait Trait<T> {}
impl<T: Id> Trait<for<'a> fn(T::This<'a>)> for T {}

trait Method<T: Id> {
fn call_me(&self)
where
T: Trait<for<'a> fn(T::This<'a>)>;
}

impl<T, U> Method<U> for T {
fn call_me(&self) {
println!("method was reachable");
}
}

fn generic<T: Id>(x: &dyn Method<T>) {
// Proving `T: Trait<for<'a> fn(T::This<'a>)>` holds.
x.call_me();
}

fn main() {
// Proving `u32: Trait<fn(u32)>` fails due to incompleteness.
// We don't add the method to the vtable of `dyn Method`, so
// calling it causes UB.
generic::<u32>(&());
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • goal: u32: Trait<fn(u32)>
  • impl candidate: ?t: Trait<for<'a> fn(<?t as Id>::This<'a>)>
  • doesn't apply in old solver as u32 eq <?t as Id>::This<'a> doesn't hold because we treat all aliases as rigid, and, its an ambig alias that cant be normalized to infer because escaping bound vars?
  • applies in new solver because we emit a <?t as Id>::This<'!a_u1> alias-relate u32 goal which can succeed once we infer ?t=u32?

Is that the right understanding of what's going on here? And then its just generally unsound for checking impossible preds to consider preds to be impossible if they actually aren't.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Correct.

In other words, the impossible preds query needs to be complete b/c we use "this goal is impossible to satisfy" responses to skip monomorphizing items with bad where clauses in codegen. Here in vtable, but also as monomorphization roots, etc.

}
Loading