Feat/effects partial inference 59

docs/specs/SPEC.adoc

@@ -324,11 +324,32 @@ Functions declare effects after `/`:
 ----
 fn pure_fn(x: Int) -> Int / Pure { x + 1 }
 fn io_fn() -> () / IO { println("hello") }
-fn fallible() -> Int / Exn[Error] { throw(Error::new()) }
-fn combined() -> () / IO + Exn[Error] { ... }
-----
-
-*Partial by Default:*
+fn fallible() -> Int / Throws[Error] { throw(Error::new()) }
+fn combined() -> () / IO + Throws[Error] { ... }
+----
+
+The v1 effect-row registry (issue #59) pins five canonical names —
+`IO`, `Async`, `Partial`, `Throws[E]`, `Mut` — plus reserved
+`Random`, `Time`, `Net`. `Throws` is written `Throws[E]` at use
+sites; the type argument is threaded (distinct under unification).
+The lowercase `io`/`state`/`exn` migration aliases and the older
+`Exn` name were retired once the stdlib was renamed to the
+canonical names.
+
+*Effect inference (tracking-only v1):*
+
+- A catch-less `try` — including the `e?` desugar (the `?` operator)
+  — lets failure short-circuit out of the body, so the enclosing
+  function performs `Partial`. A `try` with a `catch` arm handles the
+  failure locally and adds no effect.
+- When a function declares an effect row explicitly, the inferred row
+  must be a subset of the declared one (otherwise an effect-mismatch
+  error is raised). A function with *no* declared row stays permissive
+  under tracking-only v1 — its effects are not yet enforced.
+- Effect *handling* (intercepting/redirecting effects at runtime)
+  remains out of scope; see `docs/guides/effects-migration-stance.adoc`.
+
+*Partial by Default* (termination, distinct from the `Partial` effect):
 
 - Functions are partial by default (may not terminate)
 - `total` functions must provably terminate

lib/effect.ml

@@ -129,8 +129,9 @@ let string_of_eff (e : eff) : string =
     [docs/guides/effects-migration-stance.adoc]). *)
 
 (** Canonical v1 effect names.  [Throws] is written [Throws[E]] at use
-    sites; the type parameter is carried syntactically but not yet
-    threaded (tracking-only v1). *)
+    sites; the type argument is threaded by [Typecheck.lower_effect_expr]
+    (mangled into the singleton name, so [Throws[A]], [Throws[B]] and
+    bare [Throws] are distinct under effect unification). *)
 let v1_effects = [ "IO"; "Async"; "Partial"; "Throws"; "Mut" ]
 
 (** Reserved for v1.x — recognised so the names are not repurposed, not

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)