haskell: reject untypeable programs — hk-typecheck + hk-run-typed (+9 tests, 464/464)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

lib/haskell/eval.sx

@@ -790,3 +790,25 @@ negate x = 0 - x
   (fn
     (src)
     (hk-deep-force (hk-eval (hk-core-expr src) (hk-dict-copy hk-env0)))))
+
+(define
+  hk-typecheck
+  (fn
+    (prog)
+    (let
+      ((results (hk-infer-prog prog (hk-type-env0))))
+      (let
+        ((errors (filter (fn (r) (= (first r) "err")) results)))
+        (when (not (empty? errors)) (raise (nth (first errors) 1)))))))
+
+(define
+  hk-run-typed
+  (fn
+    (src)
+    (let
+      ((prog (hk-core src)))
+      (begin
+        (hk-typecheck prog)
+        (let
+          ((env (hk-eval-program prog)))
+          (cond ((has-key? env "main") (get env "main")) (:else env)))))))

lib/haskell/infer.sx

@@ -525,33 +525,37 @@
   hk-infer-decl
   (fn
     (env decl)
-    (let ((tag (first decl)))
+    (let
+      ((tag (first decl)))
       (cond
         ((= tag "fun-clause")
-         (let ((name (nth decl 1))
-               (pats (nth decl 2))
-               (body (nth decl 3)))
-           (let ((rhs (if (empty? pats) body (list "lambda" pats body))))
-             (guard
-               (e (#t (list "err" (str "in '" name "': " e))))
-               (begin
-                 (hk-reset-fresh)
-                 (let ((r (hk-w env rhs)))
-                   (list "ok" name
-                         (hk-type->str (hk-subst-apply (first r) (nth r 1))))))))))
+          (let
+            ((name (nth decl 1)) (pats (nth decl 2)) (body (nth decl 3)))
+            (let
+              ((rhs (if (empty? pats) body (list "lambda" pats body))))
+              (guard
+                (e (#t (list "err" (str "in '" name "': " e))))
+                (begin
+                  (hk-reset-fresh)
+                  (let
+                    ((r (hk-w env rhs)))
+                    (let
+                      ((final-type (hk-subst-apply (first r) (nth r 1))))
+                      (list "ok" name (hk-type->str final-type) final-type))))))))
         ((or (= tag "bind") (= tag "pat-bind"))
-         (let ((pat  (nth decl 1))
-               (body (nth decl 2)))
-           (let ((label (if (and (list? pat) (= (first pat) "p-var"))
-                          (nth pat 1)
-                          "<binding>")))
-             (guard
-               (e (#t (list "err" (str "in '" label "': " e))))
-               (begin
-                 (hk-reset-fresh)
-                 (let ((r (hk-w env body)))
-                   (list "ok" label
-                         (hk-type->str (hk-subst-apply (first r) (nth r 1))))))))))
+          (let
+            ((pat (nth decl 1)) (body (nth decl 2)))
+            (let
+              ((label (if (and (list? pat) (= (first pat) "p-var")) (nth pat 1) "<binding>")))
+              (guard
+                (e (#t (list "err" (str "in '" label "': " e))))
+                (begin
+                  (hk-reset-fresh)
+                  (let
+                    ((r (hk-w env body)))
+                    (let
+                      ((final-type (hk-subst-apply (first r) (nth r 1))))
+                      (list "ok" label (hk-type->str final-type) final-type))))))))
         (:else nil)))))
 
 ;; hk-infer-prog : program-ast × env → list of ("ok" name type) | ("err" msg)
@@ -560,18 +564,20 @@
   hk-infer-prog
   (fn
     (prog env)
-    (let ((decls (cond
-                   ((and (list? prog) (= (first prog) "program"))
-                    (nth prog 1))
-                   ((and (list? prog) (= (first prog) "module"))
-                    (nth prog 3))
-                   (:else (list))))
-          (results (list)))
+    (let
+      ((decls (cond ((and (list? prog) (= (first prog) "program")) (nth prog 1)) ((and (list? prog) (= (first prog) "module")) (nth prog 3)) (:else (list))))
+        (results (list)))
       (for-each
-        (fn (d)
-          (let ((r (hk-infer-decl env d)))
-            (when (not (nil? r))
-              (append! results r))))
+        (fn
+          (d)
+          (let
+            ((r (hk-infer-decl env d)))
+            (when
+              (not (nil? r))
+              (append! results r)
+              (when
+                (= (first r) "ok")
+                (dict-set! env (nth r 1) (nth r 3))))))
         decls)
       results)))
 

lib/haskell/test.sh

@@ -42,9 +42,9 @@ FAILED_FILES=()
 
 for FILE in "${FILES[@]}"; do
   [ -f "$FILE" ] || { echo "skip $FILE (not found)"; continue; }
-  # Load infer.sx only for infer test files (it adds ~6s overhead).
+  # Load infer.sx only for infer/typecheck test files (it adds ~6s overhead).
   INFER_LOAD=""
-  case "$FILE" in *infer*) INFER_LOAD='(load "lib/haskell/infer.sx")' ;; esac
+  case "$FILE" in *infer*|*typecheck*) INFER_LOAD='(load "lib/haskell/infer.sx")' ;; esac
   TMPFILE=$(mktemp)
   cat > "$TMPFILE" <<EPOCHS
 (epoch 1)

lib/haskell/tests/typecheck.sx

@@ -0,0 +1,44 @@
+;; typecheck.sx — tests for hk-typecheck / hk-run-typed.
+;; Verifies that untypeable programs are rejected and well-typed programs pass.
+
+(define hk-str-has? (fn (s sub) (>= (index-of s sub) 0)))
+
+;; Helper: expect a type error containing `sub`
+(define
+  hk-tc-err
+  (fn
+    (label src sub)
+    (hk-test
+      label
+      (guard
+        (e (#t (hk-str-has? e sub)))
+        (begin (hk-run-typed src) false))
+      true)))
+
+;; ─── Valid programs pass through ─────────────────────────────────────────────
+(hk-test "typed ok: simple arithmetic" (hk-run-typed "main = 1 + 2") 3)
+
+(hk-test "typed ok: boolean" (hk-run-typed "main = True") (list "True"))
+
+(hk-test "typed ok: let binding" (hk-run-typed "main = let x = 1 in x + 2") 3)
+
+(hk-test
+  "typed ok: two independent fns"
+  (hk-run-typed "f x = x + 1\nmain = f 5")
+  6)
+
+;; ─── Untypeable programs are rejected ────────────────────────────────────────
+;; Adding Int and Bool is a unification failure.
+(hk-tc-err "reject: Int + Bool mentions Int" "main = 1 + True" "Int")
+(hk-tc-err "reject: Int + Bool mentions Bool" "main = 1 + True" "Bool")
+
+;; Condition of if must be Bool.
+(hk-tc-err "reject: if non-bool condition" "main = if 1 then 2 else 3" "Bool")
+
+;; Unbound variable.
+(hk-tc-err "reject: unbound variable" "main = unknownVar + 1" "unknownVar")
+
+;; Function body type error: applying non-function.
+(hk-tc-err "reject: apply non-function" "f x = 1 x" "Int")
+
+{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail}

plans/haskell-on-sx.md

@@ -93,7 +93,7 @@ Key mappings:
 ### Phase 4 — Hindley-Milner inference
 - [x] Algorithm W: unification + type schemes + generalisation + instantiation
 - [x] Report type errors with meaningful positions
-- [ ] Reject untypeable programs that phase 3 was accepting
+- [x] Reject untypeable programs that phase 3 was accepting
 - [ ] Type-sig checking: user writes `f :: Int -> Int`; verify
 - [ ] Let-polymorphism
 - [ ] Unit tests: inference for 50+ expressions
@@ -114,6 +114,17 @@ Key mappings:
 
 _Newest first._
 
+- **2026-05-05** — Phase 4 reject untypeable programs. `hk-typecheck` runs
+  `hk-infer-prog` on a program AST and raises the first type error found.
+  `hk-run-typed` is a drop-in for `hk-run` that gates evaluation on a
+  successful type check. `hk-infer-decl` now returns a 4th element (raw type
+  value); `hk-infer-prog` propagates inferred types into the running type env
+  so multi-function programs (`f x = x+1\ng y = f y+2`) infer correctly.
+  test.sh extended to load infer.sx for `*typecheck*` files.
+  9 new tests in `tests/typecheck.sx`: 4 valid programs pass through, 5
+  invalid programs are rejected (Int+Bool, non-Bool if condition, unbound var,
+  apply non-function). 464/464 green.
+
 - **2026-05-05** — Phase 4 type error reporting. `hk-expr->brief` converts any AST
   node to a short human-readable string for error messages (handles var/con/int/float/
   str/char/bool/app/op/if/let/lambda/tuple/list/loc). `loc` nodes in `hk-w` delegate