I'm somewhat wary of approaches like that. I feel like core.typed tried something similar (maybe McVeigh's approach does better inference of unannotated code?) and it's withering on the vine as far as I can tell. IIRC there's some theoretical hints that gradual typing from the direction of untyped to typed rather than the direction of typed to untyped is fundamentally less ergonomic (some type inference stuff becomes undecidable in the former case and remains decidable in the latter and the same occurs for some varieties of type checking). Of course theory doesn't always mean you won't have practically good solutions (since when has the halting problem stopped people from making static analyzers?), but they provide some hints you'll be swimming upstream.
My limited experience with static analyzers is that you also end up with unpredictable breakages of the form "hmmm... so if I leave the variable here my static checker tells me I'm wrong, but as soon as I move the variable down one level of scope it just silently fails to see the error."
Regardless I haven't used Dialyzer myself and I have a good idea of the very very finite number of minutes I've spent with Erlang proper (as opposed to just reading about it), so who knows. It'll be fun to see where this goes. Thanks for the link!
The really big innovation I'm personally waiting for is combining static types with image-based programming (e.g. Clojure's REPL) which seems like an open problem right now because it's pretty difficult to think about what static invariants can and can't be maintained when you can hot reload arbitrary code. That and better support for type-driven programming a la Idris. Working with the compiler in a pull-and-push method (which you can get a crude approximation of in Haskell with type holes and Hoogle and some program synthesis tools, but oh man if even the toolchain for that was mature that would be huge!) was as big a revelation for me as REPL-based programming in Clojure was.