From fc2acbf614f3780686335d12a052d39f26e4bad8 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 17 May 2026 13:00:59 +0100 Subject: [PATCH] fix(typecheck): instantiate generic fn type params; prelude `mut` (#135 slice 7) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #135 slice 7 — root cause was NOT empty-array literals (those compile). It was a fundamental let-polymorphism bug: `check_fn_decl` never registered a function's explicit `` type parameters, so an uppercase param `x: T` lowered via `lower_type_expr`'s `TyCon` fallthrough to a *rigid* `TCon "T"`. `generalize` ignores `TCon`, so every generic top-level function got `sc_tyvars = []` — effectively monomorphic. The first call pinned `T`; any second instantiation (or the very first against a concrete arg) failed `Unify.TypeMismatch (T, Int)`, and `use prelude::{…}` import-checks failed transitively (result/option/…). Fix (mirrors the existing let-generalization discipline): in `check_fn_decl`, before lowering, `enter_level` and register each `fd_type_params` name in `ctx.type_env` as a fresh tyvar at the deeper level; `exit_level` before the existing `generalize`, so those vars (level > ctx.level) become the scheme's quantified `sc_tyvars`. Scoped save/restore of `type_env` so params don't leak. Applied to both the extern and normal branches. Also fixes genuine stdlib bugs surfaced once typecheck passed: prelude.affine `map`/`filter`/`range`/`repeat`/`fold` reassigned immutable `let` bindings (`result`/`i`/`acc`) → `let mut`. With both, **prelude.affine now compiles end-to-end** (resolve→typecheck→codegen). Verification: `id` instantiated at Int+Bool, generic `fold` from a monomorphic Int `sum`, monomorphic fns — all compile; the fundamental change regressed **none** of the suite. 2 regression tests; full suite green (230). Unblocks the typecheck wall for prelude (and, once visibility/slice 8 lands, result/option/collections via `use prelude`). Advances #135. Refs #128, #135. Co-Authored-By: Claude Opus 4.7 (1M context) --- lib/typecheck.ml | 30 +++++++++++++++++++++++++++++- stdlib/prelude.affine | 14 +++++++------- test/test_e2e.ml | 19 +++++++++++++++++++ 3 files changed, 55 insertions(+), 8 deletions(-) diff --git a/lib/typecheck.ml b/lib/typecheck.ml index 29a8542b..75bda100 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -1312,6 +1312,28 @@ let register_builtins (ctx : context) : unit = (** Check a top-level function declaration. *) let check_fn_decl (ctx : context) (fd : fn_decl) : unit result = + (* #135 slice 7: register the explicit `` type parameters as fresh, + generalizable unification variables before lowering param/return + types. Without this, an uppercase param like `x: T` lowered to a + *rigid* `TCon "T"` (lower_type_expr TyCon fallthrough), which + `generalize` ignores — so every generic top-level function was + effectively monomorphic and the second instantiation blew up with + `Unify.TypeMismatch (T, Int)` (and `use prelude::{…}` import-checks + failed transitively). Mirrors the let-generalization discipline: + enter a deeper level, create the vars there, generalize at the outer + level so they become the scheme's quantified tyvars. *) + let tp_names = List.map (fun (tp : type_param) -> tp.tp_name.name) + fd.fd_type_params in + let saved_tp = List.map (fun n -> (n, Hashtbl.find_opt ctx.type_env n)) + tp_names in + enter_level ctx; + List.iter (fun n -> + Hashtbl.replace ctx.type_env n (fresh_tyvar ctx.level)) tp_names; + let restore_tp () = + List.iter (fun (n, old) -> match old with + | Some t -> Hashtbl.replace ctx.type_env n t + | None -> Hashtbl.remove ctx.type_env n) saved_tp + in (* Extern functions have no body — register the signature so callers can typecheck against it, then bail out before the body-check pass. *) if fd.fd_body = FnExtern then begin @@ -1340,8 +1362,10 @@ let check_fn_decl (ctx : context) (fd : fn_decl) : unit result = in TArrow (param_ty, q, acc, fn_eff) ) param_tys fd.fd_params ret_ty in + exit_level ctx; let sc = generalize ctx fn_ty in bind_scheme ctx fd.fd_name.name sc; + restore_tp (); Ok () end else @@ -1396,9 +1420,13 @@ let check_fn_decl (ctx : context) (fd : fn_decl) : unit result = | Some sc -> Hashtbl.replace ctx.name_types n sc | None -> Hashtbl.remove ctx.name_types n ) old; - (* Generalize and rebind the function with its polymorphic type *) + (* Generalize and rebind the function with its polymorphic type. + exit_level first so the `` type-param vars (created at the deeper + level above) are quantified by `generalize` (#135 slice 7). *) + exit_level ctx; let sc = generalize ctx fn_ty in bind_scheme ctx fd.fd_name.name sc; + restore_tp (); Ok () (** Register a type declaration in the context. *) diff --git a/stdlib/prelude.affine b/stdlib/prelude.affine index 3dfed1b7..e3705a76 100644 --- a/stdlib/prelude.affine +++ b/stdlib/prelude.affine @@ -25,7 +25,7 @@ type Result = Ok(T) | Err(E) // ============================================================================ fn map(arr: [T], f: T -> U) -> [U] { - let result = []; + let mut result = []; for x in arr { result = result ++ [f(x)]; } @@ -33,7 +33,7 @@ fn map(arr: [T], f: T -> U) -> [U] { } fn filter(arr: [T], predicate: T -> Bool) -> [T] { - let result = []; + let mut result = []; for x in arr { if predicate(x) { result = result ++ [x]; @@ -43,7 +43,7 @@ fn filter(arr: [T], predicate: T -> Bool) -> [T] { } fn fold(arr: [T], init: U, f: (U, T) -> U) -> U { - let acc = init; + let mut acc = init; for x in arr { acc = f(acc, x); } @@ -121,8 +121,8 @@ fn any(arr: [Bool]) -> Bool { // ============================================================================ fn range(start: Int, end: Int) -> [Int] { - let result = []; - let i = start; + let mut result = []; + let mut i = start; while i < end { result = result ++ [i]; i = i + 1; @@ -131,8 +131,8 @@ fn range(start: Int, end: Int) -> [Int] { } fn repeat(value: T, n: Int) -> [T] { - let result = []; - let i = 0; + let mut result = []; + let mut i = 0; while i < n { result = result ++ [value]; i = i + 1; diff --git a/test/test_e2e.ml b/test/test_e2e.ml index dfb4fcbc..7a5d15f2 100644 --- a/test/test_e2e.ml +++ b/test/test_e2e.ml @@ -3363,6 +3363,23 @@ let test_trait_sig_and_assoc_not_regressed () = pub fn next(mut self) -> Option; }|}) +(* Issue #135 slice 7: top-level generic functions must instantiate their + `` scheme with fresh vars per call. Before, `` lowered to a rigid + `TCon "T"` that `generalize` ignored, so any 2nd instantiation failed + with `Unify.TypeMismatch (T, Int)` (and `use prelude` import-checks + failed transitively). *) +let test_generic_fn_multi_instantiation () = + Alcotest.(check bool) "id called at Int and Bool in one program" true + (parse_check_passes + {|fn id(x: T) -> T { return x; } + fn use_it() -> Bool { let a = id(1); let b = id(true); return b; }|}) + +let test_generic_hof_monomorphic_caller () = + Alcotest.(check bool) "generic fold called by monomorphic Int sum" true + (parse_check_passes + {|fn fold(arr: [T], init: U, f: (U, T) -> U) -> U { return init; } + fn sum(a: [Int]) -> Int { return fold(a, 0, fn(acc, x) => acc + x); }|}) + let test_multi_arg_arrow () = Alcotest.(check bool) "(A, B) -> C parses + typechecks" true (parse_check_passes @@ -3418,6 +3435,8 @@ let type_syntax_sugar_tests = [ Alcotest.test_case "effect E; + -> T / E (#135 slice 3)" `Quick test_bare_effect_and_effect_row; Alcotest.test_case "trait default body + ref self (#135 sl5)" `Quick test_trait_default_body; Alcotest.test_case "trait sig + assoc non-regressed (#135 sl5)" `Quick test_trait_sig_and_assoc_not_regressed; + Alcotest.test_case "generic fn multi-instantiation (#135 sl7)" `Quick test_generic_fn_multi_instantiation; + Alcotest.test_case "generic HOF + mono caller (#135 sl7)" `Quick test_generic_hof_monomorphic_caller; Alcotest.test_case "(A, B) -> C (multi-arg arrow)" `Quick test_multi_arg_arrow; Alcotest.test_case "(A, B) without arrow remains tuple" `Quick test_tuple_type_still_works; ]