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.

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 -> …`

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).

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