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

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?