In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It is often referred to as Type:Type because the kind Type is itself of type Type. Unfortunately, it is inconsistent as a logic. This was discovered by Girard in his famous dissertation [1], who managed to express the Burali-Forti paradox in Type:Type. Various people have analysed, generalised and simplified Girard's analysis, see e.g. [2, 3]. This analysis seems to involve showing that non-terminating terms can be typed.
I have a question about non-termination: do we get non-normalisation at the level of types? By that I mean, is there a type $T$ such that the reduction relation $\rightarrow$ used, explicitly or implicitly, to define equality of types, gives rise to an infinite reduction sequence $$ T \rightarrow T' \rightarrow T'' \rightarrow \cdots? $$
[1] J.-Y.. Girard, Une extension de l'interpretation fonctionelle de Gödel a l'analyse.
[2] T. Coquand, A New Paradox in Type Theory.
[3] A. J. C. Hurkens, A Simplification of Girard's Paradox.