Fine, but there is surprisingly no mention of Lisp in the related work, which defines a COMPILE function in its specification. In a language where the compiler is part in your runtime, type checking is equally available at different execution times. I mean, when I connect to a running instance of SBCL (Common Lisp) to compile my programs, that's exactly what happens: static-type analysis at runtime. Let's say I define a function which builds a function and compiles it:

      CL-USER> (defun foo (x) (compile () `(lambda (u) (aref ,x u))))
      FOO

Call it with an array:

      CL-USER> (foo #(2 3 2))
      #<FUNCTION (LAMBDA (U)) {100B3C610B}>
      NIL
      NIL

The resulting closure allows to access elements of that array:

      CL-USER> (funcall * 0)
      2

Call FOO again, with a bad input:

      CL-USER> (foo 332)
      ; in: LAMBDA (U)
      ;     (AREF 332 U)
      ; 
      ; note: deleting unreachable code
      ; 
      ; caught WARNING:
      ;   Constant 332 conflicts with its asserted type ARRAY.
      ;   See also:
      ;     The SBCL Manual, Node "Handling of Types"
      ; 
      ; compilation unit finished
      ;   caught 1 WARNING condition
      ;   printed 1 note
      #<FUNCTION (LAMBDA (U)) {100B41E16B}>
      T
      T

COMPILE reports a type error (an exception that I could handle if needed).