Non-termination of types in Martin-Löf's Type:Type? 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.
Short answer: yes.

Long answer: For $\mathrm{Type}:\mathrm{Type}$, non-termination at the type level is trivial. You can take a constant $X:\mathrm{False}\rightarrow \mathrm{Type}$. Then if you take the inconsistent term $\bot : \mathrm{False}$ you have
$$ X\ \bot : \mathrm{Type}$$
Which is non-terminating at the type level. You might complain that this has a head normal form, which isn't what usually leads to inconsistency in type theory. In this case you can remember that 
$$ \mathrm{False}\equiv \forall X.\ X$$
and so
$$ \bot\ \mathrm{Type}:\mathrm{Type}$$

Which has no head-normal form. In general, in this system the types and terms are so intertwined that the non-termination always seeps at the type level.

However, there is another system, called $U^-$, also described by Girard in his thesis, which was discovered to be inconsistent by Coquand (A New Paradox in Type Theory). This system is terminating at the type level, as it only has $\mathrm{system}\ F$ types at the kind level, and we know that terms are normalizing in that system (also a result of Girard!).

This means that non-termination at the type level is not necessary for having an inconsistent pure type system (a fact that I found out somewhat painfully after having proven an open question while depending on this fact).