Implement Quick Look impredicativity
This MR implements Quick Look impredicativity (#18126)
It (finally) validates, and is ready for final review. @rae, @monoidal, @trupill would be particularly welcome reviewers, but I'd love to hear from others too.
There are two commits
-
One implements Quick Look. It is very faithful to the paper.
-
The second is only loosely related; it improves kind generalisation and the error messages from kind generalisation.
However, it became hard to disentangle them, esp since both affect many error messages. They validate together, but probably not individually. Nevertheless, the commit separation may help with navigation.