Repository: HigherOrderCO/Bend
File: src/term/check/exhaustiveness.rs (Rust)

Code before:
            // Rules with a var pattern are relevant to all constructors.
            Pattern::Var(_) => next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx)),
            Pattern::Ctr(ctr_nam, _) => next_rules_to_check.get_mut(ctr_nam).unwrap().push(rule_idx),
            Pattern::Num(..) => todo!(),
            Pattern::Tup(..) => todo!(),
          }
        }
        // Match each constructor of the current pattern and recursively check the next pattern.
        for (ctr, rules_to_check) in next_rules_to_check {
          if rules_to_check.is_empty() {
            match_path.extend(vec![Pattern::Ctr(ctr.clone(), vec![]); types.len()]);
            let missing = match_path.iter().map(|p| p.to_string()).join(" ");
            return Err(format!(
              "Non-exhaustive pattern at definition '{}'. Hint: {} not covered.",
              def_name, missing
            ));
          } else {
            let mut match_path = match_path.clone();
            match_path.push(Pattern::Ctr(ctr, vec![]));
            check_pattern(&mut match_path, adts, rules, &types[1 ..], rules_to_check, def_name)?;
          }
        }
      }
      Type::Tup | Type::Num => {
        let mut match_path = match_path.clone();
        match_path.push(Pattern::Var(Some(Name::new("_"))));
        check_pattern(&mut match_path, adts, rules, &types[1 ..], rules_to_check, def_name)?
      }
    }
  }
  Ok(())
}


Review comment (bug):
If you push `Pattern::Var` here, in case of an exhaustiveness error, the error message will be wrong.
Say for example:
```
Foo (a, b) False = ...
```
With this code i think we'll get the error `Non-exhaustive pattern at definition 'Foo'. Hint: (Foo _ True) not covered` instead of `Hint: (Foo (_, _) True) not covered` or something similar (i'm not sure how these patterns are printed here)

Code after:
            // Rules with a var pattern are relevant to all constructors.
            Pattern::Var(_) => next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx)),
            Pattern::Ctr(ctr_nam, _) => next_rules_to_check.get_mut(ctr_nam).unwrap().push(rule_idx),
            Pattern::Num(..) => todo!(),
            Pattern::Tup(..) => todo!(),
          }
        }
        // Match each constructor of the current pattern and recursively check the next pattern.
        for (ctr, rules_to_check) in next_rules_to_check {
          if rules_to_check.is_empty() {
            match_path.extend(vec![Pattern::Ctr(ctr.clone(), vec![]); types.len()]);
            let missing = match_path.iter().map(|p| p.to_string()).join(" ");
            return Err(format!(
              "Non-exhaustive pattern at definition '{}'. Hint: {} not covered.",
              def_name, missing
            ));
          } else {
            let mut match_path = match_path.clone();
            match_path.push(Pattern::Ctr(ctr, vec![]));
            check_pattern(&mut match_path, adts, rules, &types[1 ..], rules_to_check, def_name)?;
          }
        }
      }
      Type::Tup => {
        let mut match_path = match_path.clone();
        match_path.push(Pattern::Tup(Some(Name::new("_")), Some(Name::new("_"))));
        check_pattern(&mut match_path, adts, rules, &types[1 ..], rules_to_check, def_name)?
      }
      Type::Num => {
        let mut next_rules_to_check: BTreeMap<Name, Vec<usize>> =
          BTreeMap::from([(Name::new("0"), vec![]), (Name::new("+"), vec![])]);
        for rule_idx in rules_to_check {
          let pat = &rules[rule_idx].pats[match_path.len()];
          match pat {
            Pattern::Num(MatchNum::Zero) => {
              next_rules_to_check.get_mut(&Name(format!("0"))).unwrap().push(rule_idx);
            }
            Pattern::Num(MatchNum::Succ(..)) => {
              next_rules_to_check.get_mut(&Name(format!("+"))).unwrap().push(rule_idx);
            }
            other => {
              return Err(format!("Expected a number but found '{other}' at definition '{def_name}'."));
            }
          }
        }
        for (num, rules_to_check) in next_rules_to_check {
          if rules_to_check.is_empty() {
            return Err(format!(
              "Non-exhaustive pattern at definition '{}'. Number pattern '{}' not covered at position {}.",
              def_name,
              num,