Are there inference systems out there smart enough to know that line 5 can't fail?

infer_this.lua

function foo(tbl)
   local var: string? = tbl.field -- string or nil
   local function f(x)
      print(x .. var) -- var must be string!
   end
   if type(var) == "string" then
      f("hello, ") -- f is only called where var is known to be string
   end
end

For traditional type inference (based on solving constraints among types), no. Type inference based on flow analysis for sets of abstract values is able to do that, but has its own issues. A recent example of this approach is http://cs.brown.edu/~sk/Publications/Papers/Published/gsk-flow-typing-theory/ (and maybe Facebook Flow, the documentation is sparse on how it works, and I haven't read the source).

If you just want your example to compile, you can lift "var" to be a parameter of f, with type string. :-)

I am not at all certain that you need flow typing, but it does look cool. Here's another link: http://whiley.org/guide/typing/flow-typing/

I think Benjamin Pierce calls the control flow construct for destructing a sum type "case". http://www.cis.upenn.edu/~bcpierce/sf/current/MoreStlc.html

If you were willing to do the lambda lifting transformation to get into first-order form, and also recognize "if type(var) == " as a kind of "case" statement, it would be simply typable, no?