I've come to believe through experience that hindley milner and its derivatives are the sweet spot. I shouldn't have to tell the compiler the types, and I shouldn't be attempting to implement business solutions in the type system. It should just know what is already there and tell me it when it can't reconcile that with what I'm adding, because that indicates a problem with my reasoning. The constraints this places on the language semantics end up being neutral-to-positive as well.