diff --git a/explorer/fuzzing/ast_to_proto.cpp b/explorer/fuzzing/ast_to_proto.cpp
index 336b3b7b3026..8b44f4be62df 100644
--- a/explorer/fuzzing/ast_to_proto.cpp
+++ b/explorer/fuzzing/ast_to_proto.cpp
@@ -13,6 +13,7 @@
 namespace Carbon {
 
 using ::llvm::cast;
+using ::llvm::dyn_cast;
 using ::llvm::isa;
 
 static auto ExpressionToProto(const Expression& expression)
@@ -481,9 +482,16 @@ static auto StatementToProto(const Statement& statement) -> Fuzzing::Statement {
           ExpressionToProto(match.expression());
       for (const Match::Clause& clause : match.clauses()) {
         auto* clause_proto = match_proto->add_clauses();
-        const bool is_default_clause =
-            clause.pattern().kind() == PatternKind::BindingPattern &&
-            cast<BindingPattern>(clause.pattern()).name() == AnonymousName;
+        // TODO: Working out whether we have a default clause after the fact
+        // like this is fragile.
+        bool is_default_clause = false;
+        if (auto* binding = dyn_cast<BindingPattern>(&clause.pattern())) {
+          if (binding->name() == AnonymousName &&
+              isa<AutoPattern>(binding->type()) &&
+              binding->source_loc() == binding->type().source_loc()) {
+            is_default_clause = true;
+          }
+        }
         if (is_default_clause) {
           clause_proto->set_is_default(true);
         } else {
diff --git a/explorer/interpreter/BUILD b/explorer/interpreter/BUILD
index 6aa3baa4b2c8..7a69670d03d1 100644
--- a/explorer/interpreter/BUILD
+++ b/explorer/interpreter/BUILD
@@ -177,6 +177,22 @@ cc_library(
     deps = ["//common:check"],
 )
 
+cc_library(
+    name = "pattern_analysis",
+    srcs = [
+        "pattern_analysis.cpp",
+    ],
+    hdrs = [
+        "pattern_analysis.h",
+    ],
+    deps = [
+        ":action_and_value",
+        "//common:error",
+        "//explorer/ast",
+        "//explorer/common:nonnull",
+        "@llvm-project//llvm:Support",
+    ],
+)
 cc_library(
     name = "type_checker",
     srcs = [
@@ -193,6 +209,7 @@ cc_library(
         ":action_and_value",
         ":dictionary",
         ":interpreter",
+        ":pattern_analysis",
         "//common:error",
         "//common:ostream",
         "//explorer/ast",
diff --git a/explorer/interpreter/pattern_analysis.cpp b/explorer/interpreter/pattern_analysis.cpp
new file mode 100644
index 000000000000..fa883658fdb7
--- /dev/null
+++ b/explorer/interpreter/pattern_analysis.cpp
@@ -0,0 +1,307 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "explorer/interpreter/pattern_analysis.h"
+
+#include <set>
+
+using llvm::cast;
+using llvm::dyn_cast;
+using llvm::isa;
+
+namespace Carbon {
+
+auto AbstractPattern::kind() const -> Kind {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    return Compound;
+  }
+  if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (isa<TupleValue, AlternativeValue, BoolValue>(value)) {
+      return Compound;
+    }
+    return Primitive;
+  }
+  CARBON_CHECK(value_.is<const WildcardTag*>());
+  return Wildcard;
+}
+
+auto AbstractPattern::discriminator() const -> std::string_view {
+  CARBON_CHECK(kind() == Compound);
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* alt_pattern = dyn_cast<AlternativePattern>(pattern)) {
+      return alt_pattern->alternative_name();
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      return alt->alt_name();
+    } else if (auto* bool_val = dyn_cast<BoolValue>(value)) {
+      return bool_val->value() ? "true" : "false";
+    }
+  }
+  return {};
+}
+
+auto AbstractPattern::elements_size() const -> int {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* tuple_pattern = dyn_cast<TuplePattern>(pattern)) {
+      return tuple_pattern->fields().size();
+    } else if (isa<AlternativePattern>(pattern)) {
+      return 1;
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* tuple = dyn_cast<TupleValue>(value)) {
+      return tuple->elements().size();
+    } else if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      return 1;
+    }
+  }
+  return 0;
+}
+
+void AbstractPattern::AppendElementsTo(
+    std::vector<AbstractPattern>& out) const {
+  if (auto* pattern = value_.dyn_cast<const Pattern*>()) {
+    if (auto* tuple_pattern = dyn_cast<TuplePattern>(pattern)) {
+      auto fields = tuple_pattern->fields();
+      out.insert(out.end(), fields.begin(), fields.end());
+    } else if (auto* alt_pattern = dyn_cast<AlternativePattern>(pattern)) {
+      out.push_back(&alt_pattern->arguments());
+    }
+  } else if (auto* value = value_.dyn_cast<const Value*>()) {
+    if (auto* tuple = dyn_cast<TupleValue>(value)) {
+      auto* tuple_type = cast<TupleValue>(type_);
+      CARBON_CHECK(tuple->elements().size() == tuple_type->elements().size());
+      for (size_t i = 0; i != tuple->elements().size(); ++i) {
+        out.push_back(
+            AbstractPattern(tuple->elements()[i], tuple_type->elements()[i]));
+      }
+    } else if (auto* alt = dyn_cast<AlternativeValue>(value)) {
+      out.push_back(AbstractPattern(
+          &alt->argument(),
+          *cast<ChoiceType>(type_)->FindAlternative(alt->alt_name())));
+    }
+  }
+}
+
+auto AbstractPattern::value() const -> const Value& {
+  CARBON_CHECK(kind() == Primitive);
+  return *value_.get<const Value*>();
+}
+
+auto AbstractPattern::type() const -> const Value& {
+  CARBON_CHECK(kind() != Wildcard);
+  return *type_;
+}
+
+void AbstractPattern::Set(Nonnull<const Pattern*> pattern) {
+  type_ = &pattern->static_type();
+  switch (pattern->kind()) {
+    case PatternKind::AddrPattern:
+    case PatternKind::AutoPattern:
+    case PatternKind::BindingPattern:
+    case PatternKind::GenericBinding:
+      value_ = static_cast<const WildcardTag*>(nullptr);
+      break;
+
+    case PatternKind::TuplePattern:
+    case PatternKind::AlternativePattern:
+      value_ = pattern;
+      break;
+
+    case PatternKind::ExpressionPattern:
+      value_ = &pattern->value();
+      break;
+
+    case PatternKind::VarPattern:
+      Set(&cast<VarPattern>(pattern)->pattern());
+      break;
+  }
+}
+
+auto PatternMatrix::IsUseful(llvm::ArrayRef<AbstractPattern> pattern,
+                             int max_exponential_depth) const -> bool {
+  if (matrix_.empty()) {
+    return true;
+  }
+
+  CARBON_CHECK(pattern.size() == matrix_[0].size());
+  if (matrix_[0].empty()) {
+    return false;
+  }
+
+  switch (pattern[0].kind()) {
+    case AbstractPattern::Wildcard: {
+      auto discrim = FirstColumnDiscriminators();
+      // Check if we hit the depth limit. If so, we act as if the
+      // constructors present in this position are not exhaustive, that is,
+      // as if the type we're matching has some other constructor not
+      // corresponding to anything written in the pattern in this position.
+      // This can lead us to conclude that a pattern is useful if it is not,
+      // and that a set of patterns is not exhaustive when it is.
+      int new_depth =
+          max_exponential_depth - (discrim.found.size() > 1 ? 1 : 0);
+      if (!discrim.any_missing && new_depth >= 0) {
+        for (auto found : discrim.found) {
+          if (Specialize(found).IsUseful(*SpecializeRow(pattern, found),
+                                         new_depth)) {
+            return true;
+          }
+        }
+        return false;
+      }
+      return Default().IsUseful(pattern.slice(1), max_exponential_depth);
+    }
+
+    case AbstractPattern::Compound: {
+      DiscriminatorInfo discrim = {.discriminator = pattern[0].discriminator(),
+                                   .size = pattern[0].elements_size()};
+      return Specialize(discrim).IsUseful(*SpecializeRow(pattern, discrim),
+                                          max_exponential_depth);
+    }
+
+    case AbstractPattern::Primitive: {
+      return Specialize(pattern[0].value())
+          .IsUseful(pattern.slice(1), max_exponential_depth);
+    }
+  }
+}
+
+auto PatternMatrix::FirstColumnDiscriminators() const -> DiscriminatorSet {
+  std::set<std::string_view> discrims;
+  std::optional<int> num_discrims;
+  std::optional<int> elem_size;
+
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        continue;
+      case AbstractPattern::Compound: {
+        const Value& type = row[0].type();
+        if (auto* tuple = dyn_cast<TupleValue>(&type)) {
+          // If we find a tuple match, we've found all constructors (there's
+          // only one!) and none were missing.
+          return {
+              .found = {{.discriminator = {},
+                         .size = static_cast<int>(tuple->elements().size())}},
+              .any_missing = false};
+        } else if (auto* choice = dyn_cast<ChoiceType>(&type)) {
+          num_discrims = choice->declaration().alternatives().size();
+          elem_size = 1;
+        } else if (isa<BoolType>(type)) {
+          // `bool` behaves like a choice type with two alternativs,
+          // and with no nested patterns for either of them.
+          num_discrims = 2;
+          elem_size = 0;
+        } else {
+          llvm_unreachable("unexpected compound type");
+        }
+        discrims.insert(row[0].discriminator());
+        break;
+      }
+      case AbstractPattern::Primitive: {
+        // We assume that primitive value matches are always incomplete, even
+        // for types like `i8` where a covering match might be possible.
+        return {.found = {}, .any_missing = true};
+      }
+    }
+  }
+
+  if (!num_discrims || *num_discrims != static_cast<int>(discrims.size())) {
+    return {.found = {}, .any_missing = true};
+  }
+
+  DiscriminatorSet result = {.found = {}, .any_missing = false};
+  result.found.reserve(discrims.size());
+  for (auto s : discrims) {
+    result.found.push_back({.discriminator = s, .size = *elem_size});
+  }
+  return result;
+}
+
+auto PatternMatrix::SpecializeRow(llvm::ArrayRef<AbstractPattern> row,
+                                  DiscriminatorInfo discriminator)
+    -> std::optional<std::vector<AbstractPattern>> {
+  CARBON_CHECK(!row.empty());
+  std::vector<AbstractPattern> new_row;
+  switch (row[0].kind()) {
+    case AbstractPattern::Wildcard:
+      new_row.reserve(discriminator.size + row.size() - 1);
+      new_row.insert(new_row.end(), discriminator.size,
+                     AbstractPattern::MakeWildcard());
+      break;
+    case AbstractPattern::Compound: {
+      if (row[0].discriminator() != discriminator.discriminator) {
+        return std::nullopt;
+      }
+      CARBON_CHECK(static_cast<int>(row[0].elements_size()) ==
+                   discriminator.size);
+      new_row.reserve(discriminator.size + row.size() - 1);
+      row[0].AppendElementsTo(new_row);
+      break;
+    }
+    case AbstractPattern::Primitive:
+      // These cases should be rejected by the type checker.
+      llvm_unreachable("matched primitive against compound");
+  }
+  new_row.insert(new_row.end(), row.begin() + 1, row.end());
+  return std::move(new_row);
+}
+
+auto PatternMatrix::Specialize(DiscriminatorInfo discriminator) const
+    -> PatternMatrix {
+  PatternMatrix specialized;
+  for (auto& row : matrix_) {
+    // TODO: If we add support for "or" patterns, specialization might
+    // produce multiple rows here.
+    if (auto new_row = SpecializeRow(row, discriminator)) {
+      specialized.Add(std::move(new_row.value()));
+    }
+  }
+  return specialized;
+}
+
+// Specialize the pattern matrix for the case where the first value is known
+// to be `value`, and is not matched.
+auto PatternMatrix::Specialize(const Value& value) const -> PatternMatrix {
+  PatternMatrix specialized;
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        break;
+      case AbstractPattern::Compound:
+        llvm_unreachable("matched compound against primitive");
+      case AbstractPattern::Primitive:
+        // TODO: Use an equality context here?
+        if (!ValueEqual(&row[0].value(), &value, std::nullopt)) {
+          continue;
+        }
+        break;
+    }
+    specialized.Add(std::vector<AbstractPattern>(row.begin() + 1, row.end()));
+  }
+  return specialized;
+}
+
+// Specialize the pattern matrix for the case where the first value uses a
+// discriminator matching none of the non-wildcard patterns.
+auto PatternMatrix::Default() const -> PatternMatrix {
+  PatternMatrix default_matrix;
+  for (auto& row : matrix_) {
+    CARBON_CHECK(!row.empty());
+    switch (row[0].kind()) {
+      case AbstractPattern::Wildcard:
+        default_matrix.Add(
+            std::vector<AbstractPattern>(row.begin() + 1, row.end()));
+        break;
+      case AbstractPattern::Compound:
+      case AbstractPattern::Primitive:
+        break;
+    }
+  }
+  return default_matrix;
+}
+
+}  // namespace Carbon
diff --git a/explorer/interpreter/pattern_analysis.h b/explorer/interpreter/pattern_analysis.h
new file mode 100644
index 000000000000..ef0da52dca2d
--- /dev/null
+++ b/explorer/interpreter/pattern_analysis.h
@@ -0,0 +1,162 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_
+#define CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_
+
+#include <vector>
+
+#include "explorer/ast/pattern.h"
+#include "explorer/common/nonnull.h"
+#include "explorer/interpreter/value.h"
+#include "llvm/ADT/PointerUnion.h"
+
+namespace Carbon {
+
+// An abstracted view of a pattern or constant value (which we view as a
+// particular kind of pattern).
+class AbstractPattern {
+ public:
+  enum Kind {
+    // A pattern that matches anything.
+    Wildcard,
+    // A pattern that matches a compound value with sub-patterns to match
+    // elements. A compound value is modeled as a discriminator name applied to
+    // a sequence of nested values: the alternative `Optional.Element(E)` has
+    // discriminator `Element` and nested value `E`, and the tuple `(A,B,C)`
+    // has an empty discriminator and nested values `A`, `B`, and `C`.
+    Compound,
+    // A pattern that matches a particular primitive value.
+    Primitive
+  };
+
+  // This is intentionally implicit to allow easy conversion from a container
+  // of `const Pattern*` to a container of `AbstractPattern`s.
+  // NOLINTNEXTLINE(google-explicit-constructor)
+  AbstractPattern(Nonnull<const Pattern*> pattern) { Set(pattern); }
+
+  AbstractPattern(Nonnull<const Value*> value, Nonnull<const Value*> type)
+      : value_(value), type_(type) {}
+
+  // Make a match-anything wildcard pattern.
+  static auto MakeWildcard() -> AbstractPattern {
+    return AbstractPattern(WildcardTag());
+  }
+
+  // Get the kind for this pattern.
+  auto kind() const -> Kind;
+
+  // Get the type, for a non-wildcard pattern.
+  auto type() const -> const Value&;
+
+  // Get the discriminator used for a compound pattern.
+  auto discriminator() const -> std::string_view;
+
+  // Get the number of nested patterns for a compound pattern.
+  auto elements_size() const -> int;
+
+  // Append the nested patterns in this compound pattern to `out`.
+  void AppendElementsTo(std::vector<AbstractPattern>& out) const;
+
+  // Get the value for a primitive pattern.
+  auto value() const -> const Value&;
+
+ private:
+  // This is aligned so that we can use it in the `PointerUnion` below.
+  struct alignas(8) WildcardTag {};
+  AbstractPattern(WildcardTag)
+      : value_(static_cast<const WildcardTag*>(nullptr)), type_(nullptr) {}
+
+  void Set(Nonnull<const Pattern*> pattern);
+
+  // The underlying pattern: either a syntactic pattern, or a constant value,
+  // or a placeholder indicating that this is a wildcard pattern.
+  llvm::PointerUnion<Nonnull<const Pattern*>, Nonnull<const Value*>,
+                     const WildcardTag*>
+      value_;
+  // Values don't always know their types, so store the type here. We only
+  // really need it for the `const Value*` case but also store it for the
+  // `const Pattern*` case for convenience.
+  const Value* type_;
+};
+
+// A matrix of patterns, used for determining exhaustiveness and redundancy of
+// patterns in a match statement.
+//
+// See http://moscova.inria.fr/~maranget/papers/warn/index.html for details on
+// the algorithm used here.
+class PatternMatrix {
+ public:
+  // Add a pattern vector row to this collection of pattern vectors.
+  void Add(std::vector<AbstractPattern> pattern_vector) {
+    CARBON_CHECK(matrix_.empty() || matrix_[0].size() == pattern_vector.size());
+    matrix_.push_back(std::move(pattern_vector));
+  }
+
+  // Returns true if the given pattern vector is redundant if it appears after
+  // the patterns in this matrix. That is, if it will never match following the
+  // other patterns because everything it matches is matched by some other
+  // pattern.
+  auto IsRedundant(llvm::ArrayRef<AbstractPattern> pattern) const -> bool {
+    return !IsUseful(pattern, MaxExponentialDepth);
+  }
+
+ private:
+  // The maximum number of times we will consider all alternatives when
+  // recursively expanding the pattern. Allowing this to happen an arbitrary
+  // number of times leads to exponential growth in the runtime of the
+  // algorithm.
+  static constexpr int MaxExponentialDepth = 8;
+
+  // Information about a constructor for a compound type.
+  struct DiscriminatorInfo {
+    // For an alternative, the name. Otherwise, empty.
+    std::string_view discriminator;
+    // The number of elements. For a tuple, the size. Always 1 for an
+    // alternative.
+    int size;
+  };
+
+  struct DiscriminatorSet {
+    std::vector<DiscriminatorInfo> found;
+    bool any_missing;
+  };
+
+  // Determine whether the given pattern vector is useful: that is, whether
+  // adding it to the matrix would allow any more values to be matched.
+  auto IsUseful(llvm::ArrayRef<AbstractPattern> pattern,
+                int max_exponential_depth) const -> bool;
+
+  // Find the discriminators used by the first column and check whether we
+  // found all of them.
+  auto FirstColumnDiscriminators() const -> DiscriminatorSet;
+
+  // Specialize the pattern vector `row` for the case that the first value
+  // matched uses `discriminator`.
+  static auto SpecializeRow(llvm::ArrayRef<AbstractPattern> row,
+                            DiscriminatorInfo discriminator)
+      -> std::optional<std::vector<AbstractPattern>>;
+
+  // Specialize the pattern matrix for the case that the first value matched
+  // uses `discriminator`, and its elements are matched.
+  auto Specialize(DiscriminatorInfo discriminator) const -> PatternMatrix;
+
+  // Specialize the pattern matrix for the case where the first value is known
+  // to be `value`, and is not matched.
+  auto Specialize(const Value& value) const -> PatternMatrix;
+
+  // Specialize the pattern matrix for the case where the first value uses a
+  // discriminator matching none of the non-wildcard patterns.
+  auto Default() const -> PatternMatrix;
+
+  // The pattern matrix itself, in row-major order. Each element of `matrix_`
+  // is a distinct sequence of patterns that can be matched against a
+  // corresponding sequence of values. Each such row has the same length and
+  // has elements of the same type.
+  std::vector<std::vector<AbstractPattern>> matrix_;
+};
+
+}  // namespace Carbon
+
+#endif  // CARBON_EXPLORER_INTERPRETER_PATTERN_ANALYSIS_H_
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index c55038c82ada..0260096e2a68 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -17,6 +17,7 @@
 #include "explorer/common/error_builders.h"
 #include "explorer/interpreter/impl_scope.h"
 #include "explorer/interpreter/interpreter.h"
