Counterexamples in Type Theory

Question

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.)

Answer 1

Coq maintains a document of historical proofs of absurdity, including brief explanations of the flaw that allowed them to pass. Most of these are more "counter-examples in type theory implementations" ("Set+2 was incorrectly simplified to Set+1", various de Bruijn indexing bugs), but the section titled "Conflicts with axioms in library" has some interesting ones (the guard checker used to be incompatible with propositional extensionality, for example).

Bug trackers are also probably good places to go digging if you want. For example, Coq's SProp UIP + impredicative Prop breaks decidability of typechecking, and the way Agda implements mutual blocks allows something very close to Very Dependent Types / Insanely Dependent Types which might or might not be inconsistent.

Answer 2

Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later.

1. A simply typed $\lambda$-term whose computation in the $\lambda\sigma$-calculus does not always terminate. [Mellies (1995)]

2. $\lambda U$ and $\lambda U^-$ are non-normalizing PTSs which are functional and non-dependent. [Girard (1972)]

3. The non-functional PTS with sorts $\{1, 2, 3\}$ and axioms $1 : 2$ and $1 : 3$ does not satisfy type unicity.

4. The PTS with sorts $\mathbb N$, no rules, and axioms $$ \mathcal A = \{(i: n) : \text{the $i$th Turing machine halts on $i$ in $n$ steps}\} $$ is strongly normalizing and functional but has undecidable type checking [Pollack, 1992]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

5. Impredicative type theory with proof-irrelevant propositional equality is not weakly normalizing. [Abel, Coquand (2020)]

6. Tight reduction (i.e., $\beta$-reduction on terms with type-annotated application and abstraction) does not satisfy CR on non-well-typed terms.

7. Cyclic F (i.e., F with the additional axiom $\square : *$) is strongly normalizing and has cyclic axioms.

Answer 3

As mentioned in this answer on this site, so-called "positive coinductive types" break subject reduction.