;;;; The boundary in both directions, and the trap when a claim is wrong.
;;;;
;;;; Typed to dyn is implicit: take-dyn is called with an i64 and the boxing is
;;;; written nowhere. Dyn to typed is not: take-i64's parameter says i64, and
;;;; that annotation is the whole of why the unboxing is allowed to happen —
;;;; and the whole of why it may fail, which the last line of main proves by
;;;; handing it a float.
;;;;
;;;; A let carries no type in this language, so the annotation sites a dyn can
;;;; be unboxed at are the ones that do: a parameter, a return type, and a
;;;; global's declared type. All three are here.

(defvar seven i64 7)
(defvar boxed dyn 21)
;; The other direction at a global: a dyn initialiser meeting a written type.
(defvar unboxed i64 boxed)

(defn take-dyn [d dyn] dyn
  (+ d 100))

(defn take-i64 [n i64] i64
  (* n 2))

(defn identity-dyn [d] dyn d)

;; A dyn value answered at a written return type, which is the third site.
(defn as-i64 [d] i64 d)

(defn main [] ()
  ;; Typed in: the i64 is boxed at the call with nothing written.
  (print (take-dyn seven))
  (print "\n")
  ;; Dyn out: the parameter is typed, so the word is unboxed at the call.
  (print (take-i64 boxed))
  (print "\n")
  (print unboxed)
  (print "\n")
  (print (as-i64 (identity-dyn 5)))
  (print "\n")
  ;; And the claim that is wrong. The runtime owns the message.
  (print (take-i64 (identity-dyn 1.5)))
  (print "\n"))