+#include "explorer/interpreter/pattern_analysis.h"
 #include "explorer/interpreter/value.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/StringExtras.h"
@@ -2933,6 +2934,7 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
       CARBON_RETURN_IF_ERROR(TypeCheckExp(&match.expression(), impl_scope));
       std::vector<Match::Clause> new_clauses;
       std::optional<Nonnull<const Value*>> expected_type;
+      PatternMatrix patterns;
       for (auto& clause : match.clauses()) {
         ImplScope clause_scope;
         clause_scope.AddParent(&impl_scope);
@@ -2953,6 +2955,12 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
         } else {
           expected_type = &clause.pattern().static_type();
         }
+        if (patterns.IsRedundant({&clause.pattern()})) {
+          return CompilationError(clause.pattern().source_loc())
+                 << "unreachable case: all values matched by this case "
+                 << "are matched by earlier cases";
+        }
+        patterns.Add({&clause.pattern()});
         CARBON_RETURN_IF_ERROR(
             TypeCheckStmt(&clause.statement(), clause_scope));
       }
@@ -3130,17 +3138,12 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
 
 // Returns true if we can statically verify that `match` is exhaustive, meaning
 // that one of its clauses will be executed for any possible operand value.
-//
-// TODO: the current rule is an extremely simplistic placeholder, with
-// many false negatives.
 static auto IsExhaustive(const Match& match) -> bool {
+  PatternMatrix matrix;
   for (const Match::Clause& clause : match.clauses()) {
-    // A pattern consisting of a single variable binding is guaranteed to match.
-    if (clause.pattern().kind() == PatternKind::BindingPattern) {
-      return true;
-    }
+    matrix.Add({&clause.pattern()});
   }
-  return false;
+  return matrix.IsRedundant({AbstractPattern::MakeWildcard()});
 }
 
 auto TypeChecker::ExpectReturnOnAllPaths(
diff --git a/explorer/testdata/function/fail_non_exhaustive_match.carbon b/explorer/testdata/function/fail_non_exhaustive_match.carbon
index 067d12976fc2..98d0a95cb851 100644
--- a/explorer/testdata/function/fail_non_exhaustive_match.carbon
+++ b/explorer/testdata/function/fail_non_exhaustive_match.carbon
@@ -11,7 +11,8 @@
 package ExplorerTest api;
 
 fn Main() -> i32 {
-  match (0) {
+  var n: i32 = 0;
+  match (n) {
     case 1 => { return 0; }
   }
 // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/function/fail_non_exhaustive_match.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
diff --git a/explorer/testdata/function/non_exhaustive_match_no_return_type.carbon b/explorer/testdata/function/non_exhaustive_match_no_return_type.carbon
new file mode 100644
index 000000000000..3d2440130947
--- /dev/null
+++ b/explorer/testdata/function/non_exhaustive_match_no_return_type.carbon
@@ -0,0 +1,24 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+fn F(n: i32) {
+  match (n) {
+    case 1 => { return; }
+  }
+  // No diagnostic: this is reachable but that's OK.
+}
+
+fn Main() -> i32 {
+  F(0);
+  return 0;
+}
diff --git a/explorer/testdata/function/non_exhaustive_match_return.carbon b/explorer/testdata/function/non_exhaustive_match_return.carbon
new file mode 100644
index 000000000000..54c900b2e8c0
--- /dev/null
+++ b/explorer/testdata/function/non_exhaustive_match_return.carbon
@@ -0,0 +1,20 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 1
+
+package ExplorerTest api;
+
+fn Main() -> i32 {
+  var n: i32 = 0;
+  match (n) {
+    case 1 => { return 0; }
+  }
+  return 1;
+}
diff --git a/explorer/testdata/match/exhaustive.carbon b/explorer/testdata/match/exhaustive.carbon
new file mode 100644
index 000000000000..b79650c3ed58
--- /dev/null
+++ b/explorer/testdata/match/exhaustive.carbon
@@ -0,0 +1,37 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 3
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    case (Opt.None(), Opt.None()) => { return 0; }
+  }
+}
+
+fn B(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.None(), _: auto) => { return 0; }
+    case (Opt.Some(n: i32), Opt.None()) => { return n; }
+    case (Opt.Some(n: i32), Opt.Some(m: i32)) => { return n + m; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1)) + B(Opt.Some(2), Opt.None());
+}
diff --git a/explorer/testdata/match/exhaustive_bool.carbon b/explorer/testdata/match/exhaustive_bool.carbon
new file mode 100644
index 000000000000..7d6b4ae77e32
--- /dev/null
+++ b/explorer/testdata/match/exhaustive_bool.carbon
@@ -0,0 +1,23 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 2
+
+package ExplorerTest api;
+
+fn A(b: bool) -> i32 {
+  match (b) {
+    case false => { return 1; }
+    case true => { return 2; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(true);
+}
diff --git a/explorer/testdata/match/exhaustive_exponential_8x.carbon b/explorer/testdata/match/exhaustive_exponential_8x.carbon
new file mode 100644
index 000000000000..3db0d472a176
--- /dev/null
+++ b/explorer/testdata/match/exhaustive_exponential_8x.carbon
@@ -0,0 +1,33 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  match ((F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 1; }
+    case (_: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 3; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 8; }
+  }
+}
diff --git a/explorer/testdata/match/exhaustive_exponential_series_t.carbon b/explorer/testdata/match/exhaustive_exponential_series_t.carbon
new file mode 100644
index 000000000000..2a322eb43230
--- /dev/null
+++ b/explorer/testdata/match/exhaustive_exponential_series_t.carbon
@@ -0,0 +1,41 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+// CHECK: result: 0
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // This is T8 from http://moscova.inria.fr/~maranget/papers/warn/warn014.html
+  match ((F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 1; }
+    case (_: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 3; }
+    case (_: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B()) => { return 9; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A()) => { return 10; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B()) => { return 11; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A()) => { return 12; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B()) => { return 13; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A()) => { return 14; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 15; }
+  }
+}
diff --git a/explorer/testdata/match/fail_exhaustive_exponential_9x.carbon b/explorer/testdata/match/fail_exhaustive_exponential_9x.carbon
new file mode 100644
index 000000000000..97de14d82782
--- /dev/null
+++ b/explorer/testdata/match/fail_exhaustive_exponential_9x.carbon
@@ -0,0 +1,35 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // Note, this match is exhaustive, but it exceeds our depth limit.
+  match ((F(), F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 1; }
+    case (_: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 3; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A(), AB.A()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 9; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_exponential_9x.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
diff --git a/explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon b/explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon
new file mode 100644
index 000000000000..1447d7f9ad66
--- /dev/null
+++ b/explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon
@@ -0,0 +1,44 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice AB {
+  A(),
+  B()
+}
+
+fn F() -> AB { return AB.A(); }
+
+fn Main() -> i32 {
+  // This is T9 from http://moscova.inria.fr/~maranget/papers/warn/warn014.html
+  // Note, this match is exhaustive, but it exceeds our depth limit.
+  match ((F(), F(), F(), F(), F(), F(), F(), F(), F())) {
+    case (AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 0; }
+    case (AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 1; }
+    case (_: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 2; }
+    case (_: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 3; }
+    case (_: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 4; }
+    case (_: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 5; }
+    case (_: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 6; }
+    case (_: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 7; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A(), AB.A()) => { return 8; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B(), AB.B()) => { return 9; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A(), AB.A()) => { return 10; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B(), AB.B()) => { return 11; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A(), AB.A()) => { return 12; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B(), AB.B()) => { return 13; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A(), AB.A()) => { return 14; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B(), AB.B()) => { return 15; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.A()) => { return 16; }
+    case (_: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  _: AB,  AB.B()) => { return 17; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_exponential_series_t.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
diff --git a/explorer/testdata/match/fail_exhaustive_int.carbon b/explorer/testdata/match/fail_exhaustive_int.carbon
new file mode 100644
index 000000000000..c77e9a20a25d
--- /dev/null
+++ b/explorer/testdata/match/fail_exhaustive_int.carbon
@@ -0,0 +1,23 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+fn A(n: i32) -> i32 {
+  match (n) {
+    case 1 => { return 1; }
+    case 2 => { return 2; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_exhaustive_int.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
+
+fn Main() -> i32 {
+  return A(0);
+}
diff --git a/explorer/testdata/match/fail_not_exhaustive.carbon b/explorer/testdata/match/fail_not_exhaustive.carbon
new file mode 100644
index 000000000000..cb882ba1a43e
--- /dev/null
+++ b/explorer/testdata/match/fail_not_exhaustive.carbon
@@ -0,0 +1,28 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+  }
+// CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_exhaustive.carbon:[[@LINE+1]]: non-exhaustive match may allow control-flow to reach the end of a function that provides a `->` return type
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}
diff --git a/explorer/testdata/match/fail_not_reachable.carbon b/explorer/testdata/match/fail_not_reachable.carbon
new file mode 100644
index 000000000000..89e42a1f9fad
--- /dev/null
+++ b/explorer/testdata/match/fail_not_reachable.carbon
@@ -0,0 +1,30 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_reachable.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    case (Opt.Some(m: i32), Opt.Some(n: i32)) => { return m + n; }
+  }
+  return 0;
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}
diff --git a/explorer/testdata/match/fail_not_reachable_default.carbon b/explorer/testdata/match/fail_not_reachable_default.carbon
new file mode 100644
index 000000000000..596b00cfe06a
--- /dev/null
+++ b/explorer/testdata/match/fail_not_reachable_default.carbon
@@ -0,0 +1,31 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+choice Opt {
+  None(),
+  Some(i32)
+}
+
+fn A(a: Opt, b: Opt) -> i32 {
+  match ((a, b)) {
+    case (Opt.None(), Opt.None()) => { return 0; }
+    case (Opt.Some(n: i32), _: auto) => { return n; }
+    case (_: auto, Opt.Some(n: i32)) => { return n; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_not_reachable_default.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    default => { return -1; }
+  }
+  return 0;
+}
+
+fn Main() -> i32 {
+  return A(Opt.None(), Opt.Some(1));
+}
diff --git a/explorer/testdata/match/fail_redundant_int.carbon b/explorer/testdata/match/fail_redundant_int.carbon
new file mode 100644
index 000000000000..144ae4176bfc
--- /dev/null
+++ b/explorer/testdata/match/fail_redundant_int.carbon
@@ -0,0 +1,24 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// RUN: %{not} %{explorer} %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
+// RUN: %{not} %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
+// RUN:   %{FileCheck} --match-full-lines --allow-unused-prefixes %s
+// AUTOUPDATE: %{explorer} %s
+
+package ExplorerTest api;
+
+fn A(n: i32) -> i32 {
+  match (n) {
+    case 1 => { return 1; }
+    // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/match/fail_redundant_int.carbon:[[@LINE+1]]: unreachable case: all values matched by this case are matched by earlier cases
+    case 1 => { return 2; }
+    case (_: i32) => { return 3; }
+  }
+}
+
+fn Main() -> i32 {
+  return A(1);
+}