  We study increasingly expressive type systems, from $F^\mu$ -- an extension
of the polymorphic lambda calculus with equirecursive types -- to
$F^{\mu;}_\omega$ -- the higher-order polymorphic lambda calculus with
equirecursive types and context-free session types. Type equivalence is given
by a standard bisimulation defined over a novel labelled transition system for
types. Our system subsumes the contractive fragment of $F^\mu_\omega$ as
studied in the literature. Decidability results for type equivalence of the
various type languages are obtained from the translation of types into objects
of an appropriate computational model: finite-state automata, simple grammars
and deterministic pushdown automata. We show that type equivalence is decidable
for a significant fragment of the type language. We further propose a
message-passing, concurrent functional language equipped with the expressive
type language and show that it enjoys preservation and absence of runtime
errors for typable processes.
