Skip to content
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

Add where to borrowck_could_not_prove #107881

Conversation

workingjubilee
Copy link
Member

This is a minute difference in an error message that generally should not be hit, but the meaning of the predicate's notation of Type: Trait is unclear when encountered in a random message, removed from surrounding Rust syntax, provoking remarks like a straight-up "What does this mean?" from people who have been programming in Rust for multiple years. We can use the where prefix, giving us where Type: Trait, which a more experienced Rust programmer is likely to recognize as using the format of a where clause and thus appropriately frame the notation of the predicate, even if the message remains fairly cryptic.

@rustbot
Copy link
Collaborator

rustbot commented Feb 10, 2023

r? @TaKO8Ki

(rustbot has picked a reviewer for you, use r? to override)

@rustbot rustbot added A-translation Area: Translation infrastructure, and migrating existing diagnostics to SessionDiagnostic S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. labels Feb 10, 2023
@rustbot
Copy link
Collaborator

rustbot commented Feb 10, 2023

rustc_error_messages was changed

cc @davidtwco, @compiler-errors, @JohnTitor, @TaKO8Ki

@workingjubilee
Copy link
Member Author

Ah yes, love you too, tidy.

@workingjubilee workingjubilee force-pushed the where-predicate-could-not-be-proven branch from c5b7142 to cb61127 Compare February 10, 2023 10:05
matthiaskrgr added a commit to matthiaskrgr/rust that referenced this pull request Feb 10, 2023
…-typos, r=compiler-errors

Cleanup typos in en_US/borrowck.ftl

Noticed these while opening rust-lang#107881.
@@ -4,15 +4,15 @@ error: higher-ranked lifetime error
LL | v.t(|| {});
| ^^^^^^^^^^
|
= note: could not prove `[closure@$DIR/issue-59311.rs:17:9: 17:11] well-formed`
= note: could not prove `where [closure@$DIR/issue-59311.rs:17:9: 17:11] well-formed`
Copy link
Member

Choose a reason for hiding this comment

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

this is strange, though more of a side-effect of us not having surface syntax for WF goals


error: higher-ranked lifetime error
--> $DIR/issue-59311.rs:17:9
|
LL | v.t(|| {});
| ^^^^^
|
= note: could not prove `for<'a> &'a V: 'static`
= note: could not prove `where for<'a> &'a V: 'static`
Copy link
Member

Choose a reason for hiding this comment

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

this doesn't seem consistent with other diagnostics that print predicates in error messages

Copy link
Member

Choose a reason for hiding this comment

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

maybe "could not prove the where-clause for<'a> ..."?

Copy link
Member Author

Choose a reason for hiding this comment

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

Well, it's a case that was, I guess, written off as too "simple" to test for here that causes the most problem, where it is a fairly down-the-line

"could not prove Type<Box<[closure@somewhere]>>: Trait<Type<Box<dyn Trait2 + Send + 'a>>"

No for<'a> required.
The real example is even longer on both sides, but otherwise what you'd expect.

The problem is that by the time you've read all the way up to the :? You've lost context here. The fact that half the predicate is just repeating the same types/traits due to it trying to describe a closure means that the : disappears into the syntactic noise.

That's why I think it's important to use where exactly, as it's the only thing that's going to force the reader's brain to even start to look for that tiny double-dot and understand what it means. They will have been trained by reading Rust code for hours upon hours upon hours to expect that very particular framing. "Hello, this is Rust syntax, please read it: where Type: Bound,".

Because what they're actually going to be dealing with is seeing, out-of-context:
Aaryusntayrust<Voyarstnday<Ayorusntu>>: Boarusntday<Aaryusntayrust<Voyarstnday<dyn Ayorusntu + 'z>>

I don't think this is enough, but the "actual fix" would be to simply rework how predicates are expressed in diagnostics (basically to the point of never surfacing them unadorned) because a little colon is not really cutting it.

Copy link
Member

Choose a reason for hiding this comment

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

Sorry, first of all I didn't mean to suggest that for<'a> was special in this error message, just didn't want to type the whole predicate.


Secondly, I guess we get away with this for regular trait errors:

error[[E0277]](https://doc.rust-lang.org/stable/error-index.html#E0277): the trait bound `i32: Foo` is not satisfied
 --> src/main.rs:6:15
  |
6 |     needs_foo(1i32);
  |     --------- ^^^^ the trait `Foo` is not implemented for `i32`

By formatting the "Aaryusntayrust<Voyarstnday<Ayorusntu>>: Boarusntday<Aaryusntayrust<Voyarstnday<dyn Ayorusntu + 'z>>" predicate verbatim in the primary message.

But later in a label, we format it like "Aaryusntayrust<Voyarstnday<Ayorusntu>> does not implement Boarusntday<Aaryusntayrust<Voyarstnday<dyn Ayorusntu + 'z>>", so it's "ok" if users don't "get it" in the primary message.


Maybe we should just special-case the presentation of trait (and projection) predicates here. Shouldn't be too hard to split them up across their : and instantiate any for<..> binders like we do for those "for all lifetimes '1" sorts of errors.

Not sure if that effort is worth it, though? "higher-ranked lifetime error"s are kinda the kitchen sink of NLL errors, and hitting them a lot suggests maybe some other error reporting path should be refactored to give a holistically better error message for them.

I'd be happy to do that quick change of special-casing the presentation of just trait/projection predicates if you don't want to.

Copy link
Member Author

@workingjubilee workingjubilee Feb 10, 2023

Choose a reason for hiding this comment

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

It's fine! I just wanted to be clear because the case that can arise isn't in the tests. Or, well, at least why it's crummy isn't shown in the tests.

Right. Reiteration and phrasing it two different ways helps a lot.

I actually agree that special-casing it is the proper solution. Yeah, it's a "kitchen sink" error, but even the worst possible error should be... acceptable? Like it's gonna be trash, but it should be okay trash.

I'd like to take a look at that refactoring actually, it just required more than "blink once" as effort.

@compiler-errors
Copy link
Member

r? @compiler-errors

feel free to ping me when you want me to review your changes.

@rustbot author

@rustbot rustbot assigned compiler-errors and unassigned TaKO8Ki Feb 16, 2023
@rustbot rustbot added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Feb 16, 2023
@bors
Copy link
Contributor

bors commented Feb 22, 2023

☔ The latest upstream changes (presumably #103042) made this pull request unmergeable. Please resolve the merge conflicts.

@Dylan-DPC
Copy link
Member

@workingjubilee any updates on this?

@workingjubilee workingjubilee marked this pull request as draft June 4, 2023 02:11
@Dylan-DPC
Copy link
Member

Closing this as inactive. Feel free to reöpen this pr or create a new pr if you get the time to work on this. Thanks

@Dylan-DPC Dylan-DPC closed this Aug 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-translation Area: Translation infrastructure, and migrating existing diagnostics to SessionDiagnostic S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants