  The importance of subtyping to enable a wider range of well-typed programs is
undeniable. However, the interaction between subtyping, recursion, and
polymorphism is not completely understood yet. In this work, we explore
subtyping in a system of nested, recursive, and polymorphic types with a
coinductive interpretation, and we prove that this problem is undecidable. Our
results will be broadly applicable, but to keep our study grounded in a
concrete setting, we work with an extension of session types with explicit
polymorphism, parametric type constructors, and nested types. We prove that
subtyping is undecidable even for the fragment with only internal choices and
nested unary recursive type constructors. Despite this negative result, we
present a subtyping algorithm for our system and prove its soundness. We
minimize the impact of the inescapable incompleteness by enabling the
programmer to seed the algorithm with subtyping declarations (that are
validated by the algorithm). We have implemented the proposed algorithm in Rast
and it showed to be efficient in various example programs.
