Skip to content

Implement Quick Look impredicativity

Simon Peyton Jones requested to merge wip/T18126 into master

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.

Edited by Sebastian Graf

Merge request reports