Has anyone ever accidentally "proven" a false theorem with type-in-type?

Question

It is possible (with some cleverness) to prove false from type-in-type. For instance, Girard proved false in Martin Lof's original system (as described in the introduction of An Intuitionistic Theory of Types). This answer has a good account of the formal details.

Most systems allow type-in-type, through a configured opt-in and sometimes even by default (Pebble, Cayenne, some Trellys languages).

Has anyone ever "proven" an incorrect theorem with type-in-type, without intending to show that the system is unsound?

Answer 1

Yes. In fact, there is a very interesting example which is tied to the history of dependent type theory:

Per Martin-Löf, in his 1971 manuscript*, studied a system with type-in-type which famously turned out to be non-normalizing and inconsistent.

However, this manuscript does includes a proof of normalization and consistency for the system. It proceeds in the now-standard (although innovative at the time) way of associating a reducibility predicate to every type, and then proving by induction on typing derivations that every well-typed term satisfies the corresponding reducibility predicate. The proof is correct as far as I know, but proving that the universe satisfies its own reducibility predicate requires type-in-type in the meta-theory.

TL;DR: using type-in-type, Per Martin-Löf proved that type-in-type is normalizing and consistent.

---

*which was never published, but is available as a historical document with the permission of the author.

Answer 2

I did this myself!

(At least, if you interpret "incorrect" as "probably not true" rather than "demonstrably false".)

In the early days of homotopy type theory, we were starting to use multiple universes in ways that, I believe, had rarely been done before in type theory. Since Coq didn't support universe polymorphism yet, the only way to formalize some results was using type-in-type. In particular, I used it when formalizing some of the initial work on modalities that eventually became the RSS paper.

One of the results I proved, at that time, was that an (idempotent monadic) modality is left exact if and only if the universe of modal types is modal. This was a really striking application of, and justification for, the notion of left exactness. In particular, it implies that the modal types for a left exact modality form a model of type theory on their own, which is useful when constructing higher-topos models of type theory since any topos is a left exact localization of a presheaf topos.

Unfortunately, when we later went back to write up and formalize these results correctly using universe polymorphism, I realized that the proof was invalid. When universe levels are tracked, what I had proven was that the type of modal types in one universe $U$ was null with respect to all $U$-small modally-connected types; but since $U$ is not $U$-small, that doesn't imply $U$ is modal — unless we assume the modality is generated by a $U$-small family, i.e. that it is $U$-accessible. (In this form, the result is Theorem 3.11 in RSS.)

I don't have a counterexample to the statement in the non-accessible case, but I doubt it is true. In fact, for a non-accessible modality there isn't necessarily a canonical way to extend a modality on one universe to a modality on larger universes, so if we have a lex modality on $U$-small types, it's not even obvious what it means to say that $U$ is modal.

Ever since this experience, I've been unconvinced by any argument along the lines of "type-in-type is okay as long as you don't do anything stupid". I'm willing to grant that what I did was stupid; the point is that it's possible to do stupid things by accident.