If my understanding is correct, type inference producing a set of possible types - instead of a single type - for each term has proven to be undecidable? This

If my understanding is correct, type inference producing a set of possible types - instead of a single type - for each term has proven to be undecidable? This is a shame, because sum types (e.g. Shape := Circle U Square U Triangle) are actually pretty useful, and languages such as Java ended up implementing them via class or interface inheritance. Languages often also required type coercion to deal with things like 0.2 + 5, otherwise + could have had a type signature like: float U int -> float U int -> float U int.