On Decidability of Nominal Subtyping with Variance

Yes, I found this article about Gödel's incompleteness theorem problem in a programming languages design. I love it. I can see that one of the authors is an author of my favorite type topic books.