fix(#555): C backend fails loud on handle/resume instead of dropping arms

The C backend's ExprHandle arm compiled the body and discarded every
handler arm (`handle 41 { return(v) => v+1 }` emitted 41, not 42), and
ExprResume was a silent argument passthrough — the same silent wrong-value
miscompile #555 fixed in the WASM/WasmGC/Deno-ESM/JS-text backends. Now
failwith (caught by codegen_c → Error), matching the loud-fail policy; use
the interpreter for algebraic effects.

Adds an E2E loud-fail test for the C backend. Documents (in the handler-
fence test block) that the Lean/Why3 text backends are experimental stubs
which drop `return` statements wholesale — a broader incompleteness than
#555, flagged separately rather than given a misleading handle-only fence.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

lib/c_codegen.ml

@@ -239,9 +239,25 @@ let rec gen_expr ctx (expr : expr) : string =
   | ExprIndex (arr, idx) ->
       Printf.sprintf "(%s)[%s]" (gen_expr ctx arr) (gen_expr ctx idx)
   | ExprSpan (inner, _) -> gen_expr ctx inner
-  | ExprHandle { eh_body; eh_handlers = _ } -> gen_expr ctx eh_body
-  | ExprResume (Some e) -> gen_expr ctx e
-  | ExprResume None     -> "((void)0)"
+  | ExprHandle _ ->
+      (* #555: compiling the body and dropping every handler arm (the previous
+         behaviour) was a silent wrong-value miscompile — `handle 41 { return(v)
+         => v + 1 }` emitted 41 instead of 42, and a `perform` would never
+         dispatch to its arm.  The C backend has no handler-dispatch / CPS
+         transform, so fail loudly (matching the WASM, WasmGC, Deno-ESM and
+         JS-text backends) rather than emit wrong code; use the interpreter
+         (`--interp` / `-i`) for algebraic effects. *)
+      failwith
+        "effect handler (handle { ... }) in the C backend — handler arms \
+         cannot be dispatched (requires a CPS transform; Refs #555); \
+         use `--interp` / `-i`"
+  | ExprResume _ ->
+      (* `resume` is only meaningful inside a handler arm; the enclosing
+         `handle` already fails above.  Fail consistently rather than emit a
+         silent argument passthrough (issue #555). *)
+      failwith
+        "`resume` expression in the C backend — only valid inside a `handle` \
+         block (Refs #555); use `--interp` / `-i`"
   | ExprRecord { er_fields; _ } ->
       let fs = List.map (fun (id, e_opt) ->
         let v = match e_opt with Some e -> gen_expr ctx e | None -> mangle id.name in

test/test_e2e.ml

@@ -2281,11 +2281,38 @@ let test_handle_deno_loud_fail () =
       Alcotest.(check bool) "error names the handler fence" true
         (contains_str "effect handler" msg)
 
+let test_handle_c_loud_fail () =
+  let result =
+    let open Result in
+    let ( let* ) = bind in
+    let* (prog, resolve_ctx) = run_frontend (fixture "handle_return_arm.affine") in
+    C_codegen.codegen_c prog resolve_ctx.symbols
+  in
+  match result with
+  | Ok _ ->
+      Alcotest.fail
+        "expected loud failure for handle on the C backend (Refs #555); \
+         got Ok — silent arm-drop has regressed"
+  | Error msg ->
+      Alcotest.(check bool) "error names the handler fence" true
+        (contains_str "effect handler" msg)
+
+(* NOTE: the Lean and Why3 text backends are experimental stubs whose
+   block-lowering only emits `let` bindings — a `return` statement (and thus
+   any expression it wraps, including `handle`) is silently dropped, so
+   `fn main() -> Int { return handle ... }` emits `def main : Int := ()`.
+   That is a *broader* incompleteness than #555 (they miscompile far more than
+   handlers), so a handle-specific fence there would be misleading. They are
+   flagged separately rather than fenced here; the reachable #555 codegen
+   holes were the production backends (WASM / WasmGC / Deno-ESM / JS-text)
+   and C, all fenced + tested above. *)
+
 let handler_fence_tests = [
   Alcotest.test_case "interp: return-arm handle still evaluates" `Quick test_handle_interp_still_works;
   Alcotest.test_case "wasm: handle → loud UnsupportedFeature"     `Quick test_handle_wasm_loud_fail;
   Alcotest.test_case "js-text: handle → loud failure"             `Quick test_handle_js_loud_fail;
   Alcotest.test_case "deno-esm: handle → loud failure"            `Quick test_handle_deno_loud_fail;
+  Alcotest.test_case "c: handle → loud failure"                   `Quick test_handle_c_loud_fail;
 ]
 
 (* ============================================================================