Add warning for unreachable pattern matching rules

CHANGELOG.md

@@ -7,8 +7,12 @@ and this project does not currently adhere to a particular versioning scheme.
 
 ## [Unreleased]
 
+### Added
+
+- Emit a warning when a rule in a pattern matching function is unreachable. ([#736][gh-736])
+
 ### Fixed
-- Fix type checker not properly unifying all the arms of a match expression.
+- Fix type checker not properly unifying all the arms of a match expression. ([#734][gh-734])
 
 ## [0.2.37] - 2024-10-18
 
@@ -379,6 +383,7 @@ and this project does not currently adhere to a particular versioning scheme.
 [0.2.35]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.35
 [0.2.36]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.36
 [0.2.37]: https://github.com/HigherOrderCO/Bend/releases/tag/0.2.37
+[Unreleased]: https://github.com/HigherOrderCO/Bend/compare/0.2.37...HEAD
 [gh-424]: https://github.com/HigherOrderCO/Bend/issues/424
 [gh-427]: https://github.com/HigherOrderCO/Bend/issues/427
 [gh-443]: https://github.com/HigherOrderCO/Bend/issues/443
@@ -436,3 +441,5 @@ and this project does not currently adhere to a particular versioning scheme.
 [gh-674]: https://github.com/HigherOrderCO/Bend/issues/674
 [gh-675]: https://github.com/HigherOrderCO/Bend/issues/675
 [gh-706]: https://github.com/HigherOrderCO/Bend/issues/706
+[gh-734]: https://github.com/HigherOrderCO/Bend/issues/734
+[gh-736]: https://github.com/HigherOrderCO/Bend/issues/736

src/fun/transform/desugar_match_defs.rs

@@ -3,13 +3,15 @@ use crate::{
   fun::{builtins, Adts, Constructors, Ctx, Definition, FanKind, Name, Num, Pattern, Rule, Tag, Term},
   maybe_grow,
 };
+use itertools::Itertools;
 use std::collections::{BTreeSet, HashSet};
 
 pub enum DesugarMatchDefErr {
   AdtNotExhaustive { adt: Name, ctr: Name },
   NumMissingDefault,
   TypeMismatch { expected: Type, found: Type, pat: Pattern },
   RepeatedBind { bind: Name },
+  UnreachableRule { idx: usize, nam: Name, pats: Vec<Pattern> },
 }
 
 impl Ctx<'_> {
@@ -30,6 +32,12 @@ impl Ctx<'_> {
             def_name.clone(),
             def.source.clone(),
           ),
+          DesugarMatchDefErr::UnreachableRule { .. } => self.info.add_function_warning(
+            err,
+            WarningType::UnreachableMatch,
+            def_name.clone(),
+            def.source.clone(),
+          ),
         }
       }
     }
