I suspect it might be fruitful to do static analysis for constraints, with type identity as just one attribute. While inferring that X is an int is useful, inferring that it's an int which is always positive and less than 256 would allow a lot of other optimizations. Even if an inference engine can't completely prove something is always a (string * int list) pair, it would still be useful to know that it's (string * (either int or double) list), and the list cannot be empty. Etc. Type declarations or inference are a bit all-or-nothing, and I think being able to read through the properties that the compiler could infer (or at least confirm) would help find bugs, suggest optimizations, etc.

If I ever get past the first dozen projects on my list, I'd like to write a compiler for a dialect of Prolog designed with constraint analysis in mind. (I also need to read more about what's already been tried, first - this is just me being curious about how far constraint analysis could go and wondering out loud.) It would be tricky, but more feasible with Prolog-like semantics than in, say, C.