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

Hi committee, I re-recommend acceptance for this proposal. 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. Along with this primary change, there is some cleanup of (loosely) related syntax: - a type synonym declaration is now required to mention all kind variables on its left-hand side (previously, you could introduce a kind variable only on the right in some circumstances) - arity inference for type synonyms and families with trailing invisible quantifiers is simplified (you've never written such a thing, I'm sure -- and yet GHC currently has special handling for this bit of esoterica) - a type family equation must now mention all kind variables on its left-hand side (just like the new rule for type synonyms) - a type family equation must now determine instantiation of all kind variables via the left-hand side patterns (this vastly increases readability and avoids some confusing behavior) The cleanups can all break existing code. And so I posted on Discourse https://discourse.haskell.org/t/feedback-requested-about-breakage-type-varia... seeking community feedback. The feedback did not suggest this breakage would cause wide harm. And thus this re-recommendation of acceptance. Please let us know what you think. I will go on holiday after April 4, so I hope to accept this proposal then. Thanks! Richard

On Oct 25, 2021, at 3:24 AM, Spiwack, Arnaud wrote:

My weak objections are no match for Simon's strong keenness :-) .

I should say that, egoistically, I'd also like 5,6,7 to happen. I was only expressing concerns about the price.

On Fri, Oct 22, 2021 at 1:00 PM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: 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 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.com mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com mailto:simonpj@microsoft.com.)

From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Spiwack, Arnaud Sent: 21 October 2021 08:03 To: Richard Eisenberg mailto:rae@richarde.dev> Cc: ghc-steering-committee mailto:ghc-steering-committee@haskell.org> 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/425 https://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.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://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

I'm still in favour. Thinking back, this only breaks pretty advanced uses of type families and type synonyms that most users are unlikely to have stumbled across. There is a deprecation period which will make sure that we can transition most packages smoothly without holding the community back (some slow-changing packages will probably be missed, but hopefully not too many, in fact maybe it can be known by compiling all of hackage with the deprecation warning on and patched in time anyway). This should work. And the result is definitely much of an improvement compared to the current situation (which is a prototypical example of an aspect of Haskell where seasoned programmers show, with a smirk, to hardly-believing-it less experienced ones “did you know you could do this?”). /Arnaud On Thu, Mar 24, 2022 at 11:27 PM Simon Peyton Jones < simon.peytonjones@gmail.com> wrote:

I strongly support

Simon

On Thu, 24 Mar 2022 at 18:47, Richard Eisenberg wrote:

...

Hi committee,

I re-recommend acceptance for this proposal.

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.

Along with this primary change, there is some cleanup of (loosely) related syntax: - a type synonym declaration is now required to mention all kind variables on its left-hand side (previously, you could introduce a kind variable only on the right in some circumstances) - arity inference for type synonyms and families with trailing invisible quantifiers is simplified (you've never written such a thing, I'm sure -- and yet GHC currently has special handling for this bit of esoterica) - a type family equation must now mention all kind variables on its left-hand side (just like the new rule for type synonyms) - a type family equation must now determine instantiation of all kind variables via the left-hand side patterns (this vastly increases readability and avoids some confusing behavior)

The cleanups can all break existing code. And so I posted on Discourse https://discourse.haskell.org/t/feedback-requested-about-breakage-type-varia... seeking community feedback. The feedback did not suggest this breakage would cause wide harm. And thus this re-recommendation of acceptance.

Please let us know what you think. I will go on holiday after April 4, so I hope to accept this proposal then.

Thanks! Richard

On Oct 25, 2021, at 3:24 AM, Spiwack, Arnaud wrote:

My weak objections are no match for Simon's strong keenness :-) .

I should say that, egoistically, I'd also like 5,6,7 to happen. I was only expressing concerns about the price.

On Fri, Oct 22, 2021 at 1:00 PM Simon Peyton Jones wrote:

...

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.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)

*From:* ghc-steering-committee < ghc-steering-committee-bounces@haskell.org> *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 wrote:

Hi all,

I am the shepherd for proposal #425, https://github.com/ghc-proposals/ghc-proposals/pull/425 https://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.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, I didn’t hear any dissent, so I’ll mark this as accepted and will merge it now. Cheers, Joachim Am Samstag, dem 26.03.2022 um 16:10 +0100 schrieb Joachim Breitner:

Hi,

sounds good to me, thanks for the good summary.

Cheers, Joachim

Am Donnerstag, dem 24.03.2022 um 18:47 +0000 schrieb Richard Eisenberg:

...

Hi committee,

I re-recommend acceptance for this proposal.

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.

Along with this primary change, there is some cleanup of (loosely) related syntax:  - a type synonym declaration is now required to mention all kind variables on its left-hand side (previously, you could introduce a kind variable only on the right in some circumstances)  - arity inference for type synonyms and families with trailing invisible quantifiers is simplified (you've never written such a thing, I'm sure -- and yet GHC currently has special handling for this bit of esoterica)  - a type family equation must now mention all kind variables on its left-hand side (just like the new rule for type synonyms)  - a type family equation must now determine instantiation of all kind variables via the left-hand side patterns (this vastly increases readability and avoids some confusing behavior)

The cleanups can all break existing code. And so I posted on Discourse seeking community feedback. The feedback did not suggest this breakage would cause wide harm. And thus this re-recommendation of acceptance.

Please let us know what you think. I will go on holiday after April 4, so I hope to accept this proposal then.

Thanks! Richard

...

On Oct 25, 2021, at 3:24 AM, Spiwack, Arnaud wrote:

My weak objections are no match for Simon's strong keenness :-) .

I should say that, egoistically, I'd also like 5,6,7 to happen. I was only expressing concerns about the price.

On Fri, Oct 22, 2021 at 1:00 PM Simon Peyton Jones wrote:

...

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 pointsimonpj@microsoft.com will cease to work.  Usesimon.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 wrote:

...

Hi all,

I am the shepherd for proposal #425, https://github.com/ghc-proposals/ghc-proposals/pull/425, 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.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/