Fully rework the algorithm and its explanation

4 files changed, 782 insertions, 665 deletions

diff --git a/compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs b/compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs
index cf9a0af33ee..8c864c9f2ec 100644
--- a/compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs
+++ b/compiler/rustc_mir_build/src/thir/pattern/deconstruct_pat.rs
@@ -1,53 +1,94 @@
-//! [`super::usefulness`] explains most of what is happening in this file. As explained there,
-//! values and patterns are made from constructors applied to fields. This file defines a
-//! `Constructor` enum, a `Fields` struct, and various operations to manipulate them and convert
-//! them from/to patterns.
+//! As explained in [`super::usefulness`], values and patterns are made from constructors applied to
+//! fields. This file defines a `Constructor` enum, a `Fields` struct, and various operations to
+//! manipulate them and convert them from/to patterns.
 //!
-//! There's one idea that is not detailed in [`super::usefulness`] because the details are not
-//! needed there: _constructor splitting_.
+//! There are two important bits of core logic in this file: constructor inclusion and constructor
+//! splitting. Constructor inclusion, i.e. whether a constructor is included in/covered by another,
+//! is straightforward and defined in [`Constructor::is_covered_by`].
 //!
-//! # Constructor splitting
+//! Constructor splitting is mentioned in [`super::usefulness`] but not detailed. We describe it
+//! precisely here.
 //!
-//! The idea is as follows: given a constructor `c` and a matrix, we want to specialize in turn
-//! with all the value constructors that are covered by `c`, and compute usefulness for each.
-//! Instead of listing all those constructors (which is intractable), we group those value
-//! constructors together as much as possible. Example:
 //!
+//! # Constructor grouping and splitting
+//!
+//! As explained in the corresponding section in [`super::usefulness`], to make usefulness tractable
+//! we need to group together constructors that have the same effect when they are used to
+//! specialize the matrix.
+//!
+//! Example:
 //! ```compile_fail,E0004
 //! match (0, false) {
-//!     (0 ..=100, true) => {} // `p_1`
-//!     (50..=150, false) => {} // `p_2`
-//!     (0 ..=200, _) => {} // `q`
+//!     (0 ..=100, true) => {}
+//!     (50..=150, false) => {}
+//!     (0 ..=200, _) => {}
 //! }
 //! ```
 //!
-//! The naive approach would try all numbers in the range `0..=200`. But we can be a lot more
-//! clever: `0` and `1` for example will match the exact same rows, and return equivalent
-//! witnesses. In fact all of `0..50` would. We can thus restrict our exploration to 4
-//! constructors: `0..50`, `50..=100`, `101..=150` and `151..=200`. That is enough and infinitely
-//! more tractable.
+//! In this example we can restrict specialization to 5 cases: `0..50`, `50..=100`, `101..=150`,
+//! `151..=200` and `200..`.
+//!
+//! In [`super::usefulness`], we had said that `specialize` only takes value-only constructors. We
+//! now relax this restriction: we allow `specialize` to take constructors like `0..50` as long as
+//! we're careful to only do that with constructors that make sense. For example, `specialize(0..50,
+//! (0..=100, true))` is sensible, but `specialize(50..=200, (0..=100, true))` is not.
+//!
+//! Constructor splitting looks at the constructors in the first column of the matrix and constructs
+//! such a sensible set of constructors. Formally, we want to find a smallest disjoint set of
+//! constructors:
+//! - Whose union covers the whole type, and
+//! - That have no non-trivial intersection with any of the constructors in the column (i.e. they're
+//!     each either disjoint with or covered by any given column constructor).
+//!
+//! We compute this in two steps: first [`ConstructorSet::for_ty`] determines the set of all
+//! possible constructors for the type. Then [`ConstructorSet::split`] looks at the column of
+//! constructors and splits the set into groups accordingly. The precise invariants of
+//! [`ConstructorSet::split`] is described in [`SplitConstructorSet`].
+//!
+//! Constructor splitting has two interesting special cases: integer range splitting (see
+//! [`IntRange::split`]) and slice splitting (see [`Slice::split`]).
 //!
-//! We capture this idea in a function `split(p_1 ... p_n, c)` which returns a list of constructors
-//! `c'` covered by `c`. Given such a `c'`, we require that all value ctors `c''` covered by `c'`
-//! return an equivalent set of witnesses after specializing and computing usefulness.
-//! In the example above, witnesses for specializing by `c''` covered by `0..50` will only differ
-//! in their first element.
 //!
-//! We usually also ask that the `c'` together cover all of the original `c`. However we allow
-//! skipping some constructors as long as it doesn't change whether the resulting list of witnesses
-//! is empty of not. We use this in the wildcard `_` case.
+//! # The `Missing` constructor
+//!
+//! We detail a special case of constructor splitting that is a bit subtle. Take the following:
+//!
+//! ```
+//! enum Direction { North, South, East, West }
+//! # let wind = (Direction::North, 0u8);
+//! match wind {
+//!     (Direction::North, 50..) => {}
+//!     (_, _) => {}
+//! }
+//! ```
+//!
+//! Here we expect constructor splitting to output two cases: `North`, and "everything else". This
+//! "everything else" is represented by [`Constructor::Missing`]. Unlike other constructors, it's a
+//! bit contextual: to know the exact list of constructors it represents we have to look at the
+//! column. In practice however we don't need to, because by construction it only matches rows that
+//! have wildcards. This is how this constructor is special: the only constructor that covers it is
+//! `Wildcard`.
+//!
+//! The only place where we care about which constructors `Missing` represents is in diagnostics
+//! (see `super::usefulness::WitnessMatrix::apply_constructor`).
+//!
+//! Extra special implementation detail: in fact, in the case where all the constructors are
+//! missing, we replace `Missing` with `Wildcard` to signal this. It only makes a difference for
+//! diagnostics: for `Missing` we list the missing constructors; for `Wildcard` we only output `_`.
+//!
+//! FIXME(Nadrieril): maybe `Missing { report_all: bool }` would be less confusing.
+//!
+//! We choose whether to specialize with `Missing`/`Wildcard` in
+//! `super::usefulness::compute_exhaustiveness_and_reachability`.
+//!
 //!
-//! Splitting is implemented in the [`Constructor::split`] function. We don't do splitting for
-//! or-patterns; instead we just try the alternatives one-by-one. For details on splitting
-//! wildcards, see [`Constructor::split`]; for integer ranges, see
-//! [`IntRange::split`]; for slices, see [`Slice::split`].
 //!
 //! ## Opaque patterns
 //!
-//! Some patterns, such as TODO, cannot be inspected, which we handle with `Constructor::Opaque`.
-//! Since we know nothing of these patterns, we assume they never cover each other. In order to
-//! respect the invariants of [`SplitConstructorSet`], we give each `Opaque` constructor a unique id
-//! so we can recognize it.
+//! Some patterns, such as constants that are not allowed to be matched structurally, cannot be
+//! inspected, which we handle with `Constructor::Opaque`. Since we know nothing of these patterns,
+//! we assume they never cover each other. In order to respect the invariants of
+//! [`SplitConstructorSet`], we give each `Opaque` constructor a unique id so we can recognize it.
 
 use std::cell::Cell;
 use std::cmp::{self, max, min, Ordering};
@@ -645,8 +686,8 @@ impl OpaqueId {
 /// `Fields`.
 #[derive(Clone, Debug, PartialEq)]
 pub(super) enum Constructor<'tcx> {
-    /// The constructor for patterns that have a single constructor, like tuples, struct patterns
-    /// and fixed-length arrays.
+    /// The constructor for patterns that have a single constructor, like tuples, struct patterns,
+    /// and references. Fixed-length arrays are treated separately with `Slice`.
     Single,
     /// Enum variants.
     Variant(VariantIdx),
@@ -678,8 +719,8 @@ pub(super) enum Constructor<'tcx> {
     /// We use this for variants behind an unstable gate as well as
     /// `#[doc(hidden)]` ones.
     Hidden,
-    /// Fake extra constructor for constructors that are not seen in the matrix, as explained in the
-    /// code for [`Constructor::split`].
+    /// Fake extra constructor for constructors that are not seen in the matrix, as explained at the
+    /// top of the file.
     Missing,
 }
 
@@ -761,104 +802,12 @@ impl<'tcx> Constructor<'tcx> {
         }
     }
 
