; Iter 16d — `__unreachable__` as an explicit user-callable primitive.
; Type: forall a. a (lowered to LLVM `unreachable`).
;
; This fixture exercises `__unreachable__` in a value position that is
; statically unreachable but still type-checks: the impossible branch
; of an if. `safe_div(a, b)` returns `a / b` when `b != 0` and panics
; via `__unreachable__` otherwise. The driver only ever calls it with
; non-zero divisors, so the panic branch is never executed.
;
; The point of the fixture is the type-system + codegen surface:
; `__unreachable__` unifies against `Int` (the fn's return type) at
; the typechecker, and codegen lowers it to `unreachable` followed by
; the rest of the if's join machinery, which is sound because the
; surrounding if's `block_terminated` flag is honoured.
;
; Expected stdout (one per line): 4, 5.

(module unreachable_demo

  (fn safe_div
    (doc "a/b for b != 0; otherwise panic via __unreachable__.")
    (type (fn-type (params (own (con Int)) (own (con Int))) (ret (own (con Int)))))
    (params a b)
    (body
      (if (app eq b 0)
          __unreachable__
          (app / a b))))

  (fn main
    (doc "Drive safe_div with non-zero divisors. Expected: 4, 5.")
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (seq (seq (app print (app safe_div 8 2)) (do io/print_str "\n"))
           (seq (app print (app safe_div 15 3)) (do io/print_str "\n"))))))