Comment by _flux
Have you seen OCaml? Though its inference stops at module boundaries (but you don't need to annotate them) and for some more special type features. In addition it solves some type inference problems by having e.g. different operators on integers and floats, there are no type-directed traits.
But in practice it's quite handy to annotate module interfaces and even individual functions.
I hear that OCaml without interface files can cause spooky-action-at-a-distance type errors[1]. Have you had experience with that?
> But in practice it's quite handy to annotate module interfaces and even individual functions.
Yes, but it also limits what information the types can represent because of syntax and human patience limitations. A fully inferred language could associate numbers with possible value ranges, lists with their sizes, enumeration of fixed string values, etc.
[1] https://news.ycombinator.com/item?id=39615796