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

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

(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".