diff --git a/compiler/src/types.ml b/compiler/src/types.ml index 0fac938..8d43ddf 100644 --- a/compiler/src/types.ml +++ b/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); _ } -> diff --git a/docs/00-status.md b/docs/00-status.md index 0e672b2..389d1d1 100644 --- a/docs/00-status.md +++ b/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 diff --git a/docs/examples/log-watcher/mcp.wo b/docs/examples/log-watcher/mcp.wo index 5773c6b..b694ce5 100644 --- a/docs/examples/log-watcher/mcp.wo +++ b/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)); } diff --git a/docs/plan/oop-vm/01-error-catalog.md b/docs/plan/oop-vm/01-error-catalog.md index 0073b22..eb1e1c5 100644 --- a/docs/plan/oop-vm/01-error-catalog.md +++ b/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`) diff --git a/tests/corpus/compile-fail/unsatisfied-interface/fixture.code b/tests/corpus/compile-fail/unsatisfied-interface/fixture.code new file mode 100644 index 0000000..8745127 --- /dev/null +++ b/tests/corpus/compile-fail/unsatisfied-interface/fixture.code @@ -0,0 +1 @@ +WO-E205 diff --git a/tests/corpus/compile-fail/unsatisfied-interface/fixture.wo b/tests/corpus/compile-fail/unsatisfied-interface/fixture.wo new file mode 100644 index 0000000..00d012f --- /dev/null +++ b/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)) +} diff --git a/tests/corpus/trap/unsatisfied-interface/fixture.trap b/tests/corpus/trap/unsatisfied-interface/fixture.trap deleted file mode 100644 index 1e8b314..0000000 --- a/tests/corpus/trap/unsatisfied-interface/fixture.trap +++ /dev/null @@ -1 +0,0 @@ -6 diff --git a/tests/corpus/trap/unsatisfied-interface/fixture.wo b/tests/corpus/trap/unsatisfied-interface/fixture.wo deleted file mode 100644 index 96b9e5a..0000000 --- a/tests/corpus/trap/unsatisfied-interface/fixture.wo +++ /dev/null @@ -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)) -}