I was indeed confused! Apologies. But my main point remains: enumerating a list of inconvenient side effects and corner cases would be a great service. 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.) | -----Original Message----- | From: Vladislav Zavialov (int-index) <vlad.z.4096@gmail.com> | Sent: 27 October 2021 10:10 | To: Simon Peyton Jones <simonpj@microsoft.com> | Cc: Spiwack, Arnaud <arnaud.spiwack@tweag.io>; Richard Eisenberg | <rae@richarde.dev>; ghc-steering-committee <ghc-steering- | committee@haskell.org> | Subject: Re: [ghc-steering-committee] Proposal #281: Visible "forall" | in terms; rec: accept | | Simon, perhaps you’re thinking of another proposal that is currently | under committee’s consideration? | | Arnaud was commenting on #281, and you seem to be talking about #425. | | - Vlad | | > On 27 Oct 2021, at 12:05, Simon Peyton Jones via ghc-steering- | committee <ghc-steering-committee@haskell.org> wrote: | > | > There are a lot of inconvenient side effects and corner cases | > | > Arnaud, could you enumerate them? Even if (as I strongly hope) we | accept this proposal, it’s good to have a concrete list of things to | bear in mind. I for one do not have such list in my head. | > | > One principle that the proposal espouses (but perhaps does not call | out explicitly) is that it should be possible to write an explicit | binder for every in-scope variable. So instead of | > data T (a :: k -> k) = … I want to write | > data T @k (a :: k -> k) = … with an explicit binder | > for k. | > | > So I see the proposal as removing an ad-hoc wart in the language. | But I may be blind to the “inconvenient side effects and corner cases” | and I’d welcome a list of such cases. | > | > Simon | > | > | > PS: I am leaving Microsoft at the end of November 2021, at which | point | > simonpj@microsoft.com will cease to work. | > Usesimon.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: 27 October 2021 09:20 | > To: Richard Eisenberg <rae@richarde.dev> | > Cc: ghc-steering-committee <ghc-steering-committee@haskell.org> | > Subject: Re: [ghc-steering-committee] Proposal #281: Visible | "forall" | > in terms; rec: accept | > | > I've been struggling to have an opinion on this PR. I'm very | sympathetic to the goal of the proposal (and this latest rendition of | the proposal is a really good document). There are a lot of | inconvenient side effects and corner cases (but, to be fair, these are | not special to this proposal: they are inherent to the dependent types | plan). But I'm fairly convinced that this is the best possible | approach, or close enough. | > | > | > | > So yes, I don't really feel strongly about it. But on balance, I | think that I'm in favour.