# lib/guest/static-types-bidirectional — design-diary plan Capture the dispatch skeleton of bidirectional type checking (synthesis/checking judgments, context as a value, pluggable subtyping and unification) as `lib/guest/static-types-bidirectional/`, so static-typed guest languages that aren't Hindley-Milner-inferred cost ~300 lines of language-specific rules instead of re-inventing the checker plumbing. Reference: `plans/lib-guest.md` (parent — two-language rule, stratification), `lib/guest/hm.sx` (sister module — full Hindley-Milner for inference-heavy languages like Haskell-on-SX), Go-on-SX (planned first consumer), TBD second consumer. **Branch:** `architecture`. SX files via `sx-tree` MCP only. ## Thesis `lib/guest/hm.sx` covers languages where the user writes few type annotations and the checker infers the rest globally (Haskell-on-SX, an eventual ML port, a typed-Scheme-with-Damas-Milner). But most modern statically-typed languages in actual production — Go, Rust, Swift, TypeScript, Kotlin, Scala 3, Hack — do **bidirectional checking instead**: declarations carry annotations, locals are inferred from immediate context, return types thread inwards from call sites. This isn't a weaker form of HM; it's a different design that scales better to mutation, subtyping, ad-hoc polymorphism, and gradual typing — none of which HM handles cleanly. If `lib/guest/` is going to credibly host the next decade of statically-typed languages, it needs a bidirectional kit alongside `hm.sx`. They're sisters, not rivals. **This plan is a design diary, not an implementation queue.** The two-language rule blocks extraction until two consumers exist. Go-on-SX is the first; the second is TBD. Until then, this plan documents what the API surface *should* be based on a single consumer, openly acknowledging that the second consumer will revise it. ## Current state (2026-05-26) - `lib/guest/hm.sx` exists, used by Haskell-on-SX. 180 lines. The HM kit is the sister extraction this plan complements. - No bidirectional kit anywhere in `lib/guest/`. - Go-on-SX does not exist yet. When it does, `lib/go/types.sx` will be the first consumer. - Second consumer is unidentified. Most likely candidates, in order: 1. **TypeScript-on-SX** — purely structural, gradual typing, the most- popular bidirectional language alive. Natural pair. 2. **Rust-on-SX** — bidirectional with substantial extras (lifetimes, traits, borrow checking). Heavyweight; lifetimes don't go in this kit. 3. **Typed Racket subset** — if anyone ports it. Bidirectional + gradual. 4. **Hack / Flow / Python-with-types** — same shape. **Status: Phase 0 (literature survey).** No code in this plan yet. ## Why bidirectional, not HM (for the languages that need it) Five reasons HM doesn't fit these languages: 1. **Subtyping.** HM unification requires equality of types; subtyping requires a different judgment (`t ⊑ u`). Go's `interface{}` accepts any concrete type that satisfies it — subtyping, not unification. 2. **Mutation.** HM's let-polymorphism interacts pathologically with mutable references (the value restriction). Go, Rust, TS all have first-class mutation and need rules that handle it directly. 3. **Annotations as ground truth.** Bidirectional treats declared types as *given*, then propagates them. HM treats every type as a variable to be solved. For languages where annotations are expected, bidirectional is the natural shape. 4. **Generics with constraints.** Go's type parameters carry constraints (`type T comparable`); Rust has trait bounds. HM has typeclasses but they're orthogonal to its constraint solver. Bidirectional weaves constraints into the checking rules naturally. 5. **Gradual typing.** TS's `any`, Hack's pessimistic mode, Python's `Any` — gradual checking is built on bidirectional's "check or skip" distinction. HM either checks or it doesn't. These languages collectively are the majority of new statically-typed code. Hosting them on lib/guest at all requires the bidirectional shape. ## API surface (proposed — design only, will revise with second consumer) ``` ;; --- judgments --- (synth ctx expr) -> {:type T} | {:error msg} ;; "expr synthesises type T in context ctx." ;; Used at function calls (arg types known), let bindings, literals. (check ctx expr expected-type) -> :ok | {:error msg} ;; "expr checks against expected-type in context ctx." ;; Used in function bodies (return type known), arguments (param type known), ;; assignments (LHS type known). ;; --- context --- (make-ctx) -> ctx (ctx-extend ctx name type) -> ctx ;; functional update (ctx-lookup ctx name) -> type | nil ;; --- pluggable rules --- (register-synth-rule! kit ast-tag synth-fn) -> nil ;; ast-tag: a keyword identifying the AST node shape (eg. :call :let :lit-int) ;; synth-fn: (ctx node) -> {:type T} | {:error msg} (register-check-rule! kit ast-tag check-fn) -> nil ;; check-fn: (ctx node expected-type) -> :ok | {:error msg} (register-type-equiv! kit pred) -> nil ;; pred: (t1 t2) -> bool. The "are these types compatible" predicate. ;; For Go: structural-interface-match-or-equal. ;; For TS: structural-equality-with-any-bidirectional-bottom. ;; For Rust: nominal equality + trait obligations. (register-subtype! kit pred) -> nil ;; pred: (sub super) -> bool. Optional; defaults to type-equiv. ;; Go has no subtyping between concrete types but interface satisfaction ;; is morally subtyping. TS has structural subtyping properly. (register-unify! kit unifier) -> nil ;; Optional; for type-variable resolution (generics). ;; unifier: (t1 t2 subst) -> {:subst s'} | {:error msg} ;; --- driver --- (make-kit) -> kit (check-program kit ctx program) -> {:ok ctx'} | {:error msg path-to-error} ``` Design notes: - **The kit dispatches on AST tags**, which is what makes it pluggable. Each language registers rules for its node types. There's no hardcoded set of expression shapes in the kit. - **Synth and check are mutually recursive.** Inside a synth-rule for `call`, the rule synthesises the function's type, then `check`s each argument against the corresponding parameter type. Inside a check-rule for `lambda`, the rule pulls argument types from the expected function type and `synth`s the body. This pingponging is the bidirectional core. - **Pluggable type-equiv + subtype + unify** is the three-knob shape. Pierce & Turner ("Local Type Inference") and Dunfield & Krishnaswami ("Sound and Complete Bidirectional Typechecking") both factor it this way. - **No type variables in the core API.** Generics handling is a kit *extension*: when a language registers a `unify` predicate, the kit threads a substitution through synth/check. Languages without generics (early Go) leave it null. - **Errors carry a path.** `{:error msg path}` where path is a list of AST tags leading to the failure. Good error messages are why bidirectional is practical; the kit must support them. ## What's NOT in the kit (language-layer concerns) Per the chiselling discipline, the kit is the dispatch skeleton; rules stay in the language. Specifically: - **The literal type table.** Go's `42` is `untyped int` until contextualised; TS's `42` is the literal type `42`. Each language ships its own. - **Specific subtyping rules.** Go's interface satisfaction is recursive structural matching against method sets. TS's depends on object property satisfaction. Each language ships its own predicate. - **Generics constraint solving.** Go's type-set-based constraints, Rust's trait bounds, TS's conditional types — each is non-trivial and language- specific. The kit threads a substitution; the language defines what's in it. - **Effects, lifetimes, ownership.** Rust's borrow checker is not a type checker in the bidirectional-kit sense — it's a separate dataflow pass. Out of scope. - **Gradual fallback.** TS's `any` lets unchecked code coexist with checked code. The kit supports this via "check returns :ok on a sentinel any-type" but the sentinel is registered by the language. ## Build order — phases ### Phase 0 — Literature survey + Go's type system specifics ⬜ - Read: Pierce & Turner "Local Type Inference" (2000); Dunfield & Krishnaswami "Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism" (2013, 2019 revision); the Go language spec § "Types" + "Expressions". - Survey how Rust / TS / Kotlin / Scala 3 implement bidirectional in practice (their compilers are open source). Note where they diverge. - Output: a short summary section "Bidirectional design space (captured 2026-MM-DD)" appended to this plan. Specifically: list every place language implementations diverge, so we can predict which divergences will show up between Go and the second consumer. - **Acceptance:** survey committed to this plan. No code. ### Phase 1 — Go independent implementation ✅ - During Go-on-SX, implement `lib/go/types.sx` from scratch. Do not write with extraction in mind — write the simplest Go-specific bidirectional checker. - Hit Go's distinctive type-system features: untyped constants, interface satisfaction (structural), generics (Go 1.18 type parameters with type-set constraints — defer this if scope explodes). - Pass Go's type-checker conformance tests. - **Acceptance:** Go conformance scoreboard includes type-checker tests, all passing. - **Output:** one consumer. Two-language rule still not met; no extraction. - **Status (2026-05-28):** Done. `lib/go/types.sx` ships: - **synth/check skeleton:** `go-synth` + `go-check` with first-class error tags `(:type-error TAG ARGS...)`. - **Untyped constants:** `:ty-untyped-int`, `:ty-untyped-float`, `:ty-untyped-string`, `:ty-untyped-rune`. Canonical pitfall handled — `var x float64 = 42 / 7` keeps untyped-int through the divide. `go-unify-untyped` pairs untyped-int+float → float. - **Interface satisfaction:** structural method-set match via `#method/TYPE/NAME` mangled keys; `go-iface-satisfies?`. - **Generics (Phase 7 closed):** `[T any]` / `[T, U any]` / `[T any, U comparable]` parsed + type-checked; opaque `(:ty-param NAME CONSTRAINT)` binding via `go-extend-with-type-params`. Type-set constraints (`int | float64`, `~int`) deferred — needs constraint-satisfaction predicate (chiselled as the kit's 3rd pluggable predicate slot). - **Index synth:** `(:index OBJ IDX)` for slice/array/map → element type. Same AST, 3 role-validators (the "shape is parser, role is validator" lemma at scale). 102 types tests pass. Two-language rule still pending: the bidirectional kit needs a SECOND consumer (TS/Rust/typed-Scheme) before extraction. Phase 2's "pick + start" is the next sister-plan-owned step. ### Phase 2 — Pick + start the second consumer ⬜ - Decide between TS, Rust-subset, or typed-Scheme-subset. Recommendation: **TypeScript** — most-different from Go (gradual, structural everywhere), testing the kit's range maximally. Rust's lifetime/borrow machinery isn't part of this kit, so a Rust port wouldn't actually exercise the kit very hard. - Implement just enough of the second language to type-check a non-trivial function. Don't port the whole language; port the type checker. - **Acceptance:** second consumer's type checker green on its small slice. ### Phase 3 — Diff and proposed kit ⬜ - Side-by-side: Go's checker vs the second consumer's checker. Where do they agree (the kit). Where does each diverge (the language). - Draft `lib/guest/static-types-bidirectional/api.sx` (signatures only). - Compare against the API sketch in this plan. The API WILL change at this step; that's the whole point of having two consumers. - **Acceptance:** revised API committed to this plan; agreement that both consumers can adopt it. ### Phase 4 — Implement the kit ⬜ - `lib/guest/static-types-bidirectional/` with the agreed API. Kit tests in `lib/guest/static-types-bidirectional/tests/` — using a minimal "toy" language (synth-rule for `:int`, check-rule for `:lambda`) to verify the dispatch skeleton works. - **Acceptance:** kit tests pass; both consumers' scoreboards still green with their own implementations. ### Phase 5 — Refactor both consumers to use the kit ⬜ - Go: `lib/go/types.sx` becomes a thin layer over the kit — registers Go's synth/check/equiv rules, calls `check-program`. Lifecycle code shrinks. - Second consumer: same exercise. - **No-regression gate:** both consumers' conformance scoreboards unchanged. - **Acceptance:** both `lib//types.sx` files meaningfully smaller; kit is doing real work. ### Phase 6 — Documentation + chiselling diary ⬜ - Document the API in lib/guest's README index. - Diary section in this plan: what we considered putting in the kit but ended up keeping language-specific, and why. - **Acceptance:** documentation present; diary captured. ## Two-language rule — gating Same as `lib-guest-scheduler.md`. The kit does not exist until both consumers independently work AND we've reviewed the diff AND we believe the shared skeleton is real. Rejected-extraction is a valid outcome. ## Relationship to `lib/guest/hm.sx` Sister modules, not rivals. Some languages will use HM (full inference, let-polymorphism); some will use bidirectional (annotation-driven, subtyping- friendly). Some might use both — Scala-on-SX, hypothetically, has local-type- inference in expressions and global-HM-style constraint solving in implicit resolution. The kit boundaries are: - `hm.sx` — unification-based, whole-expression inference. Damas-Milner core. Best for: ML family, Haskell, OCaml subset, Standard ML. - `static-types-bidirectional/` — synth/check judgments, pluggable equiv + subtype. Best for: Go, Rust, TS, Kotlin, Swift, Scala 3, Hack. A language can call into both: bidirectional for the surface, HM-style unification inside generics resolution. That's actually how Scala 3 works. The kits compose; design accordingly. ## Open questions - **Variance.** Go has none; TS has covariant/contravariant/bivariant; Rust has variance markers per type parameter. Does the kit need a variance predicate as a fourth pluggable knob? Probably yes, but defer until the second consumer forces the question. - **Effect tracking.** Some bidirectional checkers (Koka, Eff, certain capability-effect TS variants) track effects in types. Out of scope for v1; the kit must not actively prevent it though. - **Refinement types.** TS has narrowing (`typeof x === "string"` refines `x` to `string`); Hack and Flow are similar. These layer above the kit (the kit's `check` returns a refined context as part of `:ok`). Sketch this in Phase 3 if TS is the second consumer. - **Error recovery.** Real-world type checkers don't halt on first error; they recover and continue to surface as many errors as possible. The kit needs an error-accumulation mode. Design it in Phase 4. - **Performance.** For toy languages, naive synth/check is fine. For Go- sized programs, the checker has to be memoised on synthesised types of subexpressions. Not a v1 concern; flag if it bites. ## Progress log _Newest first. Append one dated entry per milestone landed._ - 2026-05-28 — **Go-on-SX consumer-side surface fully landed (609/609 tests across 7 suites).** This is the Phase-10 cross-reference entry: with all of Go's lex+parse+types+eval+sched+stdlib+e2e proven independent of the eventual kit, the type-system-kit surface that emerged from this consumer is: **Three pluggable predicates** (the kit's role-validator slots): 1. **`synth(ctx, expr) → ty | error`** — type synthesis from expression structure. Go's instance handles literals, binops, applications, indexing, composites, etc. 2. **`assignable?(got, expected) → bool`** — variance + untyped- constant rules. Go's instance handles 3-tier untyped flow (`untyped-int → int → float64` only in specific contexts). 3. **`constraint-satisfies?(ty, constraint) → bool`** — does a type fit a constraint? Go: interfaces (structural method set), `comparable`, `any`. TS would: structural subtyping. Haskell: typeclass dictionary resolution. Rust: trait impl. **Three orthogonal first-class-tag axes** (clean separation): - **AST nodes** (parser output): `:func-decl`, `:literal`, `:literal-string`, `:app`, `:index`, `:composite`, etc. - **Value-type kinds** (evaluator output): `:go-struct`, `:go-slice`, `:go-map`, `:go-chan`, `:go-fn`, `:go-method`, `:go-builtin`, `:go-builtin-fn`, `:go-package`, `:go-panic`, `:go-defer` — 11 kinds. All shape: `(:KIND PAYLOAD...)`. - **Sentinel signals** (control-flow): `:return-value`, `:break`, `:continue`, `:eval-error`, `:go-panic`. All three axes use the same `(first x) == :TAG` discipline. Kit's `kind?` and `kind-of` predicates work uniformly. **The "shape is parser, role is validator" lemma**, validated across THREE deliverables: 1. Binding-groups (`(:field NAMES TY)`): 6 consumers (struct fields, var-decls, const-decls, params, receivers, type-params), 5 distinct roles (value-typing, value-pinning, constraint-binding, kind-binding, trait-binding). 2. Control-flow sentinels: same predicate dispatch at 4+ sites. 3. Index synthesis (`(:index OBJ IDX)`): same AST, 3 role- validators (slice / array / map). **v0 limitations the kit must lift** (durable in commit trail): - Type-set constraints (`int | float64`, `~int`) — needs constraint-satisfies? predicate real implementation. - Type inference at call sites — Go's algorithm; currently relies on type erasure at eval. - nil-as-unbound — env-lookup needs an "absent" sentinel. - First-char literal classification (was a bug; fixed by `:literal-string` parser tag). Next sister-plan-owned step is Phase 2 (pick + start second consumer — recommendation: TypeScript). Two-language rule still pending until the second consumer lands. - 2026-05-28 — From Go-on-SX Phase 8 first slice — **value-type kinds confirm the "kind-tag + payload" shape as cross-runtime primitive.** When the stdlib landed, packages joined the existing registry of value-type kinds: - `(:go-struct TY-NAME FIELDS)` — composite by-field state - `(:go-slice ELEMS)` — sequential by-position state - `(:go-map ENTRIES)` — keyed state - `(:go-chan ACCESSORS)` — closure-bundle (channel) - `(:go-fn PARAMS BODY)` — user function value - `(:go-method RECV PARAMS BODY)` — method value - `(:go-builtin NAME)` — name-dispatched builtin - `(:go-builtin-fn FN)` — closure-dispatched builtin (NEW) - `(:go-package NAME ENTRIES)` — namespace value (NEW) - `(:go-panic V)` — unwinding-control value - `(:go-defer CALLEE ARGS)` — frame-cleanup record All eleven kinds use the same `(:KIND-TAG PAYLOAD...)` shape. None of them are AST nodes (those are `:func-decl`, `:literal`, etc.); they're VALUES the evaluator produces. The orthogonal axes the kit should care about: 1. **AST nodes** (parser output, evaluator input) 2. **Value-type kinds** (evaluator output, predicate input) 3. **Sentinel signals** (control-flow: return/break/panic/etc.) All three subscribe to the same first-class-tag discipline: `(first x)` answers "what kind is this?" and the rest is payload. The kit's `kind?` and `kind-of` predicates work uniformly across all three axes. For the bidirectional checker specifically, this means the `assignable?(got, expected)` predicate isn't special — it's just one predicate that operates on value-type kinds. The `synth` / `check` skeleton processes AST nodes; the validators it calls operate on value-type kinds. Clean separation: AST is what you parse, value-types are what you check, sentinels are what you propagate. None of them bleed into each other. Phase 7's index-synth and Phase 8's package-lookup both fit the same template: AST kind triggers a synth/lookup, returning a value-type kind. The validator-table dispatch from earlier diary entries is the right abstraction; the kit should expose it as a PROTOCOL (Go would phrase this as an interface, Haskell as a typeclass) so all three axes can be extended without modifying the kit. - 2026-05-28 — From Go-on-SX Phase 7 closing — **the "shape is the parser, role is the validator" lemma.** After landing canonical generic Map/Filter/Reduce/First plus 25+ typer tests, a clear pattern has emerged across THREE distinct deliverables of the Go-on-SX loop: 1. **Binding-groups** (struct fields / var-decls / params / receivers / type-params): SAME parser, SAME `(:field NAMES TY)` shape, 5 different validators based on what role TY plays. 2. **Control-flow sentinels** (return-value / break / continue / eval-error / go-panic): SAME `(go-panic? r)`-style dispatch at 4+ AST control-flow sites, each calling the same predicate list — would collapse to a single `propagates?` helper. 3. **Index synthesis** (`xs[0]` for slice / array / map): SAME `(:index OBJ IDX)` AST, 3 element-type extraction rules dispatching on OBJ's type. The validator differs per role, but the parser shape is one. The recurring lemma: **the kit's primary primitive is shape recognition (parser + AST); the kit's secondary primitive is a role-validator dispatch table.** Consumers (Go, Erlang, future guests) plug their semantics into the role table; they never need to define new shapes for things that already match an existing AST. Architectural payoff: at extraction time, the kit's API should expose: - `parse-XXX` → AST shape (one per shape) - `validate-AST(role, ctx)` → either ctx or error (one per role) - `dispatch-table(role)` → which-validator-fires-for-this-AST Reuse across guest evaluators happens automatically because the shape is shared. New guests only register new role handlers; they don't extend the parser. Concretely for the bidirectional checker: the synth/check skeleton is the shape; assignable? and constraint-satisfies? are roles. Adding a new language means adding a row to the role table, not a column to the AST. - 2026-05-28 — From Go-on-SX Phase 7 foundation — **the field binding-group is a cross-deliverable shape, confirmed by its 6th consumer (type-parameter lists).** Previously documented uses: struct fields, var-decls, const-decls, func params, method receivers. Now type-parameters re-use the EXACT same parser (`gp-parse-decl-param-group`) and the same `(list :field NAMES TY)` shape — only the meaning of TY differs (it's a *constraint* type, not a value type). This is the strongest evidence yet that the kit's primary shape should be a generic `binding-group` parametric over the role TY plays. Five roles emerge: 1. **value-typing** (struct fields, var-decls, params, receivers): TY is the type of values that bind to NAMES. 2. **value-pinning** (const-decls): TY is the type of compile- time-known values. 3. **constraint-binding** (type-parameter lists): TY is a constraint that the type-variables NAMES must satisfy. 4. **kind-binding** (anticipated for higher-kinded types): TY would be a kind that type-constructors NAMES inhabit. 5. **trait-binding** (anticipated for Rust-style impl blocks): TY would be the trait the implementations NAMES provide. All five share parser + AST shape; they differ in (a) which predicate validates the relationship between NAMES and TY, and (b) what scope NAMES are visible in. The kit should expose a single `parse-binding-group` consumer and let each role plug in its own validator. This is the same lesson the assignable? + constraint-satisfies? pluggable-predicate work surfaced — kit primitives are SHAPES, validators are PLUGINS. Concretely: when the kit extracts, the bidirectional checker exposes `extend-ctx-with-binding-group(role, group)` where role selects the validator. Go's type-params bind via role= "constraint-binding"; struct fields bind via "value-typing". Erlang's pattern bindings will bind via something else again. - 2026-05-27 — From Go-on-SX Phase 3 — **interface satisfaction** is the third pluggable predicate the kit should ship, alongside `assignable?` and the synth/check skeleton. Go's structural-and-silent satisfaction is one instance; Haskell's typeclass dictionary resolution, Rust's trait `impl` lookup, and TS's structural subtyping are others — all answer the same question with different machinery: "does this value-type fit this constraint-type?" Kit proposal: ``` (constraint-satisfies? CTX VALUE-TY CONSTRAINT-TY) → bool ``` Different consumers plug in different implementations: * Go: walk interface methods, lookup `#method/T/NAME`. * Haskell: typeclass instance resolution (with global instance table). * Rust: trait impl lookup with where-clause bound check. * TS: structural subtyping with property-by-property comparison. The judgment skeleton uses it during `check` when the expected type is itself an interface/constraint: ``` check Γ e EXPECTED → if EXPECTED is a constraint type: let GOT = synth Γ e if constraint-satisfies? Γ GOT EXPECTED then :ok else mismatch else: use the assignable? path ``` Source: Go-on-SX commit landing `go-iface-satisfies?` in `lib/go/types.sx` with the `#method/T/NAME` mangled-key storage scheme. - 2026-05-27 — Follow-up from Phase 3 scaffold: **assignability** has landed as a separate relation from structural equality. Go's untyped-constant flow (`var x float64 = 42 / 7` — 42/7 stays untyped int, then converts to float64) is one instance of a broader pattern: the value's "natural" type isn't quite the slot's type, but they're compatible under a per-language relation. **Design insight for the kit**: `check` should *not* call `equal?` on the synthesised vs expected types. It should call a pluggable `assignable?` predicate that each consumer supplies: ``` (check CTX EXPR EXPECTED) → let GOT = (synth CTX EXPR) if (assignable? GOT EXPECTED) :ok else (:mismatch EXPECTED GOT) ``` Go's `assignable?` handles untyped constants → numeric-type conversion. TS would supply structural subtyping (`{a: number, b: string}` assignable to `{a: number}`). Rust supplies lifetime-aware type identity with implicit `&T -> &U` where `T: Deref`. None of the consumers need to rewrite synth or the judgment skeleton — only swap in their variance discipline. Concretely the kit interface looks like: ``` (check-with assignable? CTX EXPR EXPECTED) — kit primitive ``` Source: Go-on-SX commit landing `go-type-assignable?` in `lib/go/types.sx`. - 2026-05-27 — From Go-on-SX Phase 3 scaffold (`lib/go/types.sx` first cut): the **independent synth/check shape** has landed. Two judgments, both consuming a context-as-value: ``` (go-synth CTX EXPR) → TYPE-NODE | (:type-error TAG ...) (go-check CTX EXPR EXPECTED) → :ok | (:type-error TAG ...) ``` Context is an association list of `(NAME TYPE)` bindings; the load-bearing extension primitive is `go-ctx-extend-field` which takes a `(:field NAMES TYPE)` binding-group node and binds every NAME to TYPE. This validates the earlier cross-deliverable observation: the parser produces `:field` once, the type checker consumes it once, same shape across struct fields / func params / var-decls. **Design insight for the kit**: the synth/check pair is the canonical judgment skeleton. `check` deferring to `synth + structural-equality` is the v0 default that every consumer overrides for subtype-ish relationships. The kit's `check` should accept a `subtype?` predicate parameter so Go (untyped-constant flow), TS (variance), and Rust (lifetime subtyping) each plug in their own variance discipline without rewriting the whole judgment. The kit's `synth` stays uniform. Error shape `(:type-error TAG ...)` with first-class tags (`:unbound`, `:mismatch`, `:unsupported-synth`) gives consumers and IDE tooling structured errors to dispatch on. Untyped-constant flow and binop-synth — the canonical Go pitfall (`var x float64 = 42 / 7`) — arrive next. Source: Go-on-SX commit landing `lib/go/types.sx`. - 2026-05-27 — From Go-on-SX Phase 2 (func decls landing): parser-side observation that's load-bearing for any bidirectional checker. Go's parser ended up with a single shape — `(list :field NAMES TYPE)` — that recurs in five contexts: struct fields, var decls, const decls, func params, and method receivers. Each represents "these names are bound to this type" — exactly the input shape `check` would consume to seed the context with typed bindings. **Design insight**: the canonical bidirectional checker should accept `:field`-shaped AST nodes uniformly across these contexts rather than each context defining a bespoke shape. The kit's `check Γ e T` judgment can dispatch on the enclosing form (struct vs var vs func-param vs ...) but the local per-binding shape stays identical. This is what statically-typed guest #2 should also produce — if it does, the kit can ship a `field-bindings → context-extension` helper that all consumers reuse. Cross-ref Go-on-SX plan's Blockers entry on `ast-binding-group` for the parallel AST-kit proposal that supports this. Source: Go-on-SX commit `parse.sx — func declarations`. - 2026-05-26 — Plan drafted as design diary. Phase 0 unstarted. Gated on Go-on-SX (first consumer) and a TBD second consumer (recommendation: TypeScript). No code yet — kit cannot exist before two consumers do.