Re: [ghc-steering-committee] Proposal #281: Visible "forall" in terms; rec: accept

Both of your suggestions (regarding lists and regarding Proxy) seem to require type information in order to resolve the meaning of an expression. Given `f e`, I’m assuming you want to parse/rename ‘e’ as an expression if ‘f’ is an ordinary function, and as a type if `f :: forall a -> …`. However, that would violate the Lexical Scoping Principle described in section 4.3.1 of the "Design for Dependent Types” proposal (#378), which states: "For every occurrence of an identifier, it is possible to uniquely identify its binding site, without involving the type system.” This principle is useful both in the implementation (it enables a clear delineation between renaming/typechecking) and when reasoning about programs. While it’s possible to violate it, I believe that writing `f (List Int)` is the lesser evil. Also, I don’t think that you’d need to "write `List Int` when it's a visible type argument, but `[Int]` everywhere else”. If consistency is an explicit goal, one can write `List Int` everywhere. - Vlad

On 29 May 2021, at 14:15, Simon Marlow wrote:

I support the goal of this proposal; indeed I would immediately use it in several places that I can think of off the top of my head.

But the name resolution aspects concern me. I forsee a lot of confusion if we can't write `[Int]` as a type argument with the usual meaning. The error message is likely to be super confusing if it has to talk about the difference between a promoted list type and the usual list type constructor, which have the same syntax. I'm not a fan of having to write `List Int` when it's a visible type argument, but `[Int]` everywhere else.

Would it be possible to require the leading quote to get the promoted meaning, otherwise defaulting to the usual meaning of `[Int]`?

Also could we defer name resolution until type checking for things like `Proxy`, so that the obvious thing doesn't require namespace gymnastics?

Cheers Simon

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