I always love this kind of article! For many more ways type systems can be unsound, see https://counterexamples.org/ .