Author here: one of my projects (the Dhall configuration language) does exactly that

score 3 · canonical

Regarding the foo(T) -> T example, I believe the compiler would be able to infer that x is an i32 without unification, whether or not foo was a built-in function or a user-defined function.

In the case of a built-in function, there would be a judgment like:

Γ ⊢ x ⇒ a
──────────────
Γ ⊢ foo(x) ⇒ a

… and in the case of a user-defined function, the foo function would require an explicit type application (e.g. foo<i32>(x)) and that would provide the information necessary to infer the type of the result. Obviously, as the post admits, it’s not ergonomic but it does work (this is basically exactly how Dhall works, and Dhall also does not support unification).

I agree with the rest of what you’re saying, though.

score 4 · canonical