Is a unification algorithm overkill for local type inference?

tl;dr: Yes, you want unification. The question I think you should consider is "How are you going to use it?"

The fun part about unification is that it's very applicable. Some variant of unification is going to ultimately be the thing you end up implementing, because it's the best tool for the task you're trying to solve - whether you need fully fledged Hindley-Milner/HM inference or not. (which is what I believe is what you're referring to with "because it was originally used for languages where you didn't have to specify the types anywhere" - unification is an algorithm, HM is another algorithm that utilizes unification for full-program type synthesis)

While HM may not be applicable to your ultimate solution in it's entirety, it does seem like a variant of it would be able to do what you want, for example, within the scope of a single function. This is what Rust does, if I recall correctly - You must provide types in various locations, but within the body of a function, it can deduce types through something very similar to HM.

Overall, I would recommend reading up on HM and an implementation of it, like algorithm J, and then consider how that might be applicable within the body of a function. (A hint: it'll be considerably simpler, because the complex part is function type inference, and you don't need that at all if I understand correctly)

Depending on your language, it might be as simple as assigning each unknown type a unifiable reference (commonly referred to as a metavariable in the literature, I believe) as a placeholder for it's type, and then unifying that reference with the real type when something like print_string(s) is found. Then, at the end of a scope of a function, you make sure no variable have an unknown type.

This means you might end up with something like:

let a = []; // type of a is `List $metavariable_0`
a.push(1); // unify `$metavariable_0` with `int`
// now a's type is `List int`

You'll note how that would work across the whole function with minimal issues due to the use of mutable references - when you change it once inside the unification function, it'll be changed everywhere, so you'll catch any sort of nasty type errors like

let a = [];  // type of a is `List $meta0`
a.push(1) // unify `$meta0` with `int`
// type of a is now `List int`
a.push("hi") // type error

I hope this can provide you some assistance.

ps. HM isn't that complex of an algorithm, most of the time! It's technically not great on worst case, but that worst case simply doesn't exist in good code, so it's really fine most of the time. My typechecker does unification similar to what I think you want to do, and it's ~200 LOC of OCaml.

I wouldn't describe unification as overkill for anything, or as heavyweight. It's conceptually simple and simple to implement. What you should be asking is whether it will work at all.

Unification means:

1. Assign a unique type variable to everything that has a type that you don't already know (every binding and subexpression without a declared type).

2. For every constraint that must be satisfied for the program to be well-typed, in an arbitrary order, specialize the unknown types as little as possible to satisfy the constraint. If you can't do it, abort with a type error.

If you make it through step 2, then you have perforce a valid typing of the program.

Hindley-Milner type inference is unification plus generalization (let-bound polymorphism), but since you're willing to require type signatures for reusable functions, you don't need the latter.

The problem with unification is that you need a type system designed so that you can "specialize the unknown types as little as possible" using only locally available information. Consider typechecking nums.map {...}. In your toy example, it's fine: you can think of .map as a function from objects to members, and it has an explicit type signature which you know because you collected it in a previous pass. But if you want more than one class to have a member named map, and you want to allow method calls on anything other than variables with explicitly declared types, then it's not so easy. Unification could specialize nums to "some object type that has a map member", which is basically a Haskell-style typeclass constraint ((HasMap a) => a). Adding typeclasses is an extra complication, but it's not too bad: you just think of them as constraints on the unknown type variables, and do the minimum necessary to ensure they're satisfied too. Unfortunately, that's not good enough, because nums is more constrained than that: it needs a member named map that is specifically a function that takes a function as its first argument (among other things). To handle that, you could try a multiparameter typeclass constraint, class HasMap o m | o -> m in Haskell syntax, expressing that the object type o has a member named map with the type m. That's more complication. But it won't work either, because the map method of Array<T> has a type that is polymorphic in U, which would require a third parameter to be added to HasMap, but there is no way for unification to know that. You could work around that by requiring members of the same name, even of unrelated classes, to have the same number of type parameters (and the same typeclass constraints on those parameters, if any), but it might be hard to explain that restriction to users.

You will run into similar issues if you want expressions like 2*x+1 to work whether x is an Int or a Float. My point is that designing a type system that is compatible with unification is not easy. (And if you succeed, you're likely to end up with Haskell's type system.)

These problems are the reason that most languages have ordered, bottom-up type inference: there has to be enough type information in the source code to determine the type of every binding without looking at its uses, and to determine the type of every subexpression without looking at its parent expression. Then it's guaranteed that the type of nums is known when you need to determine the type of .map.

Tyr uses a type inference strategy that is likely very close to what you have in mind. I call it single level return type inference. What happens is that overload resolution gets an expected return type and all the argument types and does inference based on that. If you make a decision, you cannot change it. All global entities have defined parameter types, but may infer return types based on their definitions.

Now, regarding your question, you will need to do something like unification if you want to allow recursive signatures, i.e. ones where a parameter's type uses another parameter. For example operations on equivalence relations take the underlying type and a function doing the equivalence check to derive == and != operators. Last time I checked, such definitions wouldn't be allowed in Go. The reason is that even type checking an application requires to do some sort of unification. TBH, I cannot tell the relation to HM.

However, the current binder parameter inference, which is type-checking wise likely identical to inference of local lambdas, is currently not based on unification. I haven't yet encountered an example where this would be required and, TBH, cannot tell if it would break my "single level" rule. That rule is required to provide somewhat understandable error messages. In essence, it allows creating an error location that is almost always useful.