From 644c55956d00e69192452aa4ad2817c930a0518f Mon Sep 17 00:00:00 2001 From: Dylan Moss Date: Sun, 23 Nov 2025 16:13:10 +0000 Subject: [PATCH 1/3] Add concrete type error checking to system-f-omega --- system-f-omega/src/errors.rs | 3 +++ system-f-omega/src/main.rs | 5 ++--- system-f-omega/src/worklist.rs | 18 +++++++++++++++--- 3 files changed, 20 insertions(+), 6 deletions(-) diff --git a/system-f-omega/src/errors.rs b/system-f-omega/src/errors.rs index ea8055a..cf4c4eb 100644 --- a/system-f-omega/src/errors.rs +++ b/system-f-omega/src/errors.rs @@ -51,6 +51,9 @@ pub enum TypeError { span: Option, }, + #[error("Type unification error: cannot unify type '{left}' with '{right}'")] + TypeUnificationError { left: CoreType, right: CoreType }, + #[error("Instantiation failure: cannot instantiate '{var}' with '{ty}'")] InstantiationError { var: String, diff --git a/system-f-omega/src/main.rs b/system-f-omega/src/main.rs index 3e5e6ba..055d7ee 100644 --- a/system-f-omega/src/main.rs +++ b/system-f-omega/src/main.rs @@ -436,12 +436,11 @@ mod tests { #[test] fn test_type_error() { let source = r#" - wrong :: Int; + wrong :: Unit; wrong = 42; "#; - // This should pass - just a simple value binding - assert!(typecheck_module(source, "test.hs").is_ok()); + assert!(typecheck_module(source, "test.hs").is_err()); } #[test] diff --git a/system-f-omega/src/worklist.rs b/system-f-omega/src/worklist.rs index 274d6cd..0e1ab7c 100644 --- a/system-f-omega/src/worklist.rs +++ b/system-f-omega/src/worklist.rs @@ -107,9 +107,21 @@ impl Worklist { *kind = TyVarKind::Solved(ty); return Ok(()); } - TyVarKind::Solved(_) => { - // Variable already solved, that's OK - return Ok(()); + TyVarKind::Solved(solved_ty) => { + let solved_ty = solved_ty.clone(); + + // Check that ty and solved_ty are not conflicting concrete types + match (ty.clone(), solved_ty.clone()) { + (CoreType::Con(ty_name1), CoreType::Con(ty_name2)) + if ty_name1 != ty_name2 => + { + return Err(TypeError::TypeUnificationError { + left: ty, + right: solved_ty, + }); + } + _ => return Ok(()), + } } _ => { // Skip universal variables, markers, etc. From ff65422ab1a3f42a81211c19f529ea9aa2b85148 Mon Sep 17 00:00:00 2001 From: Dylan Moss Date: Sun, 23 Nov 2025 16:15:00 +0000 Subject: [PATCH 2/3] Clean up clones --- system-f-omega/src/worklist.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/system-f-omega/src/worklist.rs b/system-f-omega/src/worklist.rs index 0e1ab7c..39e97a5 100644 --- a/system-f-omega/src/worklist.rs +++ b/system-f-omega/src/worklist.rs @@ -108,8 +108,6 @@ impl Worklist { return Ok(()); } TyVarKind::Solved(solved_ty) => { - let solved_ty = solved_ty.clone(); - // Check that ty and solved_ty are not conflicting concrete types match (ty.clone(), solved_ty.clone()) { (CoreType::Con(ty_name1), CoreType::Con(ty_name2)) @@ -117,7 +115,7 @@ impl Worklist { { return Err(TypeError::TypeUnificationError { left: ty, - right: solved_ty, + right: solved_ty.clone(), }); } _ => return Ok(()), From d18b6635934bafc4b19091ab528567241fca7685 Mon Sep 17 00:00:00 2001 From: Dylan Moss Date: Sun, 23 Nov 2025 17:33:26 +0000 Subject: [PATCH 3/3] Add other type unification checks --- system-f-omega/src/worklist.rs | 52 +++++++++++++++++++++++++++------- 1 file changed, 41 insertions(+), 11 deletions(-) diff --git a/system-f-omega/src/worklist.rs b/system-f-omega/src/worklist.rs index 39e97a5..3bc3390 100644 --- a/system-f-omega/src/worklist.rs +++ b/system-f-omega/src/worklist.rs @@ -47,6 +47,39 @@ pub enum Judgment { }, } +fn can_types_unify(ty1: &CoreType, ty2: &CoreType) -> bool { + // Checks if types can unify or if they conflict. E.g. + // int <> int => can unify + // bool <> int => conflict! + // (int -> int) <> (int -> bool) => conflict! + + match (ty1, ty2) { + (CoreType::Var(var_name1), CoreType::Var(var_name2)) => var_name1 == var_name2, + (CoreType::ETVar(_), _) | (_, CoreType::ETVar(_)) => true, + (CoreType::Con(con_ty1), CoreType::Con(con_ty2)) => con_ty1 == con_ty2, + (CoreType::Arrow(ty1_left, ty1_right), CoreType::Arrow(ty2_left, ty2_right)) => { + can_types_unify(ty1_left, ty2_left) && can_types_unify(ty1_right, ty2_right) + } + (CoreType::Forall(quantifier1, ty1_inner), CoreType::Forall(quantifier2, ty2_inner)) => { + quantifier1 == quantifier2 && can_types_unify(ty1_inner, ty2_inner) + } + (CoreType::App(ty1_left, ty1_right), CoreType::App(ty2_left, ty2_right)) => { + can_types_unify(ty1_left, ty2_left) && can_types_unify(ty1_right, ty2_right) + } + (CoreType::Product(sub_types1), CoreType::Product(sub_types2)) => { + if sub_types1.len() != sub_types2.len() { + false + } else { + sub_types1 + .iter() + .zip(sub_types2.iter()) + .all(|(sub_type1, sub_type2)| can_types_unify(sub_type1, sub_type2)) + } + } + _ => false, + } +} + #[derive(Debug, Clone)] pub struct Worklist { entries: Vec, @@ -108,17 +141,14 @@ impl Worklist { return Ok(()); } TyVarKind::Solved(solved_ty) => { - // Check that ty and solved_ty are not conflicting concrete types - match (ty.clone(), solved_ty.clone()) { - (CoreType::Con(ty_name1), CoreType::Con(ty_name2)) - if ty_name1 != ty_name2 => - { - return Err(TypeError::TypeUnificationError { - left: ty, - right: solved_ty.clone(), - }); - } - _ => return Ok(()), + // Checks that the solved type does not conflict with ty + if can_types_unify(&ty, solved_ty) { + return Ok(()); + } else { + return Err(TypeError::TypeUnificationError { + left: ty, + right: solved_ty.clone(), + }); } } _ => {