From 12e6a82f99db830a327899db48f4162743210947 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Fri, 16 Oct 2020 21:59:28 +0100
Subject: [PATCH 1/2] Explain pattern exhaustiveness checking

---
 src/pat-exhaustive-checking.md | 82 +++++++++++++++++++++++++++++++++-
 1 file changed, 81 insertions(+), 1 deletion(-)

diff --git a/src/pat-exhaustive-checking.md b/src/pat-exhaustive-checking.md
index b29bb1351..da4dab3bf 100644
--- a/src/pat-exhaustive-checking.md
+++ b/src/pat-exhaustive-checking.md
@@ -4,4 +4,84 @@ In Rust, pattern matching and bindings have a few very helpful properties. The
 compiler will check that bindings are irrefutable when made and that match arms
 are exhaustive.
 
-**TODO**: write this chapter.
+## Pattern usefulness
+
+The central question that usefulness checking answers is:
+"in this match expression, is that branch reachable?".
+More precisely, it boils down to computing whether,
+given a list of patterns we have already seen,
+a given new pattern might match any new value.
+
+For example, in the following match expression,
+we ask in turn whether each pattern might match something
+that wasn't matched by the patterns above it.
+Here we see the 4th pattern is redundant with the 1st;
+that branch will get an "unreachable" warning.
+The 3rd pattern may or may not be useful,
+depending on whether `Foo` has other variants than `Bar`.
+Finally, we can ask whether the whole match is exhaustive
+by asking whether the wildcard pattern (`_`)
+is useful relative to the list of all the patterns in that match.
+Here we can see that `_` is useful (it would catch `(false, None)`);
+this expression would therefore get a "non-exhaustive match" error.
+
+```rust
+// x: (bool, Option<Foo>)
+match x {
+    (true, _) => {} // 1
+    (false, Some(Foo::Bar)) => {} // 2
+    (false, Some(_)) => {} // 3
+    (true, None) => {} // 4
+}
+```
+
+Thus usefulness is used for two purposes:
+detecting unreachable code (which is useful to the user),
+and ensuring that matches are exhaustive (which is important for soundness).
+
+## Where it happens
+
+This check is done to any expression that desugars to a match expression in MIR.
+That includes actual `match` expressions,
+but also anything that looks like pattern matching,
+including `if let`, destructuring `let`, and similar expressions.
+
+```rust
+// `match`
+// Usefulness can detect unreachable branches and forbid non-exhaustive matches.
+match foo() {
+    Ok(x) => x,
+    Err(_) => panic!(),
+}
+
+// `if let`
+// Usefulness can detect unreachable branches.
+if let Some(x) = foo() {
+    // ...
+}
+
+// `while let`
+// Usefulness can detect infinite loops and dead loops.
+while let Some(x) = it.next() {
+    // ...
+}
+
+// Destructuring `let`
+// Usefulness can forbid non-exhaustive patterns.
+let Foo::Bar(x, y) = foo();
+
+// Destructuring function arguments
+// Usefulness can forbid non-exhaustive patterns.
+fn foo(Foo { x, y }: Foo) {
+    // ...
+}
+```
+
+## The algorithm
+
+Exhaustiveness checking is implemented in [check_match].
+The core of the algorithm is in [_match].
+That file contains a detailed description of the algorithm.
+
+[check_match]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/pattern/check_match/index.html
+[_match]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/pattern/_match/index.html

From 8fd457c97535d09111cd303262e1e7358cb22da3 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Fri, 16 Oct 2020 22:48:00 +0100
Subject: [PATCH 2/2] Explain why exhaustiveness is necessary for soundness

---
 src/pat-exhaustive-checking.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/pat-exhaustive-checking.md b/src/pat-exhaustive-checking.md
index da4dab3bf..767b7de50 100644
--- a/src/pat-exhaustive-checking.md
+++ b/src/pat-exhaustive-checking.md
@@ -37,7 +37,8 @@ match x {
 
 Thus usefulness is used for two purposes:
 detecting unreachable code (which is useful to the user),
-and ensuring that matches are exhaustive (which is important for soundness).
+and ensuring that matches are exhaustive (which is important for soundness,
+because a match expression can return a value).
 
 ## Where it happens