diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index c3786707fa..3a12372927 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -97,6 +97,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..bce4cc3a69
--- /dev/null
+++ b/src/divergence.md
@@ -0,0 +1,93 @@
+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:
+
+- [type.never.constraint] --- Function calls returning `!`.
+- [expr.loop.infinite.diverging] --- Infinite `loop` expressions.
+- [expr.loop.break.diverging] --- `break` expressions.
+- [expr.loop.continue.diverging] --- `continue` expressions.
+- [expr.return.diverging] --- `return` expressions.
+- [expr.if.diverging] --- `if` expressions.
+- [expr.match.diverging] --- `match` expressions.
+- [expr.match.empty] --- Empty `match` expressions.
+- [expr.block.diverging] --- Block expressions.
+
+> [!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 a05a487c94..783c66eebe 100644
--- a/src/expressions/block-expr.md
+++ b/src/expressions/block-expr.md
@@ -44,7 +44,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() {}
@@ -63,6 +63,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.
 
@@ -292,6 +350,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
@@ -299,6 +359,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 46636112f7..65b43b29c6 100644
--- a/src/expressions/if-expr.md
+++ b/src/expressions/if-expr.md
@@ -73,6 +73,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
 
@@ -180,4 +208,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 043077e56e..3d5b9420da 100644
--- a/src/expressions/loop-expr.md
+++ b/src/expressions/loop-expr.md
@@ -42,7 +42,7 @@ 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).
@@ -292,6 +292,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.
@@ -355,6 +358,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.
 
@@ -392,9 +398,11 @@ 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 `()`.
 
+[`!`]: 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
+[diverging]: divergence
 [scrutinee]: ../glossary.md#scrutinee
 [temporary values]: ../expressions.md#temporaries
diff --git a/src/expressions/match-expr.md b/src/expressions/match-expr.md
index 5bfbbc76db..3ad873ed29 100644
--- a/src/expressions/match-expr.md
+++ b/src/expressions/match-expr.md
@@ -96,6 +96,39 @@ 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](../type-coercions.md#r-coerce.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.
+
+> [!NOTE]
+> Even if the entire `match` expression diverges, its type may not be [`!`].
+>
+>```rust,compile_fail,E0004
+>    let a = match true {
+>        true => Some(panic!()),
+>        false => None,
+>    };
+>    // Fails to compile because `a` has the type `Option<!>`.
+>    match a {}
+>```
+
 r[expr.match.guard]
 ## Match guards
 
@@ -160,9 +193,11 @@ The only attributes that have meaning on match arms are [`cfg`] and the [lint ch
 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
 [lint check attributes]: ../attributes/diagnostics.md#lint-check-attributes
 [pattern]: ../patterns.md
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