A related result is that java generics are Turing complete [1]. As a result you can write programs which will loop the type checker! I was at the popl presentation where the author showed this result. He gave a demo where he defined a Turing program and a tape, and then let the type checker give the answer (halting with 1 will succeed type checking, halting with 0 will give a type error). This was a lot of fun.
[1] https://arxiv.org/pdf/1605.05274.pdf