diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 977ad581e2..3d426f34c9 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..5936a4fe1b
--- /dev/null
+++ b/src/divergence.md
@@ -0,0 +1,37 @@
+r[divergence]
+# Divergence
+
+r[divergence.intro]
+Divergence is the state where a particular section of code could never be encountered at runtime. Importantly, while there are certain language constructs that immediately produce a _diverging expression_ of the type [`!`](./types/never.md), divergence can also propogate to the surrounding block.
+
+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,
+> };
+> ```
+
+> [!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. -->
diff --git a/src/expressions/block-expr.md b/src/expressions/block-expr.md
index da0f93b368..7bd208bab7 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.
+Except in the case of divergence (see below), the type of a block is the type of the final operand, or `()` if the final operand is omitted.
 
 ```rust
 # fn fn_call() {}
@@ -63,6 +63,48 @@ 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.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), unless that expression is a place expression that is not read from.
+
+```rust
+# #![ feature(never_type) ]
+# fn make<T>() -> T { loop {} }
+let no_control_flow: ! = {
+    // There are no conditional statements, so this entire block is diverging.
+    loop {}
+};
+
+let control_flow_diverging: ! = {
+    // All paths are diverging, so this entire block is diverging.
+    if true {
+        loop {}
+    } else {
+        loop {}
+    }
+};
+
+let control_flow_not_diverging: () = {
+    // Some paths are not diverging, so this entire block is not diverging.
+    if true {
+        ()
+    } else {
+        loop {}
+    }
+};
+
+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;
+    };
+};
+```
+
 r[expr.block.value]
 Blocks are always [value expressions] and evaluate the last operand in value expression context.
 
diff --git a/src/expressions/if-expr.md b/src/expressions/if-expr.md
index 46636112f7..5a9658e637 100644
--- a/src/expressions/if-expr.md
+++ b/src/expressions/if-expr.md
@@ -73,6 +73,25 @@ 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
+# #![ feature(never_type) ]
+// Diverges because the condition expression diverges
+let x: ! = if { loop {}; true } {
+    ()
+} else {
+    ()
+};
+
+let x: ! = if true {
+    loop {}
+} else {
+    loop {}
+};
+```
+
 r[expr.if.let]
 ## `if let` patterns
 
diff --git a/src/expressions/loop-expr.md b/src/expressions/loop-expr.md
index 6dc669ad39..87aeb8d632 100644
--- a/src/expressions/loop-expr.md
+++ b/src/expressions/loop-expr.md
@@ -292,6 +292,8 @@ for x in 1..100 {
 assert_eq!(last, 12);
 ```
 
+Thus, the `break` expression itself is diverging and has a type of [`!`](../types/never.md).
+
 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 +357,8 @@ 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*.
 
+Thus, the `continue` expression itself has a type of [`!`](../types/never.md).
+
 r[expr.loop.continue.while]
 In the case of a `while` loop, the head is the conditional operands controlling the loop.
 
diff --git a/src/expressions/match-expr.md b/src/expressions/match-expr.md
index 5bfbbc76db..7657e7d4b2 100644
--- a/src/expressions/match-expr.md
+++ b/src/expressions/match-expr.md
@@ -96,6 +96,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](../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 [`!`](../types/never.md).
+
+r[expr.match.conditional]
+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 [`!`](../types/never.md).
+>
+>```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
 
diff --git a/src/expressions/return-expr.md b/src/expressions/return-expr.md
index ee8f59d055..d07f95f927 100644
--- a/src/expressions/return-expr.md
+++ b/src/expressions/return-expr.md
@@ -12,6 +12,8 @@ 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.
 
+Thus, a `return` expression itself has a type of [`!`](../types/never.md).
+
 An example of a `return` expression:
 
 ```rust