I am wondering what would happen if you left out the addition of run-time checks, and performed only those static checks that the partial typing has enabled? (I guess that would make it unsound, but perhaps it is worth it.)<p>I would not be at all surprised to learn that little or no static checking is possible until quite a lot of typing has been completed. We see, however, that the performance lattice in the article shows (for that particular example) that the net cost begins falling after about half of the typing is completed. Is it valid to assume that this is a result of additional type information allowing static analysis to remove or simplify run-time checks? If so, we can also note that this is a net effect, so static analysis could be having some benefit earlier in the transformation.