From f467effc99a230504c3780b84f81bd45c50f8338 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 22 Oct 2024 11:30:30 +0000 Subject: [PATCH] Fix type checker not substituting type var when unifying match arms (#735) --- CHANGELOG.md | 5 +++++ src/fun/check/type_check.rs | 2 +- tests/golden_tests.rs | 17 ++++++++++++++++- .../fail_type_bad_rec_fn_adt.bend | 0 .../non_exaustive_limit.bend | 0 .../check_file/type_err_match_arm.bend | 14 ++++++++++++++ ...ck_file__fail_type_bad_rec_fn_adt.bend.snap} | 2 +- ...> check_file__non_exaustive_limit.bend.snap} | 4 ++-- .../check_file__type_err_match_arm.bend.snap | 9 +++++++++ 9 files changed, 48 insertions(+), 5 deletions(-) rename tests/golden_tests/{desugar_file => check_file}/fail_type_bad_rec_fn_adt.bend (100%) rename tests/golden_tests/{desugar_file => check_file}/non_exaustive_limit.bend (100%) create mode 100644 tests/golden_tests/check_file/type_err_match_arm.bend rename tests/snapshots/{desugar_file__fail_type_bad_rec_fn_adt.bend.snap => check_file__fail_type_bad_rec_fn_adt.bend.snap} (67%) rename tests/snapshots/{desugar_file__non_exaustive_limit.bend.snap => check_file__non_exaustive_limit.bend.snap} (55%) create mode 100644 tests/snapshots/check_file__type_err_match_arm.bend.snap diff --git a/CHANGELOG.md b/CHANGELOG.md index 608ed60d1..0b84da7f0 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/fun/check/type_check.rs b/src/fun/check/type_check.rs index 8bcb8be27..63fc3c34c 100644 --- a/src/fun/check/type_check.rs +++ b/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 { diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index b47270d62..cf6cd3a20 100644 --- a/tests/golden_tests.rs +++ b/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() { diff --git a/tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend b/tests/golden_tests/check_file/fail_type_bad_rec_fn_adt.bend similarity index 100% rename from tests/golden_tests/desugar_file/fail_type_bad_rec_fn_adt.bend rename to tests/golden_tests/check_file/fail_type_bad_rec_fn_adt.bend diff --git a/tests/golden_tests/desugar_file/non_exaustive_limit.bend b/tests/golden_tests/check_file/non_exaustive_limit.bend similarity index 100% rename from tests/golden_tests/desugar_file/non_exaustive_limit.bend rename to tests/golden_tests/check_file/non_exaustive_limit.bend diff --git a/tests/golden_tests/check_file/type_err_match_arm.bend b/tests/golden_tests/check_file/type_err_match_arm.bend new file mode 100644 index 000000000..b7427541d --- /dev/null +++ b/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 = * diff --git a/tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap b/tests/snapshots/check_file__fail_type_bad_rec_fn_adt.bend.snap similarity index 67% rename from tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap rename to tests/snapshots/check_file__fail_type_bad_rec_fn_adt.bend.snap index 843358d27..f6fcf5ff6 100644 --- a/tests/snapshots/desugar_file__fail_type_bad_rec_fn_adt.bend.snap +++ b/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); }: diff --git a/tests/snapshots/desugar_file__non_exaustive_limit.bend.snap b/tests/snapshots/check_file__non_exaustive_limit.bend.snap similarity index 55% rename from tests/snapshots/desugar_file__non_exaustive_limit.bend.snap rename to tests/snapshots/check_file__non_exaustive_limit.bend.snap index 72a3dd7e7..a15fd52f6 100644 --- a/tests/snapshots/desugar_file__non_exaustive_limit.bend.snap +++ b/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: -In tests/golden_tests/desugar_file/non_exaustive_limit.bend : +In tests/golden_tests/check_file/non_exaustive_limit.bend : In definition 'Bar': Non-exhaustive pattern matching rule. Constructor 'Foo/B' of type 'Foo' not covered diff --git a/tests/snapshots/check_file__type_err_match_arm.bend.snap b/tests/snapshots/check_file__type_err_match_arm.bend.snap new file mode 100644 index 000000000..433908526 --- /dev/null +++ b/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_)'.