As I said, there are infinite possible programs that cannot be type checked statically. This is derived from the halting theorem trivially - lambda(p) = if p.halts() then A() else B().
However, the intersection of programs I encounter in practice with the number of programs that can be statically checked is rather large.
However, the intersection of programs I encounter in practice with the number of programs that can be statically checked is rather large.