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

[Joachim Breitner]

Hi,

I’m with Eric here.

Cheers,
Joachim

Am Freitag, den 17.01.2020, 09:16 -0500 schrieb Eric Seidel:
> I support acceptance as well. Changing the semantics of the program as part of type-checking is just bizarre and it seems like the impact in terms of required code changes is quite limited.
> 
> Given how easy the fixes appear to be, and the fact that the fixed program will compile just fine with older GHCs, I'm inclined to support option (2): ripping the code out immediately. I've left a comment on the PR asking if we can do so while providing helpful fixit hints to unaware users.
> 
> On Fri, Jan 17, 2020, at 08:49, Spiwack, Arnaud 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
> > 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/