Type-checking function calls with functional subtyping
Presumably, what Scala does (since you mentioned it) is relax your step 2. It is incorrect to check that the type of $f$ is merely 'of the form' $T → U$ because it is applied. Rather, one should check that the type of $f$ is known to be a subtype of some $T → U$.
In Scala, such subtyping 'facts' can be added by declaration when defining a type. So, arrays are declared to be subtypes of function types. You gave this as:
$$[U] &lt;: \mathsf{Int} → U$$
This is just an axiom that needs to be part of the subtyping check. Scala is actually even more complex than this, but this at least covers the subtyping part.
As Andrej mentioned in the comments, these sorts of arbitrary 'declared' subtyping axioms don't necessarily lead to the nicest behavior (principal types, decidability, etc.). There might be multiple particular strategies that you could replace your steps with to incorporate the change to step 2, and they might have different limitations on what types they can check/infer for various examples.