From 45f14c3bf2f5a11530b37c661d94d700fb3702e5 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 03:17:04 +0100 Subject: [PATCH] =?UTF-8?q?fix(typecheck):=20zero-arg=20thunk=20calls,=20t?= =?UTF-8?q?uple-destructuring=20let,=20RuntimeError=20catch=20=E2=80=94=20?= =?UTF-8?q?stdlib=20AOT=2014/19=20(#128)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three compiler-level fixes surfaced by stdlib/testing.affine: - ExprApp f []: a zero-arg call f() on an explicit () -> T thunk (record field / param / lambda) now consumes the unit and yields T. Zero-param fn *declarations* are bare-return-typed, so they are unaffected; curried/partial application never reaches this branch with an empty arg list, so peeling one unit arrow is sound. - StmtLet: each destructured name is generalized at *its own* component type, not the whole value type. let x = e is unchanged; let (a, b) = e now types a and b at their element types. - RuntimeError(String): registered as the interpreter's builtin exception variant (resolve seed + typecheck constructor_env) so try/catch arms in the honest stdlib resolve and type-check. Plus stdlib/testing.affine: let mut found; tot / float(iterations). Full suite 233/233, zero regression. Refs #128. Co-Authored-By: Claude Opus 4.7 (1M context) --- lib/resolve.ml | 5 ++++- lib/typecheck.ml | 40 ++++++++++++++++++++++++++++++++++++---- stdlib/testing.affine | 4 ++-- 3 files changed, 42 insertions(+), 7 deletions(-) diff --git a/lib/resolve.ml b/lib/resolve.ml index 0727c0ba..fce6b58d 100644 --- a/lib/resolve.ml +++ b/lib/resolve.ml @@ -88,7 +88,10 @@ let seed_builtins (symbols : Symbol.t) : unit = let defc name = let _ = Symbol.define symbols name SKConstructor Span.dummy Public in () in - defc "Some"; defc "None"; defc "Ok"; defc "Err" + defc "Some"; defc "None"; defc "Ok"; defc "Err"; + (* Interpreter builtin exception variant, pattern-matched in try/catch + arms by the honest stdlib (testing.affine, result.affine). *) + defc "RuntimeError" (** Create a new resolution context, pre-seeded with builtins. *) let create_context () : context = diff --git a/lib/typecheck.ml b/lib/typecheck.ml index dcf000d7..3de2e3d6 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -709,7 +709,24 @@ let rec synth (ctx : context) (expr : expr) : ty result = (* Function application *) | ExprApp (fn_expr, args) -> let* fn_ty = synth ctx fn_expr in - apply_args ctx fn_ty args + begin match args with + | [] -> + (* A zero-argument call [f()]. Zero-parameter function + *declarations* are typed as their bare return type (the param + fold in [check_fn_decl] is over []), so [apply_args fn_ty []] + correctly yields that type. But an explicit [() -> T] thunk + type — a record field, a parameter, a lambda — lowers to + [TArrow (Unit, _, T, _)]; invoking it must consume the unit and + yield [T]. Curried/partial application never reaches this branch + with [args = []] (it always carries a non-empty arg list at the + [ExprApp] site), so peeling a single unit arrow here is sound. *) + begin match repr fn_ty with + | TArrow (param_ty, _q, ret_ty, _eff) + when repr param_ty = ty_unit -> Ok ret_ty + | _ -> apply_args ctx fn_ty args + end + | _ -> apply_args ctx fn_ty args + end (* Tuple *) | ExprTuple exprs -> @@ -1086,10 +1103,13 @@ and check_stmt (ctx : context) (stmt : stmt) : unit result = synth ctx sl_value end in exit_level ctx; - let sc = generalize ctx val_ty in let* bindings = check_pattern ctx sl_pat val_ty in - List.iter (fun (name, _ty) -> - bind_scheme ctx name sc + (* Bind each name to *its own* type. For a plain [let x = e] the sole + binding's type is [val_ty], so this generalizes exactly as before; + for a destructuring [let (a, b) = e] / record pattern each name is + generalized at its component type rather than the whole tuple. *) + List.iter (fun (name, ty) -> + bind_scheme ctx name (generalize ctx ty) ) bindings; Ok () | StmtExpr e -> @@ -1274,6 +1294,18 @@ let register_builtins (ctx : context) : unit = { sc_tyvars = [(v_erra, Types.KType); (v_errb, Types.KType)]; sc_effvars = []; sc_rowvars = []; sc_body = err_ty }; Hashtbl.replace ctx.constructor_env "Err" err_ty; + (* [RuntimeError(String)] is the interpreter's builtin exception variant + (see [Interp]: panics surface as [VVariant ("RuntimeError", VString + msg)]). The honest stdlib pattern-matches it in [try/catch] arms + (stdlib/testing.affine, stdlib/result.affine). The catch error type is + opaque (a fresh tyvar per [try]), so the result is left polymorphic and + unifies with whatever the arm expects. *) + let (v_rte, t_rte) = fresh_named () in + let rte_ty = TArrow (ty_string, QOmega, t_rte, EPure) in + bind_scheme ctx "RuntimeError" + { sc_tyvars = [(v_rte, Types.KType)]; sc_effvars = []; sc_rowvars = []; + sc_body = rte_ty }; + Hashtbl.replace ctx.constructor_env "RuntimeError" rte_ty; bind_var ctx "string_get" (TArrow (ty_string, QOmega, TArrow (ty_int, QOmega, ty_char, EPure), EPure)); bind_var ctx "string_sub" diff --git a/stdlib/testing.affine b/stdlib/testing.affine index 14b00759..7c61d297 100644 --- a/stdlib/testing.affine +++ b/stdlib/testing.affine @@ -133,7 +133,7 @@ fn assert_length(list: [T], expected_len: Int, message: String) -> () { /// Assert list contains a specific element fn assert_contains(list: [T], element: T, message: String) -> () { - let found = false; + let mut found = false; for x in list { if x == element { found = true; @@ -303,7 +303,7 @@ fn bench(f: () -> (), iterations: Int) -> BenchResult { { iterations: iterations, total_time: tot, - avg_time: tot / (iterations + 0.0) + avg_time: tot / float(iterations) } }