-
Notifications
You must be signed in to change notification settings - Fork 559
Add a chapter on divergence #2067
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: master
Are you sure you want to change the base?
Add a chapter on divergence #2067
Conversation
3b0ec86 to
920cec4
Compare
920cec4 to
d020656
Compare
|
Thanks for the PR @jackh726; I can tell this was written carefully. It will be good to get more of this documented. In particular, it'll be good to have the fallback behavior documented. I'll leave some notes inline. Probably we'll want to move some things around. Adding more examples -- even beyond what I'll note specifically inline -- would be particularly good for this material. It's helpful when each rule has one or more concise and testable examples demonstrating exactly what the rule means to express. |
src/expressions/block-expr.md
Outdated
|
|
||
| r[expr.block.type] | ||
| The type of a block is the type of the final operand, or `()` if the final operand is omitted. | ||
| Typically, the type of a block is the type of the final operand, or `()` if the final operand is omitted. |
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.
Saying "typically" is a bit loose for the normative text. Perhaps it'd be better to put the diverging rule first (and to mention that such a block is of the never type) and then, in this rule, to say, "Otherwise, the type of a block is...". Or, alternatively, in this rule, to say "the type of a block is... except ...".
src/expressions/block-expr.md
Outdated
| r[expr.block.type.diverging] | ||
| A block is itself considered to be [diverging](../divergence.md) if all reachable control flow paths contain a [diverging expression](../divergence.md#r-divergence.diverging-expressions). |
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.
It'd be good to add some examples and counterexamples under this rule.
src/expressions/match-expr.md
Outdated
| > // Fails to compile because `a` has the type `Option<!>` | ||
| > // (or, `Option<()>` in edition 2021 and below) |
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.
| > // Fails to compile because `a` has the type `Option<!>` | |
| > // (or, `Option<()>` in edition 2021 and below) | |
| > // Fails to compile because `a` has the type `Option<!>`. |
Outside of edition admonitions, we only document the behavior of the current edition.
src/divergence.md
Outdated
| The following fails to compile because `!` does not implement `Debug`: | ||
| ```rust,compile_fail,E0277 | ||
| fn foo() -> i32 { 22 } | ||
| match foo() { | ||
| 4 => Default::default(), | ||
| _ => return, | ||
| }; | ||
| ``` |
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.
You mean does not implement Default, I think.
To match style, either this entire bit should be moved into an !EXAMPLE admonition or the narrative about it should be moved into a comment in the code. The error in the example should be notated with, e.g.:
// ERROR: The trait bound `!: Default` is not satisfied.(It does not need to match the compiler output; use whatever description is most concise and clear in context to the reader. If the reason is adequately described in other narrative comments, simply notating it with // ERROR. is OK.)
src/divergence.md
Outdated
| r[divergence.diverging-expressions.unconditional] | ||
| The following language constructs unconditonally produce a _diverging expression_ of the type [`!`](./types/never.md): | ||
|
|
||
| * [A call to a function returning `!`.](./types/never.md#r-type.never.constraint) | ||
| * [A `loop` expression with no corresponding break.](./expressions/loop-expr.md#r-expr.loop.infinite.diverging) | ||
| * [A `break` expression](./expressions/loop-expr.md#r-expr.loop.break.type) | ||
| * [A `continue` expression](./expressions/loop-expr.md#r-expr.loop.continue.type) | ||
| * [A `return` expression](./expressions/return-expr.md#r-expr.return.type) | ||
| * [A `match` expression with no arms](./expressions/match-expr.md#r-expr.match.type.diverging.empty) | ||
| * [A `block` expression that it itself is diverging.](./expressions/block-expr.md#r-expr.block.type.diverging) |
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.
We prefer to not duplicate normative rules, and this ends up adding a rule that duplicates the similar rules already present in the section for each expression.
Perhaps this should just be dropped. If we were to decide to keep it, it'd probably go in an admonition, in an index, etc.
src/divergence.md
Outdated
| r[divergence.diverging-expressions.conditional] | ||
| In a control flow expression, if all arms diverge, then the entire expression also diverges. |
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.
This rule should probably be inlined into each control flow expression.
| - [Subtyping and variance](subtyping.md) | ||
| - [Trait and lifetime bounds](trait-bounds.md) | ||
| - [Type coercions](type-coercions.md) | ||
| - [Divergence](divergence.md) |
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.
We try to keep the number of top-level chapters contained. Looking at it, perhaps most of what's here that can't be inlined on the pages for each expression would make sense appearing in the Expressions chapter (e.g., we talk about place and value expressions there -- the verbiage about when a place expression is diverging might make sense near that) and in the Never type chapter.
| r[expr.match.type] | ||
| The type of the overall `match` expression is the [least upper bound](../type-coercions.md#r-coerce.least-upper-bound) of the individual match arms. |
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.
If we're inlining the rule about determining the type based on the LUB for match, from https://doc.rust-lang.org/1.90.0/reference/type-coercions.html#r-coerce.least-upper-bound.intro, probably we'd need to do that for the other rules there also (and then either remove the list from there or convert it to an admonition or index).
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 an aside, looking into this rule is what prompted me to file:
|
Thanks for the review @traviscross. Good points here, I'll work on sorting through them today/tomorrow. Happy to jump on a call at some point too, if you think any of these could use further discussion. |
c99414f to
a11338f
Compare
a11338f to
a9d8264
Compare
| struct Foo { | ||
| x: !, | ||
| } | ||
|
|
||
| let foo = Foo { x: make() }; | ||
| let diverging_place_not_read: () = { | ||
| let _: () = { | ||
| // Asssignment to `_` means the place is not read | ||
| let _ = foo.x; | ||
| }; | ||
| }; |
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.
This compiles and produces an infinite loop.
But then, so does:
let foo = Foo { x: make() };
let diverging_place_not_read: () = {
let _: () = {
// Asssignment to something other than `_` means?
let _x = foo.x;
};
};Is there a way to demonstrate this such that let _ = .. produces distinct compile-time or runtime behavior from let _x = ..?
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.
To answer the question posed, this compiles:
trait RetId { type Ty; }
impl<T> RetId for fn() -> T { type Ty = T; }
struct S<T> {
x: T,
}
fn f(x: S<<fn() -> ! as RetId>::Ty>) -> ! {
let _x = x.x; // OK.
}But this does not:
fn f(x: S<<fn() -> ! as RetId>::Ty>) -> ! {
let _ = x.x; // ERROR: Mismatched types.
}This is one, though, where it's not immediately coming to mind how to express this without either the never type or the never type hack.
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.
Here's one way. (Of course, this is really just another instantiation of the never type hack.)
fn phantom_call<T>(_: impl FnOnce(T) -> T) {}
let _ = phantom_call(|x| -> ! {
let _x = x; // OK.
});
let _ = phantom_call(|x| -> ! {
let _ = x; // ERROR: Mismatched types.
});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.
It's interesting how it really does need the ! type to be ascribed for this to work. I.e., it doesn't work with:
struct W<T>(T);
let x = W(loop {});
let _ = || -> ! {
let _x = x.0; // ERROR.
};Any thoughts about the reason for that?
| # #![ feature(never_type) ] | ||
| # fn make<T>() -> T { loop {} } | ||
| let no_control_flow: ! = { | ||
| // There are no conditional statements, so this entire block is diverging. | ||
| loop {} | ||
| }; |
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.
You and I had talked about this. We had both thought, "maybe it's worth using the nightly never type to express this more clearly." I had mentioned I'd need to talk it over with @ehuss. In that discussion, @ehuss made a good point: why not just use functions? I.e., for the expression whose type we want to demonstrate, we can make that the trailing expression of a function that returns !. E.g.:
fn no_control_flow() -> ! {
loop {}
}That does seem likely the best approach. Sound right to you?
|
@rustbot author |
|
Error: Please file an issue on GitHub at triagebot if there's a problem with this bot, or reach out on #triagebot on Zulip. |
| Any expression of type [`!`](./types/never.md) is a _diverging expression_, but there are also diverging expressions which are not of type `!` (e.g. `Some(panic!())`). | ||
|
|
||
| r[divergence.fallback] | ||
| ## Fallback | ||
| If a type to be inferred is only unified with diverging expressions, then that type will be inferred to be `!`. | ||
|
|
||
| > [!EXAMPLE] | ||
| > ```rust,compile_fail,E0277 | ||
| > fn foo() -> i32 { 22 } | ||
| > match foo() { | ||
| > // ERROR: The trait bound `!: Default` is not satisfied. | ||
| > 4 => Default::default(), | ||
| > _ => return, | ||
| > }; | ||
| > ``` |
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.
It feels that we might need to say more here to guard against too simple a reading. We say, 1) not all diverging expressions have type ! (e.g. Some(panic!())), and 2) if a type to be inferred is only unified with diverging expressions, then the type will be inferred to be !.
However, of course, this does not compile:
trait Tr: Sized {
fn m() -> Self { loop {} }
}
impl<T> Tr for T {}
fn f() -> u8 { 0 }
fn g() -> ! {
match f() {
0 => Tr::m(),
// ^^^^^^^ There's a type to be inferred here.
_ => Some(panic!()),
// ^^^^^^^^^^^^^^ This is a diverging expression.
} // ERROR: Mismatched types.
}What might we be able to say to tease this apart?
It was little tricky when trying to describe diverging blocks. The compiler's implementation maintains sort of a "global state" when checking an expression and sub-expressions, which it resets on conditional things. Semantically, I think the way I worded it is much clearer than trying to match the implementation.
Happy to hear any specific feedback, Lcnr made did an initial review pass in rust-lang/project-goal-reference-expansion@4079171, so the second commit tries to address that.