Is simplified subsumption really necessary?

[Simon Peyton Jones]

rather, it's that it completely screws up my intuition about what should be valid Haskell.

I'm sorry to hear that Chris.   It's exactly backwards from what I would expect - the typing rules with simple subsumption are, well, simpler than those for complicated subsumption, and so one might hope that your intuition had fewer complexities to grapple with.

Maybe it's partly a matter of explanation and presentation.  Do you have an example of a case in which your intuition was screwed up by the simple subsumption rules?  Discussing in the abstract is often un-illuminating.

But wouldn't it be possible to choose a desugaring with seq that doesn't do so?

I just don't know how to do that.  Maybe someone else does.

Meanwhile, Quick Look<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/> depends strongly on simple subsumption.  And I'm very keen on QL.

Simon


From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Chris Smith
Sent: 16 June 2021 14:39
To: GHC developers <ghc-devs at haskell.org>
Subject: Is simplified subsumption really necessary?

This might be in the "ship has sailed" territory, but I'd like to bring it up anyway.  https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0287-simplify-subsumption.rst&data=04%7C01%7Csimonpj%40microsoft.com%7C6e04d0f9a068432fad8108d930cc2e1e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637594475810326243%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=r6RfLGB0CRXF%2FN%2FFvbu3uDoxg1i63oVXya2v6Zlqr7E%3D&reserved=0> says:

Suppose GHC lacked all four features, and someone proposed adding them. That proposal would never leave the launchpad.

Let's test that hypothesis.

I've been spending increasing amounts of time fighting against simplified subsumption while porting Haskell code to GHC 9.0.  It's not that any specific instance of this problem is hard to fix; rather, it's that it completely screws up my intuition about what should be valid Haskell.  It doesn't help that HLS still requires 8.10.4, so I usually don't find out I've broken my libraries for GHC 9.0 until continuous integration kicks in.  At this point, it's become fairly routine that my code that works fine with 8.10.4 is broken with 9.0, and this makes me sad.

Understandably, eta expansion reducing the strictness of terms is bad.  But wouldn't it be possible to choose a desugaring with seq that doesn't do so?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210616/8d7e63a2/attachment.html>