Today at the 20th ACM SIGPLAN International Workshop on Erlang (Erlang 2021), a paper on Bidirectional Typing for Erlang was presented (pdf). There is also a GitHub repository with the prototype.
Personally I am intrigued. Requiring annotations for functions seems reasonable. I wonder if it would be possible to type check all of Erlang syntax this way (currently it’s a subset). Also since the paper mentions Core Erlang, maybe there would be a way to run the analysis on Elixir modules