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.