diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 36f4957fc2..49caabfdd8 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -98,6 +98,7 @@
     - [Subtyping and variance](subtyping.md)
     - [Trait and lifetime bounds](trait-bounds.md)
     - [Type coercions](type-coercions.md)
+    - [Divergence](divergence.md)
     - [Destructors](destructors.md)
     - [Lifetime elision](lifetime-elision.md)
 
diff --git a/src/divergence.md b/src/divergence.md
new file mode 100644
index 0000000000..5e25d6d0d9
--- /dev/null
+++ b/src/divergence.md
@@ -0,0 +1,95 @@
+r[divergence]
+# Divergence
+
+r[divergence.intro]
+A *diverging expression* is an expression that never completes normal execution.
+
+```rust
+fn diverges() -> ! {
+    panic!("This function never returns!");
+}
+
+fn example() {
+    let x: i32 = diverges(); // This line never completes.
+    println!("This is never printed: {x}");
+}
+```
+
+See the following rules for specific expression divergence behavior:
+
+- [expr.block.diverging] --- Block expressions.
+- [expr.if.diverging] --- `if` expressions.
+- [expr.loop.block-labels.type] --- Labeled block expressions with `break`.
+- [expr.loop.break-value.diverging] --- `loop` expressions with `break`.
+- [expr.loop.break.diverging] --- `break` expressions.
+- [expr.loop.continue.diverging] --- `continue` expressions.
+- [expr.loop.infinite.diverging] --- Infinite `loop` expressions.
+- [expr.match.diverging] --- `match` expressions.
+- [expr.match.empty] --- Empty `match` expressions.
+- [expr.return.diverging] --- `return` expressions.
+- [type.never.constraint] --- Function calls returning `!`.
+
+> [!NOTE]
+> The [`panic!`] macro and related panic-generating macros like [`unreachable!`] also have the type [`!`] and are diverging.
+
+r[divergence.never]
+Any expression of type [`!`] is a diverging expression. However, diverging expressions are not limited to type [`!`]; expressions of other types may also diverge (e.g., `Some(loop {})` has type `Option<!>`).
+
+> [!NOTE]
+> Though `!` is considered an uninhabited type, a type being uninhabited is not sufficient for it to diverge.
+>
+> ```rust,compile_fail,E0308
+> enum Empty {}
+> fn make_never() -> ! {loop{}}
+> fn make_empty() -> Empty {loop{}}
+>
+> fn diverging() -> ! {
+>     // This has a type of `!`.
+>     // So, the entire function is considered diverging.
+>     make_never();
+>     // OK: The type of the body is `!` which matches the return type.
+> }
+> fn not_diverging() -> ! {
+>     // This type is uninhabited.
+>     // However, the entire function is not considered diverging.
+>     make_empty();
+>     // ERROR: The type of the body is `()` but expected type `!`.
+> }
+> ```
+
+> [!NOTE]
+> Divergence can propagate to the surrounding block. See [expr.block.diverging].
+
+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,
+> };
+> ```
+
+> [!EDITION-2024]
+> Before the 2024 edition, the type was inferred to instead be `()`.
+
+> [!NOTE]
+> Importantly, type unification may happen *structurally*, so the fallback `!` may be part of a larger type. The following compiles:
+>
+> ```rust
+> fn foo() -> i32 { 22 }
+> // This has the type `Option<!>`, not `!`
+> match foo() {
+>     4 => Default::default(),
+>     _ => Some(return),
+> };
+> ```
+
+<!-- TODO: This last point should likely should be moved to a more general "type inference" section discussing generalization + unification. -->
+
+[`!`]: type.never
diff --git a/src/expressions/block-expr.md b/src/expressions/block-expr.md
index e8f602af0c..ef5fbe1c32 100644
--- a/src/expressions/block-expr.md
+++ b/src/expressions/block-expr.md
@@ -43,7 +43,7 @@ r[expr.block.result]
 Then the final operand is executed, if given.
 
 r[expr.block.type]
-The type of a block is the type of the final operand, or `()` if the final operand is omitted.
+The type of a block is the type of its final operand; if that operand is omitted, the type is the [unit type], unless the block [diverges][expr.block.diverging], in which case it is the [never type].
 
 ```rust
 # fn fn_call() {}
@@ -62,6 +62,64 @@ assert_eq!(5, five);
 > [!NOTE]
 > As a control flow expression, if a block expression is the outer expression of an expression statement, the expected type is `()` unless it is followed immediately by a semicolon.
 
