Diverging expression not detected inside a while condition

[theemathas]

I tried this code:

#![allow(unreachable_code)]
fn main() {
    let _: bool = 'a: {
        while break 'a true {}
    };
}

I expected the code to compile. Instead, I got the following compile error:

error[E0308]: mismatched types
 --> src/main.rs:4:9
  |
4 |         while break 'a true {}
  |         ^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `()`
  |
  = note: `while` loops evaluate to unit type `()`
help: consider returning a value here
  |
4 |         while break 'a true {} /* `bool` value */
  |                                ++++++++++++++++++

For more information about this error, try `rustc --explain E0308`.

Note that I can use uninitialized variables in the unreachable code, which indicates that the compiler realizes that the expression diverges. For example, this code compiles fine:

fn main() {
    let x: i32;
    let _: bool = 'a: {
        while break 'a true {}
        x += 1;
        true  // Deleting this `true` results in a type error.
    };
}

Usually, when a diverging expression appears in a block, rust no longer checks if the last expression in the block has the expected type. For example, this code compiles fine:

fn main() {
    let x: i32;
    let _: bool = 'a: {
        if break 'a true {}
        x += 1;
        // No `true` needed here
    };
}

Although, strangely enough, leaving the if as the last expression causes the code to again not compile:

fn main() {
    let _: bool = 'a: {
        if break 'a true {}
    };
}

error[E0308]: mismatched types
 --> src/main.rs:4:26
  |
4 |         if break 'a true {}
  |                          ^^ expected `bool`, found `()`

For more information about this error, try `rustc --explain E0308`.

All of this seems rather inconsistent.

This was discovered while experimenting with #118673

Meta

Reproducible on the playground with stable rust 1.87.0.

[theemathas]

To summarize

Type error:

fn main() {
    let _: bool = 'a: {
        while break 'a true {}
    };
}

Type error:

fn main() {
    let _: bool = 'a: {
        if break 'a true {}
    };
}

Type error:

fn main() {
    let _: bool = 'a: {
        while break 'a true {}
        let _ = 1;
    };
}

Compiles fine:

fn main() {
    let _: bool = 'a: {
        if break 'a true {}
        let _ = 1;
    };
}

[asquared31415]

There are several limitations with the current reachability analysis, in particular "propagating" that information upwards through loops and blocks happens rarely. Additionally changes to loop reachability can be quite subtle, as more accurate analysis may cause more things to resolve to the never type, which has several problems with fallback.