Type-checking function calls with functional subtyping I'm relatively new to the topic. Suppose that you want to type-check an expression of the form f(a), i.e. a function call. Assuming that all the declarations are provided explicit types, I believe that a simple type-checker would behave as follows:

Given the environment, compute the types of a and f;
Check that the type of f be of the form $T\to U$;
Check that the type of a be a subtype of $T$;
Return $U$ if needed.

But now suppose that, for all $U$, the following subtyping relation holds:
$$
[U]&lt;:\text{Int}\to U
$$
where $[\thinspace\cdot\thinspace]$ denotes the array-type, and that computation (1) finds the types of a and f to be resp. $T$ and $[U]$ for some $T$, $U$. Now, $[U]$ is not a function-type, so check (2) fails. I'm assuming that the definition of $&lt;:$ is completely independent of the type-checker, so we can't just hard-code a check (2.1) for array-types, too. We could instead check that $[U]$ be a subtype of a least acceptable function-type $T\to\top$, where $\top$ denotes the universe-type, but what if function-types are invariant according to $&lt;:$?
I suspect that what I really need is a form of type-inference, rather than type-checking, even though the types of f and a are completely determined, which doesn't make sense to me. What would be the correct approach, here?
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.