Re: [ghc-steering-committee] #425: invisible binders in type declarations; rec: accept

I'm in strong support. This tidies up the design nicely. I am particularly keen on 5,6,7; indeed I wrote a whole proposal about it, which Vlad has #included here https://github.com/ghc-proposals/ghc-proposals/pull/386 Simon PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.) From: ghc-steering-committee On Behalf Of Spiwack, Arnaud Sent: 21 October 2021 08:03 To: Richard Eisenberg Cc: ghc-steering-committee Subject: Re: [ghc-steering-committee] #425: invisible binders in type declarations; rec: accept I'm generally in favour. But I'm not convinced that the secondary changes (points 4-7) are worth it. They are certainly better place than we are today, but are they worth breaking existing code for? Point 5-7 can probably be replaced by warnings. I don't know about 4. On Tue, Oct 19, 2021 at 11:20 PM Richard Eisenberg mailto:rae@richarde.dev> wrote: Hi all, I am the shepherd for proposal #425, https://github.com/ghc-proposals/ghc-proposals/pull/425https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F425&data=04%7C01%7Csimonpj%40microsoft.com%7C32604dcfdde74a09b92608d99460fef7%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637703967362805934%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=qZtG9DdB6krhuKGwEnKuL0bPZr%2FYBr1jgRLIS1tb%2B5s%3D&reserved=0, proposing to add invisible binders in type declarations. The main payload of the proposal is to allow definitions like

data Proxy @k (a :: k) = Proxy

instead of today's

data Proxy (a :: k) = Proxy

which has no explicit binding site for k. This new syntax solves a number of smallish syntax conundra, as very well outlined in the proposal. In addition, the proposal includes two small unrelated tweaks to the syntax of type family instances; these are points (6) and (7) in the proposal. Both changes will break some obscure (but still realistic, knowing Haskell) programs, but both fixes are backward compatible. --- I recommend acceptance. The proposal is motivated nicely (do check out the examples) and solves a real problem. The new syntax fits in with other similar features. The small cleanups to existing syntax will lead to better error messages. The one drawback, as I see it, is that this proposal includes point (5), which is a breaking change to the way type synonyms work. Right now, we can say

type P = (Proxy :: k -> Type)

and GHC will infer P :: forall k. k -> Type. Under this proposal, you would have to write

type P @k = (Proxy :: k -> Type)

bringing k into scope explicitly. The fix is not backward compatible, and so I think this proposal should come with a migration strategy, where we warn about the former version for some releases before banning it. (Continuing to support it is possible, but it's very awkward to have a variable mentioned only in a synonym's right-hand side.) Sorry for the delay in producing this recommendation! Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committeehttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=04%7C01%7Csimonpj%40microsoft.com%7C32604dcfdde74a09b92608d99460fef7%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637703967362815898%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=PrFP%2BiICXUykrsrJFBKkKzD9i3bS9Jd4YNdbl6CDYp8%3D&reserved=0