Sorry, I was not clear about the goal of the message. This all stems from the fact that Joachim asked me to shepherd #238. However, when trying to do so, I found that this was not the only proposal changing some of the scoping of types, but that there’s a lot going on with regards to that field.

My question to the Committee is: should we continue shepherding the proposals independently, or should we take some time to make a general judgment about how we want scoping to work on types, in the same way that we had a general Dependent Haskell proposal?

Regards,
Alejandro

El 29 jul 2021 16:38:07, Spiwack, Arnaud <arnaud.spiwack@tweag.io> escribió:
I'm not sure what way forward you are suggesting (and judging from the lack of response, it's probably not clear for the other committee members either).

Philosophically, there is a balance to strike between backward compatibility and consistency. I'd note however that all of the existing behaviour is gated behind `ScopedTypeVariables`, which is fairly stable, but not necessarily unmovable. I don't think breaking backward compatibility would be unsurmountable.

On Fri, Jul 23, 2021 at 11:50 AM Alejandro Serrano Mena <trupill@gmail.com> wrote:
Dear Committee,

There’s a lot happening right now in the GHC proposals repo about scoping of types in different elements in the language. Richard asked for our decision in #238, but following a very good suggestion from Joachim, I think it’s better to give an overview on what’s going on. In my opinion, this should lead to a consolidation of the different proposals into a unified design.


Current status

In Haskell 2010 there’s no way to refer to type variables introduced in a type signature. For a long time, GHC has shipped with -XScopedTypeVariables, which introduced scoping for types by prepending them with `forall`. We could then use it in other types, or as part of a type application if -XTypeApplications is on.

> id :: forall a. a -> a
> id x = f @a x
>   where f y = y

In the past 3 years we’ve accepted two proposals which extend this ability:
- First to patterns https://github.com/ghc-proposals/ghc-proposals/pull/126, so we can write `id @a x = …`
- Then to lambdas https://github.com/ghc-proposals/ghc-proposals/pull/155, so we can write `id = \@a x -> …`


What is going on

It seems that the accepted proposals were not quite right. We have two on-going proposals to amend the current ones:
- https://github.com/ghc-proposals/ghc-proposals/pull/291 proposes simplifications to type variable patterns. As I understand this would make type variables in patterns behave like term variables (cannot be repeated, occurrences in inner scopes shadow the outer one, and so on).
- https://github.com/ghc-proposals/ghc-proposals/pull/238 introduces -XTypeAbstractions, which make the combination of `forall` and `\@a` behave “as it should be”. But to be honest, I do not fully grasp the problems before, so neither how this amendment solves the problem; there’s a pointer to the GHC issue tracker where some incompatibility is discussed https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412
- https://github.com/ghc-proposals/ghc-proposals/pull/420 amends the current behaviour of signatures in patterns (what happens if I write `id (x :: a)` ).

So we have different ways to introduce new type variables: `f :: forall a. …`, `f @a = …`, `f = \@a -> …`, `f (x :: a) = …`; and it’s very unclear what the scoping mechanism for each one should be. I think the problem is characterised very well in the following comment by Simon PJ https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932 

Note that this problem is arising in other places, too. For example #281, which adds visible `forall a -> ` (https://github.com/ghc-proposals/ghc-proposals/pull/281) is also talking about name resolution (see https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016 for an example).


How should we proceed

Personally, I am a bit worried about having divergent designs on this matter, and the fact that no fewer than 2 amendments are being proposed (!) For me, the best would be to come up with a unified design of how scoping works for types, covering all possible ways to introduce and resolve them. I am happy to help with this.

Another important point seems to be how far we want to get from the current status quo (-XScopedTypeVariables make a type variable in a signature scope in its body, type variables in pattern signatures are always fresh), and how that fits with the overall -XDependentHaskell initiative.


Kind regards,
Alejandro
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee