I designed and built a statically-typed F-Expr LISP for my thesis, using some partial AST evaluation to trace and ensure every value had at least an initial value, and from that, type inference.

So it looked like:

    (define fib
      (lambda (n)
        (let loop ((a 0) (b 1) (n n))
          (if (= n 0) a
          (loop b (+ a b) (- n 1)))))

Which would do nothing by itself, and be eliminated as dead code unless called.

If we called it with:

    (fib 10)

It would expand, after the macro stage, to:

    (define fib
      ((Type/Number lambda) ((Type/Number n))
        (let loop (((Type/Number a) 0) ((Type/Number b) 1) (n n))
          (if (= n 0) a
          (loop b (+ a b) (- n 1)))))

If a value couldn't be inferred after ensuring the validity of the AST, it was supposed to error out with some helpful messages, but tracing the entire AST forward and back repeatedly always managed to type every value that was at least initialised, and if not, eliminate it as dead code.

Tradeoffs:

Compiling can be very lengthy, and it would be theoretically possible to write a program that would take ridiculous times to compile.

Once compiled, we can ensure type safety, and in the underlying implementation, JIT everything for a decent amount of speed.

Edit: Forgot to add lambda return type. Then added it in the wrong place.