;; lib/go/types.sx — Go bidirectional type checker.
;;
;; Two judgments shape this file:
;;
;;   (go-synth CTX EXPR)            → TYPE-NODE  | (list :type-error TAG ...)
;;     Given a context and an expression, produce a type.
;;
;;   (go-check CTX EXPR EXPECTED)   → :ok        | (list :type-error TAG ...)
;;     Given a context, expression, and expected type, verify compatibility.
;;
;; The two judgments are mutually recursive. Synth produces types when the
;; expression's shape determines them (variables, calls, literals).
;; Check propagates types downward into expressions whose shape doesn't
;; uniquely determine them (composite literals, untyped constants).
;;
;; Type representations reuse the parser's :ty-* AST nodes from
;; lib/go/parse.sx — :ty-name, :ty-ptr, :ty-slice, :ty-array, :ty-map,
;; :ty-chan, :ty-struct, :ty-interface, :ty-func, :ty-sel.
;;
;; Context: an association list of (NAME TYPE) bindings. Per-block scope
;; via a fresh extension on entry.
;;
;; **Independent implementation.** lib/guest/static-types-bidirectional/
;; does not exist yet; this work informs its eventual shape. Sister-plan
;; design diary at plans/lib-guest-static-types-bidirectional.md tracks
;; the chiselling insights as Phase 3 progresses.

;; ── context ───────────────────────────────────────────────────────

(define go-ctx-empty (list))

(define
  go-ctx-lookup
  (fn
    (ctx name)
    (cond
      (= (len ctx) 0)
      nil
      (= (first (first ctx)) name)
      (nth (first ctx) 1)
      :else (go-ctx-lookup (rest ctx) name))))

(define go-ctx-extend (fn (ctx name type) (cons (list name type) ctx)))

(define
  go-ctx-extend-field
  (fn
    (ctx field)
    (let
      ((names (nth field 1)) (ty (nth field 2)))
      (cond
        (= (len names) 0)
        ctx
        :else (let
          ((rest-ctx (go-ctx-extend ctx (first names) ty)))
          (cond
            (= (len names) 1)
            rest-ctx
            :else (go-ctx-extend-field rest-ctx (list :field (rest names) ty))))))))

;; ── predeclared identifiers ──────────────────────────────────────

(define
  go-predeclared
  (list
    (list "true" (list :ty-name "bool"))
    (list "false" (list :ty-name "bool"))
    (list "nil" (list :ty-untyped-nil))))

(define
  go-predeclared-lookup
  (fn
    (name)
    (cond
      (= (len go-predeclared) 0)
      nil
      :else (go-ctx-lookup go-predeclared name))))

;; ── type predicates ──────────────────────────────────────────────

(define
  go-type-error?
  (fn
    (x)
    (and
      (list? x)
      (not (= (len x) 0))
      (= (first x) :type-error))))

(define go-type-equal? (fn (a b) (= a b)))

;; ── untyped constants ────────────────────────────────────────────
;; Go spec § Constants: literals carry an "untyped" type until they're
;; used in a context that forces a type. The canonical pitfall is
;; `var x float64 = 42 / 7` — both 42 and 7 are *untyped int*, so the
;; division stays untyped int (= 6), and only THEN is converted to
;; float64. (Wrong implementations float-coerce first, getting 6.0 from
;; what was meant to round.) The :ty-untyped-* tags below model this.

(define ty-untyped-int    (list :ty-untyped-int))
(define ty-untyped-float  (list :ty-untyped-float))
(define ty-untyped-imag   (list :ty-untyped-imag))
(define ty-untyped-string (list :ty-untyped-string))
(define ty-untyped-rune   (list :ty-untyped-rune))

(define
  go-str-any?
  (fn (pred s)
    (define
      gsa-loop
      (fn (i)
        (cond
          (>= i (len s)) false
          (pred (nth s i)) true
          :else (gsa-loop (+ i 1)))))
    (gsa-loop 0)))

