diff --git a/fathom/src/core.rs b/fathom/src/core.rs
index 47e154773..b61cba6ad 100644
--- a/fathom/src/core.rs
+++ b/fathom/src/core.rs
@@ -1,6 +1,8 @@
 //! Core language.
 
-use crate::env::{Index, Level};
+use scoped_arena::Scope;
+
+use crate::env::{EnvLen, Index, Level};
 use crate::source::{Span, StringId};
 
 pub mod binary;
@@ -185,6 +187,10 @@ pub enum Term<'arena> {
 }
 
 impl<'arena> Term<'arena> {
+    pub fn error(span: Span) -> Self {
+        Self::Prim(span, Prim::ReportedError)
+    }
+
     /// Get the source span of the term.
     pub fn span(&self) -> Span {
         match self {
@@ -255,6 +261,149 @@ impl<'arena> Term<'arena> {
             }
         }
     }
+
+    // TODO: Add a new `Weaken` variant to `core::Term` instead of eagerly traversing the term?
+    pub fn shift(&self, scope: &'arena Scope<'arena>, amount: EnvLen) -> Term<'arena> {
+        self.shift_inner(scope, Index::last(), amount)
+    }
+
+    /// Increment all `LocalVar`s greater than or equal to `min` by `amount`
+    fn shift_inner(
+        &self,
+        scope: &'arena Scope<'arena>,
+        mut min: Index,
+        amount: EnvLen,
+    ) -> Term<'arena> {
+        // Skip traversing and rebuilding the term if it would make no change. Increases sharing.
+        if amount == EnvLen::new() {
+            return self.clone();
+        }
+
+        match self {
+            Term::LocalVar(span, var) if *var >= min => Term::LocalVar(*span, *var + amount),
+            Term::LocalVar(..)
+            | Term::ItemVar(..)
+            | Term::MetaVar(..)
+            | Term::InsertedMeta(..)
+            | Term::Prim(..)
+            | Term::ConstLit(..)
+            | Term::Universe(..) => self.clone(),
+            Term::Ann(span, expr, r#type) => Term::Ann(
+                *span,
+                scope.to_scope(expr.shift_inner(scope, min, amount)),
+                scope.to_scope(r#type.shift_inner(scope, min, amount)),
+            ),
+            Term::Let(span, name, def_type, def_expr, body) => Term::Let(
+                *span,
+                *name,
+                scope.to_scope(def_type.shift_inner(scope, min, amount)),
+                scope.to_scope(def_expr.shift_inner(scope, min, amount)),
+                scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunType(span, name, input, output) => Term::FunType(
+                *span,
+                *name,
+                scope.to_scope(input.shift_inner(scope, min, amount)),
+                scope.to_scope(output.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunLit(span, name, body) => Term::FunLit(
+                *span,
+                *name,
+                scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunApp(span, fun, arg) => Term::FunApp(
+                *span,
+                scope.to_scope(fun.shift_inner(scope, min, amount)),
+                scope.to_scope(arg.shift_inner(scope, min, amount)),
+            ),
+            Term::RecordType(span, labels, types) => Term::RecordType(
+                *span,
+                labels,
+                scope.to_scope_from_iter(types.iter().map(|r#type| {
+                    let ret = r#type.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::RecordLit(span, labels, exprs) => Term::RecordLit(
+                *span,
+                labels,
+                scope.to_scope_from_iter(
+                    exprs
+                        .iter()
+                        .map(|expr| expr.shift_inner(scope, min, amount)),
+                ),
+            ),
+            Term::RecordProj(span, head, label) => Term::RecordProj(
+                *span,
+                scope.to_scope(head.shift_inner(scope, min, amount)),
+                *label,
+            ),
+            Term::ArrayLit(span, terms) => Term::ArrayLit(
+                *span,
+                scope.to_scope_from_iter(
+                    terms
+                        .iter()
+                        .map(|term| term.shift_inner(scope, min, amount)),
+                ),
+            ),
+            Term::FormatRecord(span, labels, terms) => Term::FormatRecord(
+                *span,
+                labels,
+                scope.to_scope_from_iter(terms.iter().map(|term| {
+                    let ret = term.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::FormatCond(span, name, format, pred) => Term::FormatCond(
+                *span,
+                *name,
+                scope.to_scope(format.shift_inner(scope, min, amount)),
+                scope.to_scope(pred.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FormatOverlap(span, labels, terms) => Term::FormatOverlap(
+                *span,
+                labels,
+                scope.to_scope_from_iter(terms.iter().map(|term| {
+                    let ret = term.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::ConstMatch(span, scrut, branches, default) => Term::ConstMatch(
+                *span,
+                scope.to_scope(scrut.shift_inner(scope, min, amount)),
+                scope.to_scope_from_iter(
+                    branches
+                        .iter()
+                        .map(|(r#const, term)| (*r#const, term.shift_inner(scope, min, amount))),
+                ),
+                default.map(|(name, term)| {
+                    (
+                        name,
+                        scope.to_scope(term.shift_inner(scope, min.prev(), amount)) as &_,
+                    )
+                }),
+            ),
+        }
+    }
+
+    /// Returns `true` if `self` can be evaluated in a single step.
+    /// Used as a heuristic to prevent increase in runtime when expanding pattern matches
+    pub fn is_atomic(&self) -> bool {
+        match self {
+            Term::ItemVar(_, _)
+            | Term::LocalVar(_, _)
+            | Term::MetaVar(_, _)
+            | Term::InsertedMeta(_, _, _)
+            | Term::Universe(_)
+            | Term::Prim(_, _)
+            | Term::ConstLit(_, _) => true,
+            Term::RecordProj(_, head, _) => head.is_atomic(),
+            _ => false,
+        }
+    }
 }
 
 macro_rules! def_prims {
@@ -572,6 +721,21 @@ pub enum Const {
     Ref(usize),
 }
 
+impl Const {
+    /// Return the number of inhabitants of `self`.
+    /// `None` represents infinity
+    pub fn num_inhabitants(&self) -> Option<u128> {
+        match self {
+            Const::Bool(_) => Some(2),
+            Const::U8(_, _) | Const::S8(_) => Some(1 << 8),
+            Const::U16(_, _) | Const::S16(_) => Some(1 << 16),
+            Const::U32(_, _) | Const::S32(_) => Some(1 << 32),
+            Const::U64(_, _) | Const::S64(_) => Some(1 << 64),
+            Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None,
+        }
+    }
+}
+
 impl PartialEq for Const {
     fn eq(&self, other: &Self) -> bool {
         match (*self, *other) {
diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs
index e92d1ea0b..e5b1eb7c3 100644
--- a/fathom/src/core/semantics.rs
+++ b/fathom/src/core/semantics.rs
@@ -52,6 +52,8 @@ pub enum Value<'arena> {
 }
 
 impl<'arena> Value<'arena> {
+    pub const ERROR: Self = Self::Stuck(Head::Prim(Prim::ReportedError), Vec::new());
+
     pub fn prim(prim: Prim, params: impl IntoIterator<Item = ArcValue<'arena>>) -> Value<'arena> {
         let params = params.into_iter().map(Elim::FunApp).collect();
         Value::Stuck(Head::Prim(prim), params)
@@ -71,6 +73,13 @@ impl<'arena> Value<'arena> {
             _ => None,
         }
     }
+
+    pub fn as_record_type(&self) -> Option<&Telescope<'arena>> {
+        match self {
+            Value::RecordType(_, telescope) => Some(telescope),
+            _ => None,
+        }
+    }
 }
 
 /// The head of a [stuck value][Value::Stuck].
diff --git a/fathom/src/env.rs b/fathom/src/env.rs
index d3adfe341..23d9e743e 100644
--- a/fathom/src/env.rs
+++ b/fathom/src/env.rs
@@ -17,7 +17,7 @@
 //! and [`SliceEnv`], but when we need to copy environments often, we use a
 //! [`SharedEnv`] to increase the amount of sharing at the expense of locality.
 
-use std::fmt;
+use std::{fmt, ops::Add};
 
 /// Underlying variable representation.
 type RawVar = u16;
@@ -56,6 +56,13 @@ impl Index {
     }
 }
 
+impl Add<EnvLen> for Index {
+    type Output = Self;
+    fn add(self, rhs: EnvLen) -> Self::Output {
+        Self(self.0 + rhs.0) // FIXME: check overflow?
+    }
+}
+
 impl fmt::Debug for Index {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         write!(f, "Index(")?;
@@ -140,6 +147,10 @@ impl EnvLen {
         Level(self.0)
     }
 
+    pub fn next(&self) -> EnvLen {
+        Self(self.0 + 1) // FIXME: check overflow?
+    }
+
     /// Push an entry onto the environment.
     pub fn push(&mut self) {
         self.0 += 1; // FIXME: check overflow?
diff --git a/fathom/src/surface/distillation.rs b/fathom/src/surface/distillation.rs
index 8572a9e4d..5d77a5da8 100644
--- a/fathom/src/surface/distillation.rs
+++ b/fathom/src/surface/distillation.rs
@@ -311,11 +311,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 core::Const::Ref(number) => self.check_number_literal(number),
             },
             core::Term::ConstMatch(_span, head_expr, branches, default_branch) => {
-                if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_branch)
+                if let Some(((then_name, then_expr), (else_name, else_expr))) =
+                    match_if_then_else(branches, *default_branch)
                 {
                     let cond_expr = self.check(head_expr);
-                    let then_expr = self.check(then_expr);
-                    let else_expr = self.check(else_expr);
+
+                    let then_expr = match then_name {
+                        None => self.check(then_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let then_expr = self.check(then_expr);
+                            self.pop_local();
+                            then_expr
+                        }
+                    };
+
+                    let else_expr = match else_name {
+                        None => self.check(else_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let else_expr = self.check(else_expr);
+                            self.pop_local();
+                            else_expr
+                        }
+                    };
+
                     return Term::If(
                         (),
                         self.scope.to_scope(cond_expr),
@@ -373,11 +393,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
         match core_term {
             core::Term::ItemVar(_span, var) => match self.get_item_name(*var) {
                 Some(name) => Term::Name((), name),
-                None => todo!("misbound variable"), // TODO: error?
+                None => panic!("misbound item variable: {var:?}"),
             },
             core::Term::LocalVar(_span, var) => match self.get_local_name(*var) {
                 Some(name) => Term::Name((), name),
-                None => todo!("misbound variable"), // TODO: error?
+                None => panic!("Unbound local variable: {var:?}"),
             },
             core::Term::MetaVar(_span, var) => match self.get_hole_name(*var) {
                 Some(name) => Term::Hole((), name),
@@ -643,10 +663,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 core::Const::Ref(number) => self.synth_number_literal(number, core::Prim::RefType),
             },
             core::Term::ConstMatch(_span, head_expr, branches, default_expr) => {
-                if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_expr) {
+                if let Some(((then_name, then_expr), (else_name, else_expr))) =
+                    match_if_then_else(branches, *default_expr)
+                {
                     let cond_expr = self.check(head_expr);
-                    let then_expr = self.synth(then_expr);
-                    let else_expr = self.synth(else_expr);
+
+                    let then_expr = match then_name {
+                        None => self.synth(then_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let then_expr = self.synth(then_expr);
+                            self.pop_local();
+                            then_expr
+                        }
+                    };
+
+                    let else_expr = match else_name {
+                        None => self.synth(else_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let else_expr = self.synth(else_expr);
+                            self.pop_local();
+                            else_expr
+                        }
+                    };
+
                     return Term::If(
                         (),
                         self.scope.to_scope(cond_expr),
@@ -772,15 +813,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
     }
 }
 
+#[allow(clippy::type_complexity)]
 fn match_if_then_else<'arena>(
     branches: &'arena [(Const, core::Term<'arena>)],
     default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
-) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
+) -> Option<(
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+)> {
     match (branches, default_branch) {
-        ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None)
-        // TODO: Normalise boolean branches when elaborating patterns
-        | ([(Const::Bool(true), then_expr)], Some((_, else_expr)))
-        | ([(Const::Bool(false), else_expr)], Some((_, then_expr))) => Some((then_expr, else_expr)),
+        ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) => {
+            Some(((None, then_expr), (None, else_expr)))
+        }
+        ([(Const::Bool(true), then_expr)], Some((name, else_expr))) => {
+            Some(((None, then_expr), (Some(name), else_expr)))
+        }
+        ([(Const::Bool(false), else_expr)], Some((name, then_expr))) => {
+            Some(((Some(name), then_expr), (None, else_expr)))
+        }
         _ => None,
     }
 }
diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs
index 9f0e6a4f7..6cfa839a4 100644
--- a/fathom/src/surface/elaboration.rs
+++ b/fathom/src/surface/elaboration.rs
@@ -33,6 +33,8 @@ use crate::source::{ByteRange, Span, Spanned, StringId, StringInterner};
 use crate::surface::elaboration::reporting::Message;
 use crate::surface::{distillation, pretty, BinOp, FormatField, Item, Module, Pattern, Term};
 
+use self::patterns::{CheckedPattern, PatMatrix, PatternMode};
+
 mod order;
 mod patterns;
 mod reporting;
@@ -117,6 +119,10 @@ impl<'arena> LocalEnv<'arena> {
         self.names.len()
     }
 
+    fn next_var(&self) -> ArcValue<'arena> {
+        Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level())))
+    }
+
     fn reserve(&mut self, additional: usize) {
         self.names.reserve(additional);
         self.types.reserve(additional);
@@ -138,17 +144,15 @@ impl<'arena> LocalEnv<'arena> {
     }
 
     /// Push a local parameter onto the context.
-    fn push_param(&mut self, name: Option<StringId>, r#type: ArcValue<'arena>) -> ArcValue<'arena> {
+    fn push_param(&mut self, name: Option<StringId>, r#type: ArcValue<'arena>) {
         // An expression that refers to itself once it is pushed onto the local
         // expression environment.
-        let expr = Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level())));
+        let expr = self.next_var();
 
         self.names.push(name);
         self.types.push(r#type);
         self.infos.push(core::LocalInfo::Param);
         self.exprs.push(expr.clone());
-
-        expr
     }
 
     /// Pop a local binder off the context.
@@ -765,26 +769,12 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
     /// The supplied `pattern` is expected to be irrefutable.
     fn push_local_def(
         &mut self,
-        pattern: CheckedPattern,
-        expr: ArcValue<'arena>,
+        pattern: &CheckedPattern<'arena>,
+        value: ArcValue<'arena>,
         r#type: ArcValue<'arena>,
     ) -> Option<StringId> {
-        let name = match pattern {
-            CheckedPattern::Binder(_, name) => Some(name),
-            CheckedPattern::Placeholder(_) => None,
-            // FIXME: generate failing parameter expressions?
-            CheckedPattern::ConstLit(range, _) => {
-                self.push_message(Message::RefutablePattern {
-                    pattern_range: range,
-                });
-                None
-            }
-            CheckedPattern::ReportedError(_) => None,
-            CheckedPattern::RecordLit(_, _, _) => todo!(),
-        };
-
-        self.local_env.push_def(name, expr, r#type);
-
+        let name = pattern.name();
+        self.push_pattern(pattern, value, r#type, PatternMode::Let);
         name
     }
 
@@ -792,26 +782,13 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
     /// The supplied `pattern` is expected to be irrefutable.
     fn push_local_param(
         &mut self,
-        pattern: CheckedPattern,
+        pattern: &CheckedPattern<'arena>,
         r#type: ArcValue<'arena>,
     ) -> (Option<StringId>, ArcValue<'arena>) {
-        let name = match pattern {
-            CheckedPattern::Binder(_, name) => Some(name),
-            CheckedPattern::Placeholder(_) => None,
-            // FIXME: generate failing parameter expressions?
-            CheckedPattern::ConstLit(range, _) => {
-                self.push_message(Message::RefutablePattern {
-                    pattern_range: range,
-                });
-                None
-            }
-            CheckedPattern::ReportedError(_) => None,
-            CheckedPattern::RecordLit(_, _, _) => todo!(),
-        };
-
-        let expr = self.local_env.push_param(name, r#type);
-
-        (name, expr)
+        let name = pattern.name();
+        let value = self.local_env.next_var();
+        self.push_pattern(pattern, value.clone(), r#type, PatternMode::Fun);
+        (name, value)
     }
 
     /// Check that a surface term conforms to the given type.
@@ -827,21 +804,52 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         match (surface_term, expected_type.as_ref()) {
             (Term::Let(range, def_pattern, def_type, def_expr, body_expr), _) => {
                 let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
-                let def_type = self.quote_env().quote(self.scope, &def_type_value);
-                let def_expr = self.check(def_expr, &def_type_value);
-                let def_expr_value = self.eval_env().eval(&def_expr);
+                let mut scrut = self.check_scrutinee(def_expr, def_type_value.clone());
+                let value = self.eval_env().eval(scrut.expr);
+
+                // Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
+                // and may be evaluated multiple times by the pattern match compiler
+                let extra_def = match (scrut.expr.is_atomic(), def_pattern.is_atomic()) {
+                    (false, false) => {
+                        let def_name = None; // TODO: generate a fresh name
+                        let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
+                        let def_expr = scrut.expr.clone();
+
+                        let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
+                        scrut.expr = self.scope.to_scope(var);
+                        (self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
+                        Some((def_name, def_type, def_expr))
+                    }
+                    _ => None,
+                };
 
-                let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants
+                let initial_len = self.local_env.len();
+                self.push_local_def(&def_pattern, value, scrut.r#type.clone());
                 let body_expr = self.check(body_expr, &expected_type);
-                self.local_env.pop();
-
-                core::Term::Let(
-                    range.into(),
-                    def_name,
-                    self.scope.to_scope(def_type),
-                    self.scope.to_scope(def_expr),
-                    self.scope.to_scope(body_expr),
-                )
+                self.local_env.truncate(initial_len);
+
+                let matrix = PatMatrix::singleton(scrut, def_pattern);
+                let expr = self.elab_match(
+                    matrix,
+                    &[body_expr],
+                    *range,
+                    def_expr.range(),
+                    PatternMode::Let,
+                );
+                let expr = match extra_def {
+                    None => expr,
+                    Some((def_name, def_type, def_expr)) => {
+                        self.local_env.pop();
+                        core::Term::Let(
+                            range.into(),
+                            def_name,
+                            self.scope.to_scope(def_type),
+                            self.scope.to_scope(def_expr),
+                            self.scope.to_scope(expr),
+                        )
+                    }
+                };
+                expr
             }
             (Term::If(range, cond_expr, then_expr, else_expr), _) => {
                 let cond_expr = self.check(cond_expr, &self.bool_type.clone());
@@ -1133,23 +1141,52 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
             }
             Term::Let(range, def_pattern, def_type, def_expr, body_expr) => {
                 let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
-                let def_type = self.quote_env().quote(self.scope, &def_type_value);
-                let def_expr = self.check(def_expr, &def_type_value);
-                let def_expr_value = self.eval_env().eval(&def_expr);
+                let mut scrut = self.check_scrutinee(def_expr, def_type_value.clone());
+                let value = self.eval_env().eval(scrut.expr);
+
+                // Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
+                // and may be evaluated multiple times by the pattern match compiler
+                let extra_def = match (scrut.expr.is_atomic(), def_pattern.is_atomic()) {
+                    (false, false) => {
+                        let def_name = None; // TODO: generate a fresh name
+                        let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
+                        let def_expr = scrut.expr.clone();
+
+                        let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
+                        scrut.expr = self.scope.to_scope(var);
+                        (self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
+                        Some((def_name, def_type, def_expr))
+                    }
+                    _ => None,
+                };
 
-                let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value);
+                let initial_len = self.local_env.len();
+                self.push_local_def(&def_pattern, value, scrut.r#type.clone());
                 let (body_expr, body_type) = self.synth(body_expr);
-                self.local_env.pop();
-
-                let let_expr = core::Term::Let(
-                    range.into(),
-                    def_name,
-                    self.scope.to_scope(def_type),
-                    self.scope.to_scope(def_expr),
-                    self.scope.to_scope(body_expr),
+                self.local_env.truncate(initial_len);
+
+                let matrix = patterns::PatMatrix::singleton(scrut, def_pattern);
+                let expr = self.elab_match(
+                    matrix,
+                    &[body_expr],
+                    *range,
+                    def_expr.range(),
+                    PatternMode::Let,
                 );
-
-                (let_expr, body_type)
+                let expr = match extra_def {
+                    None => expr,
+                    Some((def_name, def_type, def_expr)) => {
+                        self.local_env.pop();
+                        core::Term::Let(
+                            range.into(),
+                            def_name,
+                            self.scope.to_scope(def_type),
+                            self.scope.to_scope(def_expr),
+                            self.scope.to_scope(expr),
+                        )
+                    }
+                };
+                (expr, body_type)
             }
             Term::If(range, cond_expr, then_expr, else_expr) => {
                 let cond_expr = self.check(cond_expr, &self.bool_type.clone());
@@ -1194,35 +1231,41 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                     self.scope.to_scope(body_type),
                 );
 
-                (fun_type, self.universe.clone())
+                (fun_type, universe)
             }
             Term::FunType(range, patterns, body_type) => {
-                self.local_env.reserve(patterns.len());
-                let initial_local_len = self.local_env.len();
+                let universe = self.universe.clone();
+                let initial_len = self.local_env.len();
 
                 // Elaborate the parameters, collecting them in a stack
                 let mut params = Vec::with_capacity(patterns.len());
-                for (pattern, r#type) in *patterns {
-                    let (pattern, type_value) = self.synth_ann_pattern(pattern, *r#type);
-                    let r#type = self.quote_env().quote(self.scope, &type_value);
-                    let (name, _) = self.push_local_param(pattern, type_value);
-                    params.push((name, r#type));
+                for (pattern, r#type) in patterns.iter() {
+                    let (pattern, scrut) = self.synth_param(pattern, *r#type);
+                    let input_type_expr = self.quote_env().quote(self.scope, &scrut.r#type);
+                    let (name, _) = self.push_local_param(&pattern, scrut.r#type.clone());
+                    params.push((name, input_type_expr, pattern, scrut));
                 }
 
-                let mut fun_type = self.check(body_type, &self.universe.clone());
-                self.local_env.truncate(initial_local_len);
+                let mut fun_type = self.check(body_type, &universe);
+                self.local_env.truncate(initial_len);
 
                 // Construct the function type from the parameters in reverse
-                for (name, r#type) in params.into_iter().rev() {
+                for (name, input_type, pattern, scrut) in params.into_iter().rev() {
+                    self.local_env.push_param(None, scrut.r#type.clone());
+                    let matrix = PatMatrix::singleton(scrut, pattern);
+                    fun_type =
+                        self.elab_match(matrix, &[fun_type], *range, *range, PatternMode::Fun);
+                    self.local_env.pop();
+
                     fun_type = core::Term::FunType(
                         range.into(), // FIXME
                         name,
-                        self.scope.to_scope(r#type),
+                        self.scope.to_scope(input_type),
                         self.scope.to_scope(fun_type),
                     );
                 }
 
-                (fun_type, self.universe.clone())
+                (fun_type, universe)
             }
             Term::FunLiteral(range, patterns, body_expr) => {
                 self.synth_fun_lit(*range, patterns, body_expr, None)
@@ -1451,7 +1494,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
     fn check_fun_lit(
         &mut self,
         range: ByteRange,
-        patterns: &[(Pattern<ByteRange>, Option<&Term<'_, ByteRange>>)],
+        patterns: &[(Pattern<'_, ByteRange>, Option<&Term<'_, ByteRange>>)],
         body_expr: &Term<'_, ByteRange>,
         expected_type: &ArcValue<'arena>,
     ) -> core::Term<'arena> {
@@ -1461,12 +1504,25 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                 match body_type.as_ref() {
                     Value::FunType(_, param_type, next_body_type) => {
                         let range = ByteRange::merge(&pattern.range(), &body_expr.range()).unwrap();
-                        let pattern = self.check_ann_pattern(pattern, *r#type, param_type);
-                        let (name, arg_expr) = self.push_local_param(pattern, param_type.clone());
+                        let (pattern, scrut) = self.check_param(pattern, *r#type, param_type);
+                        let scrut_range = scrut.range;
 
+                        let initial_len = self.local_env.len();
+                        let (name, arg_expr) = self.push_local_param(&pattern, param_type.clone());
                         let body_type = self.elim_env().apply_closure(next_body_type, arg_expr);
                         let body_expr =
                             self.check_fun_lit(range, next_patterns, body_expr, &body_type);
+                        self.local_env.truncate(initial_len);
+
+                        self.local_env.push_param(None, scrut.r#type.clone());
+                        let matrix = PatMatrix::singleton(scrut, pattern.clone());
+                        let body_expr = self.elab_match(
+                            matrix,
+                            &[body_expr],
+                            range,
+                            scrut_range,
+                            PatternMode::Fun,
+                        );
                         self.local_env.pop();
 
                         core::Term::FunLit(range.into(), name, self.scope.to_scope(body_expr))
@@ -1499,24 +1555,24 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
     fn synth_fun_lit(
         &mut self,
         range: ByteRange,
-        patterns: &[(Pattern<ByteRange>, Option<&Term<ByteRange>>)],
+        patterns: &[(Pattern<'_, ByteRange>, Option<&Term<ByteRange>>)],
         body_expr: &Term<'_, ByteRange>,
         body_type: Option<&Term<'_, ByteRange>>,
     ) -> (core::Term<'arena>, ArcValue<'arena>) {
         self.local_env.reserve(patterns.len());
-        let initial_local_len = self.local_env.len();
+        let initial_len = self.local_env.len();
 
         // Elaborate the parameters, collecting them into a stack
         let mut params = Vec::with_capacity(patterns.len());
-        for (i, (pattern, r#type)) in patterns.iter().enumerate() {
-            let range = match i {
+        for (index, (pattern, r#type)) in patterns.iter().enumerate() {
+            let range = match index {
                 0 => range, // The first pattern uses the range of the full function literal
                 _ => ByteRange::merge(&pattern.range(), &body_expr.range()).unwrap(),
             };
-            let (pattern, type_value) = self.synth_ann_pattern(pattern, *r#type);
-            let r#type = self.quote_env().quote(self.scope, &type_value);
-            let (name, _) = self.push_local_param(pattern, type_value);
-            params.push((range, name, r#type));
+            let (pattern, scrut) = self.synth_param(pattern, *r#type);
+            let r#type = self.quote_env().quote(self.scope, &scrut.r#type);
+            let (name, _) = self.push_local_param(&pattern, scrut.r#type.clone());
+            params.push((range, name, r#type, pattern, scrut));
         }
 
         let (mut fun_lit, mut fun_type) = match body_type {
@@ -1531,10 +1587,22 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
             }
         };
 
-        self.local_env.truncate(initial_local_len);
+        self.local_env.truncate(initial_len);
 
         // Construct the function literal and type from the parameters in reverse
-        for (range, name, r#type) in params.into_iter().rev() {
+        for (range, name, r#type, pattern, scrut) in params.into_iter().rev() {
+            self.local_env.push_param(None, scrut.r#type.clone());
+            let matrix = PatMatrix::singleton(scrut.clone(), pattern.clone());
+            fun_lit = self.elab_match(
+                matrix.clone(),
+                &[fun_lit],
+                range,
+                scrut.range,
+                PatternMode::Fun,
+            );
+            fun_type = self.elab_match(matrix, &[fun_type], range, scrut.range, PatternMode::Fun);
+            self.local_env.pop();
+
             fun_lit = core::Term::FunLit(range.into(), name, self.scope.to_scope(fun_lit));
             fun_type = core::Term::FunType(
                 Span::Empty,
@@ -1808,13 +1876,68 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         equations: &[(Pattern<ByteRange>, Term<'_, ByteRange>)],
         expected_type: &ArcValue<'arena>,
     ) -> core::Term<'arena> {
-        let match_info = MatchInfo {
-            range,
-            scrutinee: self.synth_scrutinee(scrutinee_expr),
-            expected_type: self.elim_env().force(expected_type),
+        let expected_type = self.elim_env().force(expected_type);
+        let mut scrut = self.synth_scrutinee(scrutinee_expr);
+        let value = self.eval_env().eval(scrut.expr);
+
+        let patterns: Vec<_> = equations
+            .iter()
+            .map(|(pat, _)| self.check_pattern(pat, &scrut.r#type))
+            .collect();
+
+        // Bind the scrut to a fresh variable if it is unsafe to evaluate multiple times,
+        // and may be evaluated multiple times by the pattern match compiler
+        let extra_def = match (
+            scrut.expr.is_atomic(),
+            patterns.iter().all(|pat| pat.is_atomic()),
+        ) {
+            (false, false) => {
+                let def_name = None; // TODO: generate a fresh name
+                let def_type = self.quote_env().quote(self.scope, &scrut.r#type);
+                let def_expr = scrut.expr.clone();
+
+                let var = core::Term::LocalVar(def_expr.span(), env::Index::last());
+                scrut.expr = self.scope.to_scope(var);
+                (self.local_env).push_def(def_name, value.clone(), scrut.r#type.clone());
+                Some((def_name, def_type, def_expr))
+            }
+            _ => None,
         };
 
-        self.elab_match(&match_info, true, equations.iter())
+        let mut rows = Vec::with_capacity(equations.len());
+        let mut exprs = Vec::with_capacity(equations.len());
+
+        for (pattern, (_, expr)) in patterns.into_iter().zip(equations) {
+            let initial_len = self.local_env.len();
+            self.push_pattern(
+                &pattern,
+                value.clone(),
+                scrut.r#type.clone(),
+                PatternMode::Match,
+            );
+            let expr = self.check(expr, &expected_type);
+            self.local_env.truncate(initial_len);
+
+            rows.push(patterns::PatRow::singleton((pattern, scrut.clone())));
+            exprs.push(expr);
+        }
+
+        let matrix = patterns::PatMatrix::new(rows);
+        let expr = self.elab_match(matrix, &exprs, range, scrut.range, PatternMode::Match);
+        let expr = match extra_def {
+            None => expr,
+            Some((def_name, def_type, def_expr)) => {
+                self.local_env.pop();
+                core::Term::Let(
+                    range.into(),
+                    def_name,
+                    self.scope.to_scope(def_type),
+                    self.scope.to_scope(def_expr),
+                    self.scope.to_scope(expr),
+                )
+            }
+        };
+        expr
     }
 
     fn synth_scrutinee(&mut self, scrutinee_expr: &Term<'_, ByteRange>) -> Scrutinee<'arena> {
@@ -1826,219 +1949,61 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         }
     }
 
-    /// Elaborate a pattern match into a case tree in the core language.
-    ///
-    /// The implementation is based on the algorithm described in Section 5 of
-    /// [“The Implementation of Functional Programming Languages”][impl-fpl].
-    ///
-    /// [impl-fpl]: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/
-    fn elab_match<'a>(
+    fn check_scrutinee(
         &mut self,
-        match_info: &MatchInfo<'arena>,
-        is_reachable: bool,
-        mut equations: impl Iterator<Item = &'a (Pattern<'a, ByteRange>, Term<'a, ByteRange>)>,
-    ) -> core::Term<'arena> {
-        match equations.next() {
-            Some((pattern, body_expr)) => {
-                match self.check_pattern(pattern, &match_info.scrutinee.r#type) {
-                    // Named patterns are elaborated to let bindings, where the
-                    // scrutinee is bound as a definition in the body expression.
-                    // Subsequent patterns are unreachable.
-                    CheckedPattern::Binder(range, name) => {
-                        self.check_match_reachable(is_reachable, range);
-
-                        let def_name = Some(name);
-                        let def_expr = self.eval_env().eval(match_info.scrutinee.expr);
-                        let def_type_value = match_info.scrutinee.r#type.clone();
-                        let def_type = self.quote_env().quote(self.scope, &def_type_value);
-
-                        self.local_env.push_def(def_name, def_expr, def_type_value);
-                        let body_expr = self.check(body_expr, &match_info.expected_type);
-                        self.local_env.pop();
-
-                        self.elab_match_unreachable(match_info, equations);
-
-                        core::Term::Let(
-                            Span::merge(&range.into(), &body_expr.span()),
-                            def_name,
-                            self.scope.to_scope(def_type),
-                            match_info.scrutinee.expr,
-                            self.scope.to_scope(body_expr),
-                        )
-                    }
-                    // Placeholder patterns just elaborate to the body
-                    // expression. Subsequent patterns are unreachable.
-                    CheckedPattern::Placeholder(range) => {
-                        self.check_match_reachable(is_reachable, range);
-
-                        let body_expr = self.check(body_expr, &match_info.expected_type);
-                        self.elab_match_unreachable(match_info, equations);
-
-                        body_expr
-                    }
-                    // If we see a constant pattern we should expect a run of
-                    // constants, elaborating to a constant elimination.
-                    CheckedPattern::ConstLit(range, r#const) => {
-                        self.check_match_reachable(is_reachable, range);
-
-                        let body_expr = self.check(body_expr, &match_info.expected_type);
-                        let const_equation = (range, r#const, body_expr);
-
-                        self.elab_match_const(match_info, is_reachable, const_equation, equations)
-                    }
-                    // If we hit an error, propagate it, while still checking
-                    // the body expression and the subsequent branches.
-                    CheckedPattern::ReportedError(range) => {
-                        self.check(body_expr, &match_info.expected_type);
-                        self.elab_match_unreachable(match_info, equations);
-                        core::Term::Prim(range.into(), Prim::ReportedError)
-                    }
-                    CheckedPattern::RecordLit(_, _, _) => todo!(),
-                }
-            }
-            None => self.elab_match_absurd(is_reachable, match_info),
-        }
-    }
-
-    /// Ensure that this part of a match expression is reachable, reporting
-    /// a message if it is not.
-    fn check_match_reachable(&mut self, is_reachable: bool, range: ByteRange) {
-        if !is_reachable {
-            self.push_message(Message::UnreachablePattern { range });
+        scrutinee_expr: &Term<'_, ByteRange>,
+        expected_type: ArcValue<'arena>,
+    ) -> Scrutinee<'arena> {
+        let expr = self.check(scrutinee_expr, &expected_type);
+        Scrutinee {
+            range: scrutinee_expr.range(),
+            expr: self.scope.to_scope(expr),
+            r#type: expected_type,
         }
     }
 
-    /// Elaborate the equations, expecting a series of constant patterns
-    fn elab_match_const<'a>(
+    fn synth_param(
         &mut self,
-        match_info: &MatchInfo<'arena>,
-        is_reachable: bool,
-        (const_range, r#const, body_expr): (ByteRange, Const, core::Term<'arena>),
-        mut equations: impl Iterator<Item = &'a (Pattern<'a, ByteRange>, Term<'a, ByteRange>)>,
-    ) -> core::Term<'arena> {
-        // The full range of this series of patterns
-        let mut full_span = Span::merge(&const_range.into(), &body_expr.span());
-        // Temporary vector for accumulating branches
-        let mut branches = vec![(r#const, body_expr)];
-
-        // Elaborate a run of constant patterns.
-        'patterns: while let Some((pattern, body_expr)) = equations.next() {
-            // Update the range up to the end of the next body expression
-            full_span = Span::merge(&full_span, &body_expr.range().into());
-
-            // Default expression, defined if we arrive at a default case
-            let default_branch;
-
-            match self.check_pattern(pattern, &match_info.scrutinee.r#type) {
-                // Accumulate constant pattern. Search for it in the accumulated
-                // branches and insert it in order.
-                CheckedPattern::ConstLit(range, r#const) => {
-                    let body_expr = self.check(body_expr, &match_info.expected_type);
-
-                    // Find insertion index of the branch
-                    let insertion_index = branches.binary_search_by(|(probe_const, _)| {
-                        Const::partial_cmp(probe_const, &r#const)
-                            .expect("attempt to compare non-ordered value")
-                    });
-
-                    match insertion_index {
-                        Ok(_) => self.push_message(Message::UnreachablePattern { range }),
-                        Err(index) => {
-                            // This has not yet been covered, so it should be reachable.
-                            self.check_match_reachable(is_reachable, range);
-                            branches.insert(index, (r#const, body_expr));
-                        }
-                    }
-
-                    // No default case yet, continue looking for constant patterns.
-                    continue 'patterns;
-                }
-
-                // Time to elaborate the default pattern. The default case of
-                // `core::Term::ConstMatch` binds a variable, so both
-                // the named and  placeholder patterns should bind this.
-                CheckedPattern::Binder(range, name) => {
-                    self.check_match_reachable(is_reachable, range);
-
-                    // TODO: If we know this is an exhaustive match, bind the
-                    // scrutinee to a let binding with the elaborated body, and
-                    // add it to the branches. This will simplify the
-                    // distillation of if expressions.
-                    (self.local_env).push_param(Some(name), match_info.scrutinee.r#type.clone());
-                    let default_expr = self.check(body_expr, &match_info.expected_type);
-                    default_branch = (Some(name), self.scope.to_scope(default_expr) as &_);
-                    self.local_env.pop();
-                }
-                CheckedPattern::Placeholder(range) => {
-                    self.check_match_reachable(is_reachable, range);
-
-                    (self.local_env).push_param(None, match_info.scrutinee.r#type.clone());
-                    let default_expr = self.check(body_expr, &match_info.expected_type);
-                    default_branch = (None, self.scope.to_scope(default_expr) as &_);
-                    self.local_env.pop();
-                }
-                CheckedPattern::ReportedError(range) => {
-                    (self.local_env).push_param(None, match_info.scrutinee.r#type.clone());
-                    let default_expr = core::Term::Prim(range.into(), Prim::ReportedError);
-                    default_branch = (None, self.scope.to_scope(default_expr) as &_);
-                    self.local_env.pop();
-                }
-                CheckedPattern::RecordLit(_, _, _) => todo!(),
-            };
-
-            // A default pattern was found, check any unreachable patterns.
-            self.elab_match_unreachable(match_info, equations);
-
-            return core::Term::ConstMatch(
-                full_span,
-                match_info.scrutinee.expr,
-                self.scope.to_scope_from_iter(branches.into_iter()),
-                Some(default_branch),
-            );
-        }
-
-        // Finished all the constant patterns without encountering a default
-        // case. This should have been an exhaustive match, so check to see if
-        // all the cases were covered.
-        let default_expr = match match_info.scrutinee.r#type.match_prim_spine() {
-            // No need for a default case if all the values were covered
-            Some((Prim::BoolType, [])) if branches.len() >= 2 => None,
-            _ => Some(self.elab_match_absurd(is_reachable, match_info)),
+        pattern: &Pattern<'_, ByteRange>,
+        r#type: Option<&Term<'_, ByteRange>>,
+    ) -> (CheckedPattern<'arena>, Scrutinee<'arena>) {
+        let (pattern, r#type) = self.synth_ann_pattern(pattern, r#type);
+        let expr = core::Term::LocalVar(pattern.range().into(), env::Index::last());
+        let scrut = Scrutinee {
+            range: pattern.range(),
+            expr: self.scope.to_scope(expr),
+            r#type,
         };
-
-        core::Term::ConstMatch(
-            full_span,
-            match_info.scrutinee.expr,
-            self.scope.to_scope_from_iter(branches.into_iter()),
-            default_expr.map(|expr| (None, self.scope.to_scope(expr) as &_)),
-        )
+        (pattern, scrut)
     }
 
-    /// Elaborate unreachable match cases. This is useful for that these cases
-    /// are correctly typed, even if they are never actually needed.
-    fn elab_match_unreachable<'a>(
+    fn check_param(
         &mut self,
-        match_info: &MatchInfo<'arena>,
-        equations: impl Iterator<Item = &'a (Pattern<'a, ByteRange>, Term<'a, ByteRange>)>,
-    ) {
-        self.elab_match(match_info, false, equations);
+        pattern: &Pattern<'_, ByteRange>,
+        r#type: Option<&Term<'_, ByteRange>>,
+        expected_type: &ArcValue<'arena>,
+    ) -> (CheckedPattern<'arena>, Scrutinee<'arena>) {
+        let pattern = self.check_ann_pattern(pattern, r#type, expected_type);
+        let expr = core::Term::LocalVar(pattern.range().into(), env::Index::last());
+        let scrut = Scrutinee {
+            range: pattern.range(),
+            expr: self.scope.to_scope(expr),
+            r#type: expected_type.clone(),
+        };
+        (pattern, scrut)
     }
 
-    /// All the equations have been consumed.
-    fn elab_match_absurd(
+    fn elab_match(
         &mut self,
-        is_reachable: bool,
-        match_info: &MatchInfo<'arena>,
+        mut matrix: PatMatrix<'arena>,
+        exprs: &[core::Term<'arena>],
+        match_range: ByteRange,
+        scrut_range: ByteRange,
+        mode: PatternMode,
     ) -> core::Term<'arena> {
-        // Report if we can still reach this point
-        if is_reachable {
-            // TODO: this should be admitted if the scrutinee type is uninhabited
-            self.push_message(Message::NonExhaustiveMatchExpr {
-                match_expr_range: match_info.range,
-                scrutinee_expr_range: match_info.scrutinee.range,
-            });
-        }
-        core::Term::Prim(match_info.range.into(), Prim::ReportedError)
+        debug_assert_eq!(matrix.num_rows(), exprs.len());
+        patterns::check_coverage(self, &matrix, match_range, scrut_range);
+        patterns::compile_match(self, &mut matrix, exprs, mode, EnvLen::new())
     }
 }
 
@@ -2062,33 +2027,10 @@ impl_from_str_radix!(u16);
 impl_from_str_radix!(u32);
 impl_from_str_radix!(u64);
 
-/// Simple patterns that have had some initial elaboration performed on them
-#[derive(Debug)]
-enum CheckedPattern<'arena> {
-    /// Error sentinel
-    ReportedError(ByteRange),
-    /// Placeholder patterns that match everything
-    Placeholder(ByteRange),
-    /// Pattern that binds local variable
-    Binder(ByteRange, StringId),
-    /// Constant literals
-    ConstLit(ByteRange, Const),
-    /// Record literals
-    RecordLit(ByteRange, &'arena [StringId], &'arena [Self]),
-}
-
 /// Scrutinee of a match expression
-struct Scrutinee<'arena> {
+#[derive(Debug, Clone)]
+pub struct Scrutinee<'arena> {
     range: ByteRange,
     expr: &'arena core::Term<'arena>,
     r#type: ArcValue<'arena>,
 }
-
-struct MatchInfo<'arena> {
-    /// The full range of the match expression
-    range: ByteRange,
-    /// The expression being matched on
-    scrutinee: Scrutinee<'arena>,
-    /// The expected type of the match arms
-    expected_type: ArcValue<'arena>,
-}
diff --git a/fathom/src/surface/elaboration/patterns.rs b/fathom/src/surface/elaboration/patterns.rs
index 60cb99228..587b12fc0 100644
--- a/fathom/src/surface/elaboration/patterns.rs
+++ b/fathom/src/surface/elaboration/patterns.rs
@@ -1,4 +1,77 @@
 use super::*;
+use crate::surface::elaboration;
+
+mod compile;
+mod coverage;
+
+pub use self::compile::compile_match;
+pub use self::coverage::check_coverage;
+
+/// Simple patterns that have had some initial elaboration performed on them
+#[derive(Debug, Clone)]
+pub enum CheckedPattern<'arena> {
+    /// Error sentinel
+    ReportedError(ByteRange),
+    /// Placeholder patterns that match everything
+    Placeholder(ByteRange),
+    /// Pattern that binds local variable
+    Binder(ByteRange, StringId),
+    /// Constant literals
+    ConstLit(ByteRange, Const),
+    /// Record literals
+    RecordLit(ByteRange, &'arena [StringId], &'arena [Self]),
+}
+
+impl<'arena> CheckedPattern<'arena> {
+    pub fn range(&self) -> ByteRange {
+        match self {
+            CheckedPattern::ReportedError(range)
+            | CheckedPattern::Placeholder(range)
+            | CheckedPattern::Binder(range, _)
+            | CheckedPattern::ConstLit(range, _)
+            | CheckedPattern::RecordLit(range, _, _) => *range,
+        }
+    }
+
+    pub fn name(&self) -> Option<StringId> {
+        match self {
+            CheckedPattern::Binder(_, name) => Some(*name),
+            _ => None,
+        }
+    }
+
+    /// Returns `true` if `self` will always sucessfully match its scrutinee
+    pub fn is_wildcard(&self) -> bool {
+        match self {
+            CheckedPattern::ReportedError(_)
+            | CheckedPattern::Placeholder(_)
+            | CheckedPattern::Binder(_, _) => true,
+            CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => false,
+        }
+    }
+
+    /// Returns `true` if `self` binds its scrutinee exactly once.
+    /// Used as a heuristic to prevent increase in runtime when expanding pattern matches
+    pub fn is_atomic(&self) -> bool {
+        match self {
+            CheckedPattern::ReportedError(_)
+            | CheckedPattern::Placeholder(_)
+            | CheckedPattern::Binder(_, _)
+            | CheckedPattern::ConstLit(_, _) => true,
+            CheckedPattern::RecordLit(_, _, patterns) => {
+                patterns.len() == 1 && patterns[0].is_atomic()
+            }
+        }
+    }
+}
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum PatternMode {
+    Fun,
+    Let,
+    Match,
+    MatchInner,
+}
 
 impl<'interner, 'arena> Context<'interner, 'arena> {
     /// Check that a pattern matches an expected type.
@@ -278,4 +351,348 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
             }
         }
     }
+
+    pub(super) fn push_pattern(
+        &mut self,
+        pattern: &CheckedPattern<'arena>,
+        value: ArcValue<'arena>,
+        r#type: ArcValue<'arena>,
+        mode: PatternMode,
+    ) {
+        match pattern {
+            CheckedPattern::ReportedError(_) => match mode {
+                PatternMode::Fun => self.local_env.push_param(None, r#type),
+                PatternMode::Let => self.local_env.push_def(None, value, r#type),
+                PatternMode::Match => self.local_env.push_def(None, value, r#type),
+                PatternMode::MatchInner => {}
+            },
+            CheckedPattern::Placeholder(_) => match mode {
+                PatternMode::Fun => self.local_env.push_param(None, r#type),
+                PatternMode::Let => self.local_env.push_def(None, value, r#type),
+                PatternMode::Match => self.local_env.push_def(None, value, r#type),
+                PatternMode::MatchInner => {}
+            },
+            CheckedPattern::Binder(_, name) => match mode {
+                PatternMode::Fun => self.local_env.push_param(Some(*name), r#type),
+                PatternMode::Let => self.local_env.push_def(Some(*name), value, r#type),
+                PatternMode::Match => self.local_env.push_def(Some(*name), value, r#type),
+                PatternMode::MatchInner => self.local_env.push_def(Some(*name), value, r#type),
+            },
+            CheckedPattern::ConstLit(_, _) => match mode {
+                PatternMode::Fun => self.local_env.push_param(None, r#type),
+                PatternMode::Let => self.local_env.push_def(None, value, r#type),
+                PatternMode::Match => {}
+                PatternMode::MatchInner => {}
+            },
+            CheckedPattern::RecordLit(_, labels, patterns) => {
+                if mode == PatternMode::Fun {
+                    self.local_env.push_param(None, r#type.clone())
+                }
+
+                let mut iter = Iterator::zip(labels.iter(), patterns.iter());
+                let mut telescope = self
+                    .elim_env()
+                    .force(&r#type)
+                    .as_record_type()
+                    .unwrap()
+                    .clone();
+                while let Some(((label, pattern), (r#type, next_telescope))) = Option::zip(
+                    iter.next(),
+                    self.elim_env().split_telescope(telescope.clone()),
+                ) {
+                    telescope = next_telescope(self.local_env.next_var());
+                    self.push_pattern(
+                        pattern,
+                        self.elim_env().record_proj(value.clone(), *label),
+                        r#type,
+                        PatternMode::MatchInner,
+                    )
+                }
+            }
+        }
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
+pub enum Constructor<'arena> {
+    Const(Const),
+    Record(&'arena [StringId]),
+}
+
+impl<'arena> Constructor<'arena> {
+    /// Return number of fields `self` carries
+    pub fn arity(&self) -> usize {
+        match self {
+            Constructor::Const(_) => 0,
+            Constructor::Record(labels) => labels.len(),
+        }
+    }
+
+    pub fn is_exhaustive(ctors: &[Constructor]) -> bool {
+        match ctors.first() {
+            None => false,
+            Some(ctor) => match ctor.num_inhabitants() {
+                None => false,
+                Some(n) => ctors.len() as u128 >= n,
+            },
+        }
+    }
+
+    /// Return the number of inhabitants of `self`.
+    /// `None` represents infinity
+    pub fn num_inhabitants(&self) -> Option<u128> {
+        match self {
+            Constructor::Const(r#const) => r#const.num_inhabitants(),
+            Constructor::Record(_) => Some(1),
+        }
+    }
+
+    pub fn as_const(&self) -> Option<&Const> {
+        match self {
+            Constructor::Const(r#const) => Some(r#const),
+            _ => None,
+        }
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct PatMatrix<'arena> {
+    rows: Vec<PatRow<'arena>>,
+    bodies: Vec<Body<'arena>>,
+}
+
+#[derive(Debug, Clone)]
+pub struct Body<'arena> {
+    index: usize,
+    defs: Vec<(Option<StringId>, Scrutinee<'arena>)>,
+}
+
+impl<'arena> PatMatrix<'arena> {
+    pub fn new(rows: Vec<PatRow<'arena>>) -> Self {
+        if let Some((first, rows)) = rows.split_first() {
+            for row in rows {
+                debug_assert_eq!(
+                    first.pairs.len(),
+                    row.pairs.len(),
+                    "All rows must be same length"
+                );
+            }
+        }
+        let bodies = (0..rows.len())
+            .map(|index| Body {
+                index,
+                defs: Vec::new(),
+            })
+            .collect();
+        Self { rows, bodies }
+    }
+
+    pub fn singleton(scrut: Scrutinee<'arena>, pat: CheckedPattern<'arena>) -> Self {
+        Self::new(vec![PatRow::singleton((pat, scrut))])
+    }
+
+    pub fn num_rows(&self) -> usize {
+        self.rows.len()
+    }
+
+    pub fn num_columns(&self) -> Option<usize> {
+        self.rows.first().map(|row| row.len())
+    }
+
+    /// Return true if `self` is the null matrix, `∅` - ie `self` has zero rows
+    pub fn is_null(&self) -> bool {
+        self.num_rows() == 0
+    }
+
+    /// Return true if `self` is the unit matrix, `()` - ie `self` has zero columns and at least one row
+    pub fn is_unit(&self) -> bool {
+        self.num_columns() == Some(0)
+    }
+
+    /// Iterate over all the pairs in the `index`th column
+    pub fn column(&self, index: usize) -> impl ExactSizeIterator<Item = &PatPair<'arena>> + '_ {
+        self.rows.iter().map(move |row| &row.pairs[index])
+    }
+
+    pub fn row(&self, index: usize) -> &PatRow<'arena> {
+        &self.rows[index]
+    }
+
+    pub fn body(&self, index: usize) -> &Body<'arena> {
+        &self.bodies[index]
+    }
+
+    /// Collect all the `Constructor`s in the `index`th column
+    pub fn column_constructors(&self, index: usize) -> Vec<Constructor> {
+        let mut ctors = Vec::with_capacity(self.num_rows());
+        for (pat, _) in self.column(index) {
+            match pat {
+                CheckedPattern::ReportedError(_)
+                | CheckedPattern::Placeholder(_)
+                | CheckedPattern::Binder(_, _) => continue,
+                CheckedPattern::ConstLit(_, r#const) => ctors.push(Constructor::Const(*r#const)),
+                CheckedPattern::RecordLit(_, labels, _) => ctors.push(Constructor::Record(labels)),
+            }
+        }
+        ctors.sort_unstable();
+        ctors.dedup();
+        ctors
+    }
+
+    pub fn iter(&self) -> impl ExactSizeIterator<Item = (&PatRow<'arena>, &Body<'arena>)> {
+        self.rows.iter().zip(self.bodies.iter())
+    }
+
+    pub fn iter_mut(
+        &mut self,
+    ) -> impl ExactSizeIterator<Item = (&mut PatRow<'arena>, &mut Body<'arena>)> {
+        self.rows.iter_mut().zip(self.bodies.iter_mut())
+    }
+}
+
+pub type PatPair<'arena> = (CheckedPattern<'arena>, Scrutinee<'arena>);
+
+#[derive(Debug, Clone)]
+pub struct PatRow<'arena> {
+    pairs: Vec<PatPair<'arena>>,
+}
+
+impl<'arena> PatRow<'arena> {
+    pub fn new(pairs: Vec<PatPair<'arena>>) -> Self {
+        Self { pairs }
+    }
+
+    pub fn singleton(pair: PatPair<'arena>) -> Self {
+        Self::new(vec![pair])
+    }
+
+    pub fn tail(&self) -> Self {
+        debug_assert!(!self.is_empty());
+        Self::new(self.pairs[1..].to_vec())
+    }
+
+    pub fn len(&self) -> usize {
+        self.pairs.len()
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.pairs.is_empty()
+    }
+
+    pub fn first(&self) -> Option<&PatPair<'arena>> {
+        self.pairs.first()
+    }
+
+    pub fn all_wildcards(&self) -> bool {
+        self.pairs.iter().all(|(pat, _)| pat.is_wildcard())
+    }
+
+    pub fn split_first(&self) -> Option<(&PatPair<'arena>, Self)> {
+        let (first, rest) = self.pairs.split_first()?;
+        Some((first, Self::new(rest.to_vec())))
+    }
+
+    pub fn append(&mut self, mut other: Self) {
+        self.pairs.append(&mut other.pairs);
+    }
+}
+
+impl<'arena> CheckedPattern<'arena> {
+    /// Specialise `self` with respect to the constructor `ctor`.
+    pub fn specialize(
+        &self,
+        ctx: &mut elaboration::Context<'_, 'arena>,
+        ctor: &Constructor,
+        scrut: &Scrutinee<'arena>,
+    ) -> Option<PatRow<'arena>> {
+        match self {
+            CheckedPattern::ReportedError(range)
+            | CheckedPattern::Placeholder(range)
+            | CheckedPattern::Binder(range, _) => {
+                let columns =
+                    vec![(CheckedPattern::Placeholder(*range), scrut.clone()); ctor.arity()];
+                Some(PatRow::new(columns))
+            }
+            CheckedPattern::ConstLit(_, r#const) if *ctor == Constructor::Const(*r#const) => {
+                Some(PatRow::new(vec![]))
+            }
+            CheckedPattern::RecordLit(_, labels, patterns)
+                if *ctor == Constructor::Record(labels) =>
+            {
+                let mut columns = Vec::with_capacity(labels.len());
+                let mut iter = Iterator::zip(labels.iter(), patterns.iter());
+                let mut telescope = ctx
+                    .elim_env()
+                    .force(&scrut.r#type)
+                    .as_record_type()
+                    .unwrap()
+                    .clone();
+
+                while let Some(((label, pattern), (r#type, next_telescope))) = Option::zip(
+                    iter.next(),
+                    ctx.elim_env().split_telescope(telescope.clone()),
+                ) {
+                    telescope = next_telescope(ctx.local_env.next_var());
+                    let scrut_expr = core::Term::RecordProj(Span::Empty, scrut.expr, *label);
+                    let scrut_expr = ctx.scope.to_scope(scrut_expr);
+                    let scrut = Scrutinee {
+                        range: scrut.range,
+                        expr: scrut_expr,
+                        r#type,
+                    };
+                    columns.push((pattern.clone(), scrut));
+                }
+                Some(PatRow::new(columns))
+            }
+            CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => None,
+        }
+    }
+}
+
+impl<'arena> PatRow<'arena> {
+    /// Specialise `self` with respect to the constructor `ctor`.
+    pub fn specialize(
+        &self,
+        ctx: &mut elaboration::Context<'_, 'arena>,
+        ctor: &Constructor,
+    ) -> Option<PatRow<'arena>> {
+        debug_assert!(!self.pairs.is_empty(), "Cannot specialize empty PatRow");
+        let ((pat, scrut), rest) = self.split_first().unwrap();
+        let mut row = pat.specialize(ctx, ctor, scrut)?;
+        row.append(rest);
+        Some(row)
+    }
+}
+
+impl<'arena> PatMatrix<'arena> {
+    /// Specialize `self` with respect to the constructor `ctor`.
+    /// This is the `S` function in *Compiling pattern matching to good decision trees*
+    pub fn specialize(
+        &self,
+        ctx: &mut elaboration::Context<'_, 'arena>,
+        ctor: &Constructor,
+    ) -> Self {
+        let (rows, bodies) = self
+            .iter()
+            .flat_map(|(row, body)| {
+                let row = row.specialize(ctx, ctor)?;
+                Some((row.clone(), body.clone()))
+            })
+            .unzip();
+        Self { rows, bodies }
+    }
+
+    pub fn default(&self) -> Self {
+        debug_assert!(!self.is_unit(), "Cannot default PatMatrix with no columns");
+        let (rows, bodies) = self
+            .iter()
+            .flat_map(|(row, body)| match row.first().unwrap().0 {
+                CheckedPattern::ReportedError(_)
+                | CheckedPattern::Placeholder(_)
+                | CheckedPattern::Binder(_, _) => Some((row.tail(), body.clone())),
+                CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => None,
+            })
+            .unzip();
+        Self { rows, bodies }
+    }
 }
diff --git a/fathom/src/surface/elaboration/patterns/compile.rs b/fathom/src/surface/elaboration/patterns/compile.rs
new file mode 100644
index 000000000..2e1d0de68
--- /dev/null
+++ b/fathom/src/surface/elaboration/patterns/compile.rs
@@ -0,0 +1,210 @@
+//! # Bibliography
+//! - [Compiling pattern matching to good decision trees](https://dl.acm.org/doi/10.1145/1411304.1411311)
+//!     - <https://github.com/Lapz/Compiling-Pattern-Matching-to-Good-Decision-Trees>
+//!     - <https://github.com/SomewhatML/match-compile>
+//!     - <https://alan-j-hu.github.io/writing/pattern-matching.html>
+//! - [How to compile pattern matching](https://julesjacobs.com/notes/patternmatching/patternmatching.pdf)
+//!     - <https://gitlab.com/yorickpeterse/pattern-matching-in-rust/-/tree/main/jacobs2021>
+
+// TODO: Use join points to prevent code size explosion
+
+use super::*;
+use crate::surface::elaboration;
+
+/// Compilation of pattern matrices to decision trees.
+/// This is the `CC` function in *Compiling pattern matching to good decision trees*.
+pub fn compile_match<'arena>(
+    ctx: &mut elaboration::Context<'_, 'arena>,
+    matrix: &mut PatMatrix<'arena>,
+    exprs: &[core::Term<'arena>],
+    mode: PatternMode,
+    mut shift_amount: EnvLen,
+) -> core::Term<'arena> {
+    // Base case 1:
+    // If the matrix is empty, matching always fails.
+    if matrix.is_null() {
+        return core::Term::error(Span::Empty); // TODO
+    }
+
+    matrix.move_variables(mode);
+
+    // Base case 2:
+    // If the first row is all wildcards, matching always suceeds.
+    if matrix.row(0).all_wildcards() {
+        let Body { index, defs } = matrix.body(0);
+        let body = exprs[*index].clone();
+        match mode {
+            PatternMode::Fun => return body,
+            _ => {
+                // Insert let bindings for all the defs in body, then yield the body expr
+
+                let initial_len = ctx.local_env.len();
+                #[allow(clippy::needless_collect)]
+                let defs: Vec<_> = defs
+                    .iter()
+                    .map(|(def_name, scrut)| {
+                        let def_name = *def_name;
+                        let def_range = scrut.range;
+                        let def_type = ctx.quote_env().quote(ctx.scope, &scrut.r#type);
+                        let def_expr = scrut.expr.shift(ctx.scope, shift_amount);
+                        let def_value = ctx.eval_env().eval(&def_expr);
+                        ctx.local_env
+                            .push_def(def_name, def_value, scrut.r#type.clone());
+                        shift_amount.push();
+                        (def_range, def_name, def_type, def_expr)
+                    })
+                    .collect();
+                ctx.local_env.truncate(initial_len);
+
+                return defs.into_iter().rev().fold(
+                    body,
+                    |body, (def_range, def_name, def_type, def_expr)| {
+                        core::Term::Let(
+                            def_range.into(),
+                            def_name,
+                            ctx.scope.to_scope(def_type.clone()),
+                            ctx.scope.to_scope(def_expr.clone()),
+                            ctx.scope.to_scope(body),
+                        )
+                    },
+                );
+            }
+        };
+    }
+
+    // Inductive case:
+    // The matrix must have at least one column with at least one non-wildcard pattern.
+    // Select such a column, and for each constructor in the column, generate a decision subtree.
+    // If the column is non-exhaustive, generate a default branch as well.
+    let column = matrix.column_to_split_on().unwrap();
+    matrix.swap_columns(0, column);
+    for (pat, scrut) in matrix.column(0) {
+        match pat {
+            CheckedPattern::ConstLit(_, _) => {
+                let scrut_expr = scrut.expr.shift(ctx.scope, shift_amount);
+                let ctors = matrix.column_constructors(0);
+
+                let mut branches = SliceVec::new(ctx.scope, ctors.len());
+                for ctor in ctors.iter() {
+                    let r#const = ctor.as_const().unwrap();
+                    let mut matrix = matrix.specialize(ctx, ctor);
+                    let expr = compile_match(ctx, &mut matrix, exprs, mode, shift_amount);
+                    branches.push((*r#const, expr))
+                }
+
+                let default_branch = match Constructor::is_exhaustive(&ctors) {
+                    true => None,
+                    false => {
+                        let name = None; // TODO: recover default branch name?
+                        let mut matrix = matrix.default();
+                        let value = ctx.eval_env().eval(&scrut_expr);
+
+                        ctx.local_env.push_def(name, value, scrut.r#type.clone());
+                        shift_amount.push();
+                        let expr = compile_match(ctx, &mut matrix, exprs, mode, shift_amount);
+                        ctx.local_env.pop();
+
+                        Some((name, ctx.scope.to_scope(expr) as &_))
+                    }
+                };
+
+                return core::Term::ConstMatch(
+                    Span::Empty,
+                    ctx.scope.to_scope(scrut_expr.clone()),
+                    branches.into(),
+                    default_branch,
+                );
+            }
+
+            // There is only one constructor for each record type,
+            // so we only have to generate a single subtree (ie no branching needed)
+            CheckedPattern::RecordLit(_, labels, _) => {
+                let mut matrix = matrix.specialize(ctx, &Constructor::Record(labels));
+                return compile_match(
+                    ctx,
+                    &mut matrix,
+                    exprs,
+                    PatternMode::MatchInner,
+                    shift_amount,
+                );
+            }
+
+            // SKip over non-constructor patterns
+            CheckedPattern::ReportedError(_)
+            | CheckedPattern::Placeholder(_)
+            | CheckedPattern::Binder(_, _) => continue,
+        }
+    }
+
+    unreachable!()
+}
+
+impl<'arena> PatMatrix<'arena> {
+    /// Return the index of any column in the matrix with at least one non-wildcard pattern.
+    /// At the moment, we simply selec the leftmost column,
+    /// but more advanced splitting heuristcs can be used to minimize the size of the decision tree and potentially skip some tests altogether.
+    /// (See section 8 of "Compiling pattern matching to good decision trees")
+    pub fn column_to_split_on(&self) -> Option<usize> {
+        debug_assert!(!self.is_null(), "Cannot split null PatternMatrix");
+
+        (0..self.num_columns().unwrap()).find(|&column| {
+            self.column(column).any(|(pat, _)| match pat {
+                CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => true,
+                CheckedPattern::ReportedError(_)
+                | CheckedPattern::Placeholder(_)
+                | CheckedPattern::Binder(_, _) => false,
+            })
+        })
+    }
+
+    pub fn swap_columns(&mut self, column1: usize, column2: usize) {
+        debug_assert!(
+            column1 < self.num_columns().unwrap_or(0),
+            "column1 is out of bounds (num_columns = {:?})",
+            self.num_columns()
+        );
+        debug_assert!(
+            column2 < self.num_columns().unwrap_or(0),
+            "column2 is out of bounds (num_columns = {:?})",
+            self.num_columns()
+        );
+
+        for row in self.rows.iter_mut() {
+            row.pairs.swap(column1, column2);
+        }
+    }
+
+    /// Replace Binder patterns with Placeholders, and insert let-defs in the body for each Binder pattern
+    /// # Example
+    /// ```fathom
+    /// match scrut {
+    ///     [scrut.x is x, scrut.y is y] => body,
+    /// }
+    /// ```
+    ///
+    /// becomes
+    /// ```fathom
+    /// match scrut {
+    ///     [scrut.x is _, scrut.y is _] => let x = scrut.x;
+    ///                                     let y = scrut.y;
+    ///                                     body
+    /// }
+    /// ```
+    pub fn move_variables(&mut self, mode: PatternMode) {
+        for (row, body) in self.iter_mut() {
+            for (pat, scrut) in row.pairs.iter_mut() {
+                match pat {
+                    CheckedPattern::Placeholder(range) if mode == PatternMode::Let => {
+                        body.defs.push((None, scrut.clone()));
+                        *pat = CheckedPattern::Placeholder(*range);
+                    }
+                    CheckedPattern::Binder(range, name) => {
+                        body.defs.push((Some(*name), scrut.clone()));
+                        *pat = CheckedPattern::Placeholder(*range);
+                    }
+                    _ => {}
+                }
+            }
+        }
+    }
+}
diff --git a/fathom/src/surface/elaboration/patterns/coverage.rs b/fathom/src/surface/elaboration/patterns/coverage.rs
new file mode 100644
index 000000000..264b59c4b
--- /dev/null
+++ b/fathom/src/surface/elaboration/patterns/coverage.rs
@@ -0,0 +1,103 @@
+//! # Bibliography
+//! - [Warnings for pattern matching](http://moscova.inria.fr/~maranget/papers/warn/index.html)
+//!     - https://github.com/rust-lang/rust/blob/8a09420ac48658cad726e0a6997687ceac4151e3/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs
+//!
+
+// TODO: report exactly which patterns are missing from the matrix
+
+use super::*;
+use crate::surface::elaboration;
+
+pub fn check_coverage<'arena>(
+    ctx: &mut elaboration::Context<'_, 'arena>,
+    matrix: &PatMatrix<'arena>,
+    match_range: ByteRange,
+    scrut_range: ByteRange,
+) {
+    let dummy_scrut = Scrutinee {
+        range: scrut_range,
+        expr: ctx.scope.to_scope(core::Term::error(scrut_range.into())),
+        r#type: ArcValue::new(scrut_range.into(), Arc::new(Value::ERROR)),
+    };
+    let row = PatRow::singleton((CheckedPattern::Placeholder(match_range), dummy_scrut));
+    if is_useful(ctx, matrix, &row) {
+        ctx.push_message(Message::NonExhaustiveMatchExpr {
+            match_expr_range: match_range,
+            scrutinee_expr_range: scrut_range,
+        });
+    }
+
+    let mut rows = Vec::with_capacity(matrix.num_rows());
+    for (row, _) in matrix.iter() {
+        let matrix = PatMatrix::new(rows.clone());
+        if !is_useful(ctx, &matrix, row) {
+            let range = row.first().unwrap().0.range();
+            ctx.push_message(Message::UnreachablePattern { range });
+        }
+        rows.push(row.clone());
+    }
+}
+
+fn is_useful<'arena>(
+    ctx: &mut elaboration::Context<'_, 'arena>,
+    matrix: &PatMatrix<'arena>,
+    row: &PatRow<'arena>,
+) -> bool {
+    if let Some(n) = matrix.num_columns() {
+        debug_assert_eq!(
+            n,
+            row.len(),
+            "`row` must have a pattern for each column of `matrix`"
+        )
+    }
+
+    if matrix.is_null() {
+        return true;
+    }
+    if matrix.is_unit() {
+        return false;
+    }
+
+    let (pat, _) = row.first().unwrap();
+    match pat {
+        CheckedPattern::ReportedError(_)
+        | CheckedPattern::Placeholder(_)
+        | CheckedPattern::Binder(_, _) => {
+            let ctors = matrix.column_constructors(0);
+            match Constructor::is_exhaustive(&ctors) {
+                true => ctors.iter().any(|ctor| {
+                    let matrix = matrix.specialize(ctx, ctor);
+                    let row = row.specialize(ctx, ctor);
+                    match row {
+                        None => false,
+                        Some(row) => is_useful(ctx, &matrix, &row),
+                    }
+                }),
+                false => {
+                    let matrix = matrix.default();
+                    is_useful(ctx, &matrix, &row.tail())
+                }
+            }
+        }
+        CheckedPattern::ConstLit(_, r#const) => {
+            is_useful_ctor(ctx, matrix, row, &Constructor::Const(*r#const))
+        }
+        CheckedPattern::RecordLit(_, labels, _) => {
+            is_useful_ctor(ctx, matrix, row, &Constructor::Record(labels))
+        }
+    }
+}
+
+fn is_useful_ctor<'arena>(
+    ctx: &mut elaboration::Context<'_, 'arena>,
+    matrix: &PatMatrix<'arena>,
+    row: &PatRow<'arena>,
+    ctor: &Constructor<'arena>,
+) -> bool {
+    let matrix = matrix.specialize(ctx, ctor);
+    let row = row.specialize(ctx, ctor);
+    match row {
+        None => false,
+        Some(row) => is_useful(ctx, &matrix, &row),
+    }
+}
diff --git a/tests/fail/elaboration/boolean-literal/not-supported.snap b/tests/fail/elaboration/boolean-literal/not-supported.snap
index 0b362cde7..666177fa8 100644
--- a/tests/fail/elaboration/boolean-literal/not-supported.snap
+++ b/tests/fail/elaboration/boolean-literal/not-supported.snap
@@ -12,4 +12,10 @@ error: boolean literal not supported for expected type
 7 │     true => 1,
   │     ^^^^
 
+warning: unreachable pattern
+  ┌─ tests/fail/elaboration/boolean-literal/not-supported.fathom:7:5
+  │
+7 │     true => 1,
+  │     ^^^^
+
 '''
diff --git a/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap b/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap
index 4a84ba173..60a92a7aa 100644
--- a/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap
+++ b/tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.snap
@@ -1,11 +1,5 @@
 stdout = ''
 stderr = '''
-warning: unreachable pattern
-  ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:5:3
-  │
-5 │   true => 2
-  │   ^^^^
-
 error: non-exhaustive patterns in match expression
   ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:3:7
   │  
@@ -16,4 +10,10 @@ error: non-exhaustive patterns in match expression
 6 │ │ } : U32
   │ ╰─' in match expression
 
+warning: unreachable pattern
+  ┌─ tests/fail/elaboration/non-exhaustive-patterns/match-duplicate.fathom:5:3
+  │
+5 │   true => 2
+  │   ^^^^
+
 '''
diff --git a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap
index b43bd648e..a585c4f5a 100644
--- a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap
+++ b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap
@@ -6,12 +6,6 @@ error: cannot find `x` in scope
 3 │ match (x : U8) {
   │        ^ unbound name
 
-warning: unreachable pattern
-  ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:5
-  │
-5 │     _ => 4 : U64,
-  │     ^
-
 error: mismatched types
   ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:10
   │
@@ -21,12 +15,6 @@ error: mismatched types
   = expected `U64`
        found `U32`
 
-warning: unreachable pattern
-  ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:5
-  │
-6 │     _ => Type,
-  │     ^
-
 error: mismatched types
   ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:10
   │
@@ -36,4 +24,16 @@ error: mismatched types
   = expected `Type`
        found `U32`
 
+warning: unreachable pattern
+  ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:5
+  │
+5 │     _ => 4 : U64,
+  │     ^
+
+warning: unreachable pattern
+  ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:6:5
+  │
+6 │     _ => Type,
+  │     ^
+
 '''
diff --git a/tests/succeed/equality.snap b/tests/succeed/equality.snap
index 2e8858c71..7628439d6 100644
--- a/tests/succeed/equality.snap
+++ b/tests/succeed/equality.snap
@@ -41,12 +41,12 @@ let four_chars : fun (P : U32 -> Type) -> P "beng" -> P 1650814567 =
 refl U32 "beng";
 let three_chars : fun (P : U32 -> Type) -> P "BEN " -> P 1111838240 =
 refl U32 "BEN ";
-let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x };
+let foo : U32 -> U32 = fun x => match x { 1 => 0, _ => let x : U32 = x; x };
 let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x {
     1 => 0,
-    x => x,
-}) -> P (fun x => match x { 1 => 0, x => x }) = refl (U32 ->
-U32) (fun _ => match _ { 1 => 0, x => x });
+    _ => x,
+}) -> P (fun x => match x { 1 => 0, _ => x }) = refl (U32 ->
+U32) (fun _ => match _ { 1 => 0, _ => _ });
 Type : Type
 '''
 stderr = ''
diff --git a/tests/succeed/match/check-const-1.snap b/tests/succeed/match/check-const-1.snap
index ec77653c8..fde5f8fa6 100644
--- a/tests/succeed/match/check-const-1.snap
+++ b/tests/succeed/match/check-const-1.snap
@@ -1,4 +1,4 @@
 stdout = '''
-let x : U8 = 3; match x { 1 => 0, x => x } : U8
+let x : U8 = 3; match x { 1 => 0, _ => let x : U8 = x; x } : U8
 '''
 stderr = ''
diff --git a/tests/succeed/match/check-const-2.snap b/tests/succeed/match/check-const-2.snap
index 2023e6468..650e2da7b 100644
--- a/tests/succeed/match/check-const-2.snap
+++ b/tests/succeed/match/check-const-2.snap
@@ -1,4 +1,4 @@
 stdout = '''
-let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8
+let x : U8 = 3; match x { 1 => 0, 3 => 7, _ => let x : U8 = x; x } : U8
 '''
 stderr = ''
diff --git a/tests/succeed/match/check-const-bool.snap b/tests/succeed/match/check-const-bool.snap
index 7699f35d0..664e70ebf 100644
--- a/tests/succeed/match/check-const-bool.snap
+++ b/tests/succeed/match/check-const-bool.snap
@@ -1,4 +1,4 @@
 stdout = '''
-let x : Bool = false; if x then 1 else 0 : U8
+let x : Bool = false; if x then let x : Bool = x; 1 else 0 : U8
 '''
 stderr = ''
diff --git a/tests/succeed/match/check-const-redundant.snap b/tests/succeed/match/check-const-redundant.snap
index c1ccc9013..25eac0227 100644
--- a/tests/succeed/match/check-const-redundant.snap
+++ b/tests/succeed/match/check-const-redundant.snap
@@ -1,5 +1,6 @@
 stdout = '''
-let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8
+let x : U8 = 3;
+match x { 1 => 0, 3 => 7, 5 => let x : U8 = x; x, _ => let x : U8 = x; x } : U8
 '''
 stderr = '''
 warning: unreachable pattern
diff --git a/tests/succeed/match/synth-const-1.snap b/tests/succeed/match/synth-const-1.snap
index 098d6b2df..be7ce6364 100644
--- a/tests/succeed/match/synth-const-1.snap
+++ b/tests/succeed/match/synth-const-1.snap
@@ -1,4 +1,4 @@
 stdout = '''
-let x : U8 = 3; match x { 1 => x, x => x } : U8
+let x : U8 = 3; match x { 1 => x, _ => let x : U8 = x; x } : U8
 '''
 stderr = ''
diff --git a/tests/succeed/match/synth-const-2.snap b/tests/succeed/match/synth-const-2.snap
index 38aaac02b..8b4114854 100644
--- a/tests/succeed/match/synth-const-2.snap
+++ b/tests/succeed/match/synth-const-2.snap
@@ -1,4 +1,4 @@
 stdout = '''
-let x : U8 = 3; match x { 1 => x, 3 => x, x => x } : U8
+let x : U8 = 3; match x { 1 => x, 3 => x, _ => let x : U8 = x; x } : U8
 '''
 stderr = ''
diff --git a/tests/succeed/record-patterns/fun-lit-generic-pair.fathom b/tests/succeed/record-patterns/fun-lit-generic-pair.fathom
new file mode 100644
index 000000000..b2f844ce0
--- /dev/null
+++ b/tests/succeed/record-patterns/fun-lit-generic-pair.fathom
@@ -0,0 +1,3 @@
+let fst = fun ((A, B) : (Type, Type)) ((x, y) : (A, B)) => x;
+let snd = fun ((A, B) : (Type, Type)) ((x, y) : (A, B)) => y;
+{}
diff --git a/tests/succeed/record-patterns/fun-lit-generic-pair.snap b/tests/succeed/record-patterns/fun-lit-generic-pair.snap
new file mode 100644
index 000000000..6a80b6297
--- /dev/null
+++ b/tests/succeed/record-patterns/fun-lit-generic-pair.snap
@@ -0,0 +1,16 @@
+stdout = '''
+let fst : fun (_ : (Type, Type)) -> (_._0, _._1) -> _._0 = fun _ => let A :
+Type = _._0;
+let B : Type = _._1;
+fun _ => let x : _._0 = _._0;
+let y : _._1 = _._1;
+x;
+let snd : fun (_ : (Type, Type)) -> (_._0, _._1) -> _._1 = fun _ => let A :
+Type = _._0;
+let B : Type = _._1;
+fun _ => let x : _._0 = _._0;
+let y : _._1 = _._1;
+y;
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/fun-type-generic-pair.fathom b/tests/succeed/record-patterns/fun-type-generic-pair.fathom
new file mode 100644
index 000000000..b1dba36ee
--- /dev/null
+++ b/tests/succeed/record-patterns/fun-type-generic-pair.fathom
@@ -0,0 +1,3 @@
+let FstType = fun ((A, B) : (Type, Type)) ((a, b) : (A, B)) -> A;
+let SndType = fun ((A, B) : (Type, Type)) ((a, b) : (A, B)) -> B;
+{}
diff --git a/tests/succeed/record-patterns/fun-type-generic-pair.snap b/tests/succeed/record-patterns/fun-type-generic-pair.snap
new file mode 100644
index 000000000..bd6af78b0
--- /dev/null
+++ b/tests/succeed/record-patterns/fun-type-generic-pair.snap
@@ -0,0 +1,14 @@
+stdout = '''
+let FstType : Type = fun (_ : (Type, Type)) -> (let A : Type = _._0;
+let B : Type = _._1;
+fun (_ : (_._0, _._1)) -> (let a : _._0 = _._0;
+let b : _._1 = _._1;
+A));
+let SndType : Type = fun (_ : (Type, Type)) -> (let A : Type = _._0;
+let B : Type = _._1;
+fun (_ : (_._0, _._1)) -> (let a : _._0 = _._0;
+let b : _._1 = _._1;
+B));
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/let-check.fathom b/tests/succeed/record-patterns/let-check.fathom
new file mode 100644
index 000000000..6dc5f7354
--- /dev/null
+++ b/tests/succeed/record-patterns/let-check.fathom
@@ -0,0 +1,9 @@
+let () : () = ();
+let _ : () = ();
+
+let (x, y) : (Bool, Bool) = (false, true);
+let (a, _) : (Bool, Bool) = (false, true);
+let (_, b) : (Bool, Bool) = (false, true);
+let (_, _) : (Bool, Bool) = (false, true);
+let _ : (Bool, Bool) = (false, true);
+{}
diff --git a/tests/succeed/record-patterns/let-check.snap b/tests/succeed/record-patterns/let-check.snap
new file mode 100644
index 000000000..160928a14
--- /dev/null
+++ b/tests/succeed/record-patterns/let-check.snap
@@ -0,0 +1,15 @@
+stdout = '''
+let _ : () = ();
+let _ : () = ();
+let _ : (Bool, Bool) = (false, true);
+let x : Bool = _._0;
+let y : Bool = _._1;
+let _ : (Bool, Bool) = (false, true);
+let a : Bool = _._0;
+let _ : (Bool, Bool) = (false, true);
+let b : Bool = _._1;
+let _ : (Bool, Bool) = (false, true);
+let _ : (Bool, Bool) = (false, true);
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/let-generic-pair.fathom b/tests/succeed/record-patterns/let-generic-pair.fathom
new file mode 100644
index 000000000..9317e7f4c
--- /dev/null
+++ b/tests/succeed/record-patterns/let-generic-pair.fathom
@@ -0,0 +1,3 @@
+let fst = fun (A : Type) (B : Type) (p : (A, B)) => let (x, _) = p; x;
+let snd = fun (A : Type) (B : Type) (p : (A, B)) => let (_, y) = p; y;
+{}
diff --git a/tests/succeed/record-patterns/let-generic-pair.snap b/tests/succeed/record-patterns/let-generic-pair.snap
new file mode 100644
index 000000000..e9468fb1f
--- /dev/null
+++ b/tests/succeed/record-patterns/let-generic-pair.snap
@@ -0,0 +1,10 @@
+stdout = '''
+let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => let x : A =
+p._0;
+x;
+let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => let y : B =
+p._1;
+y;
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/let-synth.fathom b/tests/succeed/record-patterns/let-synth.fathom
new file mode 100644
index 000000000..7e94184df
--- /dev/null
+++ b/tests/succeed/record-patterns/let-synth.fathom
@@ -0,0 +1,9 @@
+let () = ();
+let _ = ();
+
+let (x, y) = (false, true);
+let (a, _) = (false, true);
+let (_, b) = (false, true);
+let (_, _) = (false, true);
+let _ = (false, true);
+{}
diff --git a/tests/succeed/record-patterns/let-synth.snap b/tests/succeed/record-patterns/let-synth.snap
new file mode 100644
index 000000000..160928a14
--- /dev/null
+++ b/tests/succeed/record-patterns/let-synth.snap
@@ -0,0 +1,15 @@
+stdout = '''
+let _ : () = ();
+let _ : () = ();
+let _ : (Bool, Bool) = (false, true);
+let x : Bool = _._0;
+let y : Bool = _._1;
+let _ : (Bool, Bool) = (false, true);
+let a : Bool = _._0;
+let _ : (Bool, Bool) = (false, true);
+let b : Bool = _._1;
+let _ : (Bool, Bool) = (false, true);
+let _ : (Bool, Bool) = (false, true);
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/match-bool-pairs.fathom b/tests/succeed/record-patterns/match-bool-pairs.fathom
new file mode 100644
index 000000000..59947a7cc
--- /dev/null
+++ b/tests/succeed/record-patterns/match-bool-pairs.fathom
@@ -0,0 +1,56 @@
+let and1 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, true) => true,
+    _ => false,
+};
+let and2 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, true) => true,
+    (_, _) => false,
+};
+let and3 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, true) => true,
+    (false, true) => false,
+    (true, false) => false,
+    (false, false) => false,
+};
+
+let or1 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (false, false) => false,
+    _ => true,
+};
+let or2 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (false, false) => false,
+    (_, _) => true,
+};
+let or3 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (false, false) => false,
+    (false, true) => true,
+    (true, false) => true,
+    (true, true) => true,
+};
+
+let xor1 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, false) => true,
+    (false, true) => true,
+    _ => false,
+};
+let xor2 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, false) => true,
+    (false, true) => true,
+    (_, _) => false,
+};
+let xor3 : Bool -> Bool -> Bool
+= fun x y => match (x, y) {
+    (true, false) => true,
+    (false, true) => true,
+    (false, false) => false,
+    (true, true) => false,
+};
+{}
diff --git a/tests/succeed/record-patterns/match-bool-pairs.snap b/tests/succeed/record-patterns/match-bool-pairs.snap
new file mode 100644
index 000000000..81010e964
--- /dev/null
+++ b/tests/succeed/record-patterns/match-bool-pairs.snap
@@ -0,0 +1,22 @@
+stdout = '''
+let and1 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then true else false else false;
+let and2 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then true else false else false;
+let and3 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then true else false  else if _._1 then false else false;
+let or1 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then true  else if _._1 then true else false;
+let or2 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then true  else if _._1 then true else false;
+let or3 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then true else true  else if _._1 then true else false;
+let xor1 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then false else true  else if _._1 then true else false;
+let xor2 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then false else true  else if _._1 then true else false;
+let xor3 : Bool -> Bool -> Bool = fun x y => let _ : (Bool, Bool) = (x, y);
+if _._0 then if _._1 then false else true  else if _._1 then true else false;
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/match-generic-pair.fathom b/tests/succeed/record-patterns/match-generic-pair.fathom
new file mode 100644
index 000000000..3b5786e05
--- /dev/null
+++ b/tests/succeed/record-patterns/match-generic-pair.fathom
@@ -0,0 +1,3 @@
+let fst = fun (A : Type) (B : Type) (p : (A, B)) => match p { (x, _) => x };
+let snd = fun (A : Type) (B : Type) (p : (A, B)) => match p { (_, y) => y };
+{}
diff --git a/tests/succeed/record-patterns/match-generic-pair.snap b/tests/succeed/record-patterns/match-generic-pair.snap
new file mode 100644
index 000000000..e9468fb1f
--- /dev/null
+++ b/tests/succeed/record-patterns/match-generic-pair.snap
@@ -0,0 +1,10 @@
+stdout = '''
+let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => let x : A =
+p._0;
+x;
+let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => let y : B =
+p._1;
+y;
+() : ()
+'''
+stderr = ''
diff --git a/tests/succeed/record-patterns/match-int-pairs.fathom b/tests/succeed/record-patterns/match-int-pairs.fathom
new file mode 100644
index 000000000..76f708193
--- /dev/null
+++ b/tests/succeed/record-patterns/match-int-pairs.fathom
@@ -0,0 +1,11 @@
+let f : U32 -> U32 -> U32
+= fun x y =>
+let p = (x, y);
+match p {
+    (0, a) => a + (1 : U32),
+    (b, 0) => b + (2 : U32),
+    (1, c) => c + (3 : U32),
+    (d, 1) => d + (4 : U32),
+    (_, _) =>     (5 : U32),
+};
+{}
diff --git a/tests/succeed/record-patterns/match-int-pairs.snap b/tests/succeed/record-patterns/match-int-pairs.snap
new file mode 100644
index 000000000..ab622529d
--- /dev/null
+++ b/tests/succeed/record-patterns/match-int-pairs.snap
@@ -0,0 +1,24 @@
+stdout = '''
+let f : U32 -> U32 -> U32 = fun x y => let p : (U32, U32) = (x, y);
+match p._0 {
+    0 => let a : U32 = p._1;
+    a + (1 : U32),
+    1 => match p._1 {
+        0 => let b : U32 = p._0;
+        b + (2 : U32),
+        1 => let c : U32 = p._1;
+        c + (3 : U32),
+        _ => let c : U32 = p._1;
+        c + (3 : U32),
+    },
+    _ => match p._1 {
+        0 => let b : U32 = p._0;
+        b + (2 : U32),
+        1 => let d : U32 = p._0;
+        d + (4 : U32),
+        _ => 5,
+    },
+};
+() : ()
+'''
+stderr = ''