+r[expr.block.diverging]
+A block is considered to be [diverging][divergence] if all reachable control flow paths contain a diverging expression, unless that expression is a [place expression] that is not read from.
+
+```rust,no_run
+# #![ feature(never_type) ]
+fn no_control_flow() -> ! {
+    // There are no conditional statements, so this entire function body is diverging.
+    loop {}
+}
+
+fn control_flow_diverging() -> ! {
+    // All paths are diverging, so this entire function body is diverging.
+    if true {
+        loop {}
+    } else {
+        loop {}
+    }
+}
+
+fn control_flow_not_diverging() -> () {
+    // Some paths are not diverging, so this entire block is not diverging.
+    if true {
+        ()
+    } else {
+        loop {}
+    }
+}
+
+// Note: This makes use of the unstable never type which is only available on
+// Rust's nightly channel. This is done for illustration purposes. It is
+// possible to encounter this scenario in stable Rust, but requires a more
+// convoluted example.
+struct Foo {
+    x: !,
+}
+
+fn make<T>() -> T { loop {} }
+
+fn diverging_place_read() -> ! {
+    let foo = Foo { x: make() };
+    // A read of a place expression produces a diverging block.
+    let _x = foo.x;
+}
+```
+
+```rust,compile_fail,E0308
+# #![ feature(never_type) ]
+# fn make<T>() -> T { loop {} }
+# struct Foo {
+#     x: !,
+# }
+fn diverging_place_not_read() -> ! {
+    let foo = Foo { x: make() };
+    // Assignment to `_` means the place is not read.
+    let _ = foo.x;
+} // ERROR: Mismatched types.
+```
+
 r[expr.block.value]
 Blocks are always [value expressions] and evaluate the last operand in value expression context.
 