(define
  go-str-contains?
  (fn (s ch) (go-str-any? (fn (c) (= c ch)) s)))

(define
  go-classify-literal-string
  ;; Heuristic detection of Go literal kind from the value-string.
  ;; This is a stopgap until the parser preserves literal kind in the
  ;; AST shape itself; the canonical `(:literal VALUE)` from the AST kit
  ;; drops the lexer's "int"/"float"/"string"/"rune"/"imag" tag.
  ;; Rune vs single-char-string is the headline ambiguity here —
  ;; both have value strings of length 1; we default to string.
  (fn (v)
    (cond
      (or (not (string? v)) (= (len v) 0)) :string
      (or (and (>= (nth v 0) "0") (<= (nth v 0) "9"))
          (and (= (nth v 0) ".") (>= (len v) 2)
               (>= (nth v 1) "0") (<= (nth v 1) "9")))
      (cond
        (= (nth v (- (len v) 1)) "i") :imag
        (go-str-contains? v ".") :float
        (and (or (go-str-contains? v "e") (go-str-contains? v "E"))
             (not (and (>= (len v) 2) (= (nth v 0) "0")
                       (or (= (nth v 1) "x") (= (nth v 1) "X")))))
        :float
        :else :int)
      :else :string)))

(define
  go-synth-literal
  (fn (v)
    (let ((k (go-classify-literal-string v)))
      (cond
        (= k :int)    ty-untyped-int
        (= k :float)  ty-untyped-float
        (= k :imag)   ty-untyped-imag
        (= k :rune)   ty-untyped-rune
        :else         ty-untyped-string))))

(define
  go-untyped?
  (fn (t)
    (and (list? t) (not (= (len t) 0))
         (or (= (first t) :ty-untyped-int)
             (= (first t) :ty-untyped-float)
             (= (first t) :ty-untyped-imag)
             (= (first t) :ty-untyped-string)
             (= (first t) :ty-untyped-rune)
             (= (first t) :ty-untyped-nil)))))

(define
  go-numeric-name?
  ;; Built-in numeric type names per Go spec § Numeric types.
  (fn (name)
    (some (fn (n) (= n name))
      (list "int" "int8" "int16" "int32" "int64"
            "uint" "uint8" "uint16" "uint32" "uint64" "uintptr"
            "byte" "rune"
            "float32" "float64"
            "complex64" "complex128"))))

(define
  go-floating-name?
  (fn (name)
    (or (= name "float32") (= name "float64"))))

(define
  go-complex-name?
  (fn (name)
    (or (= name "complex64") (= name "complex128"))))

(define
  go-type-assignable?
  ;; Can a value of type GOT be assigned to a slot of type EXPECTED?
  ;; Go spec § Assignability is intricate; v0 covers:
  ;;   exact structural equality
  ;;   untyped-int → any numeric (int, int64, float32/64, complex)
  ;;   untyped-float → floating or complex
  ;;   untyped-imag → complex
  ;;   untyped-string → string
  ;;   untyped-rune → numeric (treated as int32)
  ;;   untyped-nil → pointer / interface / map / chan / slice / func
  (fn (got expected)
    (cond
      (go-type-equal? got expected) true
      (and (list? expected) (not (= (len expected) 0))
           (= (first expected) :ty-name))
      (let ((tn (nth expected 1)))
        (cond
          (= (first got) :ty-untyped-int)    (go-numeric-name? tn)
          (= (first got) :ty-untyped-float)
          (or (go-floating-name? tn) (go-complex-name? tn))
          (= (first got) :ty-untyped-imag)   (go-complex-name? tn)
          (= (first got) :ty-untyped-rune)   (go-numeric-name? tn)
          (= (first got) :ty-untyped-string) (= tn "string")
          :else false))
      :else false)))

;; ── synth ────────────────────────────────────────────────────────

(define
  go-arith-binops (list "+" "-" "*" "/" "%"))
(define
  go-bitwise-binops (list "&" "|" "^" "<<" ">>" "&^"))
(define
  go-compare-binops (list "==" "!=" "<" "<=" ">" ">="))
