From e3866abe4be97ad0b82b0e3f4eb0fbab3cce9d9b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 10:13:58 +0100 Subject: [PATCH] feat(effects): infer Partial from catch-less try/?; check vs declared row (Refs #59) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit STAGE-B effect-tracking spine. Until now ctx.current_eff was declared but never read or mutated — effect inference did nothing, and #59's explicit motivating case ('{Partial} — short-circuit failure, ? on Result') produced no tracking. Root-cause, single concrete effect source for tracking-only v1: - ExprTry with no catch arm (incl. the 'e?' desugar, parser.mly expr_postfix QUESTION) unions Partial into ctx.current_eff; a handled try (catch arm present) discharges it and adds nothing. - check_fn_decl now snapshots/resets current_eff around the body, then — only when an effect row is *explicitly declared* — requires the inferred row ⊆ declared (Effect.eff_subset), erroring with a new EffectNotDeclared type_error. Undeclared rows stay permissive (tracking-only v1), so blast radius is zero: no stdlib/test uses '?' or an explicit row. Other effect sources (IO calls, Async) remain unconstrained for now — deliberately scoped; this stands up the accumulate→subsume path they will plug into, it does not fake full inference. Tests: test/test_effects.ml — declared /{Partial}+? ok; declared /{IO}+? rejected (#59 mismatch naming Partial); undeclared permissive; handled try adds no Partial. Full gate 257/257 (253 + 4, no regression). Refs #59 (left open for user joint-close per requirements-target rule). Co-Authored-By: Claude Opus 4.7 (1M context) --- lib/typecheck.ml | 41 ++++++++++++++++++++++ test/test_effects.ml | 83 ++++++++++++++++++++++++++++++++++++++++++++ test/test_main.ml | 1 + 3 files changed, 125 insertions(+) create mode 100644 test/test_effects.ml diff --git a/lib/typecheck.ml b/lib/typecheck.ml index 461b3a99..cb6354f6 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -106,6 +106,12 @@ type type_error = | UnknownEffect of string (** Effect name not in the v1 registry, not a legacy alias, and not a user-declared effect (issue #59). *) + | EffectNotDeclared of { inferred : string; declared : string } + (** The function body performs an effect (v1: `Partial`, from a + catch-less `try` / the `?` desugar) that is absent from the + function's explicitly declared effect row (issue #59). Only + raised when a row is declared; an undeclared row stays + permissive under tracking-only v1. *) (** Format a type error for human consumption. *) let show_type_error = function @@ -143,6 +149,13 @@ let show_type_error = function (String.concat ", " Effect.v1_effects) (String.concat ", " Effect.reserved_effects) name + | EffectNotDeclared { inferred; declared } -> + Printf.sprintf + "Effect mismatch (issue #59): the function body performs %s but its \ + declared effect row is /{%s}. A catch-less `try` / the `?` operator \ + performs `Partial` — add it to the row, e.g. /{%s}." + inferred declared + (if declared = "" then "Partial" else declared ^ ", Partial") let format_type_error = show_type_error @@ -1080,6 +1093,17 @@ let rec synth (ctx : context) (expr : expr) : ty result = let* fin_ty = synth_block ctx blk in unify_or_err fin_ty ty_unit in + (* issue #59: a catch-less `try` — including the `e?` desugar + (parser.mly: `expr_postfix QUESTION`) — lets failure + short-circuit out of the body, so the enclosing function + performs `Partial`. A handled `try` (a catch arm is present) + discharges the failure locally and adds no effect. This is the + single concrete effect source wired for tracking-only v1; the + row is enforced against the declared one in [check_fn_decl]. *) + (match et_catch with + | None -> + ctx.current_eff <- Effect.union_eff ctx.current_eff (ESingleton "Partial") + | Some _ -> ()); Ok result_ty (* Unsafe *) @@ -1514,6 +1538,12 @@ let check_fn_decl (ctx : context) (fd : fn_decl) : unit result = bind_var ctx p.p_name.name ty; (p.p_name.name, old) ) fd.fd_params param_tys in + (* issue #59 — effect inference spine: infer this body's effect row + into a fresh accumulator, then (only if a row was explicitly + declared) require the inferred row to be a subset of it. An + undeclared row stays permissive under tracking-only v1. *) + let saved_eff = ctx.current_eff in + ctx.current_eff <- EPure; (* Check the body against the return type *) let* () = begin match fd.fd_body with | FnBlock blk -> @@ -1528,6 +1558,17 @@ 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; + let inferred_eff = ctx.current_eff in + ctx.current_eff <- saved_eff; + let* () = + match fd.fd_eff with + | Some _ when not (Effect.eff_subset inferred_eff fn_eff) -> + Error (EffectNotDeclared { + inferred = Effect.string_of_eff inferred_eff; + declared = Effect.string_of_eff fn_eff; + }) + | _ -> Ok () + in (* 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). *) diff --git a/test/test_effects.ml b/test/test_effects.ml new file mode 100644 index 00000000..8a59082c --- /dev/null +++ b/test/test_effects.ml @@ -0,0 +1,83 @@ +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* Copyright (c) 2026 Jonathan D.A. Jewell *) + +(** Effect-row v1 inference tests (issue #59). + + Covers the one concrete effect source wired for tracking-only v1: + a catch-less [try] / the [?] desugar performs [Partial], and that is + checked against an explicitly declared effect row. An undeclared row + stays permissive. *) + +open Affinescript + +(** parse -> resolve -> typecheck an inline source string. + [Ok ()] = frontend accepted; [Error msg] = first stage error. *) +let frontend (src : string) : (unit, string) result = + let open Result in + let ( let* ) = bind in + let* prog = + try Ok (Parse_driver.parse_string ~file:"" src) + with + | Parse_driver.Parse_error (m, sp) -> + Error (Printf.sprintf "Parse error at %s: %s" (Span.show sp) m) + | e -> Error (Printf.sprintf "Unexpected: %s" (Printexc.to_string e)) + in + let loader = Module_loader.create (Module_loader.default_config ()) in + let* resolve_ctx = + match Resolve.resolve_program_with_loader prog loader with + | Ok (rc, _) -> Ok rc + | Error (e, _) -> Error ("Resolution error: " ^ Resolve.show_resolve_error e) + in + match Typecheck.check_program resolve_ctx.symbols prog with + | Ok _ -> Ok () + | Error e -> Error ("Type error: " ^ Typecheck.format_type_error e) + +let contains ~needle s = + let nl = String.length needle and sl = String.length s in + let rec go i = i + nl <= sl && (String.sub s i nl = needle || go (i + 1)) in + nl = 0 || go 0 + +(* A catch-less `?` inside a function whose declared row includes + Partial is accepted. *) +let declared_partial_ok () = + match frontend "fn f(r: Int) -> Int /{Partial} { r? }" with + | Ok () -> () + | Error m -> Alcotest.failf "expected Ok, got: %s" m + +(* The same body in a function declaring only /{IO} must be rejected + with the issue-#59 effect-mismatch error naming Partial. *) +let declared_missing_partial_rejected () = + match frontend "fn g(r: Int) -> Int /{IO} { r? }" with + | Ok () -> Alcotest.fail "expected an effect-mismatch error, got Ok" + | Error m -> + Alcotest.(check bool) "mentions Partial" true (contains ~needle:"Partial" m); + Alcotest.(check bool) "is the #59 mismatch" true (contains ~needle:"#59" m) + +(* No declared row → tracking-only v1 stays permissive (no error even + though the body performs Partial). *) +let undeclared_row_permissive () = + match frontend "fn h(r: Int) -> Int { r? }" with + | Ok () -> () + | Error m -> Alcotest.failf "expected permissive Ok, got: %s" m + +(* A handled `try` (catch arm present) discharges the failure and adds + no Partial, so a /{IO}-only row is fine. *) +let handled_try_no_partial () = + match + frontend + "fn k(r: Int) -> Int /{IO} { try { r } catch { _ => 0 } }" + with + | Ok () -> () + | Error m -> Alcotest.failf "handled try should add no effect, got: %s" m + +let tests = + [ + Alcotest.test_case "declared /{Partial} + ? accepted" `Quick + declared_partial_ok; + Alcotest.test_case "declared /{IO} + ? rejected (#59)" `Quick + declared_missing_partial_rejected; + Alcotest.test_case "undeclared row stays permissive" `Quick + undeclared_row_permissive; + Alcotest.test_case "handled try adds no Partial" `Quick + handled_try_no_partial; + ] diff --git a/test/test_main.ml b/test/test_main.ml index f6209d5b..13f9bc1c 100644 --- a/test/test_main.ml +++ b/test/test_main.ml @@ -10,4 +10,5 @@ let () = (* ("Parser", Test_parser.tests); *) (* TODO: Re-enable when test_parser is implemented *) ("Golden", Test_golden.tests); ("Examples", Test_golden.example_tests); + ("Effects (#59)", Test_effects.tests); ] @ Test_e2e.tests @ Test_stdlib_aot.tests)