This merge request revamps ImpredicativeTypes using a technique known as "quick look impredicativity".
For the first time, we think we have a solid, predictable implementation of impredicativity in GHC!
It's a development of our earlier paper, Guarded impredicative polymorphism (PLDI'18), which gives all the background and motivation. But our new approach is much, much, much simpler.
We do not yet have a proper paper that describes how it works, but we do have this working paper. It focuses on writing typing rules, and lacks lot of background, motivation, and explanation. But it's accurate, up to date, and (best of all) is fully implemented in this MR.