(define
  go-logical-binops (list "&&" "||"))

(define
  go-unify-untyped
  ;; When two untyped types meet in a binop, return their unified
  ;; untyped result, or nil if incompatible.
  (fn (a b)
    (cond
      (go-type-equal? a b) a
      (and (= (first a) :ty-untyped-int) (= (first b) :ty-untyped-float))
      ty-untyped-float
      (and (= (first a) :ty-untyped-float) (= (first b) :ty-untyped-int))
      ty-untyped-float
      :else nil)))

(define
  go-synth
  (fn (ctx expr)
    (cond
      (and (list? expr) (= (first expr) :literal))
      (go-synth-literal (nth expr 1))
      (and (list? expr) (= (first expr) :literal-string))
      ty-untyped-string
      (and (list? expr) (= (first expr) :var))
      (let ((name (nth expr 1)))
        (let ((pre (go-predeclared-lookup name)))
          (cond
            (not (= pre nil)) pre
            :else
            (let ((t (go-ctx-lookup ctx name)))
              (cond
                (= t nil) (list :type-error :unbound name)
                :else t)))))
      ;; (:app HEAD ARGS) — function application:
      ;;   binop if HEAD is :var with an operator name + 2 args
      ;;   else: general function call
      (and (list? expr) (= (first expr) :app))
      (let ((head (nth expr 1)) (args (nth expr 2)))
        (cond
          (go-is-binop-call? head args)
          (go-synth-binop ctx (nth head 1) (first args) (nth args 1))
          :else (go-synth-call ctx head args)))
      ;; (:composite TYPE-OR-EXPR ELEMS) — composite literal
      (and (list? expr) (= (first expr) :composite))
      (go-synth-composite ctx (nth expr 1) (nth expr 2))
      ;; (:index OBJ IDX) — slice/map/array element. v0: element type
      ;; is the slice/array element type, or the map value type.
      (and (list? expr) (= (first expr) :index))
      (let ((obj-ty (go-synth ctx (nth expr 1))))
        (cond
          (go-type-error? obj-ty) obj-ty
          (and (list? obj-ty) (= (first obj-ty) :ty-slice))
          (nth obj-ty 1)
          (and (list? obj-ty) (= (first obj-ty) :ty-array))
          (nth obj-ty 2)
          (and (list? obj-ty) (= (first obj-ty) :ty-map))
          (nth obj-ty 2)
          :else (list :type-error :index-not-indexable obj-ty)))
      :else (list :type-error :unsupported-synth expr))))

(define
  go-is-binop-call?
  (fn (head args)
    (and (list? head) (= (first head) :var)
         (= (len args) 2)
         (let ((op (nth head 1)))
           (or (some (fn (o) (= o op)) go-arith-binops)
               (some (fn (o) (= o op)) go-bitwise-binops)
               (some (fn (o) (= o op)) go-compare-binops)
               (some (fn (o) (= o op)) go-logical-binops))))))

(define
  go-check-args-against
  ;; Each arg in ARGS assignable to the corresponding PARAMS type.
  ;; Caller already verified arities match.
  (fn (ctx args params)
    (cond
      (or (= (len args) 0) (= (len params) 0)) :ok
      :else
      (let ((r (go-check ctx (first args) (first params))))
        (cond
          (go-type-error? r) r
          :else (go-check-args-against ctx (rest args) (rest params)))))))

