  Session types statically describe communication protocols between concurrent
message-passing processes. Unfortunately, parametric polymorphism even in its
restricted prenex form is not fully understood in the context of session types.
In this paper, we present the metatheory of session types extended with prenex
polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove
that type equality is decidable by exhibiting a reduction to trace equivalence
of deterministic first-order grammars. Recognizing the high theoretical
complexity of the latter, we also propose a novel type equality algorithm and
prove its soundness. We observe that the algorithm is surprisingly efficient
and, despite its incompleteness, sufficient for all our examples. We have
implemented our ideas by extending the Rast programming language with nested
session types. We conclude with several examples illustrating the expressivity
of our enhanced type system.
