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:

1. Given the environment, compute the types of a and f;
2. Check that the type of f be of the form $Tto U$;
3. Check that the type of a be a subtype of $T$;
4. Return $U$ if needed.

But now suppose that, for all $U$, the following subtyping relation holds:

$$
[U]<:text{Int}to U
$$

where $[thinspacecdotthinspace]$ 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 $<:$ 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 $Ttotop$, where $top$ denotes the universe-type, but what if function-types are invariant according to $<:$?

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?