# 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/<lang>/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<TyKind>` 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<U>`. 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.
