[ghc-steering-committee] #287: Simplify subsumption , recommendation: accept

[Spiwack, Arnaud]

I've now marked the proposal as accepted.

On Tue, Jan 21, 2020 at 8:43 AM Spiwack, Arnaud <arnaud.spiwack at tweag.io>
wrote:

> Support seems unanimous so far. Barring any counter-argument by then, I'll
> mark the proposal as accepted, with the short path, on Thursday.
>
> /Arnaud
>
> On Mon, Jan 20, 2020 at 7:08 PM Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
>> I am in support
>>
>> On Fri, Jan 17, 2020, 05:50 Spiwack, Arnaud <arnaud.spiwack at tweag.io>
>> wrote:
>>
>>> Dear all,
>>>
>>> As the shepherd for proposal #287 [
>>> https://github.com/ghc-proposals/ghc-proposals/pull/287 ], I recommend
>>> acceptance
>>>
>>> Summary
>>>
>>> The proposal is to remove a bunch of typing rules meant to make
>>> RankNTypes a bit more powerful (covariance and contravariance of the arrow
>>> constructor, as well as deep instantiation and deep skolemisation). The
>>> problem with these rules is that 1/ they complicate the type checker 2/
>>> They are implemented by performing eta-expansion during elaboration, which
>>> changes the semantics of program 3/ Dropping (some of) them is beneficial
>>> for the quick-look story (proposal currently on hold).
>>>
>>> The authors have tried this change on all of Stackage, and could come up
>>> with simple fixes (~300 lines of which) for all but 2 packages (namely,
>>> singleton, because of template haskell stuff, and labels for reason not
>>> well identified).
>>>
>>> Rationale
>>>
>>> The common point of all these features is that they jiggle the position
>>> of foralls around. Which sounds reasonable at first glance. But really,
>>> they tend to interact badly with other stuff (I don't remember the
>>> circumstances, but there was a discussion of deep instantiation and deep
>>> skolemisation in the context of linear types as well). Basically, they are
>>> rather fragile features, I'd rather we did without them.
>>>
>>> I think that 300 lines of simple fixes for all of Stackage is a very
>>> small number. So it is legitimate to consider this change to have low
>>> impact. Regarding the singleton, I'm sure Richard will be happy to fix it
>>> ;-) . Only labels remains. It shouldn't be a blocker.
>>>
>>> Remaining question
>>>
>>> There is one open question on the pull request thread. Namely, how to
>>> schedule the removal. Two paths are being discussed
>>>
>>>    1. Add a `-XLessSubsumption` flag, turn it off by default, then turn
>>>    it on by default in version n+1, then remove the subsumption rules
>>>    altogether in version n+3
>>>    2. Simply remove the code, preferably early in the release cycle,
>>>    communicate profusely.
>>>
>>> The thread participants seem to lean towards (2). The reason being that
>>> this is a change where it is easy to write code compatible with previous
>>> versions of the compiler (everything which compiles after this change also
>>> compiles before this change). Also, there is a preference for removing the
>>> relevant code sooner rather than later. But I'd like the opinion of the
>>> committee.
>>>
>>> Best,
>>> Arnaud
>>> _______________________________________________
>>> ghc-steering-committee mailing list
>>> ghc-steering-committee at haskell.org
>>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20200123/a7a6b089/attachment.html>