Introduce -XTypeAbstractions, limiting -XScopedTypeVariables

[goldfirere]

Recent discussion (on only tangentially related features) has brought to light that the accepted proposal for binding type variables does not fly. I have amended the proposal to fix the problem. Basically, we cannot have both \ @a -> ... and the scoping behavior of forall. This new version introduces a new extension -XTypeAbstractions that will control the new syntax, as well as disable the feature of -XScopedTypeVariables that brings foralld variables into scope.

Original, accepted proposal
Discussion on original proposal
Rendered new proposal

[int-index]

I agree with what's written here, except for one bit.

This new version introduces a new extension -XTypeAbstractions that will control the new syntax, as well as disable the feature of -XScopedTypeVariables that brings foralld variables into scope.

These emergent interactions between extensions aren't good. And what is left of -XScopedTypeVariables at this point? Pattern signatures!

Let's just accept #119 for -XPatternSignatures, and mark -XScopedTypeVariables incompatible with -XTypeAbstractions.

[int-index]

And what is left of -XScopedTypeVariables at this point? Pattern signatures!

Actually, this is not correct. Pattern signatures alone would not enable the expected scoping behavior:

f (x :: a) =  ...   -- either rejected or 'a' not in scope

Therefore, disregard my previous comment. I'm OK with the proposed amendment as is.

[Ericson2314]

Oh this is great! I preferred this design for aesthetic reasons anyways.

And what is left of -XScopedTypeVariables at this point? Pattern signatures!

I do still like this idea.

Is there precedent for one extension disabling part of another? I do generally like it when the set of extensions mapped to the set of accepted programs is monotonic.

Perhaps a better argument is it would be nice to deprecate forall binding in term, but that's awkward to do if we don't want to change the meaning of -XScopedTypeVariables and yet require both -XScopedTypeVariables and -XTypeApplications to get the desired behavior.

Actually, this is not correct. Pattern signatures alone would not enable the expected scoping behavior:

f (x :: a) =  ...   -- either rejected or 'a' not in scope

That makes sense to me. I'd think one would have to write something along the lines of:

f @(... a ...) (x :: a) =  ...   -- accepted, 'a' in scope

Likewise, I'd expect id :: a -> a would be an error to me if we had an extension which required explicit binding in types. (And I wish to write that extension if for no other reason than teaching.)

[int-index]

That makes sense to me. I'd think one would have to write something along the lines of:

f @(... a ...) (x :: a) =  ...   -- accepted, 'a' in scope

That's not equivalent, though. Compare:

f :: Bool -> Bool
f (x :: a) = True    -- ok, a ~ Bool

g :: Bool -> Bool
f @a (x :: a) = True     -- rejected, no 'forall' to go with the @a binder

[goldfirere]

I do generally like it when the set of extensions mapped to the set of accepted programs is monotonic.

That's already not true for a number of reasons. -XMonoLocalBinds, -XRebindableSyntax, -XTemplateHaskell (which steals syntax), etc.

What is odd about this new proposal is that -XTypeAbstractions always will override the -XScopedTypeVariables behavior, regardless of the ordering of extensions. In contrast, -XTypeFamilies implies -XMonoLocalBinds, but a user can say -XTypeFamilies -XNoMonoLocalBinds and get the behavior they want. (I did this once and it made my life better.)

Of course, we could allow -XScopedTypeVariables to dislodge (part of) the -XTypeAbstractions behavior. The only part that's problematic is when we use a type abstraction near a forall:

f :: forall a. a -> a
f @a x = ...   -- problem

g = ((\ @a x -> ...) :: forall a. a -> a)  -- problem

hr :: (forall a. a -> a) -> ...
hr = ...

j = hr (\ @a x -> x)   -- hunky dory. The `forall` does not scope here!

So maybe that suggests this breakdown:

• -XPatternSignatures: allow :: in a pattern
• -XPatternTypeVariables: implies -XPatternSignatures and allows the binding of a type variable in a pattern. These type variables will be bound to arbitrary types (not only other variables).
• -XMethodTypeVariables: allows type variables in instance heads to scope over methods and type variables in a class head to scope over method defaults
• -XScopedForAlls: allows forall to bring tyvars into scope in function bodies and expressions with signatures
• -XScopedTypeVariables: Catch-all extension that implies all of the above
• -XTypeAbstractions: Enables binding type variables with @a syntax. Implies -XNoScopedForAlls.

With this approach, a user could specify XTypeAbstractions -XScopedForAlls and then get type abstractions in the higher-rank scenario, but not in any scenario with an explicit forall. This would work just fine.

I would also favor coming up with a deprecation plan for -XScopedForAlls. Or maybe not, since it's used so widely. At least new code could be written to avoid it, and individual style guides could forbid it, if they so choose.

[int-index]

I'm skeptical of supporting a configuration where -XScopedForAlls and -XTypeAbstractions are enabled simultaneously, but the latter is limited to the higher rank scenario. We're back to the non-local interactions between extensions (in one way or the other).

Let's just roll with the current proposed amendment.

[goldfirere]

We're back to the non-local interactions between extensions (in one way or the other).

Not really. What -XScopedForAlls means is that xyz :: forall a b c. blah really means \ @a @b @c -> xyz. Indeed, this is essentially the specification of -XScopedForAlls.

The code implementing -XTypeAbstractions won't even have to check whether -XScopedForAlls is enabled. Suppose we've written (\ @a x -> (x :: a)) :: forall b. b -> b with -XTypeAbstractions -XScopedForAlls. GHC will bring b into scope in the body of the annotation, and then check \ @a x -> (x :: a) against the type b -> b, where b is a skolem. This will fail, because we allow \ @a only when checking against a forall type. With -XScopedForAlls off, we would check against forall b. b -> b, and then all would work.

[int-index]

What's the behavior of -XScopedForAlls with regards to TLKSs? Does it take arity into account or does it instantiate blindly?

That it, does this code

type T :: forall b. b -> Maybe b
type T = Just :: forall a. a -> Maybe a

get desugared into

type T :: forall b. b -> Maybe b
type T @b = Just :: forall a. a -> Maybe a

and fail?

It would work with the AScopingErr trick we discussed.

I need to know the full story, both for terms and types, to make progress on the implementation of TLKSs.

I don't have too strong an opinion on the matter, but I'd like something simple rather than six extensions with intricate interplay between them (-XPatternSignatures, -XPatternTypeVariables, -XMethodTypeVariables, -XScopedForAlls, -XScopedTypeVariables, -XTypeAbstractions).

Perhaps:

• The -XScopedTypeVariables flag continues to have its current meaning: scoped forall in terms, no effect whatsoever in types.
• Type abstractions do not need a new extension. There's a straightforward desugaring for scoped foralls, as you have shown:

  xyz :: forall a b c. blah  ==>  \ @a @b @c -> (xyz :: blah)
  

  Just keep at it in spite of user-written type abstractions. For example,

  f :: forall a. a -> a
  f @b x = ...   -- problem
  

  is mapped to

  f @a @b x = ... -- no problem, just a type error
  

  It is a type error because the @b binder does not have a matching forall in the user written signature.
  Given the fact that -XScopedTypeVariables only looks at the first forall, we can disable it with an empty forall., therefore the following is valid:

  f :: forall. forall a. a -> a
  f @b x = ...   -- no problem
  

  This time @b is a binder for forall a..
• To get rid of the forall. workaround, introduce a new extension -XScopedForAll (not -XScopedForAlls, it's singular for consistency with -XExplicitForAll) tightly coupled with -XScopedTypeVariables, which controls the forall scoping part of it. That is, -XNoScopedForAll disables forall scoping in terms (there's nothing to disable in types) and forall. is no longer needed.
• In a future release make -XNoScopedForAll the default.

[simonpj]

Gah. I'm lost again

Recent discussion (on only tangentially related features) has brought to light that the accepted proposal for binding type variables does not fly

OK so where is "the accepted proposal"?

• I start on the GHC proposals home page.
• From there I can see a link to the list of accepted proposals.
• Scrolling down that list I see "Binding type variables in lambda-expressions ". Maybe that's the one.
• Bother, no, that's the discussion about the proposal. Click on the Rendered link.
• And I get a 404 page not found.

There has to be an easier way than this to find the text of an accepted proposal!

Plus, maybe this is a snapshot of the exact accepted propsoal, and Richard has a modified version.

[goldfirere]

The accepted proposal and a rendered version of the update.

Apologies that these were not more readily available. And I've updated the link in #155.

[goldfirere]

I say -XScopedForAlls (yes, I know that -XExplicitForAll is singular, and that's always bothered me. I didn't see a need to repeat that mistake, but others may feel differently) should affect types just like terms. So the desugaring is exactly as you suggest in #238 (comment).

But that's just my current opinion at the moment, and this all may yet evolve.

[simonpj]

There has to be an easier way than this to find the text of an accepted proposal!

What is the canonical way to do this? (Admittedly, this is a tangent to the main purpose of this ticket.)

[simonpj]

The more I think about the big-lambda proposal, the less I like it. This unexpected interaction with forall-scoping has taken me aback.

---

Leave aside scoped type variables for the moment. Here are some questions.

f :: forall a b. a -> b -> b
f = let { stuff } in \@a. 
      case thing of
         True -> \x y. y
         False -> \@b. \ p q. q

I assume this is supposed to typecheck (but only if there is a signature!). But note that

• Currently TcExpr.tcPolyCheck with a CompleteSig (which is the relevant code path) always skoelmises the type immediately. Now it can't do that.
• Well, it can (and must) if there are any argument on the LHS. So we we need an extra case when there are no arguments, then we must pass in a non-skolemised type polytype, bypassing tcMatchesFun (which also skolemises).
• Then we'l get to tcPolyExpr. Oh! It skolemises too, and we mustn't do that either.
• But then when we get to the lambda, or anything else, we must skolemise.

Probably this is all do-able. But it's a change that potentially affects a lot of code, much more than I realised.

---

What about pattern bindings? Am I allowed

f :: forall a. a ->a
(f,g) = (\@a \(x:a). x,  blah)

I'm guessing not, but the proposal is silent. (Forall-scoping doesn't work for pattern bindings, incidentally.)

---

I was on the fence about this big-lambda thing; now I'm mildly against. Esp as it only works in "checking mode", so it doesn't satisfy the "you can do System F" goal. We have so many other fish to fry, I rather wionder if we should park this one. (To mix metaphors.)

[goldfirere]

I do expect there to be a non-trivial implementation burden, but I don't think the resulting code will be any worse (i.e. more complex) than what we have now. To implement type applications, we needed lazy instantiation. To implement type abstractions, we naturally need lazy skolemization.

If you're bothered by the "checking" mode requirement, we could think harder about @gridaphobe's suggestion in the committee discussion:

Why not say that \ @a -> body infers the type forall a. ty where body :: ty, and let unification handle the rest?

I think that might work, but I'd want to draw some typing rules to be sure. Would that sway you?

[simonpj]

I think some typing rules would be a very good thing!

I'm not dead set against this. I just feel uneasy. And that makes me wonder if we might be better spending our finite budget of intellectual cycles elsewhere, since this has turned out not to be the "quick win" that I initially thought it might be.

[gridaphobe]

I've updated the description of this proposal with a link to the rendered rich-text diff, which is pretty handy.

Apologies that these were not more readily available. And I've updated the link in #155.

I think this suggests a useful addition to the protocol for accepting (or rejecting!) a proposal. The link at the time of discussion will point to the author's fork of this repo, which they might well update or delete in the future. We should update the "Rendered" link in the PR with a link to the permanent home of the proposal. This suggests that we ought to also keep a store of rejected proposals too for easy future reference. (ping @nomeata)

---

I'm still pretty confused as well though. The proposal doesn't seem to explain what the problem is with having both forall binders and @ binders, unless it's in this single sentence:

One wrinkle is that, according to the rules in the Visible Type Application_ paper, type variables quantified by a forall in a type signature get brought into scope before we check the term.

But this doesn't sound like a problem to me. It sounds like the forall binder would be brought into scope first, and then the @ binder would come into scope, possibly shadowing the forall binder.

Oh, there's also this sentence that I missed at first.

Note that limiting the behavior of -XScopedTypeVariables is necessary if we think about where type variables are brought into scope. Are they brought into scope by the forall? Or by the @a? It can't be both!

Why not? We allow shadowing at the term level, and also at the type level. This feels very much like shadowing to me.

[nomeata]

There has to be an easier way than this to find the text of an accepted proposal!

What is the canonical way to do this?

Thanks for pointing this out, I change the List of accepted proposal so something accurate (albeit less pretty).

[int-index]

I say -XScopedForAlls should affect types just like terms.

@goldfirere That's impossible, we don't have Λ in types. You seem to suggest that

Just :: forall a. a -> Maybe a

maps to

\ @a -> (Just :: a -> Maybe a)

and gets rejected for lack of Λ?

Or do we map to AScopingErr? Then we should map to AScopingErr in TLKSs, too. Therefore, -XScopedForAlls would not accept any new type-level programs, it would simply change the error message from "not in scope" to "no big lambda".

[goldfirere]

About TLKSs: I say that having forall in a TLKS works just like it does in terms. For our purposes, we do have a lambda in types here, because we can bind type variables in the LHS of data type declarations. forall outside of a TLKS should do the AScopingErr thing.

I have added some text to the proposal about why we can't have both. I was secretly hoping that vigorous waving of hands (and with an exclamation point!) would allay concerns, but I was rightly mistaken.

[int-index]

About TLKSs: I say that having forall in a TLKS works just like it does in terms.

In terms, we don't have to worry about the arity. I say we want the following code to be accepted:

type T :: forall a. a -> Maybe a
type T = Just :: forall a. a -> Maybe a

And it's easy to make it accepted: map a to AScopingErr in the TLKS.

I think the rule in types should be:

• Scoped forall works like in terms for variables in TLKSs that fall within the arity of the tycon. Other variables are mapped to AScopingErr.

"Other variables" are variables in TLKSs that cannot be instantiated due to the inferred arity, and variables outside TLKSs.

This accepts more programs than the naive "just like it does in terms" rule.

[goldfirere]

I think the TLKS issue was resolved elsewhere, and I'd like to return this conversation to the proposal at hand, which is concerned with the term-level, not the type level. Any further commentary before we go to committee? Thanks!

[Ericson2314]

@goldfirere what about your alternative with many more extensions? (Meta: how do alternatives go to the committee when an existing proposal is being amended?)

[simonpj]

In my comment above I asked about pattern bindings. The proposal remains silent. Could you add language to say what is supposed to happen?

[goldfirere]

This needs attention from me, but I don't have attention to give this week. It is not abandoned, though. I shall return! (Next week, likely.)

[sgraf812]

I'm not sure if this is the right place to put this, but after talking to @goldfirere I'll post my own motivation for this: https://stackoverflow.com/questions/50159349/type-abstraction-in-ghc-haskell

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}

module Foo where

f :: Int -> (forall f. Functor f => Secret f) -> Int
f x _ = x

g :: (forall f. Functor f => Secret f) -> Int
g = f 4

type family Secret (f :: * -> *) :: * where
  Secret f = Int

This (the binding for g, in particular) currently doesn't type-check. We'd need a binding construct and 'eta-expand' the existential type parameter @f. Thinking I hit a bug (I had expected that the eta-reduced form should work anyway), I opened https://gitlab.haskell.org/ghc/ghc/issues/15119, but this was closed because we didn't have the expressivity at the time required to accept the program.

I'd really like this to become a thing, if only for reasons of symmetry with -XTypeApplications.

[goldfirere]

@cdsmith Hopefully this new version -- which does not gut -XScopedTypeVariables nearly as much, is more acceptable.

Separately, I'm not exactly sure what you're asking about, above. Perhaps this will help: in the expression (\ @a -> expr) :: forall b. ty, suppose we wish to bring b into scope. Then, what type do we check \ @a -> expr against? Is it just ty? Then the @a part is surely not going to work out. On the other hand, if we check \ @a -> expr against forall b. ty, what does it mean to have b in scope when we have a type forall b. ty around, where b is locally bound? I really don't know. I thus propose simply not to bring b into scope (and to check \ @a -> expr against forall b. ty). And, in this new version, that's the only change to -XScopedTypeVariables.

[RyanGlScott]

