As a side note, you should check out Erlang's static checker, Dialyzer. It implements a complete (i.e. no-false-positives) type system, as opposed to a sound (i.e. no-false-negatives) type system (e.g. H-M and friends). It pretty much eliminates the need to make any predictions about what the type checker will say, as it will only complain if your program can provably crash due to a type error.
Of course this still permits the possibility of type errors, but in practice it works fairly well, and does not constrain the programmer.