-    /// Some constructors (namely `Wildcard`, `IntRange` and `Slice`) actually stand for a set of
-    /// actual constructors (like variants, integers or fixed-sized slices). When specializing for
-    /// these constructors, we want to be specialising for the actual underlying constructors.
-    /// Naively, we would simply return the list of constructors they correspond to. We instead are
-    /// more clever: if there are constructors that we know will behave the same w.r.t. the current
-    /// matrix, we keep them grouped. For example, all slices of a sufficiently large length will
-    /// either be all useful or all non-useful with a given matrix.
-    ///
-    /// See the branches for details on how the splitting is done.
-    ///
-    /// This function may discard some irrelevant constructors if this preserves behavior. Eg. for
-    /// the `_` case, we ignore the constructors already present in the column, unless all of them
-    /// are.
-    pub(super) fn split<'a>(
-        &self,
-        pcx: &PatCtxt<'_, '_, 'tcx>,
-        ctors: impl Iterator<Item = &'a Constructor<'tcx>> + Clone,
-    ) -> SmallVec<[Self; 1]>
-    where
-        'tcx: 'a,
-    {
-        match self {
-            Wildcard => {
-                let split_set = ConstructorSet::for_ty(pcx.cx, pcx.ty).split(pcx, ctors);
-                if !split_set.missing.is_empty() {
-                    // We are splitting a wildcard in order to compute its usefulness. Some constructors are
-                    // not present in the column. The first thing we note is that specializing with any of
-                    // the missing constructors would select exactly the rows with wildcards. Moreover, they
-                    // would all return equivalent results. We can therefore group them all into a
-                    // fictitious `Missing` constructor.
-                    //
-                    // As an important optimization, this function will skip all the present constructors.
-                    // This is correct because specializing with any of the present constructors would
-                    // select a strict superset of the wildcard rows, and thus would only find witnesses
-                    // already found with the `Missing` constructor.
-                    // This does mean that diagnostics are incomplete: in
-                    // ```
-                    // match x {
-                    //   Some(true) => {}
-                    // }
-                    // ```
-                    // we report `None` as missing but not `Some(false)`.
-                    //
-                    // When all the constructors are missing we can equivalently return the `Wildcard`
-                    // constructor on its own. The difference between `Wildcard` and `Missing` will then
-                    // only be in diagnostics.
-
-                    // If some constructors are missing, we typically want to report those constructors,
-                    // e.g.:
-                    // ```
-                    //     enum Direction { N, S, E, W }
-                    //     let Direction::N = ...;
-                    // ```
-                    // we can report 3 witnesses: `S`, `E`, and `W`.
-                    //
-                    // However, if the user didn't actually specify a constructor
-                    // in this arm, e.g., in
-                    // ```
-                    //     let x: (Direction, Direction, bool) = ...;
-                    //     let (_, _, false) = x;
-                    // ```
-                    // we don't want to show all 16 possible witnesses `(<direction-1>, <direction-2>,
-                    // true)` - we are satisfied with `(_, _, true)`. So if all constructors are missing we
-                    // prefer to report just a wildcard `_`.
-                    //
-                    // The exception is: if we are at the top-level, for example in an empty match, we
-                    // usually prefer to report the full list of constructors.
-                    let all_missing = split_set.present.is_empty();
-                    let report_when_all_missing =
-                        pcx.is_top_level && !IntRange::is_integral(pcx.ty);
-                    let ctor =
-                        if all_missing && !report_when_all_missing { Wildcard } else { Missing };
-                    smallvec![ctor]
-                } else {
-                    split_set.present
-                }
-            }
-            // Fast-track if the range is trivial.
-            IntRange(this_range) if !this_range.is_singleton() => {
-                let column_ranges = ctors.filter_map(|ctor| ctor.as_int_range()).cloned();
-                this_range.split(column_ranges).map(|(_, range)| IntRange(range)).collect()
-            }
-            Slice(this_slice @ Slice { kind: VarLen(..), .. }) => {
-                let column_slices = ctors.filter_map(|c| c.as_slice());
-                this_slice.split(column_slices).map(|(_, slice)| Slice(slice)).collect()
-            }
-            // Any other constructor can be used unchanged.
-            _ => smallvec![self.clone()],
-        }
-    }
-
     /// Returns whether `self` is covered by `other`, i.e. whether `self` is a subset of `other`.
     /// For the simple cases, this is simply checking for equality. For the "grouped" constructors,
     /// this checks for inclusion.
     // We inline because this has a single call site in `Matrix::specialize_constructor`.
     #[inline]
     pub(super) fn is_covered_by<'p>(&self, pcx: &PatCtxt<'_, 'p, 'tcx>, other: &Self) -> bool {
-        // This must be kept in sync with `is_covered_by_any`.
         match (self, other) {
             // Wildcards cover anything
             (_, Wildcard) => true,
@@ -943,16 +892,20 @@ pub(super) enum ConstructorSet {
 /// `present` is morally the set of constructors present in the column, and `missing` is the set of
 /// constructors that exist in the type but are not present in the column.
 ///
-/// More formally, they respect the following constraints:
-/// - the union of `present` and `missing` covers the whole type
-/// - `present` and `missing` are disjoint
-/// - neither contains wildcards
-/// - each constructor in `present` is covered by some non-wildcard constructor in the column
-/// - together, the constructors in `present` cover all the non-wildcard constructor in the column
-/// - non-wildcards in the column do no cover anything in `missing`
-/// - constructors in `present` and `missing` are split for the column; in other words, they are
-///     either fully included in or disjoint from each constructor in the column. This avoids
-///     non-trivial intersections like between `0..10` and `5..15`.
+/// More formally, if we discard wildcards from the column, this respects the following constraints:
+/// 1. the union of `present` and `missing` covers the whole type
+/// 2. each constructor in `present` is covered by something in the column
+/// 3. no constructor in `missing` is covered by anything in the column
+/// 4. each constructor in the column is equal to the union of one or more constructors in `present`
+/// 5. `missing` does not contain empty constructors (see discussion about emptiness at the top of
+///    the file);
+/// 6. constructors in `present` and `missing` are split for the column; in other words, they are
+///    either fully included in or fully disjoint from each constructor in the column. In other
+///    words, there are no non-trivial intersections like between `0..10` and `5..15`.
+///
+/// We must be particularly careful with weird constructors like `Opaque`: they're not formally part
+/// of the `ConstructorSet` for the type, yet if we forgot to include them in `present` we would be
+/// ignoring any row with `Opaque`s in the algorithm. Hence the importance of point 4.
 #[derive(Debug)]
 pub(super) struct SplitConstructorSet<'tcx> {
     pub(super) present: SmallVec<[Constructor<'tcx>; 1]>,
@@ -960,6 +913,7 @@ pub(super) struct SplitConstructorSet<'tcx> {
 }
 
 impl ConstructorSet {
+    /// Creates a set that represents all the constructors of `ty`.
     #[instrument(level = "debug", skip(cx), ret)]
     pub(super) fn for_ty<'p, 'tcx>(cx: &MatchCheckCtxt<'p, 'tcx>, ty: Ty<'tcx>) -> Self {
         let make_range = |start, end| {
@@ -1095,9 +1049,10 @@ impl ConstructorSet {
         }
     }
 
-    /// This is the core logical operation of exhaustiveness checking. This analyzes a column a
-    /// constructors to 1/ determine which constructors of the type (if any) are missing; 2/ split
-    /// constructors to handle non-trivial intersections e.g. on ranges or slices.
+    /// This analyzes a column of constructors to 1/ determine which constructors of the type (if
+    /// any) are missing; 2/ split constructors to handle non-trivial intersections e.g. on ranges
+    /// or slices. This can get subtle; see [`SplitConstructorSet`] for details of this operation
+    /// and its invariants.
     #[instrument(level = "debug", skip(self, pcx, ctors), ret)]
     pub(super) fn split<'a, 'tcx>(
         &self,
@@ -1244,19 +1199,6 @@ impl ConstructorSet {
 
         SplitConstructorSet { present, missing }
     }
-
-    /// Compute the set of constructors missing from this column.
-    /// This is only used for reporting to the user.
-    pub(super) fn compute_missing<'a, 'tcx>(
-        &self,
-        pcx: &PatCtxt<'_, '_, 'tcx>,
-        ctors: impl Iterator<Item = &'a Constructor<'tcx>> + Clone,
-    ) -> Vec<Constructor<'tcx>>
-    where
-        'tcx: 'a,
-    {
-        self.split(pcx, ctors).missing
-    }
 }
 
 /// A value can be decomposed into a constructor applied to some fields. This struct represents
@@ -1422,6 +1364,8 @@ impl<'p, 'tcx> DeconstructedPat<'p, 'tcx> {
         DeconstructedPat { ctor, fields, ty, span, reachable: Cell::new(false) }
     }
 
+    /// Note: the input patterns must have been lowered through
+    /// `super::check_match::MatchVisitor::lower_pattern`.
     pub(crate) fn from_pat(cx: &MatchCheckCtxt<'p, 'tcx>, pat: &Pat<'tcx>) -> Self {
         let mkpat = |pat| DeconstructedPat::from_pat(cx, pat);
         let ctor;
@@ -1625,6 +1569,7 @@ impl<'p, 'tcx> DeconstructedPat<'p, 'tcx> {
     pub(super) fn is_or_pat(&self) -> bool {
         matches!(self.ctor, Or)
     }
+    /// Expand this (possibly-nested) or-pattern into its alternatives.
     pub(super) fn flatten_or_pat(&'p self) -> SmallVec<[&'p Self; 1]> {
         if self.is_or_pat() {
             self.iter_fields().flat_map(|p| p.flatten_or_pat()).collect()
@@ -1697,7 +1642,17 @@ impl<'p, 'tcx> DeconstructedPat<'p, 'tcx> {
         self.reachable.set(true)
     }
     pub(super) fn is_reachable(&self) -> bool {
-        self.reachable.get()
+        if self.reachable.get() {
+            true
+        } else if self.is_or_pat() && self.iter_fields().any(|f| f.is_reachable()) {
+            // We always expand or patterns in the matrix, so we will never see the actual
+            // or-pattern (the one with constructor `Or`) in the column. As such, it will not be
+            // marked as reachable itself, only its children will. We recover this information here.
+            self.set_reachable();
+            true
+        } else {
+            false
+        }
     }
 
     /// Report the spans of subpatterns that were not reachable, if any.
@@ -1706,7 +1661,6 @@ impl<'p, 'tcx> DeconstructedPat<'p, 'tcx> {
         self.collect_unreachable_spans(&mut spans);
         spans
     }
-
     fn collect_unreachable_spans(&self, spans: &mut Vec<Span>) {
         // We don't look at subpatterns if we already reported the whole pattern as unreachable.
         if !self.is_reachable() {
diff --git a/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs b/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs
index 65ae051c9b8..3819a6a95c2 100644
--- a/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs
+++ b/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs
@@ -1,46 +1,55 @@
-//! Note: tests specific to this file can be found in:
+//! # Match exhaustiveness and reachability algorithm
 //!
-//!   - `ui/pattern/usefulness`
-//!   - `ui/or-patterns`
-//!   - `ui/consts/const_in_pattern`
-//!   - `ui/rfc-2008-non-exhaustive`
-//!   - `ui/half-open-range-patterns`
-//!   - probably many others
+//! This file contains the logic for exhaustiveness and reachability checking for pattern-matching.
+//! Specifically, given a list of patterns in a match, we can tell whether:
+//! (a) a given pattern is reachable (reachability)
+//! (b) the patterns cover every possible value for the type (exhaustiveness)
 //!
-//! I (Nadrieril) prefer to put new tests in `ui/pattern/usefulness` unless there's a specific
-//! reason not to, for example if they depend on a particular feature like `or_patterns`.
+//! The algorithm implemented here is inspired from the one described in [this
+//! paper](http://moscova.inria.fr/~maranget/papers/warn/index.html). We have however changed it in
+//! various ways to accommodate the variety of patterns that Rust supports. We thus explain our
+//! version here, without being as precise.
 //!
-//! -----
+//! Fun fact: computing exhaustiveness is NP-complete, because we can encode a SAT problem as an
+//! exhaustiveness problem. See [here](https://niedzejkob.p4.team/rust-np) for the fun details.
 //!
-//! This file includes the logic for exhaustiveness and reachability checking for pattern-matching.
-//! Specifically, given a list of patterns for a type, we can tell whether:
-//! (a) each pattern is reachable (reachability)
-//! (b) the patterns cover every possible value for the type (exhaustiveness)
 //!
-//! The algorithm implemented here is a modified version of the one described in [this
-//! paper](http://moscova.inria.fr/~maranget/papers/warn/index.html). We have however generalized
-//! it to accommodate the variety of patterns that Rust supports. We thus explain our version here,
-//! without being as rigorous.
+//! # Summary
 //!
+//! The algorithm is given as input a list of patterns, one for each arm of a match, and computes
+//! the following:
+//! - a set of values that match none of the patterns (if any),
+//! - for each subpattern (taking into account or-patterns), whether it would catch any value that
+//!     isn't caught by a pattern before it, i.e. whether it is reachable.
 //!
-//! # Summary
+//! To a first approximation, the algorithm works by exploring all possible values for the type
+//! being matched on, and determining which arm(s) catch which value. To make this tractable we
+//! cleverly group together values, as we'll see below.
 //!
-//! The core of the algorithm is the notion of "usefulness". A pattern `q` is said to be *useful*
-//! relative to another pattern `p` of the same type if there is a value that is matched by `q` and
-//! not matched by `p`. This generalizes to many `p`s: `q` is useful w.r.t. a list of patterns
-//! `p_1 .. p_n` if there is a value that is matched by `q` and by none of the `p_i`. We write
-//! `usefulness(p_1 .. p_n, q)` for a function that returns a list of such values. The aim of this
-//! file is to compute it efficiently.
-//!
-//! This is enough to compute reachability: a pattern in a `match` expression is reachable iff it
-//! is useful w.r.t. the patterns above it:
-//! ```rust
-//! # fn foo(x: Option<i32>) {
-//! match x {
-//!     Some(_) => {},
-//!     None => {},    // reachable: `None` is matched by this but not the branch above
-//!     Some(0) => {}, // unreachable: all the values this matches are already matched by
-//!                    // `Some(_)` above
+//! The entrypoint of this file is the [`compute_match_usefulness`] function, which computes
+//! reachability for each subpattern and exhaustiveness for the whole match.
+//!
+//! In this page we explain the necessary concepts to understand how the algorithm works.
+//!
+//!
+//! # Usefulness
+//!
+//! The central concept of this file is the notion of "usefulness". Given some patterns `p_1 ..
+//! p_n`, a pattern `q` is said to be *useful* if there is a value that is matched by `q` and by
+//! none of the `p_i`. We write `usefulness(p_1 .. p_n, q)` for a function that returns a list of
+//! such values. The aim of this file is to compute it efficiently.
+//!
+//! This is enough to compute reachability: a pattern in a `match` expression is reachable iff it is
+//! useful w.r.t. the patterns above it:
+//! ```compile_fail,E0004
+//! # #![feature(exclusive_range_pattern)]
+//! # fn foo() {
+//! match Some(0u32) {
+//!     Some(0..100) => {},
+//!     Some(90..190) => {}, // reachable: `Some(150)` is matched by this but not the branch above
+//!     Some(50..150) => {}, // unreachable: all the values this matches are already matched by
+//!                          //   the branches above
+//!     None => {},          // reachable: `None` is matched by this but not the branches above
 //! }
 //! # }
 //! ```
@@ -49,48 +58,35 @@
 //! pattern is _not_ useful w.r.t. the patterns in the match. The values returned by `usefulness`
 //! are used to tell the user which values are missing.
 //! ```compile_fail,E0004
-//! # fn foo(x: Option<i32>) {
+//! # fn foo(x: Option<u32>) {
 //! match x {
-//!     Some(0) => {},
 //!     None => {},
+//!     Some(0) => {},
 //!     // not exhaustive: `_` is useful because it matches `Some(1)`
 //! }
 //! # }
 //! ```
 //!
-//! The entrypoint of this file is the [`compute_match_usefulness`] function, which computes
-//! reachability for each match branch and exhaustiveness for the whole match.
-//!
 //!
 //! # Constructors and fields
 //!
-//! Note: we will often abbreviate "constructor" as "ctor".
-//!
-//! The idea that powers everything that is done in this file is the following: a (matchable)
-//! value is made from a constructor applied to a number of subvalues. Examples of constructors are
-//! `Some`, `None`, `(,)` (the 2-tuple constructor), `Foo {..}` (the constructor for a struct
-//! `Foo`), and `2` (the constructor for the number `2`). This is natural when we think of
-//! pattern-matching, and this is the basis for what follows.
-//!
-//! Some of the ctors listed above might feel weird: `None` and `2` don't take any arguments.
-//! That's ok: those are ctors that take a list of 0 arguments; they are the simplest case of
-//! ctors. We treat `2` as a ctor because `u64` and other number types behave exactly like a huge
-//! `enum`, with one variant for each number. This allows us to see any matchable value as made up
-//! from a tree of ctors, each having a set number of children. For example: `Foo { bar: None,
-//! baz: Ok(0) }` is made from 4 different ctors, namely `Foo{..}`, `None`, `Ok` and `0`.
-//!
-//! This idea can be extended to patterns: they are also made from constructors applied to fields.
-//! A pattern for a given type is allowed to use all the ctors for values of that type (which we
-//! call "value constructors"), but there are also pattern-only ctors. The most important one is
-//! the wildcard (`_`), and the others are integer ranges (`0..=10`), variable-length slices (`[x,
-//! ..]`), and or-patterns (`Ok(0) | Err(_)`). Examples of valid patterns are `42`, `Some(_)`, `Foo
-//! { bar: Some(0) | None, baz: _ }`. Note that a binder in a pattern (e.g. `Some(x)`) matches the
-//! same values as a wildcard (e.g. `Some(_)`), so we treat both as wildcards.
-//!
-//! From this deconstruction we can compute whether a given value matches a given pattern; we
-//! simply look at ctors one at a time. Given a pattern `p` and a value `v`, we want to compute
-//! `matches!(v, p)`. It's mostly straightforward: we compare the head ctors and when they match
-//! we compare their fields recursively. A few representative examples:
+//! In the value `Pair(Some(0), true)`, `Pair` is called the constructor of the value, and `Some(0)`
+//! and `true` are its fields. Every matcheable value can be decomposed in this way. Examples of
+//! constructors are: `Some`, `None`, `(,)` (the 2-tuple constructor), `Foo {..}` (the constructor
+//! for a struct `Foo`), and `2` (the constructor for the number `2`).
+//!
+//! Each constructor takes a fixed number of fields; this is called its arity. `Pair` and `(,)` have
+//! arity 2, `Some` has arity 1, `None` and `42` have arity 0. Each type has a known set of
+//! constructors. Some types have many constructors (like `u64`) or even an infinitely many (like
+//! `&str` and `&[T]`).
+//!
+//! Patterns are similar: `Pair(Some(_), _)` has constructor `Pair` and two fields. The difference
+//! is that we get some extra pattern-only constructors, namely: the wildcard `_`, variable
+//! bindings, integer ranges like `0..=10`, and variable-length slices like `[_, .., _]`. We treat
+//! or-patterns separately, see the dedicated section below.
+//!
+//! Now to check if a value `v` matches a pattern `p`, we check if `v`'s constructor matches `p`'s
+//! constructor, then recursively compare their fields if necessary. A few representative examples:
 //!
 //! - `matches!(v, _) := true`
 //! - `matches!((v0,  v1), (p0,  p1)) := matches!(v0, p0) && matches!(v1, p1)`
@@ -100,213 +96,398 @@
 //! - `matches!(v, 1..=100) := matches!(v, 1) || ... || matches!(v, 100)`
 //! - `matches!([v0], [p0, .., p1]) := false` (incompatible lengths)
 //! - `matches!([v0, v1, v2], [p0, .., p1]) := matches!(v0, p0) && matches!(v2, p1)`
-//! - `matches!(v, p0 | p1) := matches!(v, p0) || matches!(v, p1)`
 //!
-//! Constructors, fields and relevant operations are defined in the [`super::deconstruct_pat`] module.
+//! Constructors, fields and relevant operations are defined in the [`super::deconstruct_pat`]
+//! module. The question of whether a constructor is matched by another one is answered by
+//! [`Constructor::is_covered_by`].
 //!
-//! Note: this constructors/fields distinction may not straightforwardly apply to every Rust type.
-//! For example a value of type `Rc<u64>` can't be deconstructed that way, and `&str` has an
-//! infinitude of constructors. There are also subtleties with visibility of fields and
-//! uninhabitedness and various other things. The constructors idea can be extended to handle most
-//! of these subtleties though; caveats are documented where relevant throughout the code.
+//! Note 1: variable bindings (like the `x` in `Some(x)`) match anything, so we treat them as wildcards.
+//! Note 2: this only applies to matcheable values. For example a value of type `Rc<u64>` can't be
+//! deconstructed that way.
 //!
-//! Whether constructors cover each other is computed by [`Constructor::is_covered_by`].
 //!
 //!
 //! # Specialization
 //!
-//! Recall that we wish to compute `usefulness(p_1 .. p_n, q)`: given a list of patterns `p_1 ..
-//! p_n` and a pattern `q`, all of the same type, we want to find a list of values (called
-//! "witnesses") that are matched by `q` and by none of the `p_i`. We obviously don't just
-//! enumerate all possible values. From the discussion above we see that we can proceed
-//! ctor-by-ctor: for each value ctor of the given type, we ask "is there a value that starts with
-//! this constructor and matches `q` and none of the `p_i`?". As we saw above, there's a lot we can
-//! say from knowing only the first constructor of our candidate value.
+//! The examples in the previous section motivate the operation at the heart of the algorithm:
+//! "specialization". It captures this idea of "removing one layer of constructor".
+//!
+//! `specialize(c, p)` takes a value-only constructor `c` and a pattern `p`, and returns a
+//! pattern-tuple or nothing. It works as follows:
+//!
+//! - Specializing for the wrong constructor returns nothing
+//!
+//!   - `specialize(None, Some(p0)) := <nothing>`
+//!   - `specialize([,,,], [p0]) := <nothing>`
+//!
+//! - Specializing for the correct constructor returns a tuple of the fields
+//!
+//!   - `specialize(Variant1, Variant1(p0, p1, p2)) := (p0, p1, p2)`
+//!   - `specialize(Foo{ bar, baz, quz }, Foo { bar: p0, baz: p1, .. }) := (p0, p1, _)`
+//!   - `specialize([,,,], [p0, .., p1]) := (p0, _, _, p1)`
+//!
+//! We get the following property: for any values `v_1, .., v_n` of appropriate types, we have:
+//! ```text
+//! matches!(c(v_1, .., v_n), p)
+//! <=> specialize(c, p) returns something
+//!     && matches!((v_1, .., v_n), specialize(c, p))
+//! ```
+//!
+//! We also extend specialization to pattern-tuples by applying it to the first pattern:
+//! `specialize(c, (p_0, .., p_n)) := specialize(c, p_0) ++ (p_1, .., p_m)`
+//! where `++` is concatenation of tuples.
+//!
+//!
+//! The previous property extends to pattern-tuples:
+//! ```text
+//! matches!((c(v_1, .., v_n), w_1, .., w_m), (p_0, p_1, .., p_m))
+//! <=> specialize(c, p_0) does not error
+//!     && matches!((v_1, .., v_n, w_1, .., w_m), specialize(c, (p_0, p_1, .., p_m)))
+//! ```
+//!
+//! Whether specialization returns something or not is given by [`Constructor::is_covered_by`].
+//! Specialization of a pattern is computed in [`DeconstructedPat::specialize`]. Specialization for
+//! a pattern-tuple is computed in [`PatStack::pop_head_constructor`]. Finally, specialization for a
+//! set of pattern-tuples is computed in [`Matrix::specialize_constructor`].
+//!
+//!
+//!
+//! # Undoing specialization
+//!
+//! To construct witnesses we will need an inverse of specialization. If `c` is a constructor of
+//! arity `n`, we define `unspecialize` as:
+//! `unspecialize(c, (p_1, .., p_n, q_1, .., q_m)) := (c(p_1, .., p_n), q_1, .., q_m)`.
+//!
+//! This is done for a single witness-tuple in [`WitnessStack::apply_constructor`], and for a set of
+//! witness-tuples in [`WitnessMatrix::apply_constructor`].
+//!
+//!
+//!
+//! # Computing usefulness
+//!
+//! We now present a naive version of the algorithm for computing usefulness. From now on we operate
+//! on pattern-tuples.
+//!
+//! Let `pt_1, .., pt_n` and `qt` be length-m tuples of patterns for the same type `(T_1, .., T_m)`.
+//! We compute `usefulness(tp_1, .., tp_n, tq)` as follows:
+//!
+//! - Base case: `m == 0`.
+//!     The pattern-tuples are all empty, i.e. they're all `()`. Thus `tq` is useful iff there are
+//!     no rows above it, i.e. if `n == 0`. In that case we return `()` as a witness-tuple of
+//!     usefulness of `tq`.
+//!
+//! - Inductive case: `m > 0`.
+//!     In this naive version, we list all the possible constructors for values of type `T1` (we
+//!     will be more clever in the next section).
+//!
+//!     - For each such constructor `c` for which `specialize(c, tq)` is not nothing:
+//!         - We recursively compute `usefulness(specialize(c, tp_1) ... specialize(c, tp_n), specialize(c, tq))`,
+//!             where we discard any `specialize(c, p_i)` that returns nothing.
+//!         - For each witness-tuple `w` found, we apply `unspecialize(c, w)` to it.
+//!
+//!     - We return the all the witnesses found, if any.
+//!
 //!
 //! Let's take the following example:
 //! ```compile_fail,E0004
 //! # enum Enum { Variant1(()), Variant2(Option<bool>, u32)}
+//! # use Enum::*;
 //! # fn foo(x: Enum) {
 //! match x {
-//!     Enum::Variant1(_) => {} // `p1`
-//!     Enum::Variant2(None, 0) => {} // `p2`
-//!     Enum::Variant2(Some(_), 0) => {} // `q`
+//!     Variant1(_) => {} // `p1`
+//!     Variant2(None, 0) => {} // `p2`
+//!     Variant2(Some(_), 0) => {} // `q`
 //! }
 //! # }
 //! ```
 //!
-//! We can easily see that if our candidate value `v` starts with `Variant1` it will not match `q`.
-//! If `v = Variant2(v0, v1)` however, whether or not it matches `p2` and `q` will depend on `v0`
-//! and `v1`. In fact, such a `v` will be a witness of usefulness of `q` exactly when the tuple
-//! `(v0, v1)` is a witness of usefulness of `q'` in the following reduced match:
-//!
-//! ```compile_fail,E0004
-//! # fn foo(x: (Option<bool>, u32)) {
-//! match x {
-//!     (None, 0) => {} // `p2'`
-//!     (Some(_), 0) => {} // `q'`
-//! }
-//! # }
+//! To compute the usefulness of `q`, we would proceed as follows:
+//! ```text
+//! Start:
+//!   `tp1 = [Variant1(_)]`
+//!   `tp2 = [Variant2(None, 0)]`
+//!   `tq  = [Variant2(Some(true), 0)]`
+//!
+//!   Constructors are `Variant1` and `Variant2`. Only `Variant2` can specialize `tq`.
+//!   Specialize with `Variant2`:
+//!     `tp2 = [None, 0]`
+//!     `tq  = [Some(true), 0]`
+//!
+//!     Constructors are `None` and `Some`. Only `Some` can specialize `tq`.
+//!     Specialize with `Some`:
+//!       `tq  = [true, 0]`
+//!
+//!       Constructors are `false` and `true`. Only `true` can specialize `tq`.
+//!       Specialize with `true`:
+//!         `tq  = [0]`
+//!
+//!         Constructors are `0`, `1`, .. up to infinity. Only `0` can specialize `tq`.
+//!         Specialize with `0`:
+//!           `tq  = []`
+//!
+//!           m == 0 and n == 0, so `tq` is useful with witness `[]`.
+//!             `witness  = []`
+//!
+//!         Unspecialize with `0`:
+//!           `witness  = [0]`
+//!       Unspecialize with `true`:
+//!         `witness  = [true, 0]`
+//!     Unspecialize with `Some`:
+//!       `witness  = [Some(true), 0]`
+//!   Unspecialize with `Variant2`:
+//!     `witness  = [Variant2(Some(true), 0)]`
 //! ```
 //!
-//! This motivates a new step in computing usefulness, that we call _specialization_.
-//! Specialization consist of filtering a list of patterns for those that match a constructor, and
-//! then looking into the constructor's fields. This enables usefulness to be computed recursively.
-//!
-//! Instead of acting on a single pattern in each row, we will consider a list of patterns for each
-//! row, and we call such a list a _pattern-stack_. The idea is that we will specialize the
-//! leftmost pattern, which amounts to popping the constructor and pushing its fields, which feels
-//! like a stack. We note a pattern-stack simply with `[p_1 ... p_n]`.
-//! Here's a sequence of specializations of a list of pattern-stacks, to illustrate what's
-//! happening:
-//! ```ignore (illustrative)
-//! [Enum::Variant1(_)]
-//! [Enum::Variant2(None, 0)]
-//! [Enum::Variant2(Some(_), 0)]
-//! //==>> specialize with `Variant2`
-//! [None, 0]
-//! [Some(_), 0]
-//! //==>> specialize with `Some`
-//! [_, 0]
-//! //==>> specialize with `true` (say the type was `bool`)
-//! [0]
-//! //==>> specialize with `0`
-//! []
-//! ```
+//! Therefore `usefulness(tp_1, tp_2, tq)` returns the single witness-tuple `[Variant2(Some(true), 0)]`.
 //!
-//! The function `specialize(c, p)` takes a value constructor `c` and a pattern `p`, and returns 0
-//! or more pattern-stacks. If `c` does not match the head constructor of `p`, it returns nothing;
-//! otherwise if returns the fields of the constructor. This only returns more than one
-//! pattern-stack if `p` has a pattern-only constructor.
 //!
-//! - Specializing for the wrong constructor returns nothing
+//! Computing the set of constructors for a type is done in [`ConstructorSet::for_ty`]. See the
+//! following sections for more accurate versions of the algorithm and corresponding links.
 //!
-//!   `specialize(None, Some(p0)) := []`
 //!
-//! - Specializing for the correct constructor returns a single row with the fields
 //!
-//!   `specialize(Variant1, Variant1(p0, p1, p2)) := [[p0, p1, p2]]`
+//! # Computing reachability and exhaustiveness in one go
 //!
-//!   `specialize(Foo{..}, Foo { bar: p0, baz: p1 }) := [[p0, p1]]`
+//! The algorithm we have described so far computes usefulness of each pattern in turn to check if
+//! it is reachable, and ends by checking if `_` is useful to determine exhaustiveness of the whole
+//! match. In practice, instead of doing "for each pattern { for each constructor { ... } }", we do
+//! "for each constructor { for each pattern { ... } }". This allows us to compute everything in one
+//! go.
 //!
-//! - For or-patterns, we specialize each branch and concatenate the results
+//! [`Matrix`] stores the set of pattern-tuples under consideration. We track reachability of each
+//! row mutably in the matrix as we go along. We ignore witnesses of usefulness of the match rows.
+//! We gather witnesses of the usefulness of `_` in [`WitnessMatrix`]. The algorithm that computes
+//! all this is in [`compute_exhaustiveness_and_reachability`].
 //!
-//!   `specialize(c, p0 | p1) := specialize(c, p0) ++ specialize(c, p1)`
+//! See the full example at the bottom of this documentation.
 //!
-//! - We treat the other pattern constructors as if they were a large or-pattern of all the
-//!   possibilities:
 //!
-//!   `specialize(c, _) := specialize(c, Variant1(_) | Variant2(_, _) | ...)`
 //!
-//!   `specialize(c, 1..=100) := specialize(c, 1 | ... | 100)`
+//! # Making usefulness tractable: constructor splitting
 //!
-//!   `specialize(c, [p0, .., p1]) := specialize(c, [p0, p1] | [p0, _, p1] | [p0, _, _, p1] | ...)`
+//! We're missing one last detail: which constructors do we list? Naively listing all value
+//! constructors cannot work for types like `u64` or `&str`, so we need to be more clever. The final
+//! clever idea for this algorithm is that we can group together constructors that behave the same.
 //!
-//! - If `c` is a pattern-only constructor, `specialize` is defined on a case-by-case basis. See
-//!   the discussion about constructor splitting in [`super::deconstruct_pat`].
+//! Examples:
+//! ```compile_fail,E0004
+//! match (0, false) {
+//!     (0 ..=100, true) => {}
+//!     (50..=150, false) => {}
+//!     (0 ..=200, _) => {}
+//! }
+//! ```
 //!
+//! In this example, trying any of `0`, `1`, .., `49` will give the same specialized matrix, and
+//! thus the same reachability/exhaustiveness results. We can thus accelerate the algorithm by
+//! trying them all at once. Here in fact, the only cases we need to consider are: `0..50`,
+//! `50..=100`, `101..=150`,`151..=200` and `201..`.
 //!
-//! We then extend this function to work with pattern-stacks as input, by acting on the first
-//! column and keeping the other columns untouched.
+//! ```
+//! enum Direction { North, South, East, West }
+//! # let wind = (Direction::North, 0u8);
+//! match wind {
+//!     (Direction::North, 50..) => {}
+//!     (_, _) => {}
+//! }
+//! ```
 //!
-//! Specialization for the whole matrix is done in [`Matrix::specialize_constructor`]. Note that
-//! or-patterns in the first column are expanded before being stored in the matrix. Specialization
-//! for a single patstack is done from a combination of [`Constructor::is_covered_by`] and
-//! [`PatStack::pop_head_constructor`]. The internals of how it's done mostly live in the
-//! [`super::deconstruct_pat::Fields`] struct.
+//! In this example, trying any of `South`, `East`, `West` will give the same specialized matrix. By
+//! the same reasoning, we only need to try two cases: `North`, and "everything else".
 //!
+//! We call _constructor splitting_ the operation that computes such a minimal set of cases to try.
+//! This is done in [`ConstructorSet::split`] and explained in [`super::deconstruct_pat`].
 //!
-//! # Computing usefulness
 //!
-//! We now have all we need to compute usefulness. The inputs to usefulness are a list of
-//! pattern-stacks `p_1 ... p_n` (one per row), and a new pattern_stack `q`. The paper and this
-//! file calls the list of patstacks a _matrix_. They must all have the same number of columns and
-//! the patterns in a given column must all have the same type. `usefulness` returns a (possibly
-//! empty) list of witnesses of usefulness. These witnesses will also be pattern-stacks.
-//!
-//! - base case: `n_columns == 0`.
-//!     Since a pattern-stack functions like a tuple of patterns, an empty one functions like the
-//!     unit type. Thus `q` is useful iff there are no rows above it, i.e. if `n == 0`.
-//!
-//! - inductive case: `n_columns > 0`.
-//!     We need a way to list the constructors we want to try. We will be more clever in the next
-//!     section but for now assume we list all value constructors for the type of the first column.
-//!
-//!     - for each such ctor `c`:
-//!
-//!         - for each `q'` returned by `specialize(c, q)`:
-//!
-//!             - we compute `usefulness(specialize(c, p_1) ... specialize(c, p_n), q')`
-//!
-//!         - for each witness found, we revert specialization by pushing the constructor `c` on top.
-//!
-//!     - We return the concatenation of all the witnesses found, if any.
-//!
-//! Example:
-//! ```ignore (illustrative)
-//! [Some(true)] // p_1
-//! [None] // p_2
-//! [Some(_)] // q
-//! //==>> try `None`: `specialize(None, q)` returns nothing
-//! //==>> try `Some`: `specialize(Some, q)` returns a single row
-//! [true] // p_1'
-//! [_] // q'
-//! //==>> try `true`: `specialize(true, q')` returns a single row
-//! [] // p_1''
-//! [] // q''
-//! //==>> base case; `n != 0` so `q''` is not useful.
-//! //==>> go back up a step
-//! [true] // p_1'
-//! [_] // q'
-//! //==>> try `false`: `specialize(false, q')` returns a single row
-//! [] // q''
-//! //==>> base case; `n == 0` so `q''` is useful. We return the single witness `[]`
-//! witnesses:
-//! []
-//! //==>> undo the specialization with `false`
-//! witnesses:
-//! [false]
-//! //==>> undo the specialization with `Some`
-//! witnesses:
-//! [Some(false)]
-//! //==>> we have tried all the constructors. The output is the single witness `[Some(false)]`.
-//! ```
+//! # Or-patterns
 //!
-//! This computation is done in [`is_useful`]. In practice we don't care about the list of
-//! witnesses when computing reachability; we only need to know whether any exist. We do keep the
-//! witnesses when computing exhaustiveness to report them to the user.
+//! What we have described so far works well if there are no or-patterns. To handle them, if the
+//! first pattern of a row in the matrix is an or-pattern, we expand it by duplicating the rest of
+//! the row as necessary. This is handled automatically in [`Matrix`].
 //!
+//! This makes reachability tracking subtle, because we also want to compute whether an alternative
+//! of an or-pattern is unreachable, e.g. in `Some(_) | Some(0)`. We track reachability of each
+//! subpattern by interior mutability in [`DeconstructedPat`] with `set_reachable`/`is_reachable`.
 //!
-//! # Making usefulness tractable: constructor splitting
+//! It's unfortunate that we have to use interior mutability, but believe me (Nadrieril), I have
+//! tried [other](https://github.com/rust-lang/rust/pull/80104)
+//! [solutions](https://github.com/rust-lang/rust/pull/80632) and nothing is remotely as simple.
 //!
-//! We're missing one last detail: which constructors do we list? Naively listing all value
-//! constructors cannot work for types like `u64` or `&str`, so we need to be more clever. The
-//! first obvious insight is that we only want to list constructors that are covered by the head
-//! constructor of `q`. If it's a value constructor, we only try that one. If it's a pattern-only
-//! constructor, we use the final clever idea for this algorithm: _constructor splitting_, where we
-//! group together constructors that behave the same.
 //!
-//! The details are not necessary to understand this file, so we explain them in
-//! [`super::deconstruct_pat`]. Splitting is done by the [`Constructor::split`] function.
 //!
-//! # Constants in patterns
+//! # Constants and opaques
 //!
 //! There are two kinds of constants in patterns:
 //!
 //! * literals (`1`, `true`, `"foo"`)
 //! * named or inline consts (`FOO`, `const { 5 + 6 }`)
 //!
-//! The latter are converted into other patterns with literals at the leaves. For example
+//! The latter are converted into the corresponding patterns by a previous phase. For example
 //! `const_to_pat(const { [1, 2, 3] })` becomes an `Array(vec![Const(1), Const(2), Const(3)])`
 //! pattern. This gets problematic when comparing the constant via `==` would behave differently
-//! from matching on the constant converted to a pattern. Situations like that can occur, when
-//! the user implements `PartialEq` manually, and thus could make `==` behave arbitrarily different.
-//! In order to honor the `==` implementation, constants of types that implement `PartialEq` manually
-//! stay as a full constant and become an `Opaque` pattern. These `Opaque` patterns do not participate
-//! in exhaustiveness, specialization or overlap checking.
-
-use self::ArmType::*;
-use self::Usefulness::*;
+//! from matching on the constant converted to a pattern. The situation around this is currently
+//! unclear and the lang team is working on clarifying what we want to do there. In any case, there
+//! are constants we will not turn into patterns. We capture these with `Constructor::Opaque`. These
+//! `Opaque` patterns do not participate in exhaustiveness, specialization or overlap checking.
+//!
+//!
+//!
+//! # Full example
+//!
+//! We illustrate a full run of the algorithm on the following match.
+//!
+//! ```compile_fail,E0004
+//! # struct Pair(Option<u32>, bool);
+//! # fn foo(x: Pair) -> u32 {
+//! match x {
+//!     Pair(Some(0), _) => 1,
+//!     Pair(_, false) => 2,
+//!     Pair(Some(0), false) => 3,
+//! }
+//! # }
+//! ```
+//!
+//! We keep track of the original row for illustration purposes, this is not what the algorithm
+//! actually does (it tracks reachability as a boolean on each row).
+//!
+//! ```text
+//!  ┐ Patterns:
+//!  │   1. `[Pair(Some(0), _)]`
+//!  │   2. `[Pair(_, false)]`
+//!  │   3. `[Pair(Some(0), false)]`
+//!  │
+//!  │ Specialize with `Pair`:
+//!  ├─┐ Patterns:
+//!  │ │   1. `[Some(0), _]`
+//!  │ │   2. `[_, false]`
+//!  │ │   3. `[Some(0), false]`
+//!  │ │
+//!  │ │ Specialize with `Some`:
+//!  │ ├─┐ Patterns:
+//!  │ │ │   1. `[0, _]`
+//!  │ │ │   2. `[_, false]`
+//!  │ │ │   3. `[0, false]`
+//!  │ │ │
+//!  │ │ │ Specialize with `0`:
+//!  │ │ ├─┐ Patterns:
+//!  │ │ │ │   1. `[_]`
+//!  │ │ │ │   3. `[false]`
+//!  │ │ │ │
+//!  │ │ │ │ Specialize with `true`:
+//!  │ │ │ ├─┐ Patterns:
+//!  │ │ │ │ │   1. `[]`
+//!  │ │ │ │ │
+//!  │ │ │ │ │ We note arm 1 is reachable (by `Pair(Some(0), true)`).
+//!  │ │ │ ├─┘
+//!  │ │ │ │
+//!  │ │ │ │ Specialize with `false`:
+//!  │ │ │ ├─┐ Patterns:
+//!  │ │ │ │ │   1. `[]`
+//!  │ │ │ │ │   3. `[]`
+//!  │ │ │ │ │
+//!  │ │ │ │ │ We note arm 1 is reachable (by `Pair(Some(0), false)`).
+//!  │ │ │ ├─┘
+//!  │ │ ├─┘
+//!  │ │ │
+//!  │ │ │ Specialize with `1..`:
+//!  │ │ ├─┐ Patterns:
+//!  │ │ │ │   2. `[false]`
+//!  │ │ │ │
+//!  │ │ │ │ Specialize with `true`:
+//!  │ │ │ ├─┐ Patterns:
+//!  │ │ │ │ │   // no rows left
+//!  │ │ │ │ │
+//!  │ │ │ │ │ We have found an unmatched value (`Pair(Some(1..), true)`)! This gives us a witness.
+//!  │ │ │ │ │ New witnesses:
+//!  │ │ │ │ │   `[]`
+//!  │ │ │ ├─┘
+//!  │ │ │ │ Unspecialize new witnesses with `true`:
+//!  │ │ │ │   `[true]`
+//!  │ │ │ │
+//!  │ │ │ │ Specialize with `false`:
+//!  │ │ │ ├─┐ Patterns:
+//!  │ │ │ │ │   2. `[]`
+//!  │ │ │ │ │
+//!  │ │ │ │ │ We note arm 2 is reachable (by `Pair(Some(1..), false)`).
+//!  │ │ │ ├─┘
+//!  │ │ │ │
+//!  │ │ │ │ Total witnesses for `1..`:
+//!  │ │ │ │   `[true]`
+//!  │ │ ├─┘
+//!  │ │ │ Unspecialize new witnesses with `1..`:
+//!  │ │ │   `[1.., true]`
+//!  │ │ │
+//!  │ │ │ Total witnesses for `Some`:
+//!  │ │ │   `[1.., true]`
+//!  │ ├─┘
+//!  │ │ Unspecialize new witnesses with `Some`:
+//!  │ │   `[Some(1..), true]`
+//!  │ │
+//!  │ │ Specialize with `None`:
+//!  │ ├─┐ Patterns:
+//!  │ │ │   2. `[false]`
+//!  │ │ │
+//!  │ │ │ Specialize with `true`:
+//!  │ │ ├─┐ Patterns:
+//!  │ │ │ │   // no rows left
+//!  │ │ │ │
+//!  │ │ │ │ We have found an unmatched value (`Pair(None, true)`)! This gives us a witness.
+//!  │ │ │ │ New witnesses:
+//!  │ │ │ │   `[]`
+//!  │ │ ├─┘
+//!  │ │ │ Unspecialize new witnesses with `true`:
+//!  │ │ │   `[true]`
+//!  │ │ │
+//!  │ │ │ Specialize with `false`:
+//!  │ │ ├─┐ Patterns:
+//!  │ │ │ │   2. `[]`
+//!  │ │ │ │
+//!  │ │ │ │ We note arm 2 is reachable (by `Pair(None, false)`).
+//!  │ │ ├─┘
+//!  │ │ │
+//!  │ │ │ Total witnesses for `None`:
+//!  │ │ │   `[true]`
+//!  │ ├─┘
+//!  │ │ Unspecialize new witnesses with `None`:
+//!  │ │   `[None, true]`
+//!  │ │
+//!  │ │ Total witnesses for `Pair`:
+//!  │ │   `[Some(1..), true]`
+//!  │ │   `[None, true]`
+//!  ├─┘
+//!  │ Unspecialize new witnesses with `Pair`:
+//!  │   `[Pair(Some(1..), true)]`
+//!  │   `[Pair(None, true)]`
+//!  │
+//!  │ Final witnesses:
+//!  │   `[Pair(Some(1..), true)]`
+//!  │   `[Pair(None, true)]`
+//!  ┘
+//! ```
+//!
+//! We conclude:
+//! - Arm 3 is unreachable (it was never marked as reachable);
+//! - The match is not exhaustive;
+//! - Adding arms with `Pair(Some(1..), true)` and `Pair(None, true)` would make the match exhaustive.
+//!
+//! Note that when we're deep in the algorithm, we don't know what specialization steps got us here.
+//! We can only figure out what our witnesses correspond to by unspecializing back up the stack.
+//!
+//!
+//! # Tests
+//!
+//! Note: tests specific to this file can be found in:
+//!
+//!   - `ui/pattern/usefulness`
+//!   - `ui/or-patterns`
+//!   - `ui/consts/const_in_pattern`
+//!   - `ui/rfc-2008-non-exhaustive`
+//!   - `ui/half-open-range-patterns`
+//!   - probably many others
+//!
+//! I (Nadrieril) prefer to put new tests in `ui/pattern/usefulness` unless there's a specific
+//! reason not to, for example if they crucially depend on a particular feature like `or_patterns`.
+
 use super::deconstruct_pat::{
     Constructor, ConstructorSet, DeconstructedPat, IntRange, MaybeInfiniteInt, SplitConstructorSet,
     WitnessPat,
@@ -384,21 +565,39 @@ impl<'a, 'p, 'tcx> fmt::Debug for PatCtxt<'a, 'p, 'tcx> {
     }
 }
 
-/// A row of a matrix. Rows of len 1 are very common, which is why `SmallVec[_; 2]`
-/// works well.
+/// A row of the matrix. Represents a pattern-tuple under investigation.
 #[derive(Clone)]
-pub(crate) struct PatStack<'p, 'tcx> {
+struct PatStack<'p, 'tcx> {
+    // Rows of len 1 are very common, which is why `SmallVec[_; 2]` works well.
     pats: SmallVec<[&'p DeconstructedPat<'p, 'tcx>; 2]>,
+    /// Whether the original arm had a guard.
     is_under_guard: bool,
+    /// When we specialize, we remember which row of the original matrix produced a given row of the
+    /// specialized matrix. When we unspecialize, we use this to propagate reachability back up the
+    /// callstack.
+    /// At the start of the algorithm, this is the id of the arm this comes from (but we don't use
+    /// this fact anywhere).
+    parent_row: usize,
+    /// False when the matrix is just built. This is set to `true` by
+    /// [`compute_exhaustiveness_and_reachability`] if the arm is found to be reachable.
+    reachable: bool,
 }
 
 impl<'p, 'tcx> PatStack<'p, 'tcx> {
-    fn from_pattern(pat: &'p DeconstructedPat<'p, 'tcx>, is_under_guard: bool) -> Self {
-        PatStack { pats: smallvec![pat], is_under_guard }
+    fn from_pattern(
+        pat: &'p DeconstructedPat<'p, 'tcx>,
+        parent_row: usize,
+        is_under_guard: bool,
+    ) -> Self {
+        PatStack { pats: smallvec![pat], parent_row, is_under_guard, reachable: false }
     }
 
-    fn from_vec(vec: SmallVec<[&'p DeconstructedPat<'p, 'tcx>; 2]>, is_under_guard: bool) -> Self {
-        PatStack { pats: vec, is_under_guard }
+    fn from_vec(
+        pats: SmallVec<[&'p DeconstructedPat<'p, 'tcx>; 2]>,
+        parent_row: usize,
+        is_under_guard: bool,
+    ) -> Self {
+        PatStack { pats, parent_row, is_under_guard, reachable: false }
     }
 
     fn is_empty(&self) -> bool {
@@ -417,51 +616,34 @@ impl<'p, 'tcx> PatStack<'p, 'tcx> {
         self.pats.iter().copied()
     }
 
-    // Recursively expand the first pattern into its subpatterns. Only useful if the pattern is an
-    // or-pattern. Panics if `self` is empty.
+    // Recursively expand the first or-pattern into its subpatterns. Only useful if the pattern is
+    // an or-pattern. Panics if `self` is empty.
     fn expand_or_pat<'a>(&'a self) -> impl Iterator<Item = PatStack<'p, 'tcx>> + Captures<'a> {
-        self.head().iter_fields().map(move |pat| {
-            let mut new_patstack = PatStack::from_pattern(pat, self.is_under_guard);
+        self.head().flatten_or_pat().into_iter().map(move |pat| {
+            let mut new_patstack =
+                PatStack::from_pattern(pat, self.parent_row, self.is_under_guard);
             new_patstack.pats.extend_from_slice(&self.pats[1..]);
             new_patstack
         })
     }
 
-    // Recursively expand all patterns into their subpatterns and push each `PatStack` to matrix.
-    fn expand_and_extend<'a>(&'a self, matrix: &mut Matrix<'p, 'tcx>) {
-        if !self.is_empty() && self.head().is_or_pat() {
-            for pat in self.head().iter_fields() {
-                let mut new_patstack = PatStack::from_pattern(pat, self.is_under_guard);
-                new_patstack.pats.extend_from_slice(&self.pats[1..]);
-                if !new_patstack.is_empty() && new_patstack.head().is_or_pat() {
-                    new_patstack.expand_and_extend(matrix);
-                } else if !new_patstack.is_empty() {
-                    matrix.push(new_patstack);
-                }
-            }
-        }
-    }
-
-    /// This computes `S(self.head().ctor(), self)`. See top of the file for explanations.
-    ///
-    /// Structure patterns with a partial wild pattern (Foo { a: 42, .. }) have their missing
-    /// fields filled with wild patterns.
-    ///
-    /// This is roughly the inverse of `Constructor::apply`.
+    /// This computes `specialize(ctor, self)`. See top of the file for explanations.
+    /// Only call if `ctor.is_covered_by(self.head().ctor())` is true.
     fn pop_head_constructor(
         &self,
         pcx: &PatCtxt<'_, 'p, 'tcx>,
         ctor: &Constructor<'tcx>,
+        parent_row: usize,
     ) -> PatStack<'p, 'tcx> {
         // We pop the head pattern and push the new fields extracted from the arguments of
         // `self.head()`.
         let mut new_fields: SmallVec<[_; 2]> = self.head().specialize(pcx, ctor);
         new_fields.extend_from_slice(&self.pats[1..]);
-        PatStack::from_vec(new_fields, self.is_under_guard)
+        PatStack::from_vec(new_fields, parent_row, self.is_under_guard)
     }
 }
 
-/// Pretty-printing for matrix row.
+/// Pretty-printing for a matrix row.
 impl<'p, 'tcx> fmt::Debug for PatStack<'p, 'tcx> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         write!(f, "+")?;
@@ -472,51 +654,82 @@ impl<'p, 'tcx> fmt::Debug for PatStack<'p, 'tcx> {
     }
 }
 
-/// A 2D matrix.
+/// A 2D matrix. Represents a list of pattern-tuples under investigation.
+///
+/// Invariant: each row must have the same length, and each column must have the same type.
+///
+/// Invariant: the first column must not contain or-patterns. This is handled by
+/// [`Matrix::expand_and_push`].
+///
+/// In fact each column corresponds to a place inside the scrutinee of the match. E.g. after
+/// specializing `(,)` and `Some` on a pattern of type `(Option<u32>, bool)`, the first column of
+/// the matrix will correspond to `scrutinee.0.Some.0` and the second column to `scrutinee.1`.
 #[derive(Clone)]
-pub(super) struct Matrix<'p, 'tcx> {
-    pub rows: Vec<PatStack<'p, 'tcx>>,
+struct Matrix<'p, 'tcx> {
+    rows: Vec<PatStack<'p, 'tcx>>,
 }
 
 impl<'p, 'tcx> Matrix<'p, 'tcx> {
+    /// Make an empty matrix. Internal method, prefer [`Matrix::new`].
     fn empty() -> Self {
         Matrix { rows: vec![] }
     }
-
     /// Pushes a new row to the matrix. If the row starts with an or-pattern, this recursively
-    /// expands it.
+    /// expands it. Internal method, prefer [`Matrix::new`].
     fn push(&mut self, row: PatStack<'p, 'tcx>) {
         if !row.is_empty() && row.head().is_or_pat() {
-            row.expand_and_extend(self);
+            // Expand nested or-patterns.
+            for new_row in row.expand_or_pat() {
+                self.rows.push(new_row);
+            }
         } else {
             self.rows.push(row);
         }
     }
 
+    /// Build a new matrix from an iterator of `MatchArm`s.
+    fn new<'a>(iter: impl Iterator<Item = &'a MatchArm<'p, 'tcx>>) -> Self
+    where
+        'p: 'a,
+    {
+        let mut matrix = Matrix::empty();
+        for (row_id, arm) in iter.enumerate() {
+            let v = PatStack::from_pattern(arm.pat, row_id, arm.has_guard);
+            matrix.push(v);
+        }
+        matrix
+    }
+
     fn rows<'a>(
         &'a self,
     ) -> impl Iterator<Item = &'a PatStack<'p, 'tcx>> + Clone + DoubleEndedIterator + ExactSizeIterator
     {
         self.rows.iter()
     }
+    fn rows_mut<'a>(
+        &'a mut self,
+    ) -> impl Iterator<Item = &'a mut PatStack<'p, 'tcx>> + DoubleEndedIterator + ExactSizeIterator
+    {
+        self.rows.iter_mut()
+    }
 
-    /// Iterate over the first component of each row
+    /// Iterate over the first pattern of each row.
     fn heads<'a>(
         &'a self,
     ) -> impl Iterator<Item = &'p DeconstructedPat<'p, 'tcx>> + Clone + Captures<'a> {
         self.rows().map(|r| r.head())
     }
 
-    /// This computes `S(constructor, self)`. See top of the file for explanations.
+    /// This computes `specialize(ctor, self)`. See top of the file for explanations.
     fn specialize_constructor(
         &self,
         pcx: &PatCtxt<'_, 'p, 'tcx>,
         ctor: &Constructor<'tcx>,
     ) -> Matrix<'p, 'tcx> {
         let mut matrix = Matrix::empty();
-        for row in &self.rows {
+        for (i, row) in self.rows().enumerate() {
             if ctor.is_covered_by(pcx, row.head().ctor()) {
-                let new_row = row.pop_head_constructor(pcx, ctor);
+                let new_row = row.pop_head_constructor(pcx, ctor, i);
                 matrix.push(new_row);
             }
         }
@@ -560,92 +773,17 @@ impl<'p, 'tcx> fmt::Debug for Matrix<'p, 'tcx> {
     }
 }
 
-/// This carries the results of computing usefulness, as described at the top of the file. When
-/// checking usefulness of a match branch, we use the `NoWitnesses` variant, which also keeps track
-/// of potential unreachable sub-patterns (in the presence of or-patterns). When checking
-/// exhaustiveness of a whole match, we use the `WithWitnesses` variant, which carries a list of
-/// witnesses of non-exhaustiveness when there are any.
-/// Which variant to use is dictated by `ArmType`.
-#[derive(Debug, Clone)]
-enum Usefulness<'tcx> {
-    /// If we don't care about witnesses, simply remember if the pattern was useful.
-    NoWitnesses { useful: bool },
-    /// Carries a list of witnesses of non-exhaustiveness. If empty, indicates that the whole
-    /// pattern is unreachable.
-    WithWitnesses(WitnessMatrix<'tcx>),
-}
-
-impl<'tcx> Usefulness<'tcx> {
-    fn new_useful(preference: ArmType) -> Self {
-        match preference {
-            // A single (empty) witness of reachability.
-            FakeExtraWildcard => WithWitnesses(WitnessMatrix::unit_witness()),
-            RealArm => NoWitnesses { useful: true },
-        }
-    }
-
-    fn new_not_useful(preference: ArmType) -> Self {
-        match preference {
-            FakeExtraWildcard => WithWitnesses(WitnessMatrix::empty()),
-            RealArm => NoWitnesses { useful: false },
-        }
-    }
-
-    fn is_useful(&self) -> bool {
-        match self {
-            Usefulness::NoWitnesses { useful } => *useful,
-            Usefulness::WithWitnesses(witnesses) => !witnesses.is_empty(),
-        }
-    }
-
-    /// Combine usefulnesses from two branches. This is an associative operation.
-    fn extend(&mut self, other: Self) {
-        match (&mut *self, other) {
-            (WithWitnesses(_), WithWitnesses(o)) if o.is_empty() => {}
-            (WithWitnesses(s), WithWitnesses(o)) if s.is_empty() => *self = WithWitnesses(o),
-            (WithWitnesses(s), WithWitnesses(o)) => s.extend(o),
-            (NoWitnesses { useful: s_useful }, NoWitnesses { useful: o_useful }) => {
-                *s_useful = *s_useful || o_useful
-            }
-            _ => unreachable!(),
-        }
-    }
-
-    /// After calculating usefulness after a specialization, call this to reconstruct a usefulness
-    /// that makes sense for the matrix pre-specialization. This new usefulness can then be merged
-    /// with the results of specializing with the other constructors.
-    fn apply_constructor(
-        mut self,
-        pcx: &PatCtxt<'_, '_, 'tcx>,
-        matrix: &Matrix<'_, 'tcx>, // used to compute missing ctors
-        ctor: &Constructor<'tcx>,
-    ) -> Self {
-        match &mut self {
-            NoWitnesses { .. } => {}
-            WithWitnesses(witnesses) => witnesses.apply_constructor(pcx, matrix, ctor),
-        }
-        self
-    }
-}
-
-#[derive(Copy, Clone, Debug)]
-enum ArmType {
-    FakeExtraWildcard,
-    RealArm,
-}
-
-/// A partially-constructed witness of non-exhaustiveness for error reporting, represented as a list
-/// of patterns (in reverse order of construction) with wildcards inside to represent elements that
-/// can take any inhabitant of the type as a value.
+/// A witness-tuple of non-exhaustiveness for error reporting, represented as a list of patterns (in
+/// reverse order of construction).
 ///
 /// This mirrors `PatStack`: they function similarly, except `PatStack` contains user patterns we
 /// are inspecting, and `WitnessStack` contains witnesses we are constructing.
-/// FIXME(Nadrieril): use the same order of patterns for both
+/// FIXME(Nadrieril): use the same order of patterns for both.
 ///
-/// A `WitnessStack` should have the same types and length as the `PatStacks` we are inspecting
-/// (except we store the patterns in reverse order). Because Rust `match` is always against a single
-/// pattern, at the end the stack will have length 1. In the middle of the algorithm, it can contain
-/// multiple patterns.
+/// A `WitnessStack` should have the same types and length as the `PatStack`s we are inspecting
+/// (except we store the patterns in reverse order). The same way `PatStack` starts with length 1,
+/// at the end of the algorithm this will have length 1. In the middle of the algorithm, it can
+/// contain multiple patterns.
 ///
 /// For example, if we are constructing a witness for the match against
 ///
@@ -660,6 +798,7 @@ enum ArmType {
 /// ```
 ///
 /// We'll perform the following steps (among others):
+/// ```text
 /// - Start with a matrix representing the match
 ///     `PatStack(vec![Pair(None, _)])`
 ///     `PatStack(vec![Pair(_, false)])`
@@ -682,8 +821,11 @@ enum ArmType {
 ///     `WitnessStack(vec![true, Some(_)])`
 /// - Apply `Pair`
 ///     `WitnessStack(vec![Pair(Some(_), true)])`
+/// ```
 ///
 /// The final `Pair(Some(_), true)` is then the resulting witness.
+///
+/// See the top of the file for more detailed explanations and examples.
 #[derive(Debug, Clone)]
 pub(crate) struct WitnessStack<'tcx>(Vec<WitnessPat<'tcx>>);
 
@@ -700,8 +842,11 @@ impl<'tcx> WitnessStack<'tcx> {
     }
 
     /// Reverses specialization. Given a witness obtained after specialization, this constructs a
-    /// new witness valid for before specialization. Examples:
+    /// new witness valid for before specialization. See the section on `unspecialize` at the top of
+    /// the file.
     ///
+    /// Examples:
+    /// ```text
     /// ctor: tuple of 2 elements
     /// pats: [false, "foo", _, true]
     /// result: [(false, "foo"), _, true]
@@ -709,6 +854,7 @@ impl<'tcx> WitnessStack<'tcx> {
     /// ctor: Enum::Variant { a: (bool, &'static str), b: usize}
     /// pats: [(false, "foo"), _, true]
     /// result: [Enum::Variant { a: (false, "foo"), b: _ }, true]
+    /// ```
     fn apply_constructor(&mut self, pcx: &PatCtxt<'_, '_, 'tcx>, ctor: &Constructor<'tcx>) {
         let len = self.0.len();
         let arity = ctor.arity(pcx);
@@ -718,26 +864,29 @@ impl<'tcx> WitnessStack<'tcx> {
     }
 }
 
-/// Represents a set of partially-constructed witnesses of non-exhaustiveness for error reporting.
-/// This has similar invariants as `Matrix` does.
-/// Throughout the exhaustiveness phase of the algorithm, `is_useful` maintains the invariant that
-/// the union of the `Matrix` and the `WitnessMatrix` together matches the type exhaustively. By the
-/// end of the algorithm, this has a single column, which contains the patterns that are missing for
-/// the match to be exhaustive.
+/// Represents a set of pattern-tuples that are witnesses of non-exhaustiveness for error
+/// reporting. This has similar invariants as `Matrix` does.
+///
+/// The `WitnessMatrix` returned by [`compute_exhaustiveness_and_reachability`] obeys the invariant
+/// that the union of the input `Matrix` and the output `WitnessMatrix` together matches the type
+/// exhaustively.
+///
+/// Just as the `Matrix` starts with a single column, by the end of the algorithm, this has a single
+/// column, which contains the patterns that are missing for the match to be exhaustive.
 #[derive(Debug, Clone)]
 pub struct WitnessMatrix<'tcx>(Vec<WitnessStack<'tcx>>);
 
 impl<'tcx> WitnessMatrix<'tcx> {
-    /// New matrix with no rows.
+    /// New matrix with no witnesses.
     fn empty() -> Self {
         WitnessMatrix(vec![])
     }
-    /// New matrix with one row and no columns.
+    /// New matrix with one `()` witness, i.e. with no columns.
     fn unit_witness() -> Self {
         WitnessMatrix(vec![WitnessStack(vec![])])
     }
 
-    /// Whether this has any rows.
+    /// Whether this has any witnesses.
     fn is_empty(&self) -> bool {
         self.0.is_empty()
     }
@@ -753,19 +902,20 @@ impl<'tcx> WitnessMatrix<'tcx> {
         }
     }
 
-    /// Reverses specialization by `ctor`.
+    /// Reverses specialization by `ctor`. See the section on `unspecialize` at the top of the file.
     fn apply_constructor(
         &mut self,
         pcx: &PatCtxt<'_, '_, 'tcx>,
-        matrix: &Matrix<'_, 'tcx>, // used to compute missing ctors
+        missing_ctors: &[Constructor<'tcx>],
         ctor: &Constructor<'tcx>,
     ) {
         if self.is_empty() {
             return;
         }
-        if matches!(ctor, Constructor::Missing { .. }) {
-            let missing_ctors = ConstructorSet::for_ty(pcx.cx, pcx.ty)
-                .compute_missing(pcx, matrix.heads().map(DeconstructedPat::ctor));
+        if matches!(ctor, Constructor::Wildcard) {
+            let pat = WitnessPat::wild_from_ctor(pcx, Constructor::Wildcard);
+            self.push_pattern(&pat);
+        } else if matches!(ctor, Constructor::Missing) {
             // We got the special `Missing` constructor, so each of the missing constructors gives a
             // new pattern that is not caught by the match. We list those patterns and push them
             // onto our current witnesses.
@@ -782,6 +932,12 @@ impl<'tcx> WitnessMatrix<'tcx> {
                     self.extend(witnesses_with_missing_ctor)
                 }
             }
+        } else if !missing_ctors.is_empty() {
+            // `ctor` isn't `Wildcard` or `Missing` and some ctors are missing, so we know
+            // `split_ctors` will contain `Wildcard` or `Missing`.
+            // For diagnostic purposes we choose to discard witnesses we got under `ctor`, which
+            // will let only the `Wildcard` or `Missing` be reported.
+            self.0.clear();
         } else {
             for witness in self.0.iter_mut() {
                 witness.apply_constructor(pcx, ctor)
@@ -789,123 +945,129 @@ impl<'tcx> WitnessMatrix<'tcx> {
         }
     }
 
-    /// Merges the rows of two witness matrices. Their column types must match.
+    /// Merges the witnesses of two matrices. Their column types must match.
     fn extend(&mut self, other: Self) {
         self.0.extend(other.0)
     }
 }
 
-/// Algorithm from <http://moscova.inria.fr/~maranget/papers/warn/index.html>.
-/// The algorithm from the paper has been modified to correctly handle empty
-/// types. The changes are:
-///   (0) We don't exit early if the pattern matrix has zero rows. We just
-///       continue to recurse over columns.
-///   (1) all_constructors will only return constructors that are statically
-///       possible. E.g., it will only return `Ok` for `Result<T, !>`.
+/// The core of the algorithm.
 ///
-/// This finds whether a (row) vector `v` of patterns is 'useful' in relation
-/// to a set of such vectors `m` - this is defined as there being a set of
-/// inputs that will match `v` but not any of the sets in `m`.
+/// This recursively computes witnesses of the non-exhaustiveness of `matrix` (if any). Also tracks
+/// usefulness of each row in the matrix (in `row.reachable`). We track reachability of each
+/// subpattern using interior mutability in `DeconstructedPat`.
 ///
-/// All the patterns at each column of the `matrix ++ v` matrix must have the same type.
+/// The input `Matrix` and the output `WitnessMatrix` together match the type exhaustively.
 ///
-/// This is used both for reachability checking (if a pattern isn't useful in
-/// relation to preceding patterns, it is not reachable) and exhaustiveness
-/// checking (if a wildcard pattern is useful in relation to a matrix, the
-/// matrix isn't exhaustive).
+/// The key steps are:
+/// - specialization, where we dig into the rows that have a specific constructor and call ourselves
+///     recursively;
+/// - unspecialization, where we lift the results from the previous step into results for this step
+///     (using `apply_constructor` and by updating `row.reachable` for each parent row).
+/// This is all explained at the top of the file.
 ///
-/// `is_under_guard` is used to inform if the pattern has a guard. If it
-/// has one it must not be inserted into the matrix. This shouldn't be
-/// relied on for soundness.
-#[instrument(level = "debug", skip(cx, matrix, lint_root), ret)]
-fn is_useful<'p, 'tcx>(
+/// `wildcard_row` is a fictitious matrix row that has only wildcards, with the appropriate types to
+/// match what's in the columns of `matrix`.
+#[instrument(level = "debug", skip(cx, is_top_level), ret)]
+fn compute_exhaustiveness_and_reachability<'p, 'tcx>(
     cx: &MatchCheckCtxt<'p, 'tcx>,
-    matrix: &Matrix<'p, 'tcx>,
-    v: &PatStack<'p, 'tcx>,
-    witness_preference: ArmType,
-    lint_root: HirId,
+    matrix: &mut Matrix<'p, 'tcx>,
+    wildcard_row: &PatStack<'p, 'tcx>,
     is_top_level: bool,
-) -> Usefulness<'tcx> {
-    debug!(?matrix, ?v);
-    // The base case. We are pattern-matching on () and the return value is
-    // based on whether our matrix has a row or not.
-    // NOTE: This could potentially be optimized by checking rows.is_empty()
-    // first and then, if v is non-empty, the return value is based on whether
-    // the type of the tuple we're checking is inhabited or not.
-    if v.is_empty() {
-        let ret = if matrix.rows().all(|r| r.is_under_guard) {
-            Usefulness::new_useful(witness_preference)
-        } else {
-            Usefulness::new_not_useful(witness_preference)
-        };
-        debug!(?ret);
-        return ret;
-    }
-
-    debug_assert!(matrix.rows().all(|r| r.len() == v.len()));
-
-    // If the first pattern is an or-pattern, expand it.
-    let mut ret = Usefulness::new_not_useful(witness_preference);
-    if v.head().is_or_pat() {
-        debug!("expanding or-pattern");
-        // We try each or-pattern branch in turn.
-        let mut matrix = matrix.clone();
-        for v in v.expand_or_pat() {
-            debug!(?v);
-            let usefulness = ensure_sufficient_stack(|| {
-                is_useful(cx, &matrix, &v, witness_preference, lint_root, false)
-            });
-            debug!(?usefulness);
-            ret.extend(usefulness);
-            // We push the already-seen patterns into the matrix in order to detect redundant
-            // branches like `Some(_) | Some(0)`.
-            matrix.push(v);
+) -> WitnessMatrix<'tcx> {
+    debug_assert!(matrix.rows().all(|r| r.len() == wildcard_row.len()));
+
+    if wildcard_row.is_empty() {
+        // The base case. We are morally pattern-matching on (). A row is reachable iff it has no
+        // (unguarded) rows above it.
+        for row in matrix.rows_mut() {
+            // All rows are reachable until we find one without a guard.
+            row.reachable = true;
+            if !row.is_under_guard {
+                // There's an unguarded row, so the match is exhaustive, and any subsequent row is
+                // unreachable.
+                return WitnessMatrix::empty();
+            }
         }
-    } else {
-        let mut ty = v.head().ty();
+        // No (unguarded) rows, so the match is not exhaustive. We return a new witness.
+        return WitnessMatrix::unit_witness();
+    }
 
-        // Opaque types can't get destructured/split, but the patterns can
-        // actually hint at hidden types, so we use the patterns' types instead.
-        if let ty::Alias(ty::Opaque, ..) = ty.kind() {
-            if let Some(row) = matrix.rows().next() {
-                ty = row.head().ty();
+    let mut ty = wildcard_row.head().ty();
+    // If the type is opaque and it is revealed anywhere in the column, we take the revealed
+    // version. Otherwise we could encounter constructors for the revealed type and crash.
+    let is_opaque = |ty: Ty<'tcx>| matches!(ty.kind(), ty::Alias(ty::Opaque, ..));
+    if is_opaque(ty) {
+        for pat in matrix.heads() {
+            let pat_ty = pat.ty();
+            if !is_opaque(pat_ty) {
+                ty = pat_ty;
+                break;
             }
         }
-        debug!("v.head: {:?}, v.span: {:?}", v.head(), v.head().span());
-        let pcx = &PatCtxt { cx, ty, span: v.head().span(), is_top_level };
-
-        let v_ctor = v.head().ctor();
-        debug!(?v_ctor);
-        // We split the head constructor of `v`.
-        let split_ctors = v_ctor.split(pcx, matrix.heads().map(DeconstructedPat::ctor));
-        // For each constructor, we compute whether there's a value that starts with it that would
-        // witness the usefulness of `v`.
-        let start_matrix = &matrix;
-        for ctor in split_ctors {
-            debug!("specialize({:?})", ctor);
-            // We cache the result of `Fields::wildcards` because it is used a lot.
-            let spec_matrix = start_matrix.specialize_constructor(pcx, &ctor);
-            let v = v.pop_head_constructor(pcx, &ctor);
-            let usefulness = ensure_sufficient_stack(|| {
-                is_useful(cx, &spec_matrix, &v, witness_preference, lint_root, false)
-            });
-            let usefulness = usefulness.apply_constructor(pcx, start_matrix, &ctor);
-            ret.extend(usefulness);
-        }
     }
 
-    if ret.is_useful() {
-        v.head().set_reachable();
+    debug!("ty: {ty:?}");
+    let pcx = &PatCtxt { cx, ty, span: DUMMY_SP, is_top_level };
+
+    // Analyze the constructors present in this column.
+    let ctors = matrix.heads().map(|p| p.ctor());
+    let split_set = ConstructorSet::for_ty(pcx.cx, pcx.ty).split(pcx, ctors);
+    let mut split_ctors = split_set.present;
+    // We want to iterate over a full set of constructors, so if any is missing we add a wildcard.
+    if !split_set.missing.is_empty() {
+        let all_missing = split_ctors.is_empty();
+        let always_report_missing = is_top_level && !IntRange::is_integral(pcx.ty);
+        let ctor = if all_missing && !always_report_missing {
+            Constructor::Wildcard
+        } else {
+            // Like `Wildcard`, except if it doesn't match a row this will report all the missing
+            // constructors instead of just `_`.
+            Constructor::Missing
+        };
+        split_ctors.push(ctor);
+    }
+
+    let mut ret = WitnessMatrix::empty();
+    for ctor in split_ctors {
+        debug!("specialize({:?})", ctor);
+        // Dig into rows that match `ctor`.
+        let mut spec_matrix = matrix.specialize_constructor(pcx, &ctor);
+        let wildcard_row = wildcard_row.pop_head_constructor(pcx, &ctor, usize::MAX);
+        let mut witnesses = ensure_sufficient_stack(|| {
+            compute_exhaustiveness_and_reachability(cx, &mut spec_matrix, &wildcard_row, false)
+        });
+        // Transform witnesses for `spec_matrix` into witnesses for `matrix`.
+        witnesses.apply_constructor(pcx, &split_set.missing, &ctor);
+        ret.extend(witnesses);
+
+        // A parent row is useful if any of its children is.
+        for child_row in spec_matrix.rows() {
+            let parent_row = &mut matrix.rows[child_row.parent_row];
+            parent_row.reachable = parent_row.reachable || child_row.reachable;
+        }
     }
 
+    // Record that the subpattern is reachable.
+    for row in matrix.rows() {
+        if row.reachable {
+            row.head().set_reachable();
+        }
+    }
     ret
 }
 
 /// A column of patterns in the matrix, where a column is the intuitive notion of "subpatterns that
-/// inspect the same subvalue".
+/// inspect the same subvalue/place".
 /// This is used to traverse patterns column-by-column for lints. Despite similarities with
-/// `is_useful`, this is a different traversal. Notably this is linear in the depth of patterns,
-/// whereas `is_useful` is worst-case exponential (exhaustiveness is NP-complete).
+/// [`compute_exhaustiveness_and_reachability`], this does a different traversal. Notably this is
+/// linear in the depth of patterns, whereas `compute_exhaustiveness_and_reachability` is worst-case
+/// exponential (exhaustiveness is NP-complete). The core difference is that we treat sub-columns
+/// separately.
+///
+/// This must not contain an or-pattern. `specialize` takes care to expand them.
+///
+/// This is not used in the main algorithm; only in lints.
 #[derive(Debug)]
 struct PatternColumn<'p, 'tcx> {
     patterns: Vec<&'p DeconstructedPat<'p, 'tcx>>,
@@ -938,17 +1100,19 @@ impl<'p, 'tcx> PatternColumn<'p, 'tcx> {
         Some(first_ty)
     }
 
+    /// Do constructor splitting on the constructors of the column.
     fn analyze_ctors(&self, pcx: &PatCtxt<'_, 'p, 'tcx>) -> SplitConstructorSet<'tcx> {
         let column_ctors = self.patterns.iter().map(|p| p.ctor());
         ConstructorSet::for_ty(pcx.cx, pcx.ty).split(pcx, column_ctors)
     }
+
     fn iter<'a>(&'a self) -> impl Iterator<Item = &'p DeconstructedPat<'p, 'tcx>> + Captures<'a> {
         self.patterns.iter().copied()
     }
 
     /// Does specialization: given a constructor, this takes the patterns from the column that match
     /// the constructor, and outputs their fields.
-    /// This returns one column per field of the constructor. The normally all have the same length
+    /// This returns one column per field of the constructor. They usually all have the same length
     /// (the number of patterns in `self` that matched `ctor`), except that we expand or-patterns
     /// which may change the lengths.
     fn specialize(&self, pcx: &PatCtxt<'_, 'p, 'tcx>, ctor: &Constructor<'tcx>) -> Vec<Self> {
@@ -1138,11 +1302,8 @@ pub(crate) struct UsefulnessReport<'p, 'tcx> {
     pub(crate) non_exhaustiveness_witnesses: Vec<WitnessPat<'tcx>>,
 }
 
-/// The entrypoint for the usefulness algorithm. Computes whether a match is exhaustive and which
-/// of its arms are reachable.
-///
-/// Note: the input patterns must have been lowered through
-/// `check_match::MatchVisitor::lower_pattern`.
+/// The entrypoint for this file. Computes whether a match is exhaustive and which of its arms are
+/// reachable.
 #[instrument(skip(cx, arms), level = "debug")]
 pub(crate) fn compute_match_usefulness<'p, 'tcx>(
     cx: &MatchCheckCtxt<'p, 'tcx>,
@@ -1151,15 +1312,18 @@ pub(crate) fn compute_match_usefulness<'p, 'tcx>(
     scrut_ty: Ty<'tcx>,
     scrut_span: Span,
 ) -> UsefulnessReport<'p, 'tcx> {
-    let mut matrix = Matrix::empty();
+    let wild_pattern = cx.pattern_arena.alloc(DeconstructedPat::wildcard(scrut_ty, DUMMY_SP));
+    let wildcard_row = PatStack::from_pattern(wild_pattern, usize::MAX, false);
+    let mut matrix = Matrix::new(arms.iter());
+    let non_exhaustiveness_witnesses =
+        compute_exhaustiveness_and_reachability(cx, &mut matrix, &wildcard_row, true);
+
+    let non_exhaustiveness_witnesses: Vec<_> = non_exhaustiveness_witnesses.single_column();
     let arm_usefulness: Vec<_> = arms
         .iter()
         .copied()
         .map(|arm| {
             debug!(?arm);
-            let v = PatStack::from_pattern(arm.pat, arm.has_guard);
-            is_useful(cx, &matrix, &v, RealArm, arm.hir_id, true);
-            matrix.push(v);
             let reachability = if arm.pat.is_reachable() {
                 Reachability::Reachable(arm.pat.unreachable_spans())
             } else {
@@ -1168,28 +1332,20 @@ pub(crate) fn compute_match_usefulness<'p, 'tcx>(
             (arm, reachability)
         })
         .collect();
+    let report = UsefulnessReport { arm_usefulness, non_exhaustiveness_witnesses };
 
-    let wild_pattern = cx.pattern_arena.alloc(DeconstructedPat::wildcard(scrut_ty, DUMMY_SP));
-    let v = PatStack::from_pattern(wild_pattern, false);
-    let usefulness = is_useful(cx, &matrix, &v, FakeExtraWildcard, lint_root, true);
-    let non_exhaustiveness_witnesses: Vec<_> = match usefulness {
-        WithWitnesses(witness_matrix) => witness_matrix.single_column(),
-        NoWitnesses { .. } => bug!(),
-    };
-
-    let pat_column = arms.iter().flat_map(|arm| arm.pat.flatten_or_pat()).collect::<Vec<_>>();
-    let pat_column = PatternColumn::new(pat_column);
+    let pat_column = PatternColumn::new(matrix.heads().collect());
+    // Lint on ranges that overlap on their endpoints, which is likely a mistake.
     lint_overlapping_range_endpoints(cx, &pat_column, lint_root);
 
     // Run the non_exhaustive_omitted_patterns lint. Only run on refutable patterns to avoid hitting
     // `if let`s. Only run if the match is exhaustive otherwise the error is redundant.
-    if cx.refutable && non_exhaustiveness_witnesses.is_empty() {
+    if cx.refutable && report.non_exhaustiveness_witnesses.is_empty() {
         if !matches!(
             cx.tcx.lint_level_at_node(NON_EXHAUSTIVE_OMITTED_PATTERNS, lint_root).0,
             rustc_session::lint::Level::Allow
         ) {
             let witnesses = collect_nonexhaustive_missing_variants(cx, &pat_column);
-
             if !witnesses.is_empty() {
                 // Report that a match of a `non_exhaustive` enum marked with `non_exhaustive_omitted_patterns`
                 // is not exhaustive enough.
@@ -1230,5 +1386,5 @@ pub(crate) fn compute_match_usefulness<'p, 'tcx>(
         }
     }
 
-    UsefulnessReport { arm_usefulness, non_exhaustiveness_witnesses }
+    report
 }
diff --git a/tests/ui/pattern/usefulness/integer-ranges/reachability.rs b/tests/ui/pattern/usefulness/integer-ranges/reachability.rs
index fb4d59b0578..247fdd91572 100644
--- a/tests/ui/pattern/usefulness/integer-ranges/reachability.rs
+++ b/tests/ui/pattern/usefulness/integer-ranges/reachability.rs
@@ -9,9 +9,10 @@ macro_rules! m {
             $t2 => {}
             _ => {}
         }
-    }
+    };
 }
 
+#[rustfmt::skip]
 fn main() {
     m!(0u8, 42, 41);
     m!(0u8, 42, 42); //~ ERROR unreachable pattern
@@ -85,7 +86,7 @@ fn main() {
     match 'a' {
         '\u{0}'..='\u{D7FF}' => {},
         '\u{E000}'..='\u{10_FFFF}' => {},
-        '\u{D7FF}'..='\u{E000}' => {}, // FIXME should be unreachable
+        '\u{D7FF}'..='\u{E000}' => {}, //~ ERROR unreachable pattern
     }
 
     match (0u8, true) {
diff --git a/tests/ui/pattern/usefulness/integer-ranges/reachability.stderr b/tests/ui/pattern/usefulness/integer-ranges/reachability.stderr
index 0ffb0ffd82a..c5b028d2038 100644
--- a/tests/ui/pattern/usefulness/integer-ranges/reachability.stderr
+++ b/tests/ui/pattern/usefulness/integer-ranges/reachability.stderr
@@ -1,5 +1,5 @@
 error: unreachable pattern
-  --> $DIR/reachability.rs:17:17
+  --> $DIR/reachability.rs:18:17
    |
 LL |     m!(0u8, 42, 42);
    |                 ^^
@@ -11,127 +11,127 @@ LL | #![deny(unreachable_patterns)]
    |         ^^^^^^^^^^^^^^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:21:22
+  --> $DIR/reachability.rs:22:22
    |
 LL |     m!(0u8, 20..=30, 20);
    |                      ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:22:22
+  --> $DIR/reachability.rs:23:22
    |
 LL |     m!(0u8, 20..=30, 21);
    |                      ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:23:22
+  --> $DIR/reachability.rs:24:22
    |
 LL |     m!(0u8, 20..=30, 25);
    |                      ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:24:22
+  --> $DIR/reachability.rs:25:22
    |
 LL |     m!(0u8, 20..=30, 29);
    |                      ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:25:22
+  --> $DIR/reachability.rs:26:22
    |
 LL |     m!(0u8, 20..=30, 30);
    |                      ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:28:21
+  --> $DIR/reachability.rs:29:21
    |
 LL |     m!(0u8, 20..30, 20);
    |                     ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:29:21
+  --> $DIR/reachability.rs:30:21
    |
 LL |     m!(0u8, 20..30, 21);
    |                     ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:30:21
+  --> $DIR/reachability.rs:31:21
    |
 LL |     m!(0u8, 20..30, 25);
    |                     ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:31:21
+  --> $DIR/reachability.rs:32:21
    |
 LL |     m!(0u8, 20..30, 29);
    |                     ^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:35:22
+  --> $DIR/reachability.rs:36:22
    |
 LL |     m!(0u8, 20..=30, 20..=30);
    |                      ^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:36:22
+  --> $DIR/reachability.rs:37:22
    |
 LL |     m!(0u8, 20.. 30, 20.. 30);
    |                      ^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:37:22
+  --> $DIR/reachability.rs:38:22
    |
 LL |     m!(0u8, 20..=30, 20.. 30);
    |                      ^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:39:22
+  --> $DIR/reachability.rs:40:22
    |
 LL |     m!(0u8, 20..=30, 21..=30);
    |                      ^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:40:22
+  --> $DIR/reachability.rs:41:22
    |
 LL |     m!(0u8, 20..=30, 20..=29);
    |                      ^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:42:24
+  --> $DIR/reachability.rs:43:24
    |
 LL |     m!('a', 'A'..='z', 'a'..='z');
    |                        ^^^^^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:49:9
+  --> $DIR/reachability.rs:50:9
    |
 LL |         5..=8 => {},
    |         ^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:55:9
+  --> $DIR/reachability.rs:56:9
    |
 LL |         5..15 => {},
    |         ^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:62:9
+  --> $DIR/reachability.rs:63:9
    |
 LL |         5..25 => {},
    |         ^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:70:9
+  --> $DIR/reachability.rs:71:9
    |
 LL |         5..25 => {},
    |         ^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:76:9
+  --> $DIR/reachability.rs:77:9
    |
 LL |         5..15 => {},
    |         ^^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:83:9
+  --> $DIR/reachability.rs:84:9
    |
 LL |         _ => {},
    |         - matches any value
@@ -139,16 +139,22 @@ LL |         '\u{D7FF}'..='\u{E000}' => {},
    |         ^^^^^^^^^^^^^^^^^^^^^^^ unreachable pattern
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:104:9
+  --> $DIR/reachability.rs:89:9
+   |
+LL |         '\u{D7FF}'..='\u{E000}' => {},
+   |         ^^^^^^^^^^^^^^^^^^^^^^^
+
+error: unreachable pattern
+  --> $DIR/reachability.rs:105:9
    |
 LL |         &FOO => {}
    |         ^^^^
 
 error: unreachable pattern
-  --> $DIR/reachability.rs:105:9
+  --> $DIR/reachability.rs:106:9
    |
 LL |         BAR => {}
    |         ^^^
 
-error: aborting due to 24 previous errors
+error: aborting due to 25 previous errors