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.

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

Add where to borrowck_could_not_prove #107881

Closed
wants to merge 1 commit into from
Closed

Add where to borrowck_could_not_prove #107881

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
2 changes: 1 addition & 1 deletion compiler/rustc_error_messages/locales/en-US/borrowck.ftl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ borrowck_higher_ranked_lifetime_error =
higher-ranked lifetime error

borrowck_could_not_prove =
could not prove `{$predicate}`
could not prove `where {$predicate}`

borrowck_could_not_normalize =
could not normalize `{$value}`
Expand Down
4 changes: 2 additions & 2 deletions tests/ui/higher-rank-trait-bounds/issue-59311.stderr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 •
edited
Loading

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.


error: aborting due to 2 previous errors

2 changes: 1 addition & 1 deletion tests/ui/lifetimes/re-empty-in-error.stderr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: higher-ranked lifetime error
LL | foo(&10);
| ^^^^^^^^
|
= note: could not prove `for<'b> &'b (): 'a`
= note: could not prove `where for<'b> &'b (): 'a`

error: aborting due to previous error