Implement Quick Look impredicativity
This MR implements Quick Look impredicativity (#18126)
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.