<html><body><div dir="ltr">Dear Committee,<div><br></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>Current status</i></div><div dir="ltr"><i><br></i></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr">> id :: forall a. a -> a</div><div dir="ltr">> id x = f @a x</div><div dir="ltr">> where f y = y</div><div dir="ltr"><br></div><div dir="ltr">In the past 3 years we’ve accepted two proposals which extend this ability:</div><div dir="ltr">- First to patterns <a href="https://github.com/ghc-proposals/ghc-proposals/pull/126">https://github.com/ghc-proposals/ghc-proposals/pull/126</a>, so we can write `id @a x = …`</div><div dir="ltr">- Then to lambdas <a href="https://github.com/ghc-proposals/ghc-proposals/pull/155">https://github.com/ghc-proposals/ghc-proposals/pull/155</a>, so we can write `id = \@a x -> …`</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>What is going on</i></div><div dir="ltr"><br></div><div dir="ltr">It seems that the accepted proposals were not quite right. We have two on-going proposals to <b>amend</b> the current ones:</div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/291">https://github.com/ghc-proposals/ghc-proposals/pull/291</a> 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).</div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/238">https://github.com/ghc-proposals/ghc-proposals/pull/238</a> 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 <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412">https://gitlab.haskell.org/ghc/ghc/-/issues/16734#note_203412</a></div><div dir="ltr">- <a href="https://github.com/ghc-proposals/ghc-proposals/pull/420">https://github.com/ghc-proposals/ghc-proposals/pull/420</a> amends the current behaviour of signatures in patterns (what happens if I write `id (x :: a)` ).</div><div dir="ltr"><br></div><div dir="ltr">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 <a href="https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932">https://github.com/ghc-proposals/ghc-proposals/pull/291#issuecomment-726715932</a> </div><div dir="ltr"><br></div><div dir="ltr">Note that this problem is arising in other places, too. For example #281, which adds visible `forall a -> ` (<a href="https://github.com/ghc-proposals/ghc-proposals/pull/281">https://github.com/ghc-proposals/ghc-proposals/pull/281</a>) is also talking about name resolution (see <a href="https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016">https://github.com/ghc-proposals/ghc-proposals/pull/281#issuecomment-884810016</a> for an example).</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr"><i>How should we proceed</i></div><div dir="ltr"><br></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr"><br></div><div dir="ltr">Kind regards,</div><div dir="ltr">Alejandro</div></div></body></html>