[DRAFT] Make alias bounds sound in the new solver#110628
Closed
compiler-errors wants to merge 4 commits intorust-lang:masterfrom
Closed
[DRAFT] Make alias bounds sound in the new solver#110628compiler-errors wants to merge 4 commits intorust-lang:masterfrom
compiler-errors wants to merge 4 commits intorust-lang:masterfrom
Conversation
rustbot
added
S-waiting-on-review
compiler-errors
commented
Apr 20, 2023
| // since they're not implied by the well-formedness of the object type. | ||
| fn consider_object_bound_candidate( | ||
| // since they're not implied by the well-formedness of anything necessarily. | ||
| fn consider_non_wf_assumption( |
Contributor
Author
There was a problem hiding this comment.
This is a version of consider_implied_clause that registers all of the bounds relevant to a trait, namely its supertraits and item bounds. I assume we'll be using this in all of the built-in impls and for user impls too (or something like it).
Naming bikeshed I guess.
| } | ||
|
|
||
| #[instrument(level = "debug", skip(self), ret)] | ||
| pub(super) fn evaluate_alias_bound_self_is_well_formed<G: GoalKind<'tcx>>( |
Contributor
Author
There was a problem hiding this comment.
This is the logic we had discussed before, essentially that an alias bound only holds if the trait ref of the alias is satisfied via a param-env candidate.
Comment on lines
+641
to
+654
| // FIXME: Bad bad bad bad bad !!!!! | ||
| let lang_items = self.tcx().lang_items(); | ||
| let trait_def_id = projection_trait_ref.def_id; | ||
| let funky_built_in_res = if lang_items.pointee_trait() == Some(trait_def_id) { | ||
| G::consider_builtin_pointee_candidate(self, goal) | ||
| } else if lang_items.discriminant_kind_trait() == Some(trait_def_id) { | ||
| G::consider_builtin_discriminant_kind_candidate(self, goal) | ||
| } else { | ||
| Err(NoSolution) | ||
| }; | ||
| if let Ok(result) = funky_built_in_res { | ||
| param_env_candidates | ||
| .push(Candidate { source: CandidateSource::BuiltinImpl, result }); | ||
| } |
Contributor
Author
There was a problem hiding this comment.
Comment on lines
+525
to
+526
| // Always coinductive in the new solver. | ||
| _ if tcx.trait_solver_next() => true, |
Contributor
Author
There was a problem hiding this comment.
| @@ -0,0 +1,18 @@ | |||
| error[E0275]: overflow evaluating the requirement `for<'a> dyn for<'a> Trait<'a, for<'a> Item = ()>: Trait<'a>` | |||
Contributor
Author
There was a problem hiding this comment.
This goal causes one of those infinite runaways of placeholders in increasingly higher universes, like we see with WF goals currently.
compiler-errors
commented
Apr 20, 2023
| // Can't come up with an example yet, though, and the worst case | ||
| // we can have is a compiler stack overflow... | ||
| self.assemble_param_env_candidates(trait_goal, &mut param_env_candidates); | ||
| self.assemble_alias_bound_candidates(trait_goal, &mut param_env_candidates); |
Contributor
Author
There was a problem hiding this comment.
We need to consider nested alias bounds here I think - https://hackmd.io/frHMYxD5S4-rWlxkx_eWNw#3-Nested-alias-bound-candidates
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this pull request
May 10, 2023
…lcnr Make alias bounds sound in the new solver (take 2) Make alias bounds sound in the new solver (in a way that does not require coinduction) by only considering them for projection types whose corresponding trait refs come from a param-env candidate. That is, given `<T as Trait>::Assoc: Bound`, we only *really* need to consider the alias bound if `T: Trait` is satisfied via a param-env candidate. If it's instead satisfied, e.g., via an user provided impl candidate or a , then that impl should have a concrete type to which we could otherwise normalize `<T as Trait>::Assoc`, and that concrete type is then responsible to prove the `Bound` on it. Similar consideration is given to opaque types, since we only need to consider alias bounds if we're *not* in reveal-all mode, since similarly we'd be able to reveal the opaque types and prove any bounds that way. This does not remove that hacky "eager projection replacement" logic from object bounds, which are somewhat like alias bounds. But removing this eager normalization behavior (added in rust-lang#108333) would require full coinduction to be enabled. Compare to rust-lang#110628, which does remove this object-bound custom logic but requires coinduction to be sound. r? `@lcnr`
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
r? @ghost
This is not complete (nor is it sound yet, nor is it necessarily ready to even consider yet). Putting this up for self-review with inline comments and discussion with @lcnr mostly.