(define
  go-check-composite-elems
  ;; KEY-TY is nil for slice/array; non-nil for map.
  ;; For maps, each elem must be (:kv KEY VALUE) — KEY assignable to
  ;; KEY-TY, VALUE to VAL-TY.
  ;; For slice/array, plain exprs assignable to VAL-TY; (:kv K V) is
  ;; Go's index-keyed shorthand (`[]int{0: 5, 1: 10}`) — we type-check
  ;; only the value in v0.
  (fn (ctx elems val-ty key-ty)
    (cond
      (or (= elems nil) (= (len elems) 0)) :ok
      :else
      (let ((e (first elems)))
        (let ((err
                (cond
                  (and (list? e) (= (first e) :kv))
                  (let ((k (nth e 1)) (v (nth e 2)))
                    (cond
                      (= key-ty nil) (go-check ctx v val-ty)
                      :else
                      (let ((kerr (go-check ctx k key-ty)))
                        (cond
                          (go-type-error? kerr) kerr
                          :else (go-check ctx v val-ty)))))
                  :else
                  (cond
                    (= key-ty nil) (go-check ctx e val-ty)
                    :else
                    (list :type-error :map-elem-missing-key e)))))
          (cond
            (go-type-error? err) err
            :else
            (go-check-composite-elems ctx (rest elems) val-ty key-ty)))))))

(define
  go-synth-composite
  ;; Composite literal: (:composite TYPE-OR-EXPR ELEMS).
  ;;   []T{...}            — each elem assignable to T; result :ty-slice T
  ;;   [N]T{...}           — same; result :ty-array N T
  ;;   map[K]V{...}        — each :kv key:K, value:V; result :ty-map K V
  ;; Named-type literals (Point{...}, pkg.T{...}) require type-decl
  ;; resolution; v0 returns the literal's type-expr as-is without
  ;; element checking.
  (fn (ctx ty elems)
    (cond
      (and (list? ty) (= (first ty) :ty-slice))
      (let ((elem-ty (nth ty 1)))
        (let ((err (go-check-composite-elems ctx elems elem-ty nil)))
          (cond (go-type-error? err) err :else ty)))
      (and (list? ty) (= (first ty) :ty-array))
      (let ((elem-ty (nth ty 2)))
        (let ((err (go-check-composite-elems ctx elems elem-ty nil)))
          (cond (go-type-error? err) err :else ty)))
      (and (list? ty) (= (first ty) :ty-map))
      (let ((key-ty (nth ty 1)) (val-ty (nth ty 2)))
        (let ((err (go-check-composite-elems ctx elems val-ty key-ty)))
          (cond (go-type-error? err) err :else ty)))
      :else ty)))

(define
  go-synth-call
  ;; Synth a function call. Returns the result type, or :type-error.
  ;;   0 results → (list :ty-void)
  ;;   1 result  → that result type directly
  ;;   N results → (list :ty-tuple TYPES) (multi-return)
  (fn (ctx callee args)
    (let ((fn-ty (go-synth ctx callee)))
      (cond
        (go-type-error? fn-ty) fn-ty
        (not (and (list? fn-ty) (= (first fn-ty) :ty-func)))
        (list :type-error :not-callable fn-ty)
        :else
        (let ((params (nth fn-ty 1)) (results (nth fn-ty 2)))
          (cond
            (not (= (len args) (len params)))
            (list :type-error :arity-mismatch
              (len params) (len args))
            :else
            (let ((err (go-check-args-against ctx args params)))
              (cond
                (go-type-error? err) err
                (= (len results) 0) (list :ty-void)
                (= (len results) 1) (first results)
                :else (list :ty-tuple results)))))))))

(define
  go-synth-binop
  (fn (ctx op lhs rhs)
    (let ((lt (go-synth ctx lhs)) (rt (go-synth ctx rhs)))
      (cond
        (go-type-error? lt) lt
        (go-type-error? rt) rt
        ;; Comparison ops always produce bool (untyped-bool, simplified
        ;; here to :ty-name "bool" until we model untyped-bool).
        (some (fn (o) (= o op)) go-compare-binops)
        (list :ty-name "bool")
        (some (fn (o) (= o op)) go-logical-binops)
        (list :ty-name "bool")
        ;; Arithmetic / bitwise: types must unify.
        (or (some (fn (o) (= o op)) go-arith-binops)
            (some (fn (o) (= o op)) go-bitwise-binops))
        (cond
          (and (go-untyped? lt) (go-untyped? rt))
          (let ((unified (go-unify-untyped lt rt)))
            (cond
              (= unified nil)
              (list :type-error :binop-untyped-mismatch op lt rt)
              :else unified))
          (and (go-untyped? lt) (not (go-untyped? rt)))
          (cond
            (go-type-assignable? lt rt) rt
            :else (list :type-error :binop-mismatch op lt rt))
          (and (not (go-untyped? lt)) (go-untyped? rt))
          (cond
            (go-type-assignable? rt lt) lt
            :else (list :type-error :binop-mismatch op lt rt))
          (go-type-equal? lt rt) lt
          :else (list :type-error :binop-mismatch op lt rt))
        :else (list :type-error :unsupported-binop op)))))

