[ghc-steering-committee] Proposal #274: Quicklook impredicativity, recommendation: accept

[Spiwack, Arnaud]

Dear all,

Last time around that we had a discussion about this proposal, the authors
asked to have some more time to revise a few things. Since then, the
proposal has been simplified, and the paper accepted (congratulations!).

Last time around, those of us who opined were mostly in agreement with
accepting the proposal, though there were some distracting complications.
Which have since been forked (and accepted) as proposal #287
<https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst>.
I do believe that this iteration of the proposal is a no-brainer. It simply
gives a clear semantics to the unspecified -XImpredicativeTypes. It’s
useful, and an implementation already exists (!3220
<https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220>).

The summary of the proposed specification is: to instantiate a type
variable to something of the form forall a. …, go through arguments and
look for an absolutely necessary such instantiation (which will happen when
there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t).

The only point which we may want to discuss is ($), which currently has an
ad hoc typing rule baked in the type checker. The proposal suggests
removing this baked in rule, and replacing it with making ($) always use
the -XImpredicativeTypes typing rule. An alternative, of course, is to
simply not treat ($) any specially, and require -XImpredicativeTypes to be
explicitly turned on when one wants runST $ do …. But, as the proposal
points out, this would break a lot of existing programs. So I agree with
the proposal’s choice.

In summary, I recommend accepting this proposal in its current state.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20200603/3466ab18/attachment.html>