-
-
Notifications
You must be signed in to change notification settings - Fork 14.7k
Remove the NormalizesTo/Projection split
#154108
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
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -97,13 +97,19 @@ pub(super) fn instantiate_and_apply_query_response<D, I>( | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original_values: &[I::GenericArg], | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| response: CanonicalResponse<I>, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| span: I::Span, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| prev_universe: ty::UniverseIndex, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) -> (NestedNormalizationGoals<I>, Certainty) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| where | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| D: SolverDelegate<Interner = I>, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| I: Interner, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| { | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let instantiation = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| compute_query_response_instantiation_values(delegate, &original_values, &response, span); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let instantiation = compute_query_response_instantiation_values( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| delegate, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| &original_values, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| &response, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| span, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| prev_universe, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let Response { var_values, external_constraints, certainty } = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| delegate.instantiate_canonical(response, instantiation); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
@@ -127,6 +133,7 @@ fn compute_query_response_instantiation_values<D, I, T>( | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| original_values: &[I::GenericArg], | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| response: &Canonical<I, T>, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| span: I::Span, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| prev_universe: ty::UniverseIndex, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ) -> CanonicalVarValues<I> | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| where | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| D: SolverDelegate<Interner = I>, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
@@ -136,7 +143,6 @@ where | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| // FIXME: Longterm canonical queries should deal with all placeholders | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| // created inside of the query directly instead of returning them to the | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| // caller. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let prev_universe = delegate.universe(); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The change here is
Currently, we don't instantiate the canonicalized response within the very same query, but as per rust-lang/trait-system-refactor-initiative#223 (comment) (5. the root of the Projection goal then instantiates this query result inside of the same query using the var_values with the added entry for the new infer var) we should do. In such cases, the current instantiation is not so idempotent modulo universes. Suppose that the current query's rust/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs Lines 564 to 567 in 1f7f8ea
rust/compiler/rustc_next_trait_solver/src/canonical/mod.rs Lines 139 to 143 in 1f7f8ea
And we have some max universe Suppose that we have a region var with universe rust/compiler/rustc_next_trait_solver/src/canonical/mod.rs Lines 187 to 194 in 1f7f8ea
Then when we finally finishing the query, we canonicalize it as a response, but since our rust/compiler/rustc_next_trait_solver/src/canonical/canonicalizer.rs Lines 458 to 468 in 1f7f8ea
rust/compiler/rustc_next_trait_solver/src/canonical/canonicalizer.rs Lines 300 to 313 in 1f7f8ea
the resulting universe of that region becomes This might result into a leak check failure or other higher-kinded error. So, we should either do use
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. i agree, annoying issue. I think we shouldn't canonicalize an input while inside of a binder, so not immediately clear how to handle higher-kinded
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah, I'll think about the proper fix 😅 |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let universes_created_in_query = response.max_universe.index(); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| for _ in 0..universes_created_in_query { | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| delegate.create_next_universe(); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
@@ -328,8 +334,13 @@ where | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| .map(|&arg| delegate.fresh_var_for_kind_with_span(arg, span)), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let instantiation = | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| compute_query_response_instantiation_values(delegate, orig_values, &state, span); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let instantiation = compute_query_response_instantiation_values( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| delegate, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| orig_values, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| &state, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| span, | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| delegate.universe(), | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let inspect::State { var_values, data } = delegate.instantiate_canonical(state, instantiation); | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -40,7 +40,7 @@ mod probe; | |
| /// This has effects on cycle handling handling and on how we compute | ||
| /// query responses, see the variant descriptions for more info. | ||
| #[derive(Debug, Copy, Clone)] | ||
| enum CurrentGoalKind { | ||
| pub(super) enum CurrentGoalKind { | ||
| Misc, | ||
| /// We're proving an trait goal for a coinductive trait, either an auto trait or `Sized`. | ||
| /// | ||
|
|
@@ -93,15 +93,15 @@ where | |
| /// If some `InferCtxt` method is missing, please first think defensively about | ||
| /// the method's compatibility with this solver, or if an existing one does | ||
| /// the job already. | ||
| delegate: &'a D, | ||
| pub(super) delegate: &'a D, | ||
|
|
||
| /// The variable info for the `var_values`, only used to make an ambiguous response | ||
| /// with no constraints. | ||
| var_kinds: I::CanonicalVarKinds, | ||
| pub(super) var_kinds: I::CanonicalVarKinds, | ||
|
|
||
| /// What kind of goal we're currently computing, see the enum definition | ||
| /// for more info. | ||
| current_goal_kind: CurrentGoalKind, | ||
| pub(super) current_goal_kind: CurrentGoalKind, | ||
| pub(super) var_values: CanonicalVarValues<I>, | ||
|
|
||
| /// The highest universe index nameable by the caller. | ||
|
|
@@ -486,6 +486,7 @@ where | |
| &orig_values, | ||
| response, | ||
| self.origin_span, | ||
| self.delegate.universe(), | ||
| ); | ||
|
|
||
| // FIXME: We previously had an assert here that checked that recomputing | ||
|
|
@@ -564,7 +565,7 @@ where | |
| pub(super) fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> { | ||
| let Goal { param_env, predicate } = goal; | ||
| let kind = predicate.kind(); | ||
| self.enter_forall(kind, |ecx, kind| match kind { | ||
| let resp = 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) | ||
| } | ||
|
|
@@ -604,16 +605,18 @@ where | |
| 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::NormalizesTo(_) => { | ||
| unreachable!() | ||
| } | ||
| 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) | ||
| } | ||
| }) | ||
| })?; | ||
| debug_assert!(resp.value.external_constraints.normalization_nested_goals.is_empty()); | ||
|
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
| Ok(resp) | ||
| } | ||
|
|
||
| // Recursively evaluates all the goals added to this `EvalCtxt` to completion, returning | ||
|
|
@@ -806,6 +809,7 @@ where | |
| /// | ||
| /// This is the case if the `term` does not occur in any other part of the predicate | ||
| /// and is able to name all other placeholder and inference variables. | ||
| #[allow(unused)] | ||
| #[instrument(level = "trace", skip(self), ret)] | ||
| pub(super) fn term_is_fully_unconstrained(&self, goal: Goal<I, ty::NormalizesTo<I>>) -> bool { | ||
| let universe_of_term = match goal.predicate.term.kind() { | ||
|
|
@@ -832,6 +836,7 @@ where | |
| cache: HashSet<I::Ty>, | ||
| } | ||
|
|
||
| #[allow(unused)] | ||
| impl<D: SolverDelegate<Interner = I>, I: Interner> ContainsTermOrNotNameable<'_, D, I> { | ||
| fn check_nameable(&self, universe: ty::UniverseIndex) -> ControlFlow<()> { | ||
| if self.universe_of_term.can_name(universe) { | ||
|
|
@@ -1423,16 +1428,15 @@ where | |
|
|
||
| fn fold_ty(&mut self, ty: I::Ty) -> I::Ty { | ||
| match ty.kind() { | ||
| ty::Alias(..) if !ty.has_escaping_bound_vars() => { | ||
| ty::Alias(_, alias) if !ty.has_escaping_bound_vars() => { | ||
| let infer_ty = self.ecx.next_ty_infer(); | ||
| let normalizes_to = ty::PredicateKind::AliasRelate( | ||
| ty.into(), | ||
| infer_ty.into(), | ||
| ty::AliasRelationDirection::Equate, | ||
| ); | ||
| let projection = ty::ClauseKind::Projection(ty::ProjectionPredicate { | ||
| projection_term: alias.into(), | ||
| term: infer_ty.into(), | ||
| }); | ||
| self.ecx.add_goal( | ||
| self.normalization_goal_source, | ||
| Goal::new(self.cx(), self.param_env, normalizes_to), | ||
| Goal::new(self.cx(), self.param_env, projection), | ||
| ); | ||
| infer_ty | ||
| } | ||
|
|
@@ -1452,16 +1456,15 @@ where | |
|
|
||
| fn fold_const(&mut self, ct: I::Const) -> I::Const { | ||
| match ct.kind() { | ||
| ty::ConstKind::Unevaluated(..) if !ct.has_escaping_bound_vars() => { | ||
| ty::ConstKind::Unevaluated(uc) if !ct.has_escaping_bound_vars() => { | ||
| let infer_ct = self.ecx.next_const_infer(); | ||
| let normalizes_to = ty::PredicateKind::AliasRelate( | ||
| ct.into(), | ||
| infer_ct.into(), | ||
| ty::AliasRelationDirection::Equate, | ||
| ); | ||
| let projection = ty::ClauseKind::Projection(ty::ProjectionPredicate { | ||
| projection_term: uc.into(), | ||
| term: infer_ct.into(), | ||
| }); | ||
| self.ecx.add_goal( | ||
| self.normalization_goal_source, | ||
| Goal::new(self.cx(), self.param_env, normalizes_to), | ||
| Goal::new(self.cx(), self.param_env, projection), | ||
| ); | ||
| infer_ct | ||
| } | ||
|
|
@@ -1528,6 +1531,7 @@ pub(super) fn evaluate_root_goal_for_proof_tree<D: SolverDelegate<Interner = I>, | |
| &proof_tree.orig_values, | ||
| response, | ||
| origin_span, | ||
| delegate.universe(), | ||
| ); | ||
|
|
||
| (Ok(normalization_nested_goals), proof_tree) | ||
|
|
||
This file was deleted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As the
NormalizesTois going to be replaced byProjection, this function can be called upon some non-projection aliasesThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
an exhaustive match please (and comment)