Pattern Coverage
Once the type checker has admitted a match expression as well-typed, a second pass decides whether the arms together cover every value the scrutinee could take, and whether any arm is shadowed by the earlier ones. These are the two halves of a single problem: a clause is reachable when there exists some value the previous matrix does not match but the new row does, and a match is exhaustive when no value escapes the matrix as a whole. The coverage pass implements the classical matrix decision procedure for both questions, as developed by the authors of Warnings for pattern matching, restricted to the algebraic datatypes that System Fω admits.
The pattern language is small. Wildcards and variables match any value of the relevant type, constructors match values of a specific shape with sub-patterns for each field.
\[ \begin{align*} \text{patterns} \quad p &::= \_ \mid x \mid C\, \overline{p} \end{align*} \]
The metavariable \(p\) ranges over patterns. The wildcard \(\_\) matches any value without binding a name. The variable \(x\) also matches any value but binds the matched value to \(x\) in the arm body. The constructor pattern \(C\, \overline{p}\) matches a value of the form \(C\, \overline{v}\) when every sub-pattern \(p_i\) matches its corresponding \(v_i\), with the overline \(\overline{p}\) denoting the list of sub-patterns whose length is fixed by the arity of the constructor \(C\). The interesting case is the constructor: it carries the only structural information the algorithm can split on, and its sub-patterns recurse into the same grammar, which is what allows the procedure to discover non-exhaustiveness arbitrarily deep inside a value.
The pass operates on the core form of patterns, after surface variables have been desugared and after the type checker has resolved every constructor name to its declaring datatype.
#![allow(unused)] fn main() { use std::fmt; /// Core language for System-F-ω with explicit type applications and /// abstractions #[derive(Debug, Clone, PartialEq)] pub struct CoreModule { pub type_defs: Vec<TypeDef>, pub term_defs: Vec<TermDef>, } #[derive(Debug, Clone, PartialEq)] pub struct TypeDef { pub name: String, pub kind: Kind, pub constructors: Vec<DataConstructor>, } #[derive(Debug, Clone, PartialEq)] pub struct DataConstructor { pub name: String, pub ty: CoreType, } #[derive(Debug, Clone, PartialEq)] pub struct TermDef { pub name: String, pub ty: CoreType, pub body: CoreTerm, } /// Kinds for types #[derive(Debug, Clone, PartialEq)] pub enum Kind { /// Base kind: * Star, /// Function kind: k1 -> k2 Arrow(Box<Kind>, Box<Kind>), } /// Core types (System-F-ω) #[derive(Debug, Clone, PartialEq)] pub enum CoreType { /// Type variable: a Var(String), /// Existential type variable: ^a ETVar(String), /// Type constructor: Int, Bool Con(String), /// Function type: T1 -> T2 Arrow(Box<CoreType>, Box<CoreType>), /// Universal quantification: ∀a. T Forall(String, Box<CoreType>), /// Type application: F T App(Box<CoreType>, Box<CoreType>), /// Product type: T1 × T2 Product(Vec<CoreType>), } /// Core terms (System-F) #[derive(Debug, Clone, PartialEq)] pub enum CoreTerm { /// Variable: x Var(String), /// Integer literal: 42 LitInt(i64), /// Lambda abstraction: λx:T. e Lambda { param: String, param_ty: CoreType, body: Box<CoreTerm>, }, /// Application: e1 e2 App { func: Box<CoreTerm>, arg: Box<CoreTerm>, }, /// Type abstraction: Λα. e TypeLambda { param: String, body: Box<CoreTerm> }, /// Constructor: C e1 ... en Constructor { name: String, args: Vec<CoreTerm> }, /// Pattern matching: case e of { p1 -> e1; ... } Case { scrutinee: Box<CoreTerm>, arms: Vec<CaseArm>, }, /// Built-in operations BinOp { op: CoreBinOp, left: Box<CoreTerm>, right: Box<CoreTerm>, }, /// Conditional: if e1 then e2 else e3 If { cond: Box<CoreTerm>, then_branch: Box<CoreTerm>, else_branch: Box<CoreTerm>, }, /// Intrinsic function call IntrinsicCall { name: String, args: Vec<CoreTerm> }, } #[derive(Debug, Clone, PartialEq)] pub struct CaseArm { pub pattern: CorePattern, pub body: CoreTerm, } #[derive(Debug, Clone, PartialEq)] pub enum CoreBinOp { Add, Sub, Mul, Div, Lt, Le, } impl fmt::Display for Kind { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { Kind::Star => write!(f, "*"), Kind::Arrow(k1, k2) => write!(f, "{} -> {}", k1, k2), } } } impl fmt::Display for CoreType { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { CoreType::Var(name) => write!(f, "{}", name), CoreType::ETVar(name) => write!(f, "^{}", name), CoreType::Con(name) => write!(f, "{}", name), CoreType::Arrow(t1, t2) => write!(f, "{} -> {}", t1, t2), CoreType::Forall(var, ty) => write!(f, "∀{}. {}", var, ty), CoreType::App(t1, t2) => write!(f, "({} {})", t1, t2), CoreType::Product(types) => { write!(f, "(")?; for (i, ty) in types.iter().enumerate() { if i > 0 { write!(f, " × ")?; } write!(f, "{}", ty)?; } write!(f, ")") } } } } impl fmt::Display for CoreBinOp { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { CoreBinOp::Add => write!(f, "+"), CoreBinOp::Sub => write!(f, "-"), CoreBinOp::Mul => write!(f, "*"), CoreBinOp::Div => write!(f, "/"), CoreBinOp::Lt => write!(f, "<"), CoreBinOp::Le => write!(f, "<="), } } } impl fmt::Display for CoreTerm { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { CoreTerm::Var(name) => write!(f, "{}", name), CoreTerm::LitInt(n) => write!(f, "{}", n), CoreTerm::Lambda { param, param_ty, body, } => { write!(f, "λ{} : {}. {}", param, param_ty, body) } CoreTerm::App { func, arg } => write!(f, "{} {}", func, arg), CoreTerm::Constructor { name, args } => { if args.is_empty() { write!(f, "{}", name) } else { write!(f, "{}", name)?; for arg in args { write!(f, " {}", arg)?; } Ok(()) } } CoreTerm::If { cond, then_branch, else_branch, } => { write!(f, "if {} then {} else {}", cond, then_branch, else_branch) } CoreTerm::Case { scrutinee, arms: _ } => { write!(f, "match {} {{ ... }}", scrutinee) } CoreTerm::BinOp { op, left, right } => { write!(f, "{} {} {}", left, op, right) } CoreTerm::IntrinsicCall { name, args } => { write!(f, "{}(", name)?; for (i, arg) in args.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", arg)?; } write!(f, ")") } _ => write!(f, "<term>"), } } } #[derive(Debug, Clone, PartialEq)] pub enum CorePattern { /// Wildcard: _ Wildcard, /// Variable: x Var(String), /// Constructor: C p1 ... pn Constructor { name: String, args: Vec<CorePattern>, }, } }
Constructor Environment
The decision procedure needs to know, for any constructor name encountered in a column, which other constructors share the same parent datatype. The environment is built once from the module’s type declarations and indexes constructors by name.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } }
The ctors map sends a constructor name to its parent type’s name. The siblings map sends a parent name to the full list of its constructors together with their arities. When the algorithm meets the head constructor of a column it looks up the parent in ctors, asks siblings for the complete list, and compares the present heads against that list to decide whether the column is saturated. The arity of each sibling is read off the constructor’s compiled type by peeling outer foralls and counting arrows.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } }
Matrix Operations
The state of the algorithm is a matrix of patterns, one row per surviving arm and one column per outstanding scrutinee position. Two operations rewrite the matrix into a simpler one as the algorithm descends.
The first is specialization. Given a head constructor \(C\) of arity \(k\), every row whose first cell matches \(C\) is rewritten so that the constructor pattern is replaced by its \(k\) sub-patterns, lengthening the row to width \(k + n - 1\). Rows headed by a wildcard or variable produce \(k\) fresh wildcards in place of the head, matching every possible argument tuple. Rows headed by a different constructor are dropped.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } }
The second is the default matrix. It keeps only the rows headed by a wildcard or variable, dropping the head cell, so the remaining matrix describes which values can flow past the first column without committing to any specific constructor.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } }
These two operations together form the recursive step. Specialization explores what happens when a value of a specific shape is matched, the default matrix explores what happens when the value does not match any of the constructors present in the column.
Usefulness
The reachability check is phrased as the usefulness predicate. A new row is useful with respect to the matrix above it when there exists some value vector matched by the row but not by any earlier row. The recursion splits on the head pattern of the candidate row.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } }
When the head is a constructor, the matrix is specialized at that constructor and the candidate row’s sub-patterns are spliced into the front of its tail, then the question recurs at the reduced shape. When the head is a wildcard, the algorithm asks whether the column is saturated by the constructors present in the matrix. If every sibling of the parent datatype appears, the wildcard must match through one of them, so usefulness is established by finding any specific constructor at which the specialized matrix admits the wildcard row. If the column is not saturated, the wildcard can escape down a constructor that the matrix has never mentioned, so usefulness reduces to the question on the default matrix and the row’s tail.
The driver runs this check on each arm as the matrix grows. If an arm is not useful, it is shadowed by some combination of earlier arms and an error is raised pointing at its index.
Witness Search
Exhaustiveness is the dual question. The match is exhaustive when the entire matrix is useful against no row of all wildcards, which is the same as saying that the empty row at width one is not useful. Rather than answer that question directly, the algorithm constructs a witness: a value vector that no row matches. If a witness exists the match is non-exhaustive and the witness is reported as the missing pattern; if no witness exists the match is exhaustive.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } }
Witness search mirrors the usefulness recursion but returns a value rather than a boolean.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } }
When the current column has no constructors, the witness is a wildcard at this position and the search recurses on the default matrix. When some constructors appear, the algorithm first looks for a missing sibling: if any constructor of the parent datatype is absent from the column, a value built from that constructor with wildcard arguments is unmatched by every row, so the witness is built directly from the missing sibling. If every sibling is present, the witness must be built underneath one of the existing constructors, so the algorithm specializes the matrix at each present constructor in turn and asks whether a witness exists for the specialized problem. The first specialization that produces a witness gives the answer; the constructor’s sub-patterns and the tail are reassembled into a full witness.
The key invariant is that the witness search descends into sub-patterns in the same way the type system descends into sub-types. A non-exhaustive match on Maybe (Either Int Int) that handles Nothing and Just (Left _) produces the witness Just (Right _) rather than just Just _, because the recursion on Just’s sub-pattern column rediscovers that Right is absent from the inner matrix and lifts a fresh Right _ witness back through the outer Just constructor. The pretty-printed witness reads as a concrete missing pattern, which is what the error message reports.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } }
Driver
The driver assembles the two checks into a single pass over a list of arms. It threads the matrix forward, raises an UnreachableMatchArm error on the first arm that fails usefulness, and after every arm has been added asks for a witness against the full matrix. A witness becomes a NonExhaustiveMatch error carrying its pretty form.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } }
The module-level entry point walks every term definition and invokes check_match at every Case node it finds. The pass runs after bidirectional type checking has succeeded, so every constructor name in the patterns is known to belong to a declared datatype and every column has a parent in the environment built up front. The two error variants live in the standard error enum and flow through the same diagnostic pipeline as the type errors above them.
#![allow(unused)] fn main() { use std::collections::HashMap; use std::fmt; use crate::core::{CaseArm, CoreModule, CorePattern, CoreTerm}; use crate::errors::TypeError; #[derive(Debug, Clone)] pub struct CtorInfo { pub parent: String, } #[derive(Debug, Clone)] pub struct CoverageEnv { pub ctors: HashMap<String, CtorInfo>, pub siblings: HashMap<String, Vec<(String, usize)>>, } impl CoverageEnv { pub fn from_module(module: &CoreModule) -> Self { let mut ctors = HashMap::new(); let mut siblings = HashMap::new(); for tdef in &module.type_defs { let mut entries = Vec::new(); for dctor in &tdef.constructors { let arity = arrow_arity(&dctor.ty); ctors.insert( dctor.name.clone(), CtorInfo { parent: tdef.name.clone(), }, ); entries.push((dctor.name.clone(), arity)); } siblings.insert(tdef.name.clone(), entries); } CoverageEnv { ctors, siblings } } } fn arrow_arity(ty: &crate::core::CoreType) -> usize { let mut current = ty; while let crate::core::CoreType::Forall(_, body) = current { current = body; } let mut n = 0; while let crate::core::CoreType::Arrow(_, rest) = current { n += 1; current = rest; } n } #[derive(Debug, Clone)] pub enum Witness { Wild, Ctor(String, Vec<Witness>), } impl fmt::Display for Witness { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Witness::Wild => write!(f, "_"), Witness::Ctor(name, args) if args.is_empty() => write!(f, "{}", name), Witness::Ctor(name, args) => { write!(f, "{}", name)?; for a in args { match a { Witness::Ctor(_, sub) if !sub.is_empty() => write!(f, " ({})", a)?, _ => write!(f, " {}", a)?, } } Ok(()) } } } } type Row = Vec<CorePattern>; type Matrix = Vec<Row>; fn head_ctor(p: &CorePattern) -> Option<(&str, &[CorePattern])> { match p { CorePattern::Constructor { name, args } => Some((name.as_str(), args.as_slice())), _ => None, } } fn specialize(matrix: &Matrix, ctor: &str, arity: usize) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Constructor { name, args } if name == ctor => { let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Wildcard | CorePattern::Var(_) => { let mut new_row: Row = vec![CorePattern::Wildcard; arity]; new_row.extend_from_slice(rest); out.push(new_row); } CorePattern::Constructor { .. } => {} } } out } fn default_matrix(matrix: &Matrix) -> Matrix { let mut out = Matrix::new(); for row in matrix { let Some((head, rest)) = row.split_first() else { continue; }; match head { CorePattern::Wildcard | CorePattern::Var(_) => out.push(rest.to_vec()), CorePattern::Constructor { .. } => {} } } out } fn column_ctors(matrix: &Matrix) -> Vec<(String, usize)> { let mut seen = Vec::new(); for row in matrix { if let Some(first) = row.first() { if let Some((name, args)) = head_ctor(first) { if !seen.iter().any(|(n, _): &(String, usize)| n == name) { seen.push((name.to_string(), args.len())); } } } } seen } fn find_witness(matrix: &Matrix, width: usize, env: &CoverageEnv) -> Option<Vec<Witness>> { if width == 0 { return if matrix.is_empty() { Some(Vec::new()) } else { None }; } let present = column_ctors(matrix); if present.is_empty() { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); return Some(out); } let parent = env.ctors.get(&present[0].0).map(|c| c.parent.clone()); let all_siblings = parent.as_ref().and_then(|p| env.siblings.get(p)).cloned(); if let Some(siblings) = all_siblings { for (sname, sarity) in &siblings { if !present.iter().any(|(n, _)| n == sname) { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let args = vec![Witness::Wild; *sarity]; let mut out = vec![Witness::Ctor(sname.clone(), args)]; out.extend(tail); return Some(out); } } for (cname, carity) in &present { let sub = specialize(matrix, cname, *carity); if let Some(witness) = find_witness(&sub, carity + width - 1, env) { let (head_args, tail) = witness.split_at(*carity); let mut out = vec![Witness::Ctor(cname.clone(), head_args.to_vec())]; out.extend(tail.iter().cloned()); return Some(out); } } None } else { let sub = default_matrix(matrix); let tail = find_witness(&sub, width - 1, env)?; let mut out = vec![Witness::Wild]; out.extend(tail); Some(out) } } fn is_useful(matrix: &Matrix, row: &Row, env: &CoverageEnv) -> bool { if row.is_empty() { return matrix.is_empty(); } let (head, rest) = row.split_first().unwrap(); match head { CorePattern::Constructor { name, args } => { let sub = specialize(matrix, name, args.len()); let mut new_row: Row = args.clone(); new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) } CorePattern::Wildcard | CorePattern::Var(_) => { let present = column_ctors(matrix); let parent = env .ctors .get(&present.first().map(|c| c.0.clone()).unwrap_or_default()); let siblings = parent.and_then(|c| env.siblings.get(&c.parent)).cloned(); let exhaustive = siblings .as_ref() .map(|s| s.iter().all(|(n, _)| present.iter().any(|(p, _)| p == n))) .unwrap_or(false); if exhaustive { present.iter().any(|(name, arity)| { let sub = specialize(matrix, name, *arity); let mut new_row: Row = vec![CorePattern::Wildcard; *arity]; new_row.extend_from_slice(rest); is_useful(&sub, &new_row, env) }) } else { let sub = default_matrix(matrix); is_useful(&sub, &rest.to_vec(), env) } } } } pub fn check_match(arms: &[CaseArm], env: &CoverageEnv) -> Result<(), TypeError> { let mut matrix: Matrix = Vec::new(); for (i, arm) in arms.iter().enumerate() { let row = vec![arm.pattern.clone()]; if !is_useful(&matrix, &row, env) { return Err(TypeError::UnreachableMatchArm { index: i, span: None, }); } matrix.push(row); } if let Some(witness) = find_witness(&matrix, 1, env) { let pretty = witness .into_iter() .map(|w| w.to_string()) .collect::<Vec<_>>() .join(" "); return Err(TypeError::NonExhaustiveMatch { missing: pretty, span: None, }); } Ok(()) } fn walk_term(term: &CoreTerm, env: &CoverageEnv) -> Result<(), TypeError> { match term { CoreTerm::Var(_) | CoreTerm::LitInt(_) => Ok(()), CoreTerm::Lambda { body, .. } | CoreTerm::TypeLambda { body, .. } => walk_term(body, env), CoreTerm::App { func, arg } => { walk_term(func, env)?; walk_term(arg, env) } CoreTerm::Constructor { args, .. } | CoreTerm::IntrinsicCall { args, .. } => { for a in args { walk_term(a, env)?; } Ok(()) } CoreTerm::BinOp { left, right, .. } => { walk_term(left, env)?; walk_term(right, env) } CoreTerm::If { cond, then_branch, else_branch, } => { walk_term(cond, env)?; walk_term(then_branch, env)?; walk_term(else_branch, env) } CoreTerm::Case { scrutinee, arms } => { walk_term(scrutinee, env)?; for arm in arms { walk_term(&arm.body, env)?; } check_match(arms, env) } } } pub fn check_module(module: &CoreModule) -> Result<(), TypeError> { let env = CoverageEnv::from_module(module); for tdef in &module.term_defs { walk_term(&tdef.body, &env)?; } Ok(()) } }
A non-exhaustive match on a nested datatype illustrates the structural witness. The program
data Either a b = Left a | Right b;
data Maybe a = Nothing | Just a;
test :: Maybe (Either Int Int) -> Int;
test m = match m {
Nothing -> 0;
Just (Left x) -> x;
};
is rejected with the diagnostic Match is non-exhaustive; missing pattern: Just (Right _). The witness was produced by specialization at Just, which exposed the inner column over Either, where Right was found absent and lifted back out. The same procedure that flags this nested gap also rejects redundant arms: appending a second Nothing -> 1 to the same body raises Unreachable match arm at index 2, since the new row’s head specializes against an already-saturated default matrix and the recursion bottoms out with no useful position.