What do you think about e.g. Roc having whole-program type inference that always works and always infers the most general types?
In isolation, I love the idea. I don't have a strong sense of how the tradeoffs would affect things in practice though.
Perhaps they are not a big deal, but if they are too restrictive, then maybe the next best thing would be to have anything go (like in Python or Javascript), but the compiler guides you to where it's having trouble inferring things.
FWIW, there are definitely ways to do it "right" in languages like Python, but it's a slightly different approach to dev than in other languages, so people create a mess if they don't shift, or if they are just untrained/sloppy/lazy/whatever. But when you have a team of people doing it right, it's really quite nice, even as the codebase grows large.
But if even just one person on the team can't be trusted to do it that way, you're probably better off in some other language.