FWIW, I've seen many IDEs and plugins add inline type annotations so it reads as though they are there, but aren't. I think the first time I saw this was with the JetBrains IntelliJ Rust plugin in 2019.

I like being able to read code in nano or vi

I would rather see the type annotations too. This whole essay has a flimsy premise.

Around every integer? Around every expression? On every let-bound function, on every where-bound function? Should the 'forall. a' included if 'a' is a polytype?

It depends on the aesthetics of the language I think. What are core concepts that you must know? (there should be few). Striking the right balance is hard.

Code is read a lot more than is written in my experience, so saving time writing it is optimizing for the wrong thing.

Languages with much inference for me REQUIRE IDEs that help you see what the code is actually doing. Forget about using a text editor or reading a diff and getting what the implications are.

It would be nice to have them auto-generated in the source, like a autofixable lint rule where the compiler add the annotations to your source code.