It's not possible, because functions, pattern matching, guards, typespecs and success typing are fundamentally incommensurable: each specifies and/or enforces a subset of the other, they are all useful in their own way, but not isomorphic.

Formal attempts have repeatedly failed, even when they exclude message passing, which is the most difficult (and most useful) aspect. If Wadler cannot do it, I'm sure I (or you) cannot.

A typesafe concurrent language is possible, but only a new language layer on top of E/E and the BEAM.