;; ── check ────────────────────────────────────────────────────────

(define
  go-check
  (fn
    (ctx expr expected)
    (let
      ((got (go-synth ctx expr)))
      (cond
        (go-type-error? got)
        got
        (go-type-assignable? got expected)
        :ok :else
        (list :type-error :mismatch expected got)))))

;; ── default types ────────────────────────────────────────────────
;; Go spec § Constants: the *default type* of an untyped constant
;; is what it becomes when assigned to a sloppily-typed slot
;; (e.g., `var x = 42` makes x an int).

(define
  go-default-type
  (fn (t)
    (cond
      (not (list? t)) t
      (= (first t) :ty-untyped-int)    (list :ty-name "int")
      (= (first t) :ty-untyped-float)  (list :ty-name "float64")
      (= (first t) :ty-untyped-imag)   (list :ty-name "complex128")
      (= (first t) :ty-untyped-string) (list :ty-name "string")
      (= (first t) :ty-untyped-rune)   (list :ty-name "int32")
      :else t)))

;; ── declaration checking ────────────────────────────────────────
;; Returns either:
;;   the extended context (success)
;;   (list :type-error TAG ...) (failure)

(define
  go-check-exprs-against
  ;; Check every EXPR in EXPRS is assignable to EXPECTED. Returns the
  ;; first :type-error encountered, or :ok.
  (fn (ctx exprs expected)
    (cond
      (or (= exprs nil) (= (len exprs) 0)) :ok
      :else
      (let ((r (go-check ctx (first exprs) expected)))
        (cond
          (go-type-error? r) r
          :else (go-check-exprs-against ctx (rest exprs) expected))))))

