Elaborate supertraits in dyn candidates

This commit is contained in:
Michael Goulet 2024-07-18 12:08:57 -04:00
parent 6a891ec4fe
commit fa9ae7b9d3
3 changed files with 15 additions and 6 deletions

View File

@ -7,7 +7,7 @@ use rustc_type_ir::data_structures::HashMap;
use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable}; use rustc_type_ir::fold::{TypeFoldable, TypeFolder, TypeSuperFoldable};
use rustc_type_ir::inherent::*; use rustc_type_ir::inherent::*;
use rustc_type_ir::lang_items::TraitSolverLangItem; use rustc_type_ir::lang_items::TraitSolverLangItem;
use rustc_type_ir::{self as ty, Interner, Upcast as _}; use rustc_type_ir::{self as ty, elaborate, Interner, Upcast as _};
use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic}; use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
use tracing::instrument; use tracing::instrument;
@ -671,11 +671,19 @@ where
{ {
let cx = ecx.cx(); let cx = ecx.cx();
let mut requirements = vec![]; let mut requirements = vec![];
requirements.extend( // Elaborating all supertrait outlives obligations here is not soundness critical,
// since if we just used the unelaborated set, then the transitive supertraits would
// be reachable when proving the former. However, since we elaborate all supertrait
// outlives obligations when confirming impls, we would end up with a different set
// of outlives obligations here if we didn't do the same, leading to ambiguity.
// FIXME(-Znext-solver=coinductive): Adding supertraits here can be removed once we
// make impls coinductive always, since they'll always need to prove their supertraits.
requirements.extend(elaborate::elaborate(
cx,
cx.explicit_super_predicates_of(trait_ref.def_id) cx.explicit_super_predicates_of(trait_ref.def_id)
.iter_instantiated(cx, trait_ref.args) .iter_instantiated(cx, trait_ref.args)
.map(|(pred, _)| pred), .map(|(pred, _)| pred),
); ));
// FIXME(associated_const_equality): Also add associated consts to // FIXME(associated_const_equality): Also add associated consts to
// the requirements here. // the requirements here.

View File

@ -87,9 +87,9 @@ where
.map(|pred| goal.with(cx, pred)); .map(|pred| goal.with(cx, pred));
ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds); ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
// We currently elaborate all supertrait obligations from impls. This // We currently elaborate all supertrait outlives obligations from impls.
// can be removed when we actually do coinduction correctly and just // This can be removed when we actually do coinduction correctly, and prove
// register that the impl header must be WF. // all supertrait obligations unconditionally.
let goal_clause: I::Clause = goal.predicate.upcast(cx); let goal_clause: I::Clause = goal.predicate.upcast(cx);
for clause in elaborate::elaborate(cx, [goal_clause]) { for clause in elaborate::elaborate(cx, [goal_clause]) {
if matches!( if matches!(

View File

@ -2800,6 +2800,7 @@ impl<'tcx> SelectionContext<'_, 'tcx> {
}); });
} }
// Register any outlives obligations from the trait here, cc #124336.
if matches!(self.tcx().def_kind(def_id), DefKind::Impl { of_trait: true }) if matches!(self.tcx().def_kind(def_id), DefKind::Impl { of_trait: true })
&& let Some(header) = self.tcx().impl_trait_header(def_id) && let Some(header) = self.tcx().impl_trait_header(def_id)
{ {