  Many type systems include infinite types. In session type systems, which are
the focus of this paper, infinite types are important because they allow the
specification of communication protocols that are unbounded in time. Usually
infinite session types are introduced as simple finite-state expressions
$\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$.
Alternatively, some systems of label- or value-dependent session types go
beyond simple recursive types. However, leaving dependent types aside, there is
a much richer world of infinite session types, ranging through various forms of
parametric equational definitions, all the way to arbitrary infinite types in a
coinductively defined space. We study infinite session types across a spectrum
of shades of grey on the way to the bright light of general infinite types. We
identify four points on the spectrum, characterised by different styles of
equational definitions, and show that they form a strict hierarchy by
establishing bidirectional correspondences with classes of automata:
finite-state, 1-counter, pushdown and 2-counter. This allows us to establish
decidability and undecidability results for the problems of type formation,
type equivalence and duality in each class of types. We also consider previous
work on context-free session types (and extend it to higher-order) and nested
session types, and locate them on our spectrum of infinite types.
