The dialyzer method of typing is success typing, it only ensures that what you type is sensible and logical, but it falls back to assuming the programmer knows what they are doing when it hits something that it cannot figure out. This is a perfectly reasonable typing system, however it has absolutely zero/zilch/nil/none/etc of the capabilities of, say, an HM typing system, which allows you to do type specific calls, like for example:
Right now you have to do this, because if you do
f(x) then it does a direct function call because it does not not know what ‘f’ should be, like if it is a string then it knows it could instead call a direct version, but it does not know, hence why Elixir does a LISP-2 style system where functions and bindings are different scopes to work around it. If, however, the system itself was typed well enough to know that f is a binding and it binds to a function type then you could just do
f(x) and it would call the binding if the binding was a function or a direct call if it were not, thus unifying the syntax and scopes now that you can safely do so thanks to the type information.
Plus a lot more like conditional branching at compile-time based on types, conditional compile-time dispatch (without the ‘virtual call’ of anonymous functions or the testing of the type) based on type, etc… etc…
Alpaca is more traditionally HM, but they are making a couple odd decisions in my opinion… ^.^;