@@ -49,10 +57,22 @@ impl Definition {
 
     let args = (0..self.arity()).map(|i| Name::new(format!("%arg{i}"))).collect::<Vec<_>>();
     let rules = std::mem::take(&mut self.rules);
-    match simplify_rule_match(args.clone(), rules, vec![], ctrs, adts) {
+    let idx = (0..rules.len()).collect::<Vec<_>>();
+    let mut used = BTreeSet::new();
+    match simplify_rule_match(args.clone(), rules.clone(), idx.clone(), vec![], &mut used, ctrs, adts) {
       Ok(body) => {
         let body = Term::rfold_lams(body, args.into_iter().map(Some));
         self.rules = vec![Rule { pats: vec![], body }];
+        for i in idx {
+          if !used.contains(&i) {
+            let e = DesugarMatchDefErr::UnreachableRule {
+              idx: i,
+              nam: self.name.clone(),
+              pats: rules[i].pats.clone(),
+            };
+            errs.push(e);
+          }
+        }
       }
       Err(e) => errs.push(e),
     }
@@ -123,32 +143,40 @@ fn fix_repeated_binds(rules: &mut [Rule]) -> Vec<DesugarMatchDefErr> {
 /// expression, together with the remaining match arguments.
 ///
 /// Linearizes all the arguments that are used in at least one of the bodies.
+///
+/// `args`: Name of the generated argument variables that sill have to be processed.
+/// `rules`: The rules to simplify.
+/// `idx`: The original index of the rules, to check for unreachable rules.
+/// `with`: Name of the variables to be inserted in the `with` clauses.
 fn simplify_rule_match(
   args: Vec<Name>,
   rules: Vec<Rule>,
+  idx: Vec<usize>,
   with: Vec<Name>,
+  used: &mut BTreeSet<usize>,
   ctrs: &Constructors,
   adts: &Adts,
 ) -> Result<Term, DesugarMatchDefErr> {
   if args.is_empty() {
+    used.insert(idx[0]);
     Ok(rules.into_iter().next().unwrap().body)
   } else if rules[0].pats.iter().all(|p| p.is_wildcard()) {
-    Ok(irrefutable_fst_row_rule(args, rules.into_iter().next().unwrap()))
+    Ok(irrefutable_fst_row_rule(args, rules.into_iter().next().unwrap(), idx[0], used))
   } else {
     let typ = Type::infer_from_def_arg(&rules, 0, ctrs)?;
     match typ {
-      Type::Any => var_rule(args, rules, with, ctrs, adts),
-      Type::Fan(fan, tag, tup_len) => fan_rule(args, rules, with, fan, tag, tup_len, ctrs, adts),
-      Type::Num => num_rule(args, rules, with, ctrs, adts),
-      Type::Adt(adt_name) => switch_rule(args, rules, with, adt_name, ctrs, adts),
+      Type::Any => var_rule(args, rules, idx, with, used, ctrs, adts),
+      Type::Fan(fan, tag, tup_len) => fan_rule(args, rules, idx, with, used, fan, tag, tup_len, ctrs, adts),
+      Type::Num => num_rule(args, rules, idx, with, used, ctrs, adts),
+      Type::Adt(adt_name) => switch_rule(args, rules, idx, with, adt_name, used, ctrs, adts),
     }
   }
 }
 
 /// Irrefutable first row rule.
 /// Short-circuits the encoding in case the first rule always matches.
 /// This is useful to avoid unnecessary pattern matching.
-fn irrefutable_fst_row_rule(args: Vec<Name>, rule: Rule) -> Term {
+fn irrefutable_fst_row_rule(args: Vec<Name>, rule: Rule, idx: usize, used: &mut BTreeSet<usize>) -> Term {
   let mut term = rule.body;
   for (arg, pat) in args.into_iter().zip(rule.pats.into_iter()) {
     match pat {
@@ -166,6 +194,7 @@ fn irrefutable_fst_row_rule(args: Vec<Name>, rule: Rule) -> Term {
       _ => unreachable!(),
     }
   }
+  used.insert(idx);
   term
 }
 
@@ -176,7 +205,9 @@ fn irrefutable_fst_row_rule(args: Vec<Name>, rule: Rule) -> Term {
 fn var_rule(
   mut args: Vec<Name>,
   rules: Vec<Rule>,
+  idx: Vec<usize>,
   mut with: Vec<Name>,
+  used: &mut BTreeSet<usize>,
   ctrs: &Constructors,
   adts: &Adts,
 ) -> Result<Term, DesugarMatchDefErr> {
@@ -202,7 +233,7 @@ fn var_rule(
 
   with.push(arg);
 
-  simplify_rule_match(new_args, new_rules, with, ctrs, adts)
+  simplify_rule_match(new_args, new_rules, idx, with, used, ctrs, adts)
 }
 
 /// Tuple rule.
@@ -224,7 +255,9 @@ fn var_rule(
 fn fan_rule(
   mut args: Vec<Name>,
   rules: Vec<Rule>,
+  idx: Vec<usize>,
   with: Vec<Name>,
+  used: &mut BTreeSet<usize>,
   fan: FanKind,
   tag: Tag,
   len: usize,
@@ -263,7 +296,7 @@ fn fan_rule(
 
   let bnd = new_args.clone().map(|x| Pattern::Var(Some(x))).collect();
   let args = new_args.chain(old_args).collect();
-  let nxt = simplify_rule_match(args, new_rules, with, ctrs, adts)?;
+  let nxt = simplify_rule_match(args, new_rules, idx, with, used, ctrs, adts)?;
   let term = Term::Let {
     pat: Box::new(Pattern::Fan(fan, tag.clone(), bnd)),
     val: Box::new(Term::Var { nam: arg }),
@@ -276,7 +309,9 @@ fn fan_rule(
 fn num_rule(
   mut args: Vec<Name>,
   rules: Vec<Rule>,
+  idx: Vec<usize>,
   with: Vec<Name>,
+  used: &mut BTreeSet<usize>,
   ctrs: &Constructors,
   adts: &Adts,
 ) -> Result<Term, DesugarMatchDefErr> {
@@ -303,12 +338,14 @@ fn num_rule(
   let mut num_bodies = vec![];
   for num in nums.iter() {
     let mut new_rules = vec![];
-    for rule in rules.iter() {
+    let mut new_idx = vec![];
+    for (rule, &idx) in rules.iter().zip(&idx) {
       match &rule.pats[0] {
         Pattern::Num(n) if n == num => {
           let body = rule.body.clone();
           let rule = Rule { pats: rule.pats[1..].to_vec(), body };
           new_rules.push(rule);
+          new_idx.push(idx);
         }
         Pattern::Var(var) => {
           let mut body = rule.body.clone();
@@ -321,17 +358,19 @@ fn num_rule(
           }
           let rule = Rule { pats: rule.pats[1..].to_vec(), body };
           new_rules.push(rule);
+          new_idx.push(idx);
         }
         _ => (),
       }
     }
-    let body = simplify_rule_match(args.clone(), new_rules, with.clone(), ctrs, adts)?;
+    let body = simplify_rule_match(args.clone(), new_rules, new_idx, with.clone(), used, ctrs, adts)?;
     num_bodies.push(body);
   }
 
   // Default case
   let mut new_rules = vec![];
-  for rule in rules {
+  let mut new_idx = vec![];
+  for (rule, &idx) in rules.into_iter().zip(&idx) {
     if let Pattern::Var(var) = &rule.pats[0] {
       let mut body = rule.body.clone();
       if let Some(var) = var {
@@ -343,11 +382,12 @@ fn num_rule(
       }
       let rule = Rule { pats: rule.pats[1..].to_vec(), body };
       new_rules.push(rule);
+      new_idx.push(idx);
     }
   }
   let mut default_with = with.clone();
   default_with.push(pred_var.clone());
-  let default_body = simplify_rule_match(args.clone(), new_rules, default_with, ctrs, adts)?;
+  let default_body = simplify_rule_match(args.clone(), new_rules, new_idx, default_with, used, ctrs, adts)?;
 
   // Linearize previously matched vars and current args.
   let with = with.into_iter().chain(args).collect::<Vec<_>>();
@@ -446,11 +486,14 @@ fn fast_pred_access(body: &mut Term, cur_num: u32, var: &Name, pred_var: &Name)
 /// }
 /// ```
 /// Where `case` represents a call of the [`simplify_rule_match`] function.
+#[allow(clippy::too_many_arguments)]
 fn switch_rule(
   mut args: Vec<Name>,
   rules: Vec<Rule>,
+  idx: Vec<usize>,
   with: Vec<Name>,
   adt_name: Name,
+  used: &mut BTreeSet<usize>,
   ctrs: &Constructors,
   adts: &Adts,
 ) -> Result<Term, DesugarMatchDefErr> {
@@ -463,7 +506,8 @@ fn switch_rule(
     let args = new_args.clone().chain(old_args.clone()).collect();
 
     let mut new_rules = vec![];
-    for rule in &rules {
+    let mut new_idx = vec![];
+    for (rule, &idx) in rules.iter().zip(&idx) {
       let old_pats = rule.pats[1..].to_vec();
       match &rule.pats[0] {
         // Same ctr, extract subpatterns.
@@ -475,6 +519,7 @@ fn switch_rule(
           let body = rule.body.clone();
           let rule = Rule { pats, body };
           new_rules.push(rule);
+          new_idx.push(idx);
         }
         // Var, match and rebuild the constructor.
         // var pat1 ... patN: body
@@ -493,6 +538,7 @@ fn switch_rule(
           }
           let rule = Rule { pats, body };
           new_rules.push(rule);
+          new_idx.push(idx);
         }
         _ => (),
       }
@@ -502,7 +548,7 @@ fn switch_rule(
       return Err(DesugarMatchDefErr::AdtNotExhaustive { adt: adt_name, ctr: ctr_nam.clone() });
     }
 
-    let body = simplify_rule_match(args, new_rules, with.clone(), ctrs, adts)?;
+    let body = simplify_rule_match(args, new_rules, new_idx, with.clone(), used, ctrs, adts)?;
     new_arms.push((Some(ctr_nam.clone()), new_args.map(Some).collect(), body));
   }
 
@@ -606,6 +652,14 @@ impl std::fmt::Display for DesugarMatchDefErr {
       DesugarMatchDefErr::RepeatedBind { bind } => {
         write!(f, "Repeated bind in pattern matching rule: '{bind}'.")
       }
+      DesugarMatchDefErr::UnreachableRule { idx, nam, pats } => {
+        write!(
+          f,
+          "Unreachable pattern matching rule '({}{})' (rule index {idx}).",
+          nam,
+          pats.iter().map(|p| format!(" {p}")).join("")
+        )
+      }
     }
   }
 }

tests/golden_tests.rs

@@ -245,7 +245,9 @@ fn readback_hvm() {
 fn simplify_matches() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let diagnostics_cfg = DiagnosticsConfig {
-      irrefutable_match: Severity::Allow,
+      unused_definition: Severity::Allow,
+      irrefutable_match: Severity::Warning,
+      unreachable_match: Severity::Warning,
       ..DiagnosticsConfig::new(Severity::Error, true)
     };
     let mut book = parse_book_single_file(code, path)?;
@@ -275,7 +277,7 @@ fn simplify_matches() {
     ctx.book.make_var_names_unique();
     ctx.prune(false);
 
-    Ok(ctx.book.to_string())
+    Ok(format!("{}\n{}", ctx.book, ctx.info))
   })
 }
 

tests/snapshots/simplify_matches__adt_tup_era.bend.snap

@@ -13,3 +13,7 @@ Tuple/Pair/tag: _
 
 Tuple/Pair: (Any -> Any -> Tuple)
 (Tuple/Pair) = λa λb λc (c Tuple/Pair/tag a b)
+Warnings:
+In tests/golden_tests/simplify_matches/adt_tup_era.bend :
+In definition 'Foo':
+  Unreachable pattern matching rule '(Foo *)' (rule index 1).

tests/snapshots/simplify_matches__already_flat.bend.snap

@@ -73,3 +73,9 @@ Baz/CtrB3/tag: _
 
 Baz/CtrB3: (Any -> Baz)
 (Baz/CtrB3) = λa λb (b Baz/CtrB3/tag a)
+Warnings:
+In tests/golden_tests/simplify_matches/already_flat.bend :
+In definition 'Rule4':
+  Unreachable pattern matching rule '(Rule4 x)' (rule index 2).
+In definition 'Rule6':
+  Unreachable pattern matching rule '(Rule6 b)' (rule index 1).

tests/snapshots/simplify_matches__double_unwrap_box.bend.snap

@@ -13,3 +13,7 @@ Boxed/Box/tag: _
 
 Boxed/Box: (Any -> Boxed)
 (Boxed/Box) = λa λb (b Boxed/Box/tag a)
+Warnings:
+In tests/golden_tests/simplify_matches/double_unwrap_box.bend :
+In definition 'DoubleUnbox':
+  Unreachable pattern matching rule '(DoubleUnbox * x)' (rule index 1).

tests/snapshots/simplify_matches__irrefutable_case.bend.snap

@@ -22,3 +22,25 @@ unchecked v5: Any
 
 unchecked main: Any
 (main) = (v1, v2, v3, v4, v5)
+Warnings:
+In tests/golden_tests/simplify_matches/irrefutable_case.bend :
+In definition 'v1':
+  Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.
+In definition 'v2':
+  Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.
+In definition 'v3':
+  Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.
+In definition 'v4':
+  Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.
+In definition 'v5':
+  Irrefutable 'match' expression. All cases after variable pattern 'x' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.

tests/snapshots/simplify_matches__nested.bend.snap

@@ -34,3 +34,8 @@ Baz/CtrC/tag: _
 
 Baz/CtrC: Baz
 (Baz/CtrC) = λa (a Baz/CtrC/tag)
+Warnings:
+In tests/golden_tests/simplify_matches/nested.bend :
+In definition 'Rule':
+  Unreachable pattern matching rule '(Rule (Foo/CtrA a b))' (rule index 2).
+  Unreachable pattern matching rule '(Rule x)' (rule index 4).

tests/snapshots/simplify_matches__redundant_with_era.bend.snap

@@ -7,3 +7,8 @@ unchecked Fn2: Any
 
 unchecked main: Any
 (main) = *
+Warnings:
+In tests/golden_tests/simplify_matches/redundant_with_era.bend :
+In definition 'Fn2':
+  Unreachable pattern matching rule '(Fn2 0 *)' (rule index 1).
+  Unreachable pattern matching rule '(Fn2 a *)' (rule index 2).