When a type is a value?
I will offer a semantic perspective. The relationship between values and general computations may be expressed in terms of an adjunction between two categories:
\begin{align*}
F &amp;: \mathcal{V} \to \mathcal{C} \\
U &amp;: \mathcal{C} \to \mathcal{V} \\
F &amp;\vdash U
\end{align*}
Here $\mathcal{V}$ is a category of values, $\mathcal{C}$ is a category of computations. The prototypical example comes from domain theory:


$\mathcal{V}$ is the category of predomains, i.e., $\omega$-chain complete posets which may not have a list element,
$\mathcal{C}$ is the category of domains, i.e., $\omega$-chain complete posets with a least element,
$F$ is the lifting functor
$U$ is the forgetful functor


This view is closely related to Paul Levy's call-by-push-value (CBPV).

The semantic picture suggests that we should not only distinguish values and computations, but also value types and computations types. Thus, instead of saying that there are terms of type $A$, some of which are values and others are computations, we say instead that there are two kinds of types: the elements of value types are always values, while the elements of computation types are always computations.

In CBPV languages the distinction is explicit. For instance $\mathtt{nat}$ is a value type and $42 : \mathtt{nat}$ while $F \mathtt{nat}$ is a computation type inhabited by computations such as $\mathtt{return}\;42$ and $(\lambda n . n \cdot n + 6) \; 6$.

From a theoretical point of view such a typing discipline is desirable, because the value/computation distinction becomes a proper mathematical concept, rather than a syntactic device that drives normalization algorithms. (I warned you that I will offer the semantic perspective.)

We may think about the distinction between values and computations for dependent types and other corners of Barndregt's cube. The semantic picture suggests that we should again distinguish value types from computation types. Thus, we really should replace the judgement $\Gamma \vdash A \ \mathrm{type}$ ($A$ is a type in context $\Gamma$) with two judgements:


$\Gamma \vdash A \ \mathrm{vtype}$
$\Gamma \vdash C \ \mathrm{ctype}$


Of course, the next step requires us to figure out precisely how to extend the above picture to the rather more complicated situation that arises through dependencies. This is a topic of current research, and a great deal of past research. 

Now, as to whether something like $(\lambda T .  \mathrm{return}\,T) (\prod_{x : A} B(x))$ itself is a value or a computation can be phrased in terms of universes. There ought to be a universe of value types $\mathcal{U}_V$ and a universe of computations $\mathcal{U}_C$, each reflecting the two kinds of judgements above. We also have to decide whether $\mathcal{U}_V$ and $\mathcal{U}_C$ themselves are value or computation types (probably value types, with corresponding computation types $F \mathcal{U}_V$ and $F \mathcal{U}_C$). The typing rules would place $(\lambda T .  T) (\prod_{x : A} B(x))$ into one or the other universe (presumably in this case the universe of computations).

I do not really want to give a definitive answer here, I just want to place the question into a proper mathematical context that allows us to consider the mathematical possibilities rather than look for an answer based on experience with normalizing algorithms.