Because a program's types can serve as part of its documentation.
So many times I will accidentally return 42 or Result<Result<42>> when I mean to return Result<42>. With annotations, my error is instantly obvious. Otherwise I accidentally have a function that returns Result<Result<number>> and it may lead to a very weird error message when I use `foo().map(_ + 100)` somewhere else.
That's letting the computer doing more work, not less of it. Relying too much on inference can bow back into the human doing more of the work to figure out what the types actually are in a given spot.
The computer can only tell you what types your code _has_ (from inference), but not what type it _should_ have based on your intentions. Type inference can only complain when your code contradicts with itself (on a type level), but can't tell you when it contradicts with your intentions.
If you don't write out your intentions, you'd have to hover over everything to see if the inferred types differ from your expectations.
IDE hover types and collapsible type annotations (and alternatively also collapsible implementation) are still useful as a way to declutter your UI when reading code.
Right - that's not global type inference. It's intra-module type-inference.
Aside, when I decide to change where I put module boundaries, full program inference helps too: I just throw away the old module definitions, draw different boundaries and re-run inference.
(1) Hack until I've got something stable. Note: at the start of coding I typically don't quite know what the right abstractions are, so a lot of code (and associated types) are in constant flux.
(2) Once program is stable, wrap it in a module, let the compiler work out all types and put them in as module interface.
That gives me the best of all possible worlds: type annotations at abstraction boundaries but you don't have to type them out. Writing out explicit types inhibits fast change. I wish the languages I'm using at the moment (Scala, Rust, C++) allowed a flow like that. Alas, full type inference stops being possible with more expressive typing systems.