@@ -279,6 +337,8 @@ fn is_unix_platform() -> bool {
 [inner attributes]: ../attributes.md
 [method]: ../items/associated-items.md#methods
 [mutable reference]: ../types/pointer.md#mutables-references-
+[never type]: type.never
+[place expression]: expr.place-value.place-memory-location
 [scopes]: ../names/scopes.md
 [shared references]: ../types/pointer.md#shared-references-
 [statement]: ../statements.md
@@ -286,6 +346,7 @@ fn is_unix_platform() -> bool {
 [struct]: struct-expr.md
 [the lint check attributes]: ../attributes/diagnostics.md#lint-check-attributes
 [tuple expressions]: tuple-expr.md
+[unit type]: type.tuple.unit
 [unsafe operations]: ../unsafety.md
 [value expressions]: ../expressions.md#place-expressions-and-value-expressions
 [Loops and other breakable expressions]: expr.loop.block-labels
diff --git a/src/expressions/if-expr.md b/src/expressions/if-expr.md
index 96772782f8..26b895dcf2 100644
--- a/src/expressions/if-expr.md
+++ b/src/expressions/if-expr.md
@@ -70,6 +70,34 @@ let y = if 12 * 15 > 150 {
 assert_eq!(y, "Bigger");
 ```
 
+r[expr.if.diverging]
+An `if` expression [diverges] if either the condition expression diverges or if all arms diverge.
+
+```rust,no_run
+fn diverging_condition() -> ! {
+    // Diverges because the condition expression diverges
+    if loop {} {
+        ()
+    } else {
+        ()
+    };
+    // The semicolon above is important: The type of the `if` expression is
+    // `()`, despite being diverging. When the final body expression is
+    // elided, the type of the body is inferred to ! because the function body
+    // diverges. Without the semicolon, the `if` would be the tail expression
+    // with type `()`, which would fail to match the return type `!`.
+}
+
+fn diverging_arms() -> ! {
+    // Diverges because all arms diverge
+    if true {
+        loop {}
+    } else {
+        loop {}
+    }
+}
+```
+
 r[expr.if.let]
 ## `if let` patterns
 
@@ -174,4 +202,5 @@ r[expr.if.edition2024]
 
 [`match` expressions]: match-expr.md
 [boolean type]: ../types/boolean.md
+[diverges]: divergence
 [scrutinee]: ../glossary.md#scrutinee
diff --git a/src/expressions/loop-expr.md b/src/expressions/loop-expr.md
index cc4100dd49..00e40ce1dd 100644
--- a/src/expressions/loop-expr.md
+++ b/src/expressions/loop-expr.md
@@ -41,7 +41,7 @@ r[expr.loop.infinite.intro]
 A `loop` expression repeats execution of its body continuously: `loop { println!("I live."); }`.
 
 r[expr.loop.infinite.diverging]
-A `loop` expression without an associated `break` expression is diverging and has type [`!`](../types/never.md).
+A `loop` expression without an associated `break` expression is [diverging] and has type [`!`].
 
 r[expr.loop.infinite.break]
 A `loop` expression containing associated [`break` expression(s)](#break-expressions) may terminate, and must have type compatible with the value of the `break` expression(s).
@@ -282,6 +282,9 @@ for x in 1..100 {
 assert_eq!(last, 12);
 ```
 
+r[expr.loop.break.diverging]
+A `break` expression is [diverging] and has a type of [`!`].
+
 r[expr.loop.break.label]
 A `break` expression is normally associated with the innermost `loop`, `for` or `while` loop enclosing the `break` expression, but a [label](#loop-labels) can be used to specify which enclosing loop is affected. Example:
 
@@ -296,6 +299,9 @@ A `break` expression is normally associated with the innermost `loop`, `for` or
 r[expr.loop.break.value]
 A `break` expression is only permitted in the body of a loop, and has one of the forms `break`, `break 'label` or ([see below](#break-and-loop-values)) `break EXPR` or `break 'label EXPR`.
 
+r[expr.loop.break-value.implicit-value]
+In a [`loop` with break expressions][expr.loop.break-value] or a [labeled block expression], a `break` without an expression is equivalent to `break ()`.
+
 r[expr.loop.block-labels]
 ## Labeled block expressions
 
@@ -332,6 +338,23 @@ let result = 'block: {
 };
 ```
 
+r[expr.loop.block-labels.type]
+The type of a labeled block expression is the [least upper bound] of all of the break operands and the final operand. If the final operand is omitted, the type of the final operand defaults to the [unit type], unless the block [diverges][expr.block.diverging], in which case it is the [never type].
+
+> [!EXAMPLE]
+> ```rust
+> fn example(condition: bool) {
+>     let s = String::from("owned");
+>
+>     let _: &str = 'block: {
+>         if condition {
+>             break 'block &s;  // &String coerced to &str via Deref
+>         }
+>         break 'block "literal";  // &'static str coerced to &str
+>     };
+> }
+> ```
+
 r[expr.loop.continue]
 ## `continue` expressions
 
@@ -343,6 +366,9 @@ ContinueExpression -> `continue` LIFETIME_OR_LABEL?
 r[expr.loop.continue.intro]
 When `continue` is encountered, the current iteration of the associated loop body is immediately terminated, returning control to the loop *head*.
 
+r[expr.loop.continue.diverging]
+A `continue` expression is [diverging] and has a type of [`!`].
+
 r[expr.loop.continue.while]
 In the case of a `while` loop, the head is the conditional operands controlling the loop.
 
@@ -375,12 +401,64 @@ let result = loop {
 assert_eq!(result, 13);
 ```
 
-r[expr.loop.break-value.loop]
-In the case a `loop` has an associated `break`, it is not considered diverging, and the `loop` must have a type compatible with each `break` expression. `break` without an expression is considered identical to `break` with expression `()`.
-
+r[expr.loop.break-value.type]
+The type of a `loop` with associated `break` expressions is the [least upper bound] of all of the break operands.
+
+> [!EXAMPLE]
+> ```rust
+> fn example(condition: bool) {
+>     let s = String::from("owned");
+>
+>     let _: &str = loop {
+>         if condition {
+>             break &s; // &String coerced to &str via Deref
+>         }
+>         break "literal"; // &'static str coerced to &str
+>     };
+> }
+> ```
+
+r[expr.loop.break-value.diverging]
+A `loop` with associated `break` expressions does not [diverge] if any of the break operands do not diverge. If all of the `break` operands diverge, then the `loop` expression also diverges.
+
+> [!EXAMPLE]
+> ```rust
+> fn diverging_loop_with_break(condition: bool) -> ! {
+>     // This loop is diverging because all `break` operands are diverging.
+>     loop {
+>         if condition {
+>             break loop {};
+>         } else {
+>             break panic!();
+>         }
+>     }
+> }
+> ```
+>
+> ```rust,compile_fail,E0308
+> fn loop_with_non_diverging_break(condition: bool) -> ! {
+>     // The type of this loop is i32 even though one of the breaks is
+>     // diverging.
+>     loop {
+>         if condition {
+>             break loop {};
+>         } else {
+>             break 123i32;
+>         }
+>     } // ERROR: expected `!`, found `i32`
+> }
+> ```
+
+[`!`]: type.never
 [`if` condition chains]: if-expr.md#chains-of-conditions
 [`if` expressions]: if-expr.md
 [`match` expression]: match-expr.md
 [boolean type]: ../types/boolean.md
+[diverge]: divergence
+[diverging]: divergence
+[labeled block expression]: expr.loop.block-labels
+[least upper bound]: coerce.least-upper-bound
+[never type]: type.never
 [scrutinee]: ../glossary.md#scrutinee
 [temporary values]: ../expressions.md#temporaries
+[unit type]: type.tuple.unit
diff --git a/src/expressions/match-expr.md b/src/expressions/match-expr.md
index 72fe7ab2ce..1ab5dc36f5 100644
--- a/src/expressions/match-expr.md
+++ b/src/expressions/match-expr.md
@@ -91,6 +91,27 @@ Every binding in each `|` separated pattern must appear in all of the patterns i
 r[expr.match.binding-restriction]
 Every binding of the same name must have the same type, and have the same binding mode.
 
+r[expr.match.type]
+The type of the overall `match` expression is the [least upper bound] of the individual match arms.
+
+r[expr.match.empty]
+If there are no match arms, then the `match` expression is [diverging] and the type is [`!`].
+
+> [!EXAMPLE]
+> ```rust
+> # fn make<T>() -> T { loop {} }
+> enum Empty {}
+>
+> fn diverging_match_no_arms() -> ! {
+>     let e: Empty = make();
+>     match e {}
+> }
+> ```
+
+
+r[expr.match.diverging]
+If either the scrutinee expression or all of the match arms diverge, then the entire `match` expression also diverges.
+
 r[expr.match.guard]
 ## Match guards
 
@@ -151,10 +172,13 @@ Outer attributes are allowed on match arms. The only attributes that have meanin
 r[expr.match.attributes.inner]
 [Inner attributes] are allowed directly after the opening brace of the match expression in the same expression contexts as [attributes on block expressions].
 
+[`!`]: type.never
 [`cfg`]: ../conditional-compilation.md
 [attributes on block expressions]: block-expr.md#attributes-on-block-expressions
 [binding mode]: ../patterns.md#binding-modes
+[diverging]: divergence
 [Inner attributes]: ../attributes.md
+[least upper bound]: coerce.least-upper-bound
 [lint check attributes]: ../attributes/diagnostics.md#lint-check-attributes
 [pattern]: ../patterns.md
 [place expression]: ../expressions.md#place-expressions-and-value-expressions
diff --git a/src/expressions/return-expr.md b/src/expressions/return-expr.md
index ee8f59d055..67569d5c5f 100644
--- a/src/expressions/return-expr.md
+++ b/src/expressions/return-expr.md
@@ -12,6 +12,9 @@ Return expressions are denoted with the keyword `return`.
 r[expr.return.behavior]
 Evaluating a `return` expression moves its argument into the designated output location for the current function call, destroys the current function activation frame, and transfers control to the caller frame.
 
+r[expr.return.diverging]
+A `return` expression is [diverging] and has a type of [`!`].
+
 An example of a `return` expression:
 
 ```rust
@@ -22,3 +25,6 @@ fn max(a: i32, b: i32) -> i32 {
     return b;
 }
 ```
+
+[`!`]: type.never
+[diverging]: divergence
diff --git a/src/type-coercions.md b/src/type-coercions.md
index ae60c3df96..227e960a23 100644
--- a/src/type-coercions.md
+++ b/src/type-coercions.md
@@ -208,6 +208,8 @@ In some contexts, the compiler must coerce together multiple types to try and fi
 + To find the common type for a series of if branches.
 + To find the common type for a series of match arms.
 + To find the common type for array elements.
++ To find the common type for a [labeled block expression] among the break operands and the final block operand.
++ To find the common type for an [`loop` expression with break expressions] among the break operands.
 + To find the type for the return type of a closure with multiple return statements.
 + To check the type for the return type of a function with multiple return statements.
 
@@ -285,5 +287,7 @@ This description is obviously informal. Making it more precise is expected to pr
 [type cast operator]: expressions/operator-expr.md#type-cast-expressions
 [`Unsize`]: std::marker::Unsize
 [`CoerceUnsized`]: std::ops::CoerceUnsized
+[labeled block expression]: expr.loop.block-labels
+[`loop` expression with break expressions]: expr.loop.break-value
 [method-call expressions]: expressions/method-call-expr.md
 [supertraits]: items/traits.md#supertraits