The author answers this question in the Discussion section at the end: To summarize, Theorem 1 has two practical implications: 1. If one intends to implement

The author answers this question in the Discussion section at the end: To summarize, Theorem 1 has two practical implications: 1. If one intends to implement a formally verified type checker for Java, it is necessary to choose a subset of the type system that is decidable. 2. If reified generics are added to Java, then one needs to find some solution for not turning instanceof into a security problem.