Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are given here.
Intuitively, as far as I understand, this inhabitant should have the form $\lambda x:A.\lambda y:B(x). P(x,y)$ for some $P: A\to B(x)\to \ast$. (If this is not right, let me know.)
Formally, I got to this point. So I proved that $\lambda y:B(x). P(x,y) : \Pi y:B(x).\ast$ in a certain context. But then I cannot abstract over $x:A$ because the "flag" (assumption) $P:A\to B(x)\to \ast$ doesn't let me do so. And I cannot move this flag before the flag "$x:A$" because I must assume $x:A$ before assuming $P: A\to B(x) \to \ast$ since $B(x)$ depends on $x:A$. What should I do in this situation?