Add a chapter on divergence

[jackh726]

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.

[traviscross]

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.

[traviscross]

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.

[traviscross]

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).

[traviscross]

As an aside, looking into this rule is what prompted me to file:

• Test of least upper bound coercion behavior triggers ICE rust#148283

[jackh726]

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.

[traviscross]

This compiles and produces an infinite loop.

Playground link

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;
        };
    };

Playground link

Is there a way to demonstrate this such that let _ = .. produces distinct compile-time or runtime behavior from let _x = ..?

[traviscross]

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.

[traviscross]

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.
});

[traviscross]

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?

[jackh726]

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?

This one nearly stumped me, because I had my mind set that this was a closure thing. But then I realized, this also fails:

let _: ! = {
    let _x = x.0;
};

The important bit to remember here is that x.0 is an inference var which does not produce divergence (only place expressions that produce types of ! do). The "expectation" value of the block (either as the block's type, or the closure's return value) does not constrain that inference variable.

[traviscross]

Makes sense, thanks. (And yes, the only purpose of the closure in the examples is to be able to ascribe the type without nightly features.)

Coincidentally, prompted by lcnr apropos of lcnr's work, I was just looking at something else today with a similar flavor:

trait Tr: Sized {
    fn abs(self) -> i32 { 0 }
}
impl Tr for i32 {}

fn main() {
    let x = -42;
    let y: i32 = x.abs();
    assert!(y != x.abs()); // Surprising, but true.
}

[traviscross]

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?

[traviscross]

@rustbot author

[rustbot]

Error: shortcut handler unexpectedly failed in this comment: failed to remove Label { name: "S-waiting-on-review" }

Please file an issue on GitHub at triagebot if there's a problem with this bot, or reach out on #triagebot on Zulip.

[traviscross]

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?