Type systems are really good for detecting contradictions; they're much less good at figuring out which piece should be different. For any given type error, there may be half a dozen different changes to the code that would resolve it in different ways. Type systems often have no real way of guessing the user-intent there. There are loose heuristics, like... an explicit return type is more likely to be intentional (and therefore correct) than the type of the local value that's being returned. But I'm not aware of any formalism around this "ranking" of which types are most likely to be unintentional. Maybe we need one.

The only immediate solution I can see is to keep types simple enough that the user can fit the entire relevant type-space in their head (and in the IDE dialog!), so that they themselves can determine which part is actually "wrong" (as opposed to just contradictory).