[TYPES] Example uses of impredicativity

[Stefan Monnier]

Hi,

I was recently reminded that not only I only understand impredicativity
in a very superficial way, but on top of that, I don't know of many
uses of it.

Basically, I know of its use in Church encodings, in Shao et. al.'s λₕ
(from Type-safe Certified Binaries, which I also used in my "swiss
coercion"), as well as in type-preserving closure conversion, but that's
pretty much it.

When I started to look for examples in Coq, I soon realized that many
Coq libraries have definitions whose universe level is affected by
impredicativity but it's a lot more work to discover if the same
development would work as well without impredicativity.

Is there some place where I could find a kind of "collection" of
developments/techniques which rely on impredicativity?

Short of that, I'd be happy to hear from examples which
I could assemble to make such a collection.


        Stefan