Modern type theories (e.g. Calculus of Constructions) seem to effect an extensional conflation of dependent and polymorphic types. E.g., in Coq, after declaring
Variable n: forall (x:Prop), x.
n, a polymorphic (function) term, has both a dependent (depending on x) and a polymorphic (over Prop) type. So the dependent/polymorphic distinction becomes merely intensional in these theories1, reducing to that of a perspective. Is this analysis correct or am I missing something? Also, can one pull off dependent types w/out polymorphism in Coq? Vice versa it's possible, as we can get (subtype) polymorphism w/out dependent types:
Parameter natT:> nat -> Type.
Check 1: nat. Check 1: Type.
1 On the other hand, due to the Curry-Howard isomorphism,
first-order logic corresponds to dependent and second-order logic to polymorphic types. However, my understanding is that the (second-order) polymorphic terms still have dependent types -- just not dependent on terms but on types. (Is this correct?)
Much of your question is unclear. I'm going to attempt an end run around it.
The lambda cube is a collection of related type theories that are individually important and serve as archetypical systems. (That said, I sometimes get the impression that people put too much significance on the lambda cube. It is nowhere near comprehensive.)
The simplest system in the lambda cube is $\lambda\!\!\to$, the simply typed lambda calculus. From $\lambda\!\!\to$ there are three directions (axes) we can go. We can add the ability for terms to depend on types producing $\lambda2$, the polymorphic lambda calculus. We can add the ability for types to depend on types producing $\lambda\underline\omega$, the simply typed lambda calculus with operators. Finally, we can add the ability for types to depend on terms producing $\lambda P$, the dependent lambda calculus. "Dependently typed" always refers to types depending on terms. Other possible dependencies (potentially between sorts not mentioned) are not referred to as "dependent types". This is just what "dependent types" means, types that depend on terms. (Note, in $\lambda\!\!\to$, terms can depend on terms. That's what lambda abstraction does.) There is no (trivial, at least) embedding of any of these three extensions into the others.
In particular, a type like $\forall \alpha.\alpha\to\alpha$ in $\lambda2$ has no counterpart in $\lambda P$, i.e. $\lambda P$ cannot express a polymorphic identity function. Conversely, a type like $\Pi n:\mathbb N.n+n > n$ in $\lambda P$ has no analogue in $\lambda2$. So you can have dependently typed lambda calculi without (parametric) polymorphism and polymorphic lambda calculi without dependent types.
I don't know why you bring up subtyping at all, but most lambda calculi with subtyping in the literature are usually variations of the polymorphic lambda calculus ($\lambda2$) also known as System F. In particular, one of the most notable such systems is System F${}_{<:}$. If you wanted to talk about pre-generics Java (i.e. Java before Java 1.5), you potentially wouldn't even need parametric polymorphism, e.g. you could work within a simply typed lambda calculus extended with subtyping. Nothing stops you from combining subtyping and dependent typing, though. Subtyping is a different feature altogether and adding it takes you off the lambda cube entirely (which, as I mentioned before, is perfectly okay).
The Calculus of Constructions is equivalent to the system produced by adding all three extensions simultaneously. For the purposes of polymorphism, and not thinking in terms of the lambda cube, the key addition over $\lambda P$ is a universe, i.e. a "type of types". Let's use $\mathcal U$ to notate it. (It is often called $\mathsf{Type}$ or $\mathsf{Set}$.) With $\mathcal U$ added to $\lambda P$, call the system $\lambda P+\mathcal U$ we can easily embed $\lambda2$ by turning quantifications over types into abstractions over terms of type $\mathcal U$, e.g. $\forall \alpha.\alpha\to\alpha$ becomes $\Pi \alpha:\mathcal U.\alpha\to\alpha$. That said, within $\lambda P + \mathcal U$, we'd want $\forall \alpha.\alpha\to\alpha$ to mean something more, and, in particular, we would expect that you could instantiate a term of that type to $\mathcal U$. We can't apply a term of type $\Pi \alpha:\mathcal U.\alpha\to\alpha$ to $\mathcal U$ though since it is not the case that $\mathcal U : \mathcal U$. This can be added as an axiom, but it is inconsistent. Another question is whether $(\Pi \alpha:\mathcal U.\alpha\to\alpha):\mathcal U$. If it is, then $\mathcal U$ is called impredicative, otherwise it is predicative. In Coq, $\mathsf{Prop}$ is impredicative but $\mathsf{Set}$ is not. This is one of the major distinctions between $\mathsf{Prop}$ and $\mathsf{Set}$. In the (impredicative) Calculus of Constructions as described on Wikipedia, what it writes as $\forall x:\mathsf{P}.e$ would correspond to $\Pi x:\mathsf{Prop}.e$, while what it writes as $\forall x:\mathsf{T}.e$ would correspond to $\forall x.e$.