The title pretty much covers it. I'm wondering if someone is maintaining a list of counterexamples in type theory. I'm aware of Counterexamples in Type Systems, which I think is very nice, but I guess I'm more interested in something closer to the mentality of Counterexamples in Topology or counterexamples in category theory. I'm thinking of something like a list of type systems which don't have desired meta-theoretic properties because of interesting features (e.g., non-normalization of impredicativity + proof-irrelevant equality [Abel, Coquand, 2020]) or which lie in a general class of systems that one might expect to be well-behaved (e.g., the cute example in [Pollack 1992] of a strongly normalizing functional PTS without decidable type checking).
(This is obviously a soft question, and personally, I would also love to also see answers/comments with some greatest-hits counterexamples, especially if such a document doesn't exist, but I'm admittedly somewhat new to StackExchange and don't know if that fits into the ethos of the site. So feel free to cross this part out if it doesn't.)