That would be an interesting tool.

Run a program while it is instrumented. The tool figures out what every type seems to be. Then goes back through the program and tries to prove that those types are correct.

It could then automatically annotate large chunks of code in a way that lets them run faster and will produce a warning if an unexpected type makes its way in in a future iteration. (An unexpected type, of course, being either a bug or a likely candidate for something that might expose latent bugs.)