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-boun...@haskell.org> On Behalf Of Chris Smith
Sent: 16 June 2021 14:39
To: GHC developers <ghc-devs@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?
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reply via email to