I think that writing (and publishing) an implementable and reasonable formal specification has an even bigger advantage: you need to make it understandable and regular (which benefits users). To fix a bug like SI-5298, you just need to translate bounds to constraints directly; with an ideal proof of "completeness", such a bug would likely be impossible by design, although existing completeness proofs for local type inference systems seem to often have various restrictions. The only obstacle is that defining the formalization risks being extremely complicated - I think it could even be enough for a PhD thesis.
But wasn't Hubert Plociniczak, PhD candidate, planning to use constraint solving to improve both Scala type inference and for the type debugger , based on research by Martin Odersky et al. on one side, and GHC hackers on the other? He also gives a number of convincing arguments on why one should use constraint systems. Among others, it's easier to explain type inference errors in terms of constraints.
Of course research proposals for PhD students are not binding - my research proposal had absolutely no relevance (I'm a PhD student). A lot of disclaimers apply for me too: my knowledge of type inference goes barely beyond Pierce's TAPL book, and I've only skimmed his research proposal (too hard for me, sorry).
 Hubert Plociniczak, 2010. Making sense out of an advanced type system. Edic research proposal. Available at