The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) \rightarrow \tau \rightarrow \tau $, a result of Schwichtenberg showed that expressible functions are the extended polynomials.
If inputs are Church numerals given more complex types than $Int$, exponentiation and predecessor can be expressed (however Statman showed that equality, ordering and subtraction are not expressibile for any typing of church numerals.
However we should be more permissive and provide only an output restriction: a boolean type ( $Bool = \tau \rightarrow \tau \rightarrow \tau $). Under this convention, Statman's theorem that "deciding equivalence of normal forms of two simply typed lambda-terms is not elementary recursive" can be seen as an expressibility result (right?): we can express nonelementary functions.
Pushing to the limit, where we can arrive? Of course (by strong normalization) we can express only total functions. But I'm asking if there is a precise upper bound to simply typed lambda calculus expressive power.
I've found many articles, in particular "On the expressive power of simply typed and let-polymorphic lambda calculi" but I'm not able to understand if it is what I'm looking for.