;; 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-deep-force (hk-run-typed "main = 1 + 2")) 3)

(hk-test "typed ok: boolean"
  (hk-deep-force (hk-run-typed "main = True")) (list "True"))

(hk-test "typed ok: let binding"
  (hk-deep-force (hk-run-typed "main = let x = 1 in x + 2")) 3)

(hk-test
  "typed ok: two independent fns"
  (hk-deep-force (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")

(define prog-sig1 (hk-core "f :: Int -> Int\nf x = x + 1"))

(define prog-sig2 (hk-core "f :: Bool -> Bool\nf x = x + 1"))

(define prog-sig3 (hk-core "id :: a -> a\nid x = x"))

(hk-test
  "sig ok: Int->Int accepted"
  (first (nth (hk-infer-prog prog-sig1 (hk-type-env0)) 0))
  "ok")

(hk-test
  "sig fail: Bool->Bool rejected"
  (first (nth (hk-infer-prog prog-sig2 (hk-type-env0)) 0))
  "err")

(hk-test
  "sig fail: error mentions mismatch"
  (hk-str-has?
    (nth (nth (hk-infer-prog prog-sig2 (hk-type-env0)) 0) 1)
    "mismatch")
  true)

(hk-test
  "sig ok: polymorphic a->a accepted"
  (first (nth (hk-infer-prog prog-sig3 (hk-type-env0)) 0))
  "ok")

(hk-tc-err
  "run-typed sig fail: Bool declared, Int inferred"
  "main :: Bool\nmain = 1 + 2"
  "mismatch")

(hk-test
  "run-typed sig ok: Int declared matches"
  (hk-deep-force (hk-run-typed "main :: Int\nmain = 1 + 2"))
  3)

{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail}