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

[Spiwack, Arnaud]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20200117/089dea75/attachment.html>