Skip to content

Commit e3d4806

Browse files
fix(typecheck): zero-arg thunk calls, tuple-destructuring let, RuntimeError catch — stdlib AOT 14/19 (#128) (#186)
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) <noreply@anthropic.com>
1 parent c1fcd21 commit e3d4806

3 files changed

Lines changed: 42 additions & 7 deletions

File tree

lib/resolve.ml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,10 @@ let seed_builtins (symbols : Symbol.t) : unit =
8888
let defc name =
8989
let _ = Symbol.define symbols name SKConstructor Span.dummy Public in ()
9090
in
91-
defc "Some"; defc "None"; defc "Ok"; defc "Err"
91+
defc "Some"; defc "None"; defc "Ok"; defc "Err";
92+
(* Interpreter builtin exception variant, pattern-matched in try/catch
93+
arms by the honest stdlib (testing.affine, result.affine). *)
94+
defc "RuntimeError"
9295

9396
(** Create a new resolution context, pre-seeded with builtins. *)
9497
let create_context () : context =

lib/typecheck.ml

Lines changed: 36 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -709,7 +709,24 @@ let rec synth (ctx : context) (expr : expr) : ty result =
709709
(* Function application *)
710710
| ExprApp (fn_expr, args) ->
711711
let* fn_ty = synth ctx fn_expr in
712-
apply_args ctx fn_ty args
712+
begin match args with
713+
| [] ->
714+
(* A zero-argument call [f()]. Zero-parameter function
715+
*declarations* are typed as their bare return type (the param
716+
fold in [check_fn_decl] is over []), so [apply_args fn_ty []]
717+
correctly yields that type. But an explicit [() -> T] thunk
718+
type — a record field, a parameter, a lambda — lowers to
719+
[TArrow (Unit, _, T, _)]; invoking it must consume the unit and
720+
yield [T]. Curried/partial application never reaches this branch
721+
with [args = []] (it always carries a non-empty arg list at the
722+
[ExprApp] site), so peeling a single unit arrow here is sound. *)
723+
begin match repr fn_ty with
724+
| TArrow (param_ty, _q, ret_ty, _eff)
725+
when repr param_ty = ty_unit -> Ok ret_ty
726+
| _ -> apply_args ctx fn_ty args
727+
end
728+
| _ -> apply_args ctx fn_ty args
729+
end
713730

714731
(* Tuple *)
715732
| ExprTuple exprs ->
@@ -1086,10 +1103,13 @@ and check_stmt (ctx : context) (stmt : stmt) : unit result =
10861103
synth ctx sl_value
10871104
end in
10881105
exit_level ctx;
1089-
let sc = generalize ctx val_ty in
10901106
let* bindings = check_pattern ctx sl_pat val_ty in
1091-
List.iter (fun (name, _ty) ->
1092-
bind_scheme ctx name sc
1107+
(* Bind each name to *its own* type. For a plain [let x = e] the sole
1108+
binding's type is [val_ty], so this generalizes exactly as before;
1109+
for a destructuring [let (a, b) = e] / record pattern each name is
1110+
generalized at its component type rather than the whole tuple. *)
1111+
List.iter (fun (name, ty) ->
1112+
bind_scheme ctx name (generalize ctx ty)
10931113
) bindings;
10941114
Ok ()
10951115
| StmtExpr e ->
@@ -1274,6 +1294,18 @@ let register_builtins (ctx : context) : unit =
12741294
{ sc_tyvars = [(v_erra, Types.KType); (v_errb, Types.KType)];
12751295
sc_effvars = []; sc_rowvars = []; sc_body = err_ty };
12761296
Hashtbl.replace ctx.constructor_env "Err" err_ty;
1297+
(* [RuntimeError(String)] is the interpreter's builtin exception variant
1298+
(see [Interp]: panics surface as [VVariant ("RuntimeError", VString
1299+
msg)]). The honest stdlib pattern-matches it in [try/catch] arms
1300+
(stdlib/testing.affine, stdlib/result.affine). The catch error type is
1301+
opaque (a fresh tyvar per [try]), so the result is left polymorphic and
1302+
unifies with whatever the arm expects. *)
1303+
let (v_rte, t_rte) = fresh_named () in
1304+
let rte_ty = TArrow (ty_string, QOmega, t_rte, EPure) in
1305+
bind_scheme ctx "RuntimeError"
1306+
{ sc_tyvars = [(v_rte, Types.KType)]; sc_effvars = []; sc_rowvars = [];
1307+
sc_body = rte_ty };
1308+
Hashtbl.replace ctx.constructor_env "RuntimeError" rte_ty;
12771309
bind_var ctx "string_get"
12781310
(TArrow (ty_string, QOmega, TArrow (ty_int, QOmega, ty_char, EPure), EPure));
12791311
bind_var ctx "string_sub"

stdlib/testing.affine

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ fn assert_length<T>(list: [T], expected_len: Int, message: String) -> () {
133133

134134
/// Assert list contains a specific element
135135
fn assert_contains<T>(list: [T], element: T, message: String) -> () {
136-
let found = false;
136+
let mut found = false;
137137
for x in list {
138138
if x == element {
139139
found = true;
@@ -303,7 +303,7 @@ fn bench(f: () -> (), iterations: Int) -> BenchResult {
303303
{
304304
iterations: iterations,
305305
total_time: tot,
306-
avg_time: tot / (iterations + 0.0)
306+
avg_time: tot / float(iterations)
307307
}
308308
}
309309

0 commit comments

Comments
 (0)