Fix type checker not substituting type var when unifying match arms (#…

…735)

CHANGELOG.md

@@ -5,6 +5,11 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project does not currently adhere to a particular versioning scheme.
 
+## [Unreleased]
+
+### Fixed
+- Fix type checker not properly unifying all the arms of a match expression.
+
 ## [0.2.37] - 2024-10-18
 
 ### Fixed

src/fun/check/type_check.rs

@@ -591,7 +591,7 @@ fn infer_match_cases(
       // Recurse and unify with the other arms.
       let s = s2.compose(s1);
       let (s_rest, t_rest) = infer_match_cases(env.subst(&s), book, types, adt, rest, adt_s, var_gen)?;
-      let (t_final, s_final) = unify_term(&t1, &t_rest, bod)?;
+      let (t_final, s_final) = unify_term(&t1.subst(&s), &t_rest, bod)?;
 
       Ok((s_final.compose(s_rest).compose(s), t_final))
     } else {

tests/golden_tests.rs

@@ -9,7 +9,7 @@
 //! CLI tool. Then, run `cargo insta review` to review these changes.
 
 use bend::{
-  compile_book, desugar_book,
+  check_book, compile_book, desugar_book,
   diagnostics::{Diagnostics, DiagnosticsConfig, Severity},
   fun::{
     load_book::do_parse_book, net_to_term::net_to_term, parser::ParseBook, term_to_net::Labels, Book, Ctx,
@@ -334,6 +334,21 @@ fn parse_file() {
   })
 }
 
+/// Runs the check command on a file.
+#[test]
+fn check_file() {
+  run_golden_test_dir(function_name!(), &|code, path| {
+    let compile_opts = CompileOpts::default();
+    let diagnostics_cfg = DiagnosticsConfig {
+      unused_definition: Severity::Allow,
+      ..DiagnosticsConfig::new(Severity::Error, true)
+    };
+    let mut book = parse_book_single_file(code, path)?;
+    check_book(&mut book, diagnostics_cfg, compile_opts)?;
+    Ok(book.to_string())
+  })
+}
+
 /// Runs compilation up to the last term-level pass (`bend desugar` command).
 #[test]
 fn desugar_file() {

tests/golden_tests/check_file/type_err_match_arm.bend

@@ -0,0 +1,14 @@
+type Nat_:
+  Zero
+  Succ {x: Unit, pred: Nat_}
+
+type Unit:
+  Unit
+
+Test1: Nat_ -> (Nat_, Nat_)
+Test1 = λx match x {
+  Nat_/Zero: (Nat_/Zero, Nat_/Zero)
+  Nat_/Succ: (x.x, x.pred)
+}
+
+main = *

tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap → tests/snapshots/check_file__fail_type_bad_rec_fn_adt.bend.snap

@@ -1,6 +1,6 @@
 ---
 source: tests/golden_tests.rs
-input_file: tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend
+input_file: tests/golden_tests/check_file/fail_type_bad_rec_fn_adt.bend
 ---
 Errors:
 In λa match a { Box/Box b: (Erase b); }:

tests/snapshots/desugar_file__non_exaustive_limit.bend.snap → tests/snapshots/check_file__non_exaustive_limit.bend.snap

@@ -1,8 +1,8 @@
 ---
 source: tests/golden_tests.rs
-input_file: tests/golden_tests/desugar_file/non_exaustive_limit.bend
+input_file: tests/golden_tests/check_file/non_exaustive_limit.bend
 ---
 Errors:
-[1mIn [4mtests/golden_tests/desugar_file/non_exaustive_limit.bend[0m[1m :[0m
+[1mIn [4mtests/golden_tests/check_file/non_exaustive_limit.bend[0m[1m :[0m
 In definition 'Bar':
   Non-exhaustive pattern matching rule. Constructor 'Foo/B' of type 'Foo' not covered

tests/snapshots/check_file__type_err_match_arm.bend.snap

@@ -0,0 +1,9 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/check_file/type_err_match_arm.bend
+---
+Errors:
+In tests/golden_tests/check_file/type_err_match_arm.bend :
+In definition 'Test1':
+  In (Nat_/Zero, Nat_/Zero):
+  Can't unify '(Nat_, Nat_)' and '(Unit, Nat_)'.