(define
  go-bind-names-to-synth
  ;; Pair each NAME with the synthesised default-typed type of the
  ;; corresponding EXPR; extend CTX with all pairs. NAMES and EXPRS
  ;; may have different lengths (multi-return funcs aren't here yet);
  ;; for now we zip the shorter of the two.
  (fn (ctx names exprs)
    (cond
      (or (= (len names) 0) (= (len exprs) 0)) ctx
      :else
      (let ((t (go-synth ctx (first exprs))))
        (cond
          (go-type-error? t) t
          :else
          (let ((ctx2 (go-ctx-extend ctx (first names)
                       (go-default-type t))))
            (go-bind-names-to-synth ctx2 (rest names) (rest exprs))))))))

(define
  go-check-var-decl
  ;; Shape: (:var-decl (:field NAMES TYPE-or-nil) EXPRS-or-nil)
  ;; or     (:const-decl (:field NAMES TYPE-or-nil) EXPRS).
  ;; Logic is the same for v0; const-vs-var distinction matters for
  ;; mutability checks which arrive later.
  (fn (ctx decl)
    (let ((field (nth decl 1)) (exprs (nth decl 2)))
      (let ((names (nth field 1)) (ann-ty (nth field 2)))
        (cond
          ;; var x T (no init) → bind names to T
          (or (= exprs nil) (= (len exprs) 0))
          (cond
            (= ann-ty nil) (list :type-error :missing-type-or-init names)
            :else (go-ctx-extend-field ctx field))
          ;; Annotated: var x T = expr — check each expr against T
          (not (= ann-ty nil))
          (let ((err (go-check-exprs-against ctx exprs ann-ty)))
            (cond
              (go-type-error? err) err
              :else (go-ctx-extend-field ctx field)))
          ;; Inferred: var x = expr — bind names to default(synth(expr))
          :else (go-bind-names-to-synth ctx names exprs))))))

(define
  go-check-short-decl
  ;; Shape: (:short-decl LHS-LIST EXPRS). LHS is a list of (:var NAME).
  ;; Extracts the names and falls through to bind-names-to-synth.
  (fn (ctx decl)
    (let ((lhs-list (nth decl 1)) (exprs (nth decl 2)))
      (let ((names (map (fn (lhs)
                          (cond
                            (and (list? lhs) (= (first lhs) :var))
                            (nth lhs 1)
                            :else :unknown))
                        lhs-list)))
        (go-bind-names-to-synth ctx names exprs)))))

(define
  go-check-decl
  ;; Top-level dispatcher: accepts any decl AST shape, returns extended
  ;; context or :type-error.
  (fn (ctx decl)
    (cond
      (and (list? decl) (= (first decl) :var-decl))   (go-check-var-decl ctx decl)
      (and (list? decl) (= (first decl) :const-decl)) (go-check-var-decl ctx decl)
      (and (list? decl) (= (first decl) :short-decl)) (go-check-short-decl ctx decl)
      (and (list? decl) (= (first decl) :type-decl))
      (let ((name (nth decl 1)) (ty (nth decl 2)))
        (go-ctx-extend ctx name ty))
      (and (list? decl) (= (first decl) :func-decl))
      (go-check-func-decl ctx decl)
      (and (list? decl) (= (first decl) :method-decl))
      (go-check-method-decl ctx decl)
      :else ctx)))

;; ── method declarations and interface satisfaction ──────────────
;; Methods are recorded in CTX under a mangled key
;;   "#method/RECV-TYPE-NAME/METHOD-NAME"
;; bound to the method's :ty-func signature. Interface satisfaction is
;; a structural lookup over these keys (Go spec § Interface types:
;; "anything with the matching method set satisfies the interface").

(define
  go-method-key
  (fn (recv-ty-name method-name)
    (str "#method/" recv-ty-name "/" method-name)))

(define
  go-extract-recv-ty-name
  ;; Receiver type is T or *T; return the named type's name string.
  (fn (recv-ty)
    (cond
      (and (list? recv-ty) (= (first recv-ty) :ty-name))
      (nth recv-ty 1)
      (and (list? recv-ty) (= (first recv-ty) :ty-ptr))
      (go-extract-recv-ty-name (nth recv-ty 1))
      :else nil)))

(define
  go-check-method-decl
  ;; (list :method-decl RECV NAME PARAMS RESULTS BODY)
  ;; Binds the method under the mangled key, then checks body with
  ;; receiver + params extended.
  (fn (ctx decl)
    (let ((recv (nth decl 1)) (name (nth decl 2))
          (params (nth decl 3)) (results (nth decl 4))
          (body (nth decl 5)))
      (let ((recv-ty (nth recv 2)))
        (let ((recv-name (go-extract-recv-ty-name recv-ty)))
          (let ((sig (list :ty-func
                       (go-decl-params-to-ty-list params) results)))
            (let ((ctx2
                    (cond
                      (= recv-name nil) ctx
                      :else
                      (go-ctx-extend ctx
                        (go-method-key recv-name name) sig))))
              (cond
                (= body nil) ctx2
                (and (list? body) (= (first body) :block))
                (let ((body-ctx
                        (go-extend-with-params
                          (go-ctx-extend-field ctx2 recv) params)))
                  (let ((err
                          (go-check-block body-ctx
                            (nth body 1) results)))
                    (cond
                      (go-type-error? err) err
                      :else ctx2)))
                :else ctx2))))))))

(define
  go-iface-elems-satisfied?
  ;; Each :method element in ELEMS must have a matching method in CTX
  ;; under #method/TY-NAME/M-NAME. :embed elements are skipped in v0
  ;; (they'd need recursive interface resolution).
  (fn (ctx ty-name elems)
    (cond
      (= (len elems) 0) true
      :else
      (let ((e (first elems)))
        (cond
          (= (first e) :method)
          (let ((m-name (nth e 1)) (m-params (nth e 2))
                (m-results (nth e 3)))
            (let ((found (go-ctx-lookup ctx
                           (go-method-key ty-name m-name))))
              (cond
                (= found nil) false
                (and (= (nth found 1) m-params)
                     (= (nth found 2) m-results))
                (go-iface-elems-satisfied? ctx ty-name (rest elems))
                :else false)))
          (= (first e) :embed)
          (go-iface-elems-satisfied? ctx ty-name (rest elems))
          :else
          (go-iface-elems-satisfied? ctx ty-name (rest elems)))))))

(define
  go-iface-satisfies?
  ;; Does the type named TY-NAME satisfy the interface IFACE-TYPE
  ;; under context CTX? Structural method-set match per Go spec.
  (fn (ctx ty-name iface-type)
    (cond
      (not (and (list? iface-type) (= (first iface-type) :ty-interface)))
      false
      :else (go-iface-elems-satisfied? ctx ty-name (nth iface-type 1)))))

;; ── function-decl checking ──────────────────────────────────────

(define
  go-repeat-ty
  (fn (n ty acc)
    (cond
      (<= n 0) acc
      :else (go-repeat-ty (- n 1) ty (cons ty acc)))))

(define
  go-decl-params-to-ty-list
  ;; Flatten (:field NAMES TYPE) param groups into a list of types,
  ;; one entry per name. For func-type signatures.
  (fn (params)
    (cond
      (or (= params nil) (= (len params) 0)) (list)
      :else
      (let ((field (first params)))
        (let ((names (nth field 1)) (ty (nth field 2)))
          (let ((rest-tys (go-decl-params-to-ty-list (rest params))))
            (go-repeat-ty (len names) ty rest-tys)))))))

(define
  go-extend-with-params
  ;; Extend CTX with every binding in every (:field NAMES TYPE) param group.
  (fn (ctx params)
    (cond
      (or (= params nil) (= (len params) 0)) ctx
      :else
      (go-extend-with-params
        (go-ctx-extend-field ctx (first params))
        (rest params)))))

(define
  go-check-return-list
  ;; Each EXPR assignable to the corresponding RESULTS type.
  ;; v0: lengths must match; multi-return funcs deferred.
  (fn (ctx exprs results)
    (cond
      (and (= (len exprs) 0) (= (len results) 0)) :ok
      (not (= (len exprs) (len results)))
      (list :type-error :return-count-mismatch
        (len exprs) (len results))
      :else
      (let ((r (go-check ctx (first exprs) (first results))))
        (cond
          (go-type-error? r) r
          :else (go-check-return-list ctx (rest exprs) (rest results)))))))

(define
  go-check-assign
  (fn (ctx stmt)
    (let ((lhs-list (nth stmt 1)) (rhs-list (nth stmt 2)))
      (cond
        (not (= (len lhs-list) (len rhs-list)))
        (list :type-error :assign-count-mismatch
          (len lhs-list) (len rhs-list))
        :else (go-check-assign-pairs ctx lhs-list rhs-list)))))

(define
  go-check-assign-pairs
  (fn (ctx lhs-list rhs-list)
    (cond
      (= (len lhs-list) 0) :ok
      :else
      (let ((lhs-ty (go-synth ctx (first lhs-list))))
        (cond
          (go-type-error? lhs-ty) lhs-ty
          :else
          (let ((r (go-check ctx (first rhs-list) lhs-ty)))
            (cond
              (go-type-error? r) r
              :else
              (go-check-assign-pairs ctx (rest lhs-list)
                (rest rhs-list)))))))))

(define
  go-check-stmt
  ;; Returns either an extended CTX (decls), :ok (sealed stmts), or
  ;; :type-error. RESULTS is the enclosing func's declared return types
  ;; (used by :return).
  (fn (ctx stmt results)
    (cond
      (and (list? stmt) (= (first stmt) :var-decl))
      (go-check-decl ctx stmt)
      (and (list? stmt) (= (first stmt) :const-decl))
      (go-check-decl ctx stmt)
      (and (list? stmt) (= (first stmt) :short-decl))
      (go-check-decl ctx stmt)
      (and (list? stmt) (= (first stmt) :type-decl))
      (go-check-decl ctx stmt)
      (and (list? stmt) (= (first stmt) :return))
      (let ((exprs (nth stmt 1)))
        (let ((err (go-check-return-list ctx exprs results)))
          (cond (go-type-error? err) err :else ctx)))
      (and (list? stmt) (= (first stmt) :block))
      (let ((err (go-check-block ctx (nth stmt 1) results)))
        (cond (go-type-error? err) err :else ctx))
      (and (list? stmt) (= (first stmt) :assign))
      (let ((err (go-check-assign ctx stmt)))
        (cond (go-type-error? err) err :else ctx))
      :else
      (let ((t (go-synth ctx stmt)))
        (cond (go-type-error? t) t :else ctx)))))

(define
  go-check-block
  ;; Thread ctx through stmts; if any stmt is a decl, its extension
  ;; propagates to subsequent stmts. Returns :ok or :type-error.
  (fn (ctx stmts results)
    (cond
      (or (= stmts nil) (= (len stmts) 0)) :ok
      :else
      (let ((r (go-check-stmt ctx (first stmts) results)))
        (cond
          (go-type-error? r) r
          :else (go-check-block r (rest stmts) results))))))

(define
  go-check-func-decl
  ;; Bind the function in the outer ctx (so recursion works), extend
  ;; ctx with type params + value params, check the body. Returns the
  ;; outer ctx with the function bound, or :type-error.
  ;;
  ;; Type parameters become opaque type variables in the body's ctx:
  ;; each name `T` is bound as a type alias to (:ty-param "T") so the
  ;; checker treats references to T as "this type", not "unknown".
  ;; Constraint enforcement (T satisfies `comparable` etc.) is a
  ;; later refinement; v0 just allows any operation that's polymorphic
  ;; under the constraint `any`.
  (fn (ctx decl)
    (let ((name (nth decl 1)) (params (nth decl 2))
          (results (nth decl 3)) (body (nth decl 4))
          (type-params (cond (> (len decl) 5) (nth decl 5) :else nil)))
      (let ((fn-ty
              (list :ty-func
                (go-decl-params-to-ty-list params) results)))
        (let ((ctx-with-fn (go-ctx-extend ctx name fn-ty)))
          (cond
            (= body nil) ctx-with-fn
            (and (list? body) (= (first body) :block))
            (let ((body-ctx
                    (go-extend-with-type-params
                      (go-extend-with-params ctx-with-fn params)
                      type-params)))
              (let ((err
                      (go-check-block body-ctx (nth body 1) results)))
                (cond
                  (go-type-error? err) err
                  :else ctx-with-fn)))
            :else ctx-with-fn))))))

(define
  go-extend-with-type-params
  ;; Each (:field NAMES CONSTRAINT) field contributes opaque type
  ;; vars: bind each NAME as a type alias to (:ty-param NAME). The
  ;; constraint type is stored alongside so future "constraint
  ;; satisfaction" checks can find it; for v0 it's informational.
  (fn (ctx type-params)
    (cond
      (or (= type-params nil) (= (len type-params) 0)) ctx
      :else
      (let ((field (first type-params)))
        (let ((names (nth field 1)) (constraint (nth field 2)))
          (go-extend-with-type-params
            (go-extend-with-type-param-names ctx names constraint)
            (rest type-params)))))))

(define
  go-extend-with-type-param-names
  (fn (ctx names constraint)
    (cond
      (= (len names) 0) ctx
      :else
      (let ((nm (first names)))
        (go-extend-with-type-param-names
          (go-ctx-extend ctx nm
            (list :ty-param nm constraint))
          (rest names) constraint)))))
