feat(effects): infer Partial from catch-less try/?; check vs declared row (Refs #59) (#207)

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) <noreply@anthropic.com>

Author: hyperpolymath

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 `<T>` type-param vars (created at the deeper
      level above) are quantified by `generalize` (#135 slice 7). *)

test/test_effects.ml

@@ -0,0 +1,83 @@
+(* SPDX-License-Identifier: PMPL-1.0-or-later *)
+(* Copyright (c) 2026 Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk> *)
+
+(** 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:"<test_effects>" 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;
+  ]

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)