When a type is a value? In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason is that a function $\lambda x.M$ is an finished piece of data, sharing with other values like $3$ or $\mathtt{true}$ the following ontological status:  something that one can handle independently of a notion of execution. (Indeed, you cannot execute $\lambda x.M$ until you apply it to something. Of course you may reduce a $\beta$-redex in $M$, but then intuitively you are not reducing the whole piece of code $\lambda x.M$.)

Now, when it comes to dependent type theories, or more generally any type system having some vertex of Barendregt's cube as its core, all levels of the syntax - objects, types, kinds and possibly all the infinite higher kinds - have the status of terms. So it makes sense to ask when one of them is a value. Let us ask the question for types, but of course the same applies to all possible superior kinds.

Obviously a functional type $\lambda x: T. T' : \Pi x: T.A $ (for $A: \mathtt{Kind}$ and $T:\mathtt{Type}$) is a value. (Notice that in basic dependent type theory, the one without the higher-dimensional kinds $\omega$, the kind $\Pi x: T.A$ 
 is actually $T\to A$).

Now, what about the universal type $\Pi x: T.T'$ (where $T,T': \mathtt{Types}$) ? From a mathematical perspective it is a family, hence a function. It corresponds to my definition of ontology of a value above: something that one can handle independently of a notion of execution.
But on the other side $\Pi x: T.T'$  has a relevant difference from $\lambda x: T. T' $: the latter has a destruction operator (the application), whereas the former does not. In light of this, would you consider $\Pi x: T.T'$ as a value?

In a way, I am asking the following (philosophical?) question. Which intuition do you prefer:


a value is something that one can handle independently of a notion of execution
a value is something that one can handle independently of a notion of execution and when it is not ground can be decomposed via an appropriate operator. 


In case 2  the "dependent arrow" type $\Pi x: T.T'$ is not a value, only the functional type $\lambda x: T. T'$ and the polymorphic universal type $\forall X.T$ are.

I am personally inclined towards option 2, but I would like to hear from more experienced researchers.
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.