docs: RFC 0005 structural type inference + RFC 0006 success type checking

0005 proposes replacing the ad-hoc inference lattice with one recursive
structural type (a struct carries its field types, a vector its element type,
recursively), so a lookup returns its field's type and nested access is typed
end to end. It unifies :struct tracking with field tracking, subsumes the
current inference phases, and is the soft-typing (HM + a dynamic top) design:
structural types + core-fn type schemes, solved by lattice join with :any as
top instead of unify-or-fail. Includes the depth cap for termination and an
explicit design-problems section.

0006 (follow-up, depends on 0005) reuses the inference as a loose type checker
in the success-typing discipline (Dialyzer): report only PROVABLY-wrong code
(a concrete type in an operation's throwing error-domain), accept everything
ambiguous, never a false positive. Curated error-domain table, strictness
levels (off/warn/error), clear located messages, and the soundness boundaries
(closed-world, macros, unions).

docs/rfc/0005-structural-type-inference.md

@@ -0,0 +1,244 @@
+# RFC 0005 — Structural collection-type inference
+
+- **Status**: Draft
+- **Champions**: jolt maintainers
+- **Created**: 2026-06-13
+
+## Summary
+
+Replace jolt's ad-hoc inference lattice with a single recursive **structural
+type**, so that the type of a value mirrors the tree shape of the data it
+describes. A struct-map carries its field types, a vector its element type, a
+function its parameter and return types, recursively. A keyword lookup returns
+the looked-up field's type, so nested access like `(:r (:direction ray))` is
+typed end to end. This unifies the two facts the current inference tracks
+inconsistently (a vector's element type, but not a map's field types), subsumes
+the existing inference phases (jolt-99x Phases 0 to 3) as special cases, and
+closes the remaining ray-tracer gap without a hint. The system is a
+soft-typing-style inference: it never rejects a program, it assigns a concrete
+type only when it can prove one, and it falls back to `:any` (and the existing
+runtime guard) everywhere else.
+
+## Motivation
+
+The inference added in jolt-99x specializes a collection access (drops the
+`:jolt/type` guard, emits `pv-count`, and so on) when it can prove the
+collection's type. It works, it is sound, and it is fully dynamic-fallback
+safe. But its type lattice grew ad hoc:
+
+- `:struct-map` means "a raw-get-safe map" but carries **no field types**.
+- `{:vec ELEM}` carries its **element type**.
+
+These are the same idea applied to two kinds of child in the data tree, but
+only one is tracked. The cost is concrete: in the ray tracer a lookup result
+like `(:direction ray)` is typed `:any`, so `(:r (:direction ray))` keeps its
+guard, and the `vec3` functions (called all day with such values) cannot be
+typed, so the inference reaches only about 3% where the explicit `^:struct`
+hint reaches 22%. The hint wins precisely because it asserts the field/param
+shape the inference fails to derive.
+
+The fix is to make the type a structural tree, tagged as precisely as provable.
+Then `:struct` tracking and field tracking are one mechanism, the special cases
+collapse into one signature table, and nested access is typed by construction.
+
+## The type lattice
+
+A type `T` is one of:
+
+- A scalar tag: `:num`, `:str`, `:kw`, `:bool`, `:char`. (Optionally a coarser
+  `:nonnil` for "provably not nil and not false", which is what the struct-vs-phm
+  decision needs; see below.)
+- `:nil`.
+- `{:struct {field -> T}}` — a raw-get-safe map (Janet struct or record) whose
+  field `k` has type `(fields k)` or `:any` if absent. The degenerate
+  `{:struct {}}` is "a struct, fields unknown" and replaces today's
+  `:struct-map`.
+- `{:vec T}` — a vector whose elements have type `T`.
+- `{:set T}` — a set of `T`.
+- `:phm` — a persistent hash map (NOT raw-get-safe; distinct from `:struct`).
+- `{:fn {:params [T...] :ret T}}` — a function (optional precision; the current
+  flat param/return inference is the zero-arity-detail version of this).
+- `:any` — the top. Anything not provably more specific.
+- `:bottom` (represented as the absence of a type / `nil` internally) — the
+  identity for join, used to seed the fixpoint.
+
+Types are immutable values comparable by structural equality, exactly like the
+current `{:vec ELEM}` representation, so they flow across the portable
+inference and the Janet orchestrator unchanged.
+
+### Join (least upper bound)
+
+```
+join(T, T)                         = T
+join(bottom, T)                    = T
+join({:struct a}, {:struct b})     = {:struct {k -> join(a[k]?:any, b[k]?:any) for k in keys(a) ∪ keys(b)}}
+join({:vec a}, {:vec b})           = {:vec join(a, b)}
+join({:set a}, {:set b})           = {:set join(a, b)}
+join(_, _)                         = :any        ; different constructors
+```
+
+Two struct types join field-wise; a field present in only one side becomes
+`:any` in the result (it might be absent, so a lookup of it is not provably
+typed). This is the standard record lattice.
+
+### Termination: depth cap
+
+Structural types of recursive data (a tree node that contains a tree node, a
+cons cell) would be infinite. To keep types finite and the inter-procedural
+fixpoint terminating, structural types are **depth-capped**: beyond a small
+depth `D` (proposed `D = 4`) a child type is `:any`. Construction and join both
+truncate at `D`. With the cap the lattice has finite height, so the monotone
+fixpoint converges. The ray tracer's shapes (vec3 inside ray inside hit-info)
+are depth 2 to 3, well inside the cap.
+
+## Inference rules
+
+Inference is a forward pass producing `[type node']` for each IR node (the
+existing shape), threaded with a local type environment and the
+inter-procedural state from Phase 1. The rules are uniform over the structural
+type:
+
+- **Literals.** `{:k v ...}` with constant scalar keys and struct-safe values
+  builds `{:struct {:k type(v) ...}}`; otherwise `:phm`. `[a b ...]` builds
+  `{:vec (join type(a) type(b) ...)}`. `#{...}` builds `{:set ...}`. Scalars
+  build their scalar tag. (The struct-vs-phm condition is the same as the back
+  end's: scalar keys, and every value provably non-nil and non-false.)
+- **Lookup returns the field type.** `(:k m)` / `(get m :k)` where
+  `m : {:struct fs}` returns `(fs :k)` or `:any`. This is the single rule that
+  makes nesting work and that unifies field tracking with `:struct` tracking.
+- **Indexing returns the element type.** `(nth v i)` / `(v i)` where
+  `v : {:vec T}` returns `T`. `(first v)` / `(peek v)` likewise.
+- **Flow.** `let`/`loop` bind init types; `if` joins the branch types; `do`
+  takes the tail type. (As today.)
+- **Calls use signatures.** Every call result type comes from the callee's
+  signature: core fns from a fixed signature table (below), user fns from the
+  inter-procedural fixpoint's inferred signature.
+
+The Phase 1 inter-procedural fixpoint, recompile, escape gate, and closed-world
+assumption (RFC to follow / jolt-767) are unchanged. They now propagate
+structural types instead of flat tags.
+
+## Core function signatures
+
+The current special cases (`truthy-ret-fns`, `vector-ret-fns`, `elem-fns`,
+`hof-table`, and the `conj`/`range`/`reduce`/`mapv` branches) collapse into one
+table of **type schemes**, possibly parametric:
+
+```
+inc, dec, +, -, *, /, mod, ...   : (... :num) -> :num
+count                            : (Coll) -> :num
+nth        : ∀T. ({:vec T}, :num) -> T          (3-arg adds a default: -> join(T, default))
+get        : ∀T. ({:struct fs}, :k) -> (fs :k)  ; const key
+first,peek : ∀T. ({:vec T}) -> T
+conj       : ∀T. ({:vec T}, x) -> {:vec join(T, type(x))}
+assoc      : ({:struct fs}, :k, v) -> {:struct (assoc fs :k type(v))}   ; const key
+vec, mapv  : ... -> {:vec ...}
+range      : (...) -> {:vec :num}
+rand-nth   : ∀T. ({:vec T}) -> T
+map, filter, mapv, filterv, reduce, ...        ; see HOFs
+```
+
+Parametric schemes (the `∀T`) are where polymorphism actually matters, and they
+give the element/field propagation for free. **Higher-order functions are just
+schemes whose parameter is itself a function type**: `reduce`'s scheme says its
+function argument is `(Acc, Elem) -> Acc` applied to the collection's element
+type, so the closure's element parameter is typed by applying the scheme,
+replacing the hand-written `hof-table`.
+
+## Hints as seeds
+
+`^:struct x` seeds `x : {:struct {}}` (a struct, fields unknown) at a unit
+boundary the inference cannot see across. A future extension could allow a shape
+hint `^{:r :num :g :num :b :num}` to seed field types, but once inference is
+structural this is rarely needed; the hint stays the escape hatch for genuinely
+dynamic boundaries, exactly as today.
+
+## Soundness
+
+Unchanged in spirit from the current system: a concrete type is assigned only
+when proven (a literal genuinely has those fields; a fn provably returns that
+shape), and everything unprovable is `:any`, which keeps the dynamic guard. A
+wrong specialization is therefore impossible. The inter-procedural part keeps
+the closed-world (optimization-mode) assumption already adopted, which is sound
+under whole-program / source-distribution compilation.
+
+## Relationship to Hindley-Milner and soft typing
+
+This is HM-shaped with two deliberate departures, which is the textbook
+definition of **soft typing** (Wright and Cartwright, "A Practical Soft Type
+System for Scheme", 1997 — HM extended with union types and a dynamic type).
+
+Taken from HM:
+
+- The **structural type language** (records, vectors, functions as type
+  constructors). This is the "tree of types".
+- **Constraint propagation** and **type schemes** for the core library (the
+  `∀T` signatures). That parametric polymorphism is exactly what HM provides,
+  and it is where it matters (generic collection functions like `nth`,
+  `reduce`, `map`).
+
+Changed, on purpose:
+
+- Replace "unify or **fail**" with "**join over a lattice whose top is `:any`**".
+  The inference never rejects a program; an unprovable spot becomes `:any` and
+  keeps the runtime guard. This is the "fall back to dynamic when in doubt"
+  policy made principled.
+- **Monovariant** for user functions (the inter-procedural fixpoint plus
+  inlining cover the practical polymorphism); parametric schemes are kept only
+  for core functions.
+
+So: HM structural types and constraint propagation and core-fn schemes, solved
+by lattice join with a dynamic top instead of unification-or-fail. Other AOT
+inferencers for dynamic languages do the whole-program version of the same
+thing (RPython's annotator, Crystal's global inference, Shed Skin), all with a
+union/dynamic fallback.
+
+## Implementation and migration
+
+This is a refactor that **simplifies** the current code: it deletes the ad-hoc
+tag soup and the per-op special cases and replaces them with one recursive type
+plus a signature table.
+
+1. Define the structural type, `join`, the depth cap, and the predicates
+   (`struct-safe?`, `field-type`, `elem-type`) in `jolt.passes`.
+2. Rewrite `infer` so each op produces/consumes structural types: literals
+   build shapes; `(:k m)` returns the field type; calls consult the signature
+   table.
+3. Move the core-fn knowledge into a signature table (subsumes the existing
+   tables and HOF handling).
+4. The back end keeps reading the use-site type to specialize (guard drop for
+   `{:struct}`, `pv-count`/`pv-nth` for `{:vec}`), now uniformly.
+5. Keep the Phase 1 fixpoint, recompile, escape gate, and triggering as is; they
+   propagate structural types.
+
+The phases land incrementally behind the same optimization-mode gate, each
+verified against conformance (three modes), the full test gate, and the
+ray-tracer benchmark, exactly as the current phases were.
+
+## Design problems and open questions
+
+- **Recursion / termination.** Handled by the depth cap (`D = 4`). Open
+  question: is a fixed cap better than proper recursive (mu) types? A cap is
+  simpler and sound; mu-types are more precise but add complexity. Proposed:
+  start with the cap.
+- **Compile-time cost.** Structural types are larger and the fixpoint does more
+  work. Mitigations: the depth cap bounds type size; inference runs only in
+  optimization mode; the fixpoint iteration count stays bounded. Needs
+  measurement on a large namespace (clojure.core itself) to confirm acceptable.
+- **Heterogeneous data.** `[1 "a"]` joins to `{:vec :any}`; a map whose field
+  varies across branches joins that field to `:any`. Correct degradation, not a
+  problem, but worth stating.
+- **Non-constant keys.** `(assoc m k v)` / `(:k m)` with a non-constant `k`
+  cannot track a specific field; the result degrades to `{:struct {}}` or
+  `:phm` as appropriate. Field tracking only applies to constant scalar keys.
+- **`false`/`nil` field values.** A map literal is `{:struct ...}` only when
+  every value is provably non-nil and non-false (the back end stores such maps
+  as a phm). The `:nonnil` tag (or a per-type "provably truthy" predicate) is
+  what the literal rule needs; this must be carried correctly or struct
+  inference is unsound.
+- **Function-type precision.** `{:fn ...}` is optional. The current flat
+  param/return inference is enough for the collection-specialization goal;
+  full function types matter more for the type-checker (RFC 0006) and could be
+  deferred.
+- **Closed-world boundary.** Inherited from Phase 1: param/return inference
+  assumes the compiled unit is the whole program. Documented there; unchanged.

docs/rfc/0006-success-type-checking.md

@@ -0,0 +1,215 @@
+# RFC 0006 — Compile-time detection of provably-wrong code (success typing)
+
+- **Status**: Draft
+- **Champions**: jolt maintainers
+- **Created**: 2026-06-13
+- **Depends on**: RFC 0005 (structural collection-type inference)
+
+## Summary
+
+Reuse the structural type inference of RFC 0005 as a **loose type checker**: at
+compile time, flag code that is *provably* wrong, accept everything that is
+merely ambiguous, and never produce a false positive. Concretely, when an
+expression's inferred type is concrete and the operation applied to it would
+throw at runtime for that type (for example passing a string where a function
+only ever operates on numbers), report a clear compile-time error pointing at
+the offending form, with the inferred type and what was expected. When the type
+is `:any`, a union that includes a valid case, or beyond the inference's depth
+cap, accept it silently. This is **success typing** (the discipline behind
+Erlang's Dialyzer), applied to jolt for free on top of the inference we already
+need for optimization.
+
+## Motivation
+
+Once the compiler tracks concrete types for many values (RFC 0005), it can see
+some programs that cannot possibly be correct: `(inc "x")`, `(first 5)`,
+`(count :k)`, `(/ 1 "two")`. Today these compile and fail at runtime, often far
+from the cause. Reporting them at compile time, with a precise location and
+message, turns a class of runtime crashes into immediate, actionable feedback,
+at no extra inference cost.
+
+The design constraint the user set is the right one and is exactly success
+typing's contract: **accept ambiguous cases, reject only provably-wrong ones.**
+A checker that never lies about errors is one developers trust and that does not
+get in the way of correct-but-untypeable dynamic code.
+
+## Principle: success typing, never a false positive
+
+Success typing (Lindahl and Sagonas, "Practical Type Inference Based on Success
+Typings", 2006; the basis of Dialyzer) inverts the usual type-checker stance.
+A normal checker accepts only what it can prove correct and rejects the rest
+(false positives on dynamic code). A success typer accepts everything that
+*could* be correct and rejects only what *cannot* be correct under any
+execution. It is sound for **rejection**: if it reports an error, the code is
+genuinely wrong. It is intentionally incomplete: it misses errors it cannot
+prove. That is the correct trade for a dynamic language, and it matches the
+user's "accept ambiguous, reject provably wrong".
+
+Mapped onto jolt:
+
+- The inference assigns a value a concrete type only when it can prove it
+  (RFC 0005). Unprovable is `:any`.
+- A use site is reported **iff** the argument's inferred type is concrete and
+  lies entirely outside the operation's accepted domain, where the operation
+  *throws* on that domain (not merely returns a benign default).
+- `:any`, a depth-capped child, or a union that includes an accepted type is
+  **never** reported.
+
+## What "provably wrong" means
+
+The checker needs, per operation it understands, an **error domain**: the set
+of argument types for which the operation throws at runtime. This is narrower
+than "the types it is documented to accept", because Clojure is lenient in many
+places and flagging a benign case would be a false positive:
+
+- `(get 5 :k)` returns `nil`, it does not throw. NOT reported.
+- `(:k 5)` returns `nil`. NOT reported.
+- `(count 5)` throws ("count not supported on number"). Reported when the
+  argument is provably a non-countable scalar.
+- `(first 5)` throws (not seqable). Reported for a provably non-seqable scalar.
+- `(inc "x")`, `(+ 1 "x")` throw. Reported when an argument is provably a
+  non-number (`:str`, `:kw`, `:struct`, `:vec`, ...).
+- `(nth 5 0)` throws. Reported for a provably non-indexable scalar.
+
+So the checker ships a curated table of the clearest throwing operations with
+their error domains. It starts small (arithmetic on non-numbers, seq/`count`/
+`nth`/`first` on non-seqables) and grows conservatively. Anything not in the
+table is not checked, which is safe (no false positive).
+
+A use site is reported only when:
+
+1. the argument's inferred type `T` is concrete (not `:any`, not a union that
+   includes an accepted type, not truncated by the depth cap), and
+2. `T` is in the operation's error domain (the operation provably throws on `T`).
+
+## Examples
+
+```clojure
+(inc "x")                 ; ERROR: inc expects a number, got a string
+(let [n "x"] (inc n))     ; ERROR: same, n inferred :str
+(count :foo)              ; ERROR: count not supported on :kw
+(first 42)                ; ERROR: 42 is not seqable
+(:k 5)                    ; accepted (returns nil, not an error)
+(inc (rand-nth coll))     ; accepted if the element type is :any/unknown
+(inc (if c 1 "x"))        ; accepted: union {:num, :str} includes :num (ambiguous)
+(defn f [n] (inc n)) ...  ; if f is ALWAYS called with strings in-unit, ERROR at the call;
+                          ;   if its callers are unknown/varied, accepted
+```
+
+## Error reporting
+
+A reported error includes:
+
+- the source location (`file:line:col`) of the offending form;
+- the operation and the parameter position;
+- the inferred type of the argument, rendered readably (`:str`,
+  `{:struct {:r :num}}`, `{:vec :any}`);
+- what the operation requires (`a number`, `a seqable`).
+
+Example:
+
+```
+type error at scene.clj:42:18
+  (inc total) — `inc` requires a number, but `total` is a string
+```
+
+Errors are attributed to the form the user wrote. For macro-expanded code, the
+checker reports at the original form's recorded position (the loader already
+tracks `:error-pos`), never at synthesized internals.
+
+## Strictness levels
+
+A single env/compile flag controls behavior, defaulting to non-breaking:
+
+- **off** — no checking (default for now).
+- **warn** — report to stderr, do not fail compilation. The recommended rollout
+  default once the table is trusted.
+- **error** — fail compilation on a provable type error. Opt-in for CI / strict
+  builds.
+
+Because the checker only fires on provable errors, even `error` mode cannot
+break a correct program: a correct program has no provable type errors to
+report. (A correct-but-untypeable program is simply not reported, since its
+types degrade to `:any`.)
+
+## Soundness of rejection (no false positives)
+
+The whole value of this feature is that a reported error is real. The
+guarantees:
+
+- The inference assigns concrete types only when provable (RFC 0005). So a
+  concrete `T` at a use site is a genuine lower bound on what flows there in the
+  analyzed world.
+- The error-domain table lists only operations that genuinely throw on the
+  listed types, verified against the runtime.
+- Ambiguity is always accepted: `:any`, unions containing an accepted type, and
+  depth-capped children are never reported.
+
+Two boundaries need care and bound where the checker is allowed to fire:
+
+- **Closed-world / redefinition.** Inter-procedural argument types assume the
+  compiled unit is the whole program (inherited from RFC 0005). For the checker,
+  this means a reported error on a *user* function's parameter is only as sound
+  as that assumption. The conservative initial policy: only report against
+  **core-function** error domains (stable, not redefinable) and against types
+  derived without crossing an open boundary. Reporting against inferred user-fn
+  signatures is a later, opt-in escalation.
+- **Macros / generated code.** Check post-expansion IR but report at the user's
+  source location, and suppress reports inside expansions the user did not
+  write (or attribute them to the macro call site).
+
+## Relationship to other systems
+
+- **Dialyzer / success typing** (Erlang): the direct model — sound for
+  rejection, no false positives, accepts the ambiguous.
+- **Typed Clojure / core.typed**: opt-in *sound* gradual typing that rejects
+  what it cannot prove correct; the opposite trade (false positives on dynamic
+  code), which is why we do not follow it.
+- **clj-kondo**: a popular Clojure linter that flags some obvious type misuses
+  syntactically; this RFC subsumes the type-driven subset with inference-backed
+  precision and no false positives.
+
+## Implementation
+
+The checker is a thin pass over the same inference results:
+
+1. After (or during) inference, walk the IR. At each call to an operation in
+   the error-domain table, look at the inferred type of each checked argument.
+2. If concrete and in the error domain, record a diagnostic with location, the
+   inferred type, and the expected domain.
+3. Emit diagnostics per the strictness level.
+
+It adds no new inference; it consumes RFC 0005's types and a small curated
+table. It can ship after RFC 0005 lands, starting in `warn` mode with the
+smallest high-confidence table (arithmetic and seq/count/nth/first), and grow.
+
+## Design problems and open questions
+
+- **Curating the error domain.** The table must list only genuinely-throwing
+  cases. Getting it wrong (listing a lenient op) yields false positives, which
+  destroys trust. Mitigation: start tiny, test each entry against the runtime,
+  grow slowly. Open question: derive the table from the same machinery the
+  runtime uses, to avoid drift?
+- **Unions.** Today the inference joins to `:any` rather than forming unions
+  (`{:num | :str}`). Precise success typing wants unions (report only when
+  *every* member is in the error domain). Open question: add a small bounded
+  union type to RFC 0005's lattice, or keep `:any` and lose some precision (more
+  conservative, fewer reports, still no false positives)? Proposed: start with
+  `:any` (conservative), add unions if too many real errors are missed.
+- **User-function signatures.** Reporting against inferred user-fn domains is
+  more powerful but rests on the closed-world assumption and on the inferred
+  signature being a true requirement. Proposed: core fns first; user fns behind
+  an explicit opt-in.
+- **Negative/never types.** Some "provably wrong" cases are about a value being
+  the wrong arity or a fn vs a non-fn (calling a non-function). Worth including
+  the clear ones (calling a `:num` as a function) since the inference already
+  knows function-ness.
+- **Position vs intent.** Reporting at the right source location through
+  inlining and macro expansion needs the position metadata to survive the
+  passes. The loader tracks `:error-pos`; the IR may need to carry form
+  positions for precise column reporting.
+- **Interaction with the optimization gate.** The inference currently runs only
+  in optimization mode. The checker is valuable in normal builds too, so the
+  inference (at least its intra-procedural, sound-without-closed-world part)
+  may need to run for checking even when specialization is off. Open question:
+  decouple "run inference for checking" from "specialize from inference".