(I'm reading this proposal for the first time a bit late, so I apologize if I ask questions that have already been discussed.)

I want to make sure that this proposal is able to encompass all of the use cases that currently require ScopedTypeVariables. Based on my reading of this GHC User's Guide section, that consists of:

1. Declaration type signatures
2. Expression type signatures
3. Pattern type signatures
4. Class and instance declarations

As I understand it, XMethodTypeVariables completely covers use case (4), and -XPatternSignatureBinds completely covers use case (3). Use case (2) is discussed in the proposal in the sense that there is a way to migrate expression type signatures using ScopedTypeVariables over to using TypeAbstractions.

I'm least sure about use case (1). The particular case of function declaration type signatures is covered at length in this proposal, but there's surprisingly little in the way of pattern synonym declaration type signatures. For example, suppose I define a pattern synonym that uses ScopedTypeVariables/ScopedForAlls:

pattern J :: forall a. a -> Maybe a
pattern J x <- Just (x :: a)

Is it possible to convert this code over to use TypeAbstractions instead? My hunch is that you would be able to write something like this:

pattern J @a x <- Just (x :: a)

However, the proposal only discusses the changes needed for the funlhs BNF production, which covers function LHSes but not pattern synonym LHSes. Is this omission intentional? I would suspect that you would need to change the pattern_synonym_lhs Happy production in GHC's parser as well, but this assumes that the proposal is meant to cover this use case.

[JakobBruenker]

From the proposal:

If you have a function f :: forall {k} (a :: k). ..., you will have to rely on the old behavior of -XScopedTypeVariables to bring k into scope in f's definition, or you will have to use a pattern signature. This is regrettable but seems an inevitable consequence of the {k} notation.

Is there a reason not to allow @{k} in in the lhs of an equation? It admittedly is not reflected by how inferred variables work with visible type application syntax, but then, neither is @(..).

I think the proposal is also a bit unclear on how @(..) and -XScopedForAlls interact for inferred variables, seeing as inferred variables are bound by both. Edit: Actually, I was looking at an old version, it doesn't say anymore that -XScopedForAlls works for inferred variables, and I now realize that @(..) counts as @ in prefix form that disables -XScopedForAlls

[cdsmith]

@cdsmith Hopefully this new version -- which does not gut -XScopedTypeVariables nearly as much, is more acceptable.

@goldfirere For my part, I'm happy with either of the two accommodations: adding @(..) or making sure that forall binding still works when TypeAbstractions is enabled (but not used). Doing both is even better, since it make migration easier while also leaving a path to a more consistent world, since it's definitely a wart that forall will now bind type variables in some cases but not others. So this definitely addresses my concerns, twice over.

Me earlier confusion was because I didn't realize that expression signatures bound variables with ScopedTypeVariables at all, and it seems very odd that they do so. I certainly don't object to its no longer doing so in this proposal.

[maralorn]

I am a bit surprised by the @(..) solution. Aren‘t record puns with {..} considered harmful?

Is that a niche opinion or how might problems with that be different on the type level?

[ramirez7]

I am a bit surprised by the @(..) solution. Aren‘t record puns with {..} considered harmful?

Is that a niche opinion or how might problems with that be different on the type level?

RecordWildCards is a pretty commonly-used extension (for good reason - it's nice!)

There are some corners of Haskell-dom that "consider it harmful," but they are mostly driven by corporate-style programming where you must accommodate an ever-changing large-ish team. Such a situation incentivizes working with a niche but standardized subset of the language. I wouldn't say RecordWildCards is harmful as a rule, but I can see how in such a situation you would want to avoid it. The same goes for implicit imports, but they too are still plenty useful in Haskell programming.

That said, the main reason for the "considered harmful" afaiu is that wildcards potentially pollute scope in hard-to-understand ways (especially when used with let and where), which doesn't seem like as much of an issue here with type variables.

[davidsd]

Forgive me if this is tangential to this proposal, but something that has always confused me is: why isn't the scoping behavior of ScopedTypeVariables on by default, even without the forall? That is, why can't we have

id :: a -> a
id x = (x :: a)

To me, this is the most intuitive meaning of the type signature on the first line, and it makes that type signature the "single source of truth" for the names of the types below. It seems like this is the situation that we are trying to replicate with @(..).

[Ericson2314]

@maralorn the @(...) is strictly less harmful than the scoped type variables we have today: unlike with record wildcards the explicit field names are somewhat local (next to the definitions in the same module), and the @(..) is at least a reminder saying "look up!" where one might miss whether there was a forall above otheerwise.

[Ericson2314]

@davidsd Originally the choice was I believe due to backwards comparability. But while I'm happy to discard that, i am still not terribly found of automatic free variable binding like that. It is quite fragile, and all the more so when the variables are bound with a larger scope.

Note with this proposal

id :: a -> a
id @(..) x = (x :: a)

will work, so you can skip the forall if you want.

[davidsd]

@Ericson2314 Could you give an example of what you mean by fragile?

Often when editing a function, I realize I need access to one of the type variables in the arguments. I then have to scroll up to the type signature and add forall m a b p q r . ..., making the type of that one function a bit uglier than the others in the module. I also often forget to list a type variable that's in the signature somewhere, and have to contend with a few rounds of ghc errors.

Under this proposal, @(..) at the definition sites would replace forall m a b p q r . ... in the type signature. This makes me happy because it avoids the problem of scanning the type signature for free variables and listing them out in a forall. It would also make the type signatures of my program look more uniform, and this aids readability. On the other hand @(..) is a somewhat noisy string of symbols, and I am not very excited to add extra symbolic noise to the definitions.

What I really want almost 100% of the time is the ability to access type variables from the type signature in the body of my functions. forall m a b p q r. is an annoying incantation to achieve this. The proposed replacement @(..) is perhaps less annoying, but I still don't understand the need for an incantation at all (unless one wants to modify the order of the type arguments).

(By the way, I am not trying to argue against the main motivating examples of this proposal, such as usage = higherRankF (\ @a x -> ...), which are very compelling.)

[cdsmith]

Often when editing a function, I realize I need access to one of the type variables in the arguments. I then have to scroll up to the type signature and add forall m a b p q r . ..., making the type of that one function a bit uglier than the others in the module.

This is, indeed, a bit annoying. It's the combination of the forall-or-nothing rule (which makes perfect sense without scoped type variables) with the unfortunate second use of forall to bind type variables. The proposal's suggested @(..) to bring variables into scope is slightly nicer because you don't have to repeat the entire variable list and it's specific to just one binding where you might need the variables. That said, it still brings everything into scope when you only really wanted one. The proposal also (as its core suggestion) offers positional type variables as an alternative to bring just one into scope. Especially if it's the first type argument, but if not then you can write f @_ @_ @_ @m. It's rather ugly, but oh well.

At the risk of too much piling on random ideas, I think it would be awesome to have something like @{m} that means "bind the variable called m in the type signature, regardless of its position". This is consistent with the use of braces to mean a non-positional type variable. I think I might even like this better than @(..)

(There are some subtleties: This should work for all type variables, regardless of their explicitness. It probably should not consume the argument, so that f @{a} @b would mean that a refers to the variable called a in the type signature, and b refers to the first positional type variable, whatever its name in the signature. If a is itself the first positional type variable, then a ~ b. IMO, syntactic consistency would then suggest using @{..} instead of parentheses for @goldfirere's wildcard operator, if it's still implemented.)

[goldfirere]

@RyanGlScott

Pattern synonyms. Yes. Fixed now.

@JakobBruenker

Is there a reason not to allow @{k} in in the lhs of an equation?

The whole reason inferred variables exist is because we cannot pin down their ordering. Allowing @{k} in the LHS of an equation means there would be an ordering. Here is an example:

data Proxy a = MkProxy

f :: Proxy a -> Proxy b
f @{k} = ...

What does the k bind to? f's type has two inferred variables: the kind of a and the kind of b. (It also has two specified variables: a and b.) But now we have no idea which one should be called k in the body of f. You might say that you have to write the quantification over the inferred variable explicitly in the type signature in order to bind it in the definition, but now you've just introduced a middle ground between specified and inferred: explicitly inferred, where a definition can bind explicitly inferred variables with @{k}, but not inferred inferred variables. While possible, I do not want this.

@maralorn

I personally find record puns questionable (though I still use them sometimes) for two reasons:

1. A record pun introduces shadowing whenever there are field selectors (which is most of the time). This is confusing, because the punned name even has a different type than the unpunned name. I have been tripped up by this in practice.
2. A variable brought into scope by a record pun has no easily found binding site. When I've been reading code I'm less familiar with, I see a variable and want to know where it came from. If it came from a record pun, I have to search for a long time. I have been tripped up by this in practice.

Neither problem occurs with this new syntax:

1. There is no similar shadowing.
2. While the location a variable is brought into scope is a bit murky here, a textual search will find the variable mentioned in a binding site -- it's just that the binding site is in the type instead of in the definition. This is mildly confusing, but not nearly as bad as record puns. And, as @Ericson2314 points out, this is still an improvement from the status quo, where at least a @(..) tells you that something special is happening.

@davidsd

Yes, if we were happy to toss out backward compatibility, perhaps we would just always bring those type variables into scope. When I've programmed in dependently typed languages (that have a feature like the one I'm proposing here), I still sometimes wish the type variables just popped into scope without any effort. But @(..) is an improvement on those other languages, which lack such a construct. I'm not totally sold on automatic scoping always, but I can duck the question here because doing so would be backward incompatible anyway.

@cdsmith

Yes, I see the virtue in your @{m} construct. I'm not excited to have both mechanisms, though. Consider

f :: forall a b. Bool -> a -> b -> ...
f @b True (x :: b) _ = ...
f @{b} True _ (y :: b) = ...

In the two equations, the b means something different! The first equation binds b to the first type parameter of f, while the second equation binds b to its second. That's too subtle for my taste. I could imagine something more like @{m1 = m2}, where m1 is the name used in the type signature, and m2 is the local name bound here. (They, of course, could be the same.) Idris and Agda allow this. But such notation is just as useful at call sites as it is at binding sites, and I'd rather thinking about a holistic approach to named parameters first. Furthermore, I've been thinking for some time now that it's good to reserve { blah = wurble } syntax for anonymous records -- which might exist in types and thus want a @ prefix.

My bottom line here: yes, I agree that would be nice, but 1) I don't see a good way forward here and 2) the feature you want would be generally useful elsewhere, too, so it probably belongs in a separate proposal.

[cdsmith]

My bottom line here: yes, I agree that would be nice, but 1) I don't see a good way forward here and 2) the feature you want would be generally useful elsewhere, too, so it probably belongs in a separate proposal.

Sure. I might argue that the similarity between @b and @{b} isn't really so bad... but that conversation is definitely a bit far afield of this proposal's intent. I wonder if the right answer here is to go ahead and just accept that in the short term, this is going to be a poor fit with ScopedTypeVariables, but that we have some reasonable ideas about what to do to fix that, and then defer that entire discussion (including @(..), which Simon didn't seem too keen on, either) to a later proposal. In order to accept this proposal, IMO, all that's needed is to conclude that we're unlikely to end up with an indefinite fork.

[goldfirere]

I don't see how the proposal, as currently written, introduces even a short-term fork. This version is, I believe, compatible with today's -XScopedTypeVariables, with the exception of their use in expression signatures (which should be rare). I like @(..) and would want to keep it in, but I'm also OK with losing it, if we agree that such an idea is better kept until later.

Is there a forky aspect of what's here now that I'm missing?

[Ericson2314]

BTW, there is a conflict, I think because of the way the proposals were renumbered long ago to patch the PR numbers.

[goldfirere]

I think this is ready to submit to the committee, @nomeata .

[nomeata]

I'm currently away from a laptop for 3 weeks, and while I could do the steps by email, it's a bit tedious. Maybe @serras can be going through the motions (label, assign, send mail to list), and either shepherd it yourself, or pick one of your liking.

[nomeata]

I am slightly delaying the process for this proposal, because it’s part or a growing jungle of proposals, and maybe we can do better: https://mail.haskell.org/pipermail/ghc-steering-committee/2021-August/002571.html

[nomeata]

Update: @goldfirere plans to unify proposals #126, #155, #285, #291, #238, #420

[nomeata]

Obliviated by #448