[ghc-steering-committee] Quantified Constraints (#109). Recommendation: accept

[Richard Eisenberg]

The proposal for quantified constraints, #109, has been submitted for a decision.

This proposal generalizes the syntax for constraints to include forall-quantification and premise constraints. For example:

> data Rose f a = Branch a (f (Rose f a))
> 
> instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
>   Branch x1 c1 == Branch x2 c2 = x1 == x2 && c1 == c2

Note the `forall b. Eq b =>` in the constraint for this instance, which is necessary in order for the instance to be obviously terminating. There are *many* other motivations for this feature, dating back over a decade. Particularly pressing might be the fact that this feature will allow us to put `join` in the Monad type class, currently impossible due to the way roles work. See https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-us-put-join-back-in-monad/ for the details (which are not necessary in order to evaluate this proposal -- merely good motivation).

The proposal introduces -XQuantfiedConstraints, which will enable the new feature, though -XExplicitForAll will also be necessary if you wish to write a `forall` explicitly (as you likely will). There are some subtleties of the typing rules, but it all basically behaves as you would expect. Quantified constraints may induce a situation where GHC must choose one of two potential routes toward proving a goal; when this happens, the program is rejected (even if one or more of the routes would have been successful). Note that quantified constraints cannot introduce incoherence, as they do not create new instances.

Simon has already implemented this feature on a branch, and as I understand it, it's working swimmingly.

Recommendation: accept.

This feature has been wanted for a long time, is a natural extension of features GHC already has (roles, higher-rank types), and has been implemented cleanly.

As usual, I will take silence as agreement. I look forward to reading your comments.

Thanks,
Richard