In general I agree with what youre advocating for. Languages should require annotations on function parameters and return types and most top level definitions. But even if you only infer types locally you'll still want unification to do it well. Without unification local inference will hit annoying edge cases where you have to add otherwise unnecessary annotations