[ghc-steering-committee] Scoping of types

[Alejandro Serrano Mena]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210723/467b5ade/attachment.html>