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

[Vladislav Zavialov (int-index)]

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 <marlowsd at gmail.com> 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 at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee