It's about readability. You write the types for documentation, and to make it easier for people doing a code walkthrough to simulate what is happening in their heads.

IDEs can add type annotations not present in the code, but there are many contexts (source control diffs, or code in a PDF, or code in a website) where that kind of software type annotation is not available.

I find that in OCaml, which has type inference for everything (function arguments, function return type, local variables, expressions) I end up writing the types almost everywhere, for two reasons. The first is documentation: it helps me to read and understand code I wrote ages ago.

But the second is that type inference often goes haywire, because the compiler doesn't know ahead of time whether the code you wrote is in error. So when you make a mistake, like forgetting to pass the right number of arguments to a curried function, the compiler will happily propagate that mistake around, even propagating the erroneously-inferred types to other functions. And you get these incomprehensible type error messages that come from places that are very separate from where the mistake actually happened.

And then I find myself taking a random walk through the code, adding type annotations to constrain the inference until I find my mistake. So why not skip the middle step, and require annotations?

Often, however, it isn't obvious what the type of an expression is going to be, and it's easier to construct the value level than the type level. For those cases you could simply force a type error to find out the type and write it in the text.

The simplicity reason is not that inference rules vary by compiler (the rules can be put in the spec), it's that type inference (as opposed to one-directional type propagation) can be complex to implement, and for simple extensions to an H-M type system it can become undecidable.

Coming from mostly C and Java (where I didn't have inference) and Python (dynamic types, no real annotation when I was writing it) I found Rust's degree of inference (Constants, function signatures, structures must spell their types, but other types can be inferred if unambiguous) very satisfying, and I don't fancy going back.

Never written any OCaml in anger, and it has been decades since I wrote more ML of any sort, so perhaps in OCaml I'd find there's too much inference for my taste.

I think the widespread consensus view is that function signatures should have type annotations. Local variables are more contentious, but even then, you don't strictly need type inference to omit the type annotation in local variables (except for disambiguation).

I could easily modify the compiler to allow omitting types from `let` statements. Maybe for development you'd use annotation-free `let`s, and when publishing or otherwise finalizing code you have to write the type annotation.

I could be convinced to add this as a feature, but I tend to favor the strict and one-way-to-do-it approach.

I will say that I find the Java-style `Widget widget = new Widget(junk);` infuriating, this barely counts as inference, it's more like lookahead. `my widget = Widget(junk)` is easier to look at and shorter to type, while conveying the same information.

So the easy win has my vote.

Quite often it is:

    Widget w = new SpecialWidget (junk);

though. I kinda like verbosity. There is less magic to reason about in the language overall.

Languages which use only inference have been written, but it's just not ergonomic, no one wants to use that. So the Widget is always available as an annotation (although I can't read your intent out of one line of Java clearly, and depending on what that is, a cleaner type system than Java's might take care of covariance well enough that we still wouldn't care), or as a cast.

Java itself introduced syntax for eliding the type of simple variables, so this is an old complaint, but yeah: a little bit of inference goes a long way.

I really like Golang’s inference which is much dumber than Rust (left type = right type)

> offering inference means either different implementations could have different inference rules, or else, those rules must be set out in full in the specification

As a tangent, there is a third option (or a twist on the second), called "principle types": carefully design the type system so that there is only one possible type for each expression, or at least one "best" or "most general" type for each expression. The spec for this can be much smaller than a full type inference algorithm.