If you haven't already, you should see this paper from 2017 about sound gradual typing: https://www.cs.cornell.edu/~ross/publications/nomalive/nomalive-oopsla17

If you haven't already, you should see this paper from 2017 about sound gradual typing: https://www.cs.cornell.edu/~ross/publications/nomalive/nomalive-oopsla17-tr.pdf https://www.cs.cornell.edu/~ross/publications/nomalive/nomal... The performance and rigidity issues you mention are solvable. Although the research is pretty cutting-edge and not implemented in many programming languages yet.