Typed RPC: one Endpoint, both sides type-checked (Servant, properly)

[junjihashimoto]

Follow-up to the review: makes the API's input/output types checked on both the server and the client, from a single source of truth, so the wire shape can't drift (the actual point of the Servant-style claim).

The problem

Legacy LeanTea.Rpc is stringly-typed: Endpoint carries a List String of param names and Handler := List String → IO String. The server hand-decodes (ps[0]?.bind String.toInt?), the client calls a generated untyped JS function. Nothing ties the two to a shared type — a request/response shape change compiles fine on both sides and breaks at runtime.

What this adds

LeanTea.Rpc.Typed — types are part of the endpoint:

structure SetCellReq  where ref : String; formula : String  deriving Lean.ToJson, Lean.FromJson
structure SetCellResp where ok : Bool;   value : String      deriving Lean.ToJson, Lean.FromJson

def setCell : Endpoint SetCellReq SetCellResp :=
  { name := "apiSetCell", path := "/api/set", reqType := "SetCellReq", respType := "SetCellResp" }

• serve : Endpoint α β → (α → IO β) → Route — the handler is α → IO β, no List String, no manual parsing. Dispatch decodes the body to α via FromJson (400 on malformed/wrong-shape) and encodes β.
• Endpoint.clientFn — generates the browser JS (fetch + JSON.stringify(req) + await r.json()) from the same endpoint.
• Endpoint.stubDecl — generates the Lean type-check stub opaque apiFoo : Req → Async Resp.

LeanJs.TypeCheck — the client half. .leanjs is a separate DSL with no type system (its Check does arity + record-field names only). Rather than build a type checker into it — reinventing what Lean has — we emit the client to real Lean and let Lean's elaborator check it: async def → do-block, await → ←, the async effect modelled as an IO alias purely so the types line up (we elaborate, never run). Fed a prelude of the shared types + endpoint stubs, lean reports any call site that disagrees with the server's types.

Proof (examples/Tests/TypedRpcSpec.lean — 9/9)

One Endpoint SetCellReq SetCellResp drives:

• server: valid → 200 ({"ok":true,"value":"A1=42"}), malformed JSON → 400, wrong-shape → 400, unmatched → 404
• client type-check: a correct .leanjs client passes; one with a mistyped request field (formla) is rejected — checked against the same SetCellReq/SetCellResp
• client JS: apiSetCell generated, request serialized as JSON

● client (type-checked vs the same types)
    ✓ correct client type-checks
    ✓ mistyped request field rejected

Design note (why this shape)

The investigation confirmed .leanjs isn't Lean-checked and the embedded LeanTea.Js DSL is untyped Expr. The leverage was to reuse Lean's own elaborator for the client rather than hand-roll a type system — so the client and server share one definition and the check is Lean's real type checker, not an approximation.

Scope / follow-ups (not in this PR)

• Auto-generate the type-check prelude by import-ing the user's types module instead of the inline structure text the harness currently takes (removes the one remaining duplicate).
• Map lean's error line/col back to the .leanjs source (today it reports the emitted-harness position; the message itself — the offending field name — is already actionable).
• Wire TypeCheck.check into the serve-time compile pipeline so a type error fails the build; migrate one example app (Sheet/Canvas) onto the typed layer.
• .d.ts generation for external (non-Lean) JS/TS consumers.
• Legacy stringly LeanTea.Rpc kept for back-compat.

Test plan

• lake build clean (178 targets)
• typed_rpc_spec 9/9 (server dispatch + client type-check accept/reject + JS gen). Spawns lean for the client checks, same pattern as leanjs_spec (lean --run).