Yes, I think this proposal meets the criteria of "needs revision" -- if at least to clarify all the points that have been raised.

On Oct 15, 2020, at 11:41 AM, Iavor Diatchki wrote:

I agree with Arnaud's observations.

It seems that the discussion on this proposal is not converging toward a solution, and now more folks from the community have jumped in, so my inclination would be to move this proposal back to the "needs revision" phase as Simon M suggested earlier. Thoughts?

-Iavor

On Tue, Oct 13, 2020 at 12:37 AM Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io> wrote: There has been conversation to this effect on the Github PR, for a day or so, starting at https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-7070335... https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-7070335... .

But I wanted to point out that there are really two, interlocked, yet distinct, parts in this proposal. 1. Having a `forall a ->` construct for types of terms 2. How is `f blah` parsed if `f` has type `forall a -> …`?

I am definitely sympathetic to (1). As much as I like my `f @…`s I am bound to admit that it produces error messages from the 7th Circle of Hell. And, since it's a very useful pattern, making it "official" is rather neat a plan on paper.

But (2) is very very difficult, because we have really two grammars at play here: the grammar for term, and the grammar for types (I'll conflate grammar and name resolution in the following). In the `f @…` style, we switch to the type grammar to parse whatever's in the `@`. But if we want to to write type applications in the `forall a->` case as `f a`, then we sort of have to parse `a` as a term (though there is some leeway in name resolution). And that introduces all sorts of potentially weird behaviour (see the link above for a good documentation of what). Part of the difficulty, I should stress, is that, in types the apostrophe `'` means: I'm speaking of a data constructor, not a type constructor. Whereas in terms, it means: I'm opening a Template Haskell slice.

Part of the impetus for the proposal actually going in the direction of parsing the type argument as a term, is the desire to eventually merge the terms and types grammars. I don't know how widespread this desire actually is (maybe this is something we should speak about). In my personal opinion, it's not a very plausibly achievable goal, nor is it particularly necessary for dependent types. (It does, of course, have a number of advantages, which is why Coq, Agda, and Idris do have a single grammar indeed).

I think that I'd be happier if we had a sigil to switch between the type grammar and the term grammar. But, here, the issue is that nice sigils are harder and harder to come by.

My point, though, is that while this proposal may look like it has a small scope, it actually is a fairly large and intricate proposal, and requires quite a bit of attention.

/Arnaud

On Mon, Oct 5, 2020 at 7:25 PM Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: I've been following the discussion and I think we should keep it in the "committee review" phase because 1. The discussion is due to questions from the committee members, and 2. Even though it seems like a lot, mostly it's been along the lines of clarification and better phrasing of things, rather than big changes to the proposal

I don't feel strongly about it, so if others also think we should move it to the discussion phase, I'd be happy to do so, I just don't want to loose the steam we seem to have gathered :)

Let me know, -Iavor

On Mon, Oct 5, 2020 at 2:38 AM Simon Marlow mailto:marlowsd@gmail.com> wrote: There seems to have been a lot of ensuing discussion on this one, should it go back into the discussion phase?

On Fri, 2 Oct 2020 at 20:06, Richard Eisenberg mailto:rae@richarde.dev> wrote: I'm in support of this proposal, but I've pushed back on a few softer points. I've commented on GitHub.

Richard

...

On Oct 1, 2020, at 1:07 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

Proposal #281 is ready for review by the committee. My recommendation is to accept it, I've written a summary of my understanding to the proposal and my recommendation on the GitHub thread, accessible through these links:

https://github.com/ghc-proposals/ghc-proposals/pull/281 https://github.com/ghc-proposals/ghc-proposals/pull/281 https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000... https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/000...

Let the discussion begin!

-Iavor _______________________________________________ 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://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ 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://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ 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://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