feat(compiler): WO-E205 structural interface satisfaction + call-arg checks

The hybrid-boundary inversion is closed: a statically provable interface
violation now fails at COMPILE time instead of reaching wovm as an ICALL
that traps WO_T_BOUNDS at runtime.

- types.ml class_satisfies: the same rule emit.ml's `satisfies` builds
  vtable rows from (instance method with matching name + parameter count
  for every interface method; `static fn` never satisfies) — one rule, two
  consumers, so the check and the vtable can never disagree.
- check_iface_boundary fires wherever a confidently class-typed value flows
  into an interface-typed slot: call arguments against the callee's declared
  parameters (free fns, methods off confident receivers, interface-method
  sigs, statics — resolved exactly as confident_typ resolves returns),
  annotated `let`s, and `return`s. Silent when underivable.
- The same per-argument pass extends the ?T boundary to CALL ARGUMENTS
  (the previous slice covered stores/returns/operands): nil into a
  non-nullable parameter is WO-E212, an unnarrowed ?T argument is WO-E211.
- tests/corpus/trap/unsatisfied-interface -> compile-fail/ with
  fixture.code WO-E205, per the fixture's own standing instruction; its
  header comment rewritten to the wired reality.
- The new arg checks caught a real mistyped signature in the sample:
  log-watcher's rpc_error/rpc_result/call_tool declared `id: json.Value`
  while every caller legitimately passes nil (JSON-RPC id-absent) — now
  `?json.Value`; dispatch/call_tool/cron-row sites moved to the
  bind-then-narrow idiom (including an `or`-guard narrowing:
  `if spath == nil or spat == nil { return }`).
- Catalog: E205 gains its main-table row; the "owed gap" section is
  rewritten as closed. Board known-gap struck through.

Verified: woc-test 540/0 + test_diag 14/0; oop-e2e 83/0 (fixture now
compile-fail, satisfying-class negative probe compiles clean); oop-accept
ALL MET; log-watcher 7/0; employee 8/0; gc-cycle clean.

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

compiler/src/types.ml

@@ -745,6 +745,23 @@ let rec unwrap_nullable (t : typ) : typ =
 
 let is_nullable (t : typ) : bool = match t with TNullable _ -> true | _ -> false
 
+(* Structural interface satisfaction, Go-style — the SAME rule emit.ml's
+   `satisfies` uses to build vtable rows (name + parameter count, `static fn`
+   never satisfies): a class satisfies an interface when it has a matching
+   instance method for every method the interface declares. Returns the first
+   missing/mismatched method name, None when satisfied. WO-E205's test. *)
+let class_satisfies (cls : class_info) (iface : interface_info) : string option =
+  List.fold_left
+    (fun acc (sig_ : method_sig_info) ->
+      match acc with
+      | Some _ -> acc
+      | None -> (
+        match List.find_opt (fun (m : method_info) -> m.name = sig_.name) cls.methods with
+        | Some m when (not m.is_static) && List.length m.params = List.length sig_.params ->
+          None
+        | _ -> Some sig_.name))
+    None iface.methods
+
 (* ?T narrowing facts (iteration 5 strictness, WO-E211/E212/E213): which
    LOCAL names a condition proves non-nil when it is true, and when it is
    false. Only plain identifiers narrow (Haxe's own rule): a field place
@@ -1240,6 +1257,30 @@ let typecheck_program ~file ~(module_of : string -> string)
   let crosses_boundary ~(target : typ) (v : expr_type_result) : bool =
     (not (is_nullable target)) && (v.is_nil || is_nullable v.typ)
   in
+  (* WO-E205: a class value flowing into an interface-typed slot must
+     structurally satisfy the interface — provable statically (the class's
+     whole method set is known), so it fails HERE, never as the ICALL
+     no-vtable-entry trap. Checked off confident types: silent when the
+     value's type is underivable. *)
+  let check_iface_boundary (cenv : typ StringMap.t) ~(target : typ) (value : expr) : unit =
+    match (unwrap_nullable target, Option.map unwrap_nullable (confident_typ cenv value)) with
+    | TScalar iname, Some (TScalar cname) -> (
+      match (StringMap.find_opt iname syms.interfaces, StringMap.find_opt cname syms.classes) with
+      | Some iface, Some cls -> (
+        match class_satisfies cls iface with
+        | Some missing ->
+          Diag.Collector.add collector
+            (Diag.error ~code:unsatisfied_interface_code ~file ~line:value.pos.line
+               ~col:value.pos.col
+               ~message:
+                 (Printf.sprintf
+                    "`%s` does not satisfy interface `%s`: no matching instance method `%s`"
+                    cname iname missing)
+               ())
+        | None -> ())
+      | _ -> ())
+    | _ -> ()
+  in
   let expr_label (e : expr) : string =
     match e.kind with
     | Ident n -> Printf.sprintf "`%s`" n
@@ -1297,7 +1338,58 @@ let typecheck_program ~file ~(module_of : string -> string)
          | TMap (_, vt) -> { typ = vt; is_nil = false }
          | _ -> { typ = TScalar "Int"; is_nil = false })
     | Call (callee, args) ->
-        List.iter (fun arg -> ignore (typecheck_expr env cenv arg)) args;
+        let arg_results = List.map (fun arg -> typecheck_expr env cenv arg) args in
+        (* Per-argument checks against the callee's DECLARED signature
+           (resolved the same way confident_typ resolves a call's return):
+           WO-E205 interface satisfaction, and the ?T boundary the previous
+           slice enforced everywhere else. Silent when unresolvable. *)
+        let callee_params : (string * field_ty * param_conv) list option =
+          match callee.kind with
+          | Ident name -> (
+            match resolve_free_fn name with Some fi -> Some fi.params | None -> None)
+          | Field (base, mname) -> (
+            match Option.map unwrap_nullable (confident_typ cenv base) with
+            | Some (TScalar cn) -> (
+              match StringMap.find_opt cn syms.classes with
+              | Some cls -> (
+                match List.find_opt (fun (m : method_info) -> m.name = mname) cls.methods with
+                | Some m -> Some m.params
+                | None -> None)
+              | None -> (
+                match StringMap.find_opt cn syms.interfaces with
+                | Some iface -> (
+                  match
+                    List.find_opt (fun (s : method_sig_info) -> s.name = mname) iface.methods
+                  with
+                  | Some sg -> Some sg.params
+                  | None -> None)
+                | None -> None))
+            | _ -> (
+              match base.kind with
+              | Ident head -> (
+                match static_method_of syms head mname with
+                | Some m -> Some m.params
+                | None -> None)
+              | _ -> None))
+          | _ -> None
+        in
+        (match callee_params with
+         | Some ps when List.length ps = List.length args ->
+           List.iter2
+             (fun (pname, pty, _) (arg, ares) ->
+               let pt = resolve_field_ty pty in
+               check_iface_boundary cenv ~target:pt arg;
+               if not (is_nullable pt) then begin
+                 if ares.is_nil then
+                   e212 arg.pos (expr_label arg) (Printf.sprintf "parameter `%s`" pname)
+                 else
+                   match confident_typ cenv arg with
+                   | Some t when is_nullable t -> e211 arg.pos (expr_label arg)
+                   | _ -> ()
+               end)
+             ps
+             (List.combine args arg_results)
+         | _ -> ());
         (match callee.kind with
          | Ident name when Option.is_none (resolve_free_fn name) -> (
              (* "A user-declared free fn of the same name always wins"
@@ -2026,6 +2118,9 @@ let typecheck_program ~file ~(module_of : string -> string)
          | Some t when crosses_boundary ~target:t val_res ->
            e212 value.pos (expr_label value) (Printf.sprintf "`%s: %s`" name (typ_label t))
          | _ -> ());
+        (match declared with
+         | Some t -> check_iface_boundary cenv ~target:t value
+         | None -> ());
         let bound_typ = match declared with Some t -> t | None -> val_res.typ in
         let new_cenv =
           match (declared, confident_typ cenv value) with
@@ -2116,7 +2211,10 @@ let typecheck_program ~file ~(module_of : string -> string)
            (match !current_ret with
             | Some rt when crosses_boundary ~target:rt r ->
               e211 e.pos (expr_label e)
-            | _ -> ())
+            | _ -> ());
+           (match !current_ret with
+            | Some rt -> check_iface_boundary cenv ~target:rt e
+            | None -> ())
          | None -> ());
         (env, cenv)
     | ExprStmt { kind = Switch (subject, arms); _ } ->

docs/00-status.md

@@ -209,14 +209,11 @@ Gates at the end of that session: corpus 71/0, `woc` runtest 565/0, every
 
 **Known gaps carried out of iteration 4** — recorded, not silently owed:
 
-- **`WO-E205` (unsatisfied interface) is reachable but unenforced — a real
-  hybrid-boundary inversion, not just a dead code path.** A class that does
-  not structurally satisfy an interface it's passed as compiles clean (exit
-  0, zero diagnostics) even though the violation is statically provable, and
-  the mismatched call reaches `wovm` as an `ICALL` with no matching vtable
-  entry, trapping `WO_T_BOUNDS` (6) at runtime instead of failing at compile
-  time. Pinned by `tests/corpus/trap/unsatisfied-interface/`; when `WO-E205`
-  is wired, that fixture must move to `compile-fail/` in the same change.
+- ~~`WO-E205` (unsatisfied interface) reachable but unenforced~~ — **closed
+  2026-08-18** (branch `type-enforcement`): structural satisfaction is checked
+  at call arguments, annotated `let`s, and returns; the pinned fixture moved
+  to `compile-fail/unsatisfied-interface` with `fixture.code WO-E205` in the
+  same change, as its comment demanded. The hybrid boundary is restored.
 - **`set(m, k, v)`'s `@gc` retention gap on map keys/values is open** — the
   twin of the `push` bug Task 5 fixed for `multi`. `set` has no equivalent
   special case in `owner.ml`'s `analyze_call`, so a `@gc` key or value handed

docs/examples/log-watcher/mcp.wo

@@ -79,10 +79,11 @@ class Mcp {
 
   -- Mcp.hx:54-84. Tool-layer failures return isError, never protocol
   -- errors; a trap inside a tool is caught at this boundary.
-  fn call_tool(id: json.Value, params: ?RpcParams) -> HttpResp {
+  fn call_tool(id: ?json.Value, params: ?RpcParams) -> HttpResp {
     if params == nil { return rpc_error(id, -32600, "tools/call: missing params.name"); }
-    if params.name == nil { return rpc_error(id, -32600, "tools/call: missing params.name"); }
-    let o = try self.dispatch(params.name, params.arguments)
+    let pname = params.name;
+    if pname == nil { return rpc_error(id, -32600, "tools/call: missing params.name"); }
+    let o = try self.dispatch(pname, params.arguments)
             catch (e) err("tool failed: ${e.msg}");
     let content = json.encode(ToolText { type: "text", text: o.text });
     let flag = "false";
@@ -98,12 +99,15 @@ class Mcp {
         return self.tools.list_logs();
       case "tail_log":
         if args == nil { return err("tail_log: path is required"); }
-        if args.path == nil { return err("tail_log: path is required"); }
-        return self.tools.tail_log(args.path, args.lines);
+        let tpath = args.path;
+        if tpath == nil { return err("tail_log: path is required"); }
+        return self.tools.tail_log(tpath, args.lines);
       case "search_log":
         if args == nil { return err("search_log: path and pattern are required"); }
-        if args.path == nil or args.pattern == nil { return err("search_log: path and pattern are required"); }
-        return self.tools.search_log(args.path, args.pattern, args.maxMatches);
+        let spath = args.path;
+        let spat = args.pattern;
+        if spath == nil or spat == nil { return err("search_log: path and pattern are required"); }
+        return self.tools.search_log(spath, spat, args.maxMatches);
       default:
         return err("unknown tool: ${name}");
     }
@@ -184,12 +188,12 @@ class Mcp {
   }
 }
 
-fn rpc_result(id: json.Value, result_json: Text) -> HttpResp {
+fn rpc_result(id: ?json.Value, result_json: Text) -> HttpResp {
   let idj = json.encode(id);
   return HttpResp { status: 200, body: "{\"jsonrpc\":\"2.0\",\"id\":${idj},\"result\":${result_json}}" };
 }
 
-fn rpc_error(id: json.Value, code: Int, message: Text) -> HttpResp {
+fn rpc_error(id: ?json.Value, code: Int, message: Text) -> HttpResp {
   let idj = json.encode(id);
   let e = json.encode(RpcErr { code: code, message: message });
   return HttpResp { status: 200, body: "{\"jsonrpc\":\"2.0\",\"id\":${idj},\"error\":${e}}" };
@@ -261,8 +265,9 @@ class Tools {
       let nf_text: ?Text = nil;
       if nf != nil { nf_text = time.iso(nf); }
       let running = false;
-      if e.lock_path != nil {
-        running = Flock.held(e.lock_path);
+      let elk = e.lock_path;
+      if elk != nil {
+        running = Flock.held(elk);
       } else {
         running = Pgrep.alive(Tools.needle(e.command));
       }

docs/plan/oop-vm/01-error-catalog.md

@@ -8,7 +8,7 @@ per stage (`compiler/src/diag.ml`): `WO-E0xx` lexing, `WO-E1xx` parsing,
 is an enumeration of codes already in use, not an archaeology dig — see
 "Completeness method" below for how that was verified, "Reserved,
 not yet emitted" for codes the source declares but no check yet raises,
-and "Reachable but unenforced" for the one code (WO-E205) whose check
+and (until 2026-08-18) "Reachable but unenforced" for the one code (WO-E205) whose check
 site the milestone grammar *does* exercise, unlike the codes above it —
 see that section for why this is a live gap, not a scope boundary.
 One code (WO-E214) is emitted by the driver (`compiler/bin/main.ml`),
@@ -43,6 +43,7 @@ half of the story ("moved here" / "borrowed here" / etc.).
 | WO-E201 | haxe-parity Task 2. An `and`/`or` operand whose type is confidently known (the same narrow, "stay silent when underivable" deriver WO-E209 uses — `confident_typ`) and is not `Bool` — this language has no truthiness. Reserved since Task 6, its first real emission site. Haxe-parity Task 3 gave it two more sites: a `switch` expression's arms disagree on their yielded type (the switch's own type is fixed by the first arm — types.ml's "first wins" convention — every later arm is checked against it, via the regular `.typ` inference, not `confident_typ`; since haxe-parity Task 4 the comparison is *structural* — two typedef records with the same shape are the same type, `typ_equal`); and (review fix, Critical 2) a `case` value whose representation (`WO_K_TEXT` vs. `WO_K_SCALAR`) doesn't match the switch subject's — a real VM segfault if unchecked (a `Text` subject picks EQS, and EQS's `str_check` dereferences whatever sits in a mismatched `Int` case value's register), checked via `confident_typ`, silent when either side is unresolved. Haxe-parity Task 4 added the union-subject site: a `case` value over a confidently union-typed subject that does not name one of that union's variants (a misspelled variant, a variant of some other union, or a plain literal — union arms match variants, never values). Task 4's fix round 1 added three inverse/porosity sites, each a reviewer-reproduced silent-wrong-behavior hole: a variant-named `case` over a confidently **`?Union`** subject (it can never match — `switch` does not narrow `?T`; the message points at handling nil first, since forced handling is Task 6's), a variant-named `case` over a confidently **non-union** subject (`switch n { case Lo: }` over `n: Int` silently ordinal-matched), and a **cross-union `==`/`!=`** (`X == P` from two different bare unions was silently true whenever the ordinals matched; same-union comparison stays legal). Lexical scope wins at every one of these sites — a local sharing a variant's name is never misread as one. | `` `Wat` is not a variant of union `Kind` `` |
 | WO-E203 | haxe-parity Task 4 (`typedef` records + enum payload variants). A payload variant's argument count doesn't match its declaration, at either of the two places payload fields are positional: a construction (`Failed("a", "b")` against `Failed(reason: Text)`) or a `switch` pattern (`case Failed(a, b):`). The pattern site also rejects a non-name argument (`case Failed("x"):` — payload fields are bound positionally, never matched by value) and a payload-binding pattern sharing its arm with other values (`case Failed(r), Pending:` — the binding would be meaningless on the other match). Reserved since plan 2 Task 6; these are its first real emission sites, scoped to variant payloads only — user `fn`/method call arity is still the emitter's WO-E403, unchanged (see "Reserved, not yet emitted" below for the history of that gap). | `` variant `Failed` of `Status` takes 1 payload argument(s), given 2 `` |
 | WO-W201 *(retired, iteration 7b)* | Suggested `@gc` for a recursive/shared class. Retired: `@gc` no longer exists (WO-E104) and inference classifies exactly these classes as traced automatically, so the suggestion is obsolete. | *(no longer emitted)* |
+| WO-E205 | iteration 5 strictness (2026-08-18). A confidently class-typed value used at an interface-typed position — a call argument, an annotated `let`, or a `return` — where the class does not structurally satisfy the interface (Go-style: an instance method of the same name and parameter count for every interface method; a `static fn` never satisfies). Provable statically, so it fails at compile time instead of `ICALL`'s no-vtable-entry `WO_T_BOUNDS` trap — the hybrid boundary restored. Silent when the value's type is underivable. | `` `Rock` does not satisfy interface `Priced`: no matching instance method `current_price` `` |
 | WO-E202 | a `.field` access names a field that the base's class (a *declared* class — an unresolved/placeholder expression type never triggers this) doesn't have. | `unknown field \`price\` on \`Product\`` |
 | WO-E206 | a constructor literal (`ClassName { ... }`) omits a field the class declares that is neither defaulted nor nullable. Haxe-parity Task 4 narrowed it from "omits any field with no default was already the rule, but defaults were unenforceable" to the real omittability rule: a field with a declared default is filled by the emitter (`TailState {}` — the sample's defaults-fill-in pattern), and a `?`-typed field omitted is nil (the zero word `NEW` already leaves), for classes and typedef records alike. | `missing field \`sku\` in constructor of \`Product\`` |
 | WO-E207 | a constructor literal names a class that isn't declared anywhere in the (possibly multi-file) program. `typedef` records (haxe-parity Task 4) are classes to this check — a record name resolves here like any declared class. | `unknown type \`Widget\` in constructor` |
@@ -92,38 +93,17 @@ its first real emission site.
 
 ### Reachable but unenforced
 
-`unsatisfied_interface_code` (WO-E205) is declared in `types.ml` but does not
-belong in the "Reserved, not yet emitted" list above either. An earlier
-revision of this doc claimed WO-E205 was *unreachable by design* — that
-was wrong, caught and corrected in the plan-3 Task 4 review (2026-08-11).
-Structural interface satisfaction's one legal check site is where a value
-is used at an interface-typed position (a field, parameter, or return
-typed as an interface) — and the milestone grammar does exercise that
-position today. This compiles with exit 0 and zero diagnostics:
-
-```wo
-interface Priced { fn current_price() -> Int }
-class Rock { n: Int }
-fn quote(p: Priced) -> Int { return p.current_price() }
-fn main() { let r = Rock { n: 1 }
-  print_int(quote(r)) }
-```
-
-`Rock` has no `current_price` method, so it does not structurally satisfy
-`Priced` passed to `quote`'s interface-typed parameter — and `Rock`'s
-method set is fully known at compile time, so this is a *statically
-provable* violation, exactly the shape WO-E205 exists to catch. `woc
---emit` accepts it anyway. The unchecked call reaches `wovm` as an
-`ICALL` with no matching vtable slot, which traps `WO_T_BOUNDS` (6, "no
-vtable entry for receiver class") at runtime instead of failing to
-compile. That inverts the hybrid boundary WO-E3xx pins elsewhere
-(provable violation → compile-time diagnostic, unprovable → runtime
-trap): here a provable violation resolves as a trap. This is an owed
-gap, not a design decision, currently pinned as the known-gap fixture
-`tests/corpus/trap/unsatisfied-interface/` (plan 3, Task 4) — its own
-comment says it must move to `compile-fail/` with `fixture.code
-WO-E205` in the same change that implements this check, rather than
-silently going stale.
+**WO-E205 was wired 2026-08-18** (branch `type-enforcement`) — the owed gap
+this section used to record is closed. Structural satisfaction (`types.ml`'s
+`class_satisfies`, the same name+arity+non-static rule `emit.ml`'s
+`satisfies` builds vtable rows from) is checked wherever a confidently
+class-typed value flows into an interface-typed slot: a call argument
+against the callee's declared parameter, an annotated `let`, and a `return`
+against the declared return type. The canonical evidence program now fails
+compile at the `quote(r)` call site, and the known-gap fixture moved to
+`tests/corpus/compile-fail/unsatisfied-interface/` (`fixture.code WO-E205`)
+in the same change, exactly as its own comment demanded. See the WO-E205 row
+in the main table above.
 
 ## WO-E3xx — ownership / MVS (Task 7, `compiler/src/owner.ml`)
 

tests/corpus/compile-fail/unsatisfied-interface/fixture.code

@@ -0,0 +1 @@
+WO-E205

tests/corpus/compile-fail/unsatisfied-interface/fixture.wo

@@ -0,0 +1,22 @@
+-- WO-E205 (wired 2026-08-18; formerly trap/unsatisfied-interface, which
+-- pinned the old runtime-trap behavior as a KNOWN GAP). `Rock` has no
+-- `current_price` method, so it does not structurally satisfy `Priced` --
+-- provable statically (the class's whole method set is known), so by the
+-- hybrid-boundary doctrine it fails at COMPILE time, at the `quote(r)`
+-- call site, never as the ICALL no-vtable-entry trap.
+interface Priced {
+  fn current_price() -> Int
+}
+
+class Rock {
+  n: Int
+}
+
+fn quote(p: Priced) -> Int {
+  return p.current_price()
+}
+
+fn main() {
+  let r = Rock { n: 1 }
+  print_int(quote(r))
+}

tests/corpus/trap/unsatisfied-interface/fixture.trap

@@ -1 +0,0 @@
-6

tests/corpus/trap/unsatisfied-interface/fixture.wo

@@ -1,34 +0,0 @@
--- KNOWN GAP, pinned deliberately (Task 4 review, Important 2). `Rock`
--- does not have a `current_price` method, so it does not structurally
--- satisfy `Priced` -- and its full method set is known at compile time,
--- so this violation IS provable statically. By the hybrid-boundary
--- doctrine (provable -> compile-time, unprovable -> runtime) this ought
--- to be WO-E205 (unsatisfied-interface) at the `quote(r)` call site.
---
--- It isn't: WO-E205 is declared in types.ml but has no call site today
--- (docs/plan/oop-vm/01-error-catalog.md). This compiles clean (exit 0,
--- zero diagnostics) and the unsatisfied call instead reaches `wovm` as
--- an `ICALL` with no matching vtable entry, which traps `WO_T_BOUNDS`
--- (6) -- "no vtable entry for receiver class". That is the CURRENT,
--- observed behavior this fixture pins, not the desired one.
---
--- When WO-E205 is implemented, this exact program must start failing to
--- *compile* instead -- move this fixture to compile-fail/ with
--- fixture.code WO-E205 in the same change that wires the check, rather
--- than leaving a stale trap/ fixture silently describing dead behavior.
-interface Priced {
-  fn current_price() -> Int
-}
-
-class Rock {
-  n: Int
-}
-
-fn quote(p: Priced) -> Int {
-  return p.current_price()
-}
-
-fn main() {
-  let r = Rock { n: 1 }
-  print_int(quote(r))
-}