feat: success-type checker (RFC 0006) — flag provably-wrong core calls

Reuse the structural inference from RFC 0005 as a loose type checker. It reports
a core-fn call only when an argument's inferred type is concrete and lies in
that op's throwing error domain, and accepts everything ambiguous (:any, a
union that joined to :any, :truthy). By construction it never produces a false
positive: a correct program has nothing to report even in error mode.

The curated error-domain table starts with the clearest throwing cases:
arithmetic on a provable non-number, and count/first/rest/next/seq/nth on a
provable non-seqable scalar. Lenient operations like (get 5 :k) and (:k 5),
which return nil rather than throw, are deliberately not listed.

Checking is decoupled from specialization: it runs whenever JOLT_TYPE_CHECK is
warn or error, regardless of :inline?, reading the knob at compile time so no
rebuild is needed. warn prints to stderr, error fails the form's compilation,
off (the default) skips it entirely. Core init stays clean under the flag.

jolt-y3b

jolt-core/jolt/passes.clj

@@ -794,6 +794,7 @@
 (def ^:private rtenv-box (atom {}))   ;; "ns/name" -> inferred return type
 (def ^:private calls-box (atom []))   ;; collected [ "ns/name" [arg-types...] ]
 (def ^:private escapes-box (atom #{})) ;; var-keys used as a VALUE (not a call head)
+(def ^:private diag-box (atom []))    ;; success-type-check diagnostics (RFC 0006)
 ;; jolt-d6u: a var reference's VALUE type — a fn var is :truthy (non-nil), a def
 ;; var carries its inferred init type (e.g. a color table -> {:vec :struct-map}).
 ;; The orchestrator populates this from sealed (opt-mode) cell roots + def inits.
@@ -1034,6 +1035,121 @@
 
 (defn- infer-top [node] (nth (infer node {}) 1))
 
+;; ---------------------------------------------------------------------------
+;; Success-type checking (RFC 0006). Reuse the inference above as a loose type
+;; checker: flag a core-fn call ONLY when an argument's inferred type is
+;; concrete AND lies in that op's error domain (the op provably throws on it).
+;; Everything ambiguous — :any, :truthy (true/char/...), :nil — is accepted, so
+;; there are no false positives. The table is curated to genuinely-throwing
+;; cases; lenient ops ((get 5 :k) -> nil, (:k 5) -> nil) are NOT listed.
+
+;; concrete non-numbers: arithmetic provably throws on these.
+(defn- not-number? [t]
+  (or (= t :str) (= t :kw) (= t :phm)
+      (struct-type? t) (vec-type? t) (set-type? t)))
+
+;; concrete non-seqable scalars: seq/count/first/nth provably throw on these.
+;; (Strings and collections ARE seqable/countable; :truthy is ambiguous; :nil
+;; and :any are accepted.)
+(defn- not-seqable? [t] (or (= t :num) (= t :kw)))
+
+;; arithmetic / numeric ops: EVERY argument must be a number.
+(def ^:private num-ops
+  #{"+" "-" "*" "/" "inc" "dec" "mod" "rem" "quot" "min" "max" "abs"
+    "bit-and" "bit-or" "bit-xor" "bit-not" "bit-shift-left" "bit-shift-right"})
+;; seq/count/index ops: argument 0 must be seqable/countable.
+(def ^:private seq-ops #{"count" "first" "rest" "next" "seq" "nth"})
+
+(defn- type-name
+  "Render an inferred type for an error message."
+  [t]
+  (cond (struct-type? t) "a map"
+        (vec-type? t) "a vector"
+        (set-type? t) "a set"
+        (= t :str) "a string"
+        (= t :kw) "a keyword"
+        (= t :num) "a number"
+        (= t :phm) "a map"
+        :else (str t)))
+
+(defn- check-invoke
+  "If node is a core-op call whose argument type is provably in the error domain,
+  conj a diagnostic. arg-types is the vector of inferred argument types."
+  [cn args arg-types]
+  (cond
+    (contains? num-ops cn)
+    (reduce (fn [_ i]
+              (let [t (nth arg-types i)]
+                (when (not-number? t)
+                  (swap! diag-box conj
+                         {:op cn :argpos i :type (type-name t)
+                          :msg (str "`" cn "` requires a number, but argument "
+                                    (inc i) " is " (type-name t))})))
+              nil)
+            nil (range (count args)))
+    (and (contains? seq-ops cn) (> (count args) 0))
+    (let [t (nth arg-types 0)]
+      (when (not-seqable? t)
+        (swap! diag-box conj
+               {:op cn :argpos 0 :type (type-name t)
+                :msg (str "`" cn "` requires "
+                          (if (= cn "count") "a countable collection" "a seqable")
+                          ", but argument 1 is " (type-name t))})))
+    :else nil))
+
+(defn- check-walk
+  "Walk the IR, inferring argument types and recording diagnostics for
+  provably-wrong core-fn calls. Threads tenv through binders exactly like infer."
+  [node tenv]
+  (let [op (get node :op)]
+    (cond
+      (= op :invoke)
+      (let [fnode (get node :fn)
+            args (get node :args)
+            cn (when (and (= :var (get fnode :op)) (= "clojure.core" (get fnode :ns)))
+                 (get fnode :name))]
+        (when cn
+          (check-invoke cn args (mapv (fn [a] (nth (infer a tenv) 0)) args)))
+        (check-walk fnode tenv)
+        (reduce (fn [_ a] (check-walk a tenv) nil) nil args))
+      (= op :let)
+      (let [te (reduce (fn [e b]
+                         (check-walk (nth b 1) e)
+                         (assoc e (nth b 0) (nth (infer (nth b 1) e) 0)))
+                       tenv (get node :bindings))]
+        (check-walk (get node :body) te))
+      (= op :if)
+      (do (check-walk (get node :test) tenv)
+          (check-walk (get node :then) tenv)
+          (check-walk (get node :else) tenv))
+      (= op :do)
+      (do (reduce (fn [_ s] (check-walk s tenv) nil) nil (get node :statements))
+          (check-walk (get node :ret) tenv))
+      (= op :fn)
+      (reduce (fn [_ a]
+                (let [pe (reduce (fn [e p] (assoc e p :any)) tenv (get a :params))
+                      pe (if (get a :rest) (assoc pe (get a :rest) :any) pe)]
+                  (check-walk (get a :body) pe))
+                nil)
+              nil (get node :arities))
+      (= op :loop)
+      (do (reduce (fn [_ b] (check-walk (nth b 1) tenv) nil) nil (get node :bindings))
+          (check-walk (get node :body) tenv))
+      (= op :recur)
+      (reduce (fn [_ a] (check-walk a tenv) nil) nil (get node :args))
+      (= op :def) (check-walk (get node :init) tenv)
+      (= op :throw) (check-walk (get node :expr) tenv)
+      (= op :vector) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items))
+      (= op :set) (reduce (fn [_ x] (check-walk x tenv) nil) nil (get node :items))
+      (= op :map)
+      (reduce (fn [_ pr] (check-walk (nth pr 0) tenv) (check-walk (nth pr 1) tenv) nil)
+              nil (get node :pairs))
+      (= op :try)
+      (do (check-walk (get node :body) tenv)
+          (when (get node :catch-body) (check-walk (get node :catch-body) tenv))
+          (when (get node :finally) (check-walk (get node :finally) tenv)))
+      :else nil)))
+
 ;; --- Inter-procedural driver API (jolt-767) consumed by the back end --------
 (defn set-rtenv!
   "Install the current return-type estimates (a map \"ns/name\" -> type) used to
@@ -1053,6 +1169,16 @@
 (defn reset-escapes! [] (reset! escapes-box #{}))
 (defn collected-escapes [] (vec @escapes-box))
 
+(defn check-form
+  "Success-type check a single analyzed form (RFC 0006). Returns a vector of
+  diagnostics [{:op :argpos :type :msg} ...] for provably-wrong core-fn calls;
+  empty when nothing is provably wrong. Runs independently of specialization so
+  it is usable in normal builds (the decoupled checking path)."
+  [node]
+  (reset! diag-box [])
+  (check-walk node {})
+  (vec @diag-box))
+
 (defn infer-body
   "Type `body` under tenv (local-name -> type). Returns [ret-type node' calls],
   where calls is the [[\"ns/name\" [arg-types...]] ...] this body invokes (for

src/jolt/backend.janet

@@ -613,6 +613,27 @@
   [ctx]
   (build-compiler! ctx))
 
+(defn type-check!
+  "Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form
+  (absent during pre-passes bootstrap -> no-op), runs it protected so a checker
+  bug never breaks compilation, then reports each diagnostic per strictness:
+  `warn` prints to stderr, `error` throws (failing this form's compilation).
+  Because the checker only fires on PROVABLY-wrong code, a correct program has
+  nothing to report under either level."
+  [ctx ir strictness ns]
+  (def cf (ns-find (ctx-find-ns ctx "jolt.passes") "check-form"))
+  (when cf
+    (def r (protect ((var-get cf) ir)))
+    (when (r 0)
+      (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1)))
+      (when (and diags (> (length diags) 0))
+        (def loc (if ns (string ns) "?"))
+        (each d diags
+          (def msg (string "type error in " loc ": " (get d :msg)))
+          (if (= strictness "error")
+            (error msg)
+            (eprint "  " msg)))))))
+
 (defn analyze-form
   "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form,
   returning host-neutral IR."
@@ -645,14 +666,23 @@
   # Resolved lazily; absent during the pre-passes bootstrap window.
   (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES"))
             (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes")))
-  (if pv
-    (let [pr (protect ((var-get pv) (r 1) ctx))]
-      # the pass runs interpreted; a throw inside it unwinds past the
-      # interpreter's ns restores — put the compile ns back either way, or
-      # the REST of this compilation resolves in jolt.passes
-      (ctx-set-current-ns ctx saved-ns)
-      (if (pr 0) (pr 1) (r 1)))
-    (r 1)))
+  (def result
+    (if pv
+      (let [pr (protect ((var-get pv) (r 1) ctx))]
+        # the pass runs interpreted; a throw inside it unwinds past the
+        # interpreter's ns restores — put the compile ns back either way, or
+        # the REST of this compilation resolves in jolt.passes
+        (ctx-set-current-ns ctx saved-ns)
+        (if (pr 0) (pr 1) (r 1)))
+      (r 1)))
+  # Success-type check (RFC 0006), decoupled from specialization: runs whenever
+  # JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it
+  # needs no rebuild. The analyzed IR (r 1) carries no specialization; the
+  # checker does its own inference.
+  (def tc (os/getenv "JOLT_TYPE_CHECK"))
+  (when (and tc (not= tc "off") (not= tc "0"))
+    (type-check! ctx (r 1) tc saved-ns))
+  result)
 
 # The analyzer's deliberate punt signal — (uncompilable why) throws the string
 # "jolt/uncompilable: <why>". Anything else escaping the compile step is an

test/integration/type-check-test.janet

@@ -0,0 +1,57 @@
+# Success-type checking (RFC 0006, jolt-y3b). The structural inference of
+# RFC 0005, reused as a loose checker: flag a core-fn call ONLY when an argument
+# is PROVABLY the wrong type (concrete and in the op's throwing error domain).
+# Ambiguous cases (:any, unions, :truthy) are accepted — no false positives.
+(import ../../src/jolt/api :as api)
+(import ../../src/jolt/backend :as backend)
+(import ../../src/jolt/types :as types)
+(import ../../src/jolt/reader :as reader)
+
+(print "Success-type checking (jolt-y3b)...")
+
+(os/setenv "JOLT_DIRECT_LINK" "1")
+(def ctx (api/init {:compile? true}))
+(def pns (types/ctx-find-ns ctx "jolt.passes"))
+(def check (types/var-get (types/ns-find pns "check-form")))
+
+# diagnostics (a Janet tuple of diag structs) for a source form
+(defn diags [src]
+  (api/normalize-pvecs (check (backend/analyze-form ctx (reader/parse-string src)))))
+(defn nd [src] (length (diags src)))
+
+# --- provably wrong: REPORTED ------------------------------------------------
+(assert (= 1 (nd "(inc \"x\")")) "inc on a string")
+(assert (= 1 (nd "(+ 1 \"x\")")) "+ with a string arg")
+(assert (= 1 (nd "(count :foo)")) "count of a keyword")
+(assert (= 1 (nd "(count 5)")) "count of a number")
+(assert (= 1 (nd "(first 42)")) "first of a number")
+(assert (= 1 (nd "(nth :k 0)")) "nth of a keyword")
+(assert (= 1 (nd "(let [n \"x\"] (inc n))")) "inc on a let-bound string")
+(assert (= 1 (nd "(inc (count :k))")) "inner count of keyword reported (inc of :num is fine)")
+
+# --- ambiguous / lenient: ACCEPTED (no false positive) -----------------------
+(assert (= 0 (nd "(:k 5)")) "keyword lookup on a number returns nil, not an error")
+(assert (= 0 (nd "(get 5 :k)")) "get on a number returns nil, not an error")
+(assert (= 0 (nd "(fn [x] (inc x))")) "inc on an unknown (:any) param accepted")
+(assert (= 0 (nd "(fn [c] (inc (if c 1 \"x\")))")) "inc on a {:num | :str} branch -> :any, accepted")
+(assert (= 0 (nd "(count \"ab\")")) "count of a string is fine")
+(assert (= 0 (nd "(count [1 2 3])")) "count of a vector is fine")
+(assert (= 0 (nd "(first [1 2 3])")) "first of a vector is fine")
+(assert (= 0 (nd "(inc (count [1 2 3]))")) "count of vector + inc of :num both fine")
+(assert (= 0 (nd "(inc (first [1 2 3]))")) "first of vector -> :num, inc fine")
+
+# --- the diagnostic carries op + type + a message ----------------------------
+(def one (in (diags "(inc \"x\")") 0))
+(assert (= "inc" (get one :op)) "diagnostic names the op")
+(assert (string/find "number" (get one :msg)) "message says a number is required")
+
+# --- end-to-end: strictness drives compilation (decoupled from :inline?) -----
+# error mode aborts a provably-wrong form's compilation; a correct form compiles.
+(os/setenv "JOLT_TYPE_CHECK" "error")
+(assert (not (first (protect (api/eval-string ctx "(count :nope)"))))
+        "error mode aborts a provably-wrong form")
+(assert (first (protect (api/eval-string ctx "(count [1 2 3])")))
+        "error mode accepts a correct form")
+(os/setenv "JOLT_TYPE_CHECK" "off")
+
+(print "Success-type checking passed!")