I will give a partial answer, I hope others will fill in the blanks.
In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\mathsf{Str}$ for binary strings, $\mathsf{Bool}$ for Booleans) and wonder what is the complexity of the functions/problems representable/decidable by typed terms. I know a precise asnwer only in some cases, and in the simply typed case it depends on the convention used when defining "representable/decidable". Anyhow, I don't know of any case in which there is a doubly exponential upper bound.
First, a brief recap on the Lambda Cube. Its 8 calculi are obtained by enabling or disabling the following 3 kinds of dependencies on top of the simply typed $\lambda$-calculus (STLC):
- polymorphism: terms may depend on types;
- dependent types: types may depend on terms;
- higher order: types may depend on types.
(The dependency of terms on terms is always there).
Adding polymorphism yields System F. Here, you can type the Church integers with $\mathsf{Nat}:=\forall X.(X\rightarrow X)\rightarrow X\rightarrow X$, and similarly for binary strings and Booleans. Girard proved that System F terms of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ represent exactly the numerical functions whose totality is provable in second order Peano arithmetic. That's pretty much everyday mathematics (albeit without any form of choice), so the class is huge, the Ackermann function is a sort of tiny microbe in it, let alone the function $2^{2^n}$. I don't know of any "natural" numerical function which cannot be represented in System F. Examples usually are built by diagonalization, or encoding the consistency of second order PA, or other self-referential tricks (like deciding $\beta$-equality within System F itself). Of course in System F you can convert between unary integers $\mathsf{Nat}$ and their binary representation $\mathsf{Str}$, and then test for instance whether the first bit is 1, so the class of decidable problems (by terms of type $\mathsf{Str}\rightarrow\mathsf{Bool}$) is equally huge.
The other 3 calculi of the Lambda Cube which include polymorphism are therefore at least as expressive as System F. These include System F$_\omega$ (polymorphism + higher order), which can express exactly the provably total functions in higher order PA, and the Calculus of Constructions (CoC), which is the most expressive calculus of the Cube (all dependencies are enabled). I don't know a characterization of the expressiveness of the CoC in terms of arithmetical theories or set theories, but it must be pretty frightening :-)
I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get. Computationally, I don't think you get much more expressiveness than with simple types, but I may be mistaken.
So we are left with the STLC. As far as I know, this is the only calculus of the Cube with interesting (i.e., not monstrously big) complexity upper bounds. There is an unanswered question about this on TCS.SE, and in fact the situation is a bit subtle.
First, if you fix an atom $X$ and define $\mathsf{Nat}:=(X\rightarrow X)\rightarrow X\rightarrow X$, there is Schwichtenberg's result (I know there's an english translation of that paper somewhere on the web but I can't find it now) which tells you that the functions of type $\mathsf{Nat}\rightarrow\mathsf{Nat}$ are exactly the extended polynomials (with if-then-else). If you allow some "slack", i.e. you allow the parameter $X$ to be instantiated at will and consider terms of type $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}$ with $A$ arbitrary, much more can be represented. For example, any tower of exponentials (so you may go well beyond doubly exponential) as well as the predecessor function, but still no subtraction (if you consider binary functions and try to type them with $\mathsf{Nat}[A]\rightarrow\mathsf{Nat}[A']\rightarrow\mathsf{Nat}$). So the class of numerical functions representable in the STLC is a bit weird, it is a strict subset of the elementary functions but does not correspond to anything well known.
In apparent contradiction with the above, there's this paper by Mairson which shows how to encode the transition function of an arbitrary Turing machine $M$, from which you obtain a term of type $\mathsf{Nat}[A]\rightarrow\mathsf{Bool}$ (for some type $A$ depending on $M$) which, given a Church integer $n$ as input, simulates the execution of $M$ starting from a fixed initial configuration for a number of steps of the form
$$2^{2^{\vdots^{2^n}}},$$
with the height of the tower fixed. This does not show that every elementary problem is decidable by the STLC, because in the STLC there is no way of converting a binary string (of type $\mathsf{Str}$) representing the input of $M$ to the type used for representing the configurations of $M$ in Mairson's encoding. So the encoding is somehow "non-uniform": you can simulate elementarily-long executions from a fixed input, using a distinct term for each input, but there is no term that handles arbitrary inputs.
In fact, the STLC is extremely weak in what it can decide "uniformly". Let us call $\mathcal C_{ST}$ the class of languages decidable by simply typed terms of type $\mathsf{Str}[A]\rightarrow\mathsf{Bool}$ for some $A$ (like above, you allow arbitrary "slack" in the typing). As far as I know, a precise characterization of $\mathcal C_{ST}$ is missing. However, we do know that $\mathcal C_{ST}\subsetneq\mathrm{LINTIME}$ (deterministic linear time). Both the containment and the fact that it is strict may be shown by very neat semantic arguments (using the standard denotational semantics of the STLC in the category of finite sets). The former was shown recently by Terui. The latter is essentially a reformulation of old results of Statman. An example of problem in $\mathrm{LINTIME}\setminus\mathcal C_{ST}$ is MAJORITY (given a binary string, tell whether it contains strictly more 1s than 0s).
(Much) Later add-on: I just found out that the class I call $\mathcal C_{ST}$ above actually does have a precise characterization, which is moreover extremely simple. In this beautiful 1996 paper, Hillebrand and Kanellakis prove, among other things, that
Theorem. $\mathcal C_{ST}=\mathsf{REG}$ (the regular languages on $\{0,1\}$).
(This is Theorem 3.4 in their paper).
I find this doubly surprising: I am surprised by the result itself (it never occurred to me that $\mathcal C_{ST}$ could correspond to something so "neat") and by how little known it is. It is also amusing that Terui's proof of the $\mathrm{LINTIME}$ upper bound uses the same methods employed by Hillebrand and Kanellakis (interpreting the simply-typed $\lambda$-calculus in the category of finite sets). In other words, Terui (and myself) could have easily re-discovered this result were it not for the fact that we were somehow happy with $\mathcal C_{ST}$ being a "weird" class :-)
(Incidentally, I shared my surprise in this answer to a MO question about "unknown theorems").
