Amend #448 so -XPatternSignatures does not include implicit bindings

[Ericson2314]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

2nd in a series of #448 amendments, following up from #604, building towards #532

This proposal scales back #448 's reintroduced -XPatternSignatures so that it does not include pattern signature bindings. Pattern signature binds have multiple drawbacks that pattern signatures themselves do not have, so it makes sense to want them to be enabled separately. Pattern signature bindings are instead are enabled by -XScopedTypeVariables, which is unchanged.

This unblocks https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10385 by @s-and-witch. Unlike #604 this does not effect GHC 9.8, so it isn't so critically urgent to resolve.

(Instead of a rendered link, go to the Files Changed tab and toggle the rich text diff option. Rending the whole proposal is not that useful when this is a small change to a much larger proposal.)

[nomeata]

This would essentially be #119, right?

[Ericson2314]

Yes!

[AntC2]

(Rending the whole proposal is not that useful when this is a small change to a much larger proposal.)

I agree, so thank you for that. Never the less I'm having a hard time reconnecting all the dots to follow which particular convoluted position we've reached. Bear with me ...

   data T = MkT [a] (a->Int)
   f :: T -> [Int]
   f (MkT (xs :: [a]) f) = let mf :: [a] -> Int
                               mf = map f
                           in mf xs

This example appears to be ill-typed. (I'm being pedantic, but since this is one in a series of mods to a mod to a reintroduced extension, I feel pedantry is the point of the exercise.) I think we should have

 ... let mf :: [a] -> [Int]               -- result from map is still a list

Also I'm not happy with that form of data decl. tyvar a is existential(?) So shouldn't there be an explicit forall a. ... on rhs of the decl?

Here the pattern signature on xs brings a into scope, ...

Yes, but this never caused me conceptual difficulties. It's only with ScopedTypeVariables in force that you have to nervously look around for a signature somewhere that might already have introduced a. Without that extension, you can be confident the leftmost appearance in the equation for f is what's introducing the tyvar.

[Ericson2314]

The type errors are now fixed. Thanks for pointing them out to me. They are original in #523 (comment) but i hope @simonpj doesn't mind editorializing the quote to fix them.

Yes, but this never caused me conceptual difficulties. It's only with ScopedTypeVariables in force that you have to nervously look around for a signature somewhere that might already have introduced a. Without that extension, you can be confident the leftmost appearance in the equation for f is what's introducing the tyvar.

What should:

f (x :: a) = undefined
  where
    g (y :: a) = undefined

With PatternSignatures but without ScopedTypeVariables do?

In my opinion, the interpretation in this amended proposal is the only one that is both unsurprising and doesn't require "nervously looking around" for outer binders, as you put it well.

[Ericson2314]

@nomeata I would like to submit to the committee!

[AntC2]

What should:
...
With PatternSignatures but without ScopedTypeVariables do?

Good question! And I agree needs a little 'looking around' -- but only a little. I'll try a variation

ff (x :: a) = g (x, x) 
      where
        g ( x@(_, y) :: b) = y  

This compiles, infers ff :: a -> a. x appears in two different binding sites at two different types. But we know those are binding sites syntactically, so that's two different xs. b doesn't appear anywhere leftwards so that must be a binding. If I change g's :: b to :: a, GHC complains Occurs check ... infinite type .... So that a isn't appearing leftmost/can't be a binding site.

Now try (in a Haskell that supports not only PatternSignatures with binds but also ResultSignatures with binds):

ff (x ) :: a = g (x, x)     -- this `:: a` is a ResultSignature (binding)
      where
        g ( x@(_, y :: a) ) :: b = (y :: b) :: a 

This compiles, infers ff :: a -> a. My 'leftmost appearance' rule seems to be working fine.

I can change that top line to ff (x :: a) :: a = g (x, x) .... Still compiles happily. I can change the :: b on g's result to :: a. Still happy.

So what worries me with this proposal is you're taking away the ability for PatternSignatures to be binding sites. And forcing me to use the uglifying and complexifying @a mechanism.

Complexifying because why are you forcing me to distinguish a binding from a usage in types? Types don't work like terms. Types work by unification not evaluation (beta reduction). Unification means if I have an :: a here, I have the same :: a everywhere in that scope.

[AntC2]

(This is probably a q for some other proposal in this whirl but ...)

Are we sure in patterns we can distinguish @ in as-patterns vs @ for tyvar introduction? Note let foo@a = 42 in ... is valid (but admittedly silly).

To introduced tyvars appearing nested inside constructors I can't go

bar (x, y)@(a, b) = ...                     -- not this

bar @a @b ((x, y) :: (a, b)) = ...          -- but this

which seems long-winded.

[AntC2]

Another way to mentalise PatternSignatures is: I want everything marked :: a to be the same type. I don't care how you get there: you're a compiler; that's your job.

[Ericson2314]

Types work by unification not evaluation (beta reduction).

I don't think that is true (there is a mix of unification and special-cased "bidirectional typechecking" methods going on, and with GHC Issue #23639 fixed there will be even more). Moreover, this philosophy --- types are not like terms, the scoping / name resolution of type need not be explicit / types should not be thought of as substitution is decidedly not the philosophy of #448. I don't expect you to start liking this stuff when you didn't before, but I also don't think an amendment proposal like this one is the right place to re-litigate these issues.

As an aside, let me add that "types working like beta reduction" isn't just some fancy Martin Löf thing, it is also a System F thing. My strong desire to see parsing and renaming for types and terms work the same way can thus be departed from any Dependent Haskell notions.

---

Are we sure in patterns we can distinguish @ in as-patterns vs @ for tyvar introduction?

Yes that was cleaned up and properly specified by @int-index for a few releases now.

[adamgundry]

Thanks very much for this @Ericson2314! I supported this idea five years ago and I'm still strongly in favour.

[Ericson2314]

@goldfirere Had a chance to read this one yet? (Sorry I didn't think to mention this in person at ICFP.)

I recall, hopefully correctly, from the other threads that you also wanted this, but were worried others on the steering commit did not, but then they in fact were OK with this.

[goldfirere]

Sorry for losing track of this one. I'm in support of having a mechanism to forbid binding type variables in pattern signatures, but I disagree with the specifics here: with this amendment, -XScopedTypeVariables would imply -XPatternSignatures, -XMethodTypeVariables, and -XExtendedForAllScope, and the ability to bind variables in pattern signatures.

And, as far as I can see, the behavior specified in this proposal is already available, via -XPatternSignatures -Werror=pattern-signature-binds. What's not good enough about -XPatternSignatures -Werror=pattern-signature-binds? I continue to think that we abuse our extensions mechanism to perform duties better handled by the warning mechanism or a linter.

To be clear, I agree that we should support Haskellers who want to prevent their pattern signatures from binding variables. But I argue that the existing #448 already accomplishes this goal and would need to be convinced that the status quo is somehow insufficient before recommending acceptance.

(I don't mean to just unilaterally block this proposal, and so I'm happy to forward to the committee with a "reject" recommendation; perhaps others will disagree with me.)

[Ericson2314]

@goldfirere The most notable is the interaction with other features: For example, having contextual bindings like this breaks -Wpuns and -Wpun-binds's (#270) ability to simulate a single namespace:

x = 1

f (_ :: x) = 1 -- is 'x' a bind or a use? Can't change based on warnings alone!

There is a no-go situation where either this or that must be an extension, we cannot have both of them being warnings. I recall there was much more worry about punning/single namespace functionality "forking the language", whereas no one seemed to have any particular love for pattern signature binds, so it seems more prudent to make this side the extension case, and keep that side mere warnings.

This an other interactions was detailed in a the much larger #532, but I had pulled them out because I thought this change was uncontroversial. I suppose I can add them back if you like.

[goldfirere]

I'm afraid I still don't get it.

Even with the proposed amendment, the -XScopedTypeVariables language -- where (pat :: a) might bind a or be a usage of a, depending on whether a is in scope -- will still exist. You perhaps won't use it, but it will exist. So a future proposal that blends namespaces will have to have some opinion on what to do with let a = ... in ... (pat :: a) .... Will that proposal be fork-like? Or, put more directly, would that future proposal introduce an extension that changes the semantics of existing programs? I think it will have to.

Already, we're saying that you're more future-compatible with dependent types if you have -Wpuns and -Wpun-bindings. Maybe we just add -Wpattern-signature-binds to that list. I just don't see the practical difference between putting the feature behind a warning vs an extension -- other than the fact that warnings strike me as lighter-weight, and thus preferable (other things being equal).

Note that the situation with f @a = ... is different from what we're debating here, because f @a should unambiguously bind a (shadowing any other a in scope) -- and thus it would be problematic if f @a = ... could be an occurrence of an in-scope a. We've debated that point before, and I agree a warning is insufficient there. For better or worse, this case here, in a signature, is different.

[Ericson2314]

@goldfire Sorry let me be more explicit:

1. The issue is that the x is my example will be considered a bind, and get a warning, because pattern signature binds only considers the type namespace (absent new unproposed language extensions) as doing otherwise would be a breaking change.

2. That leaves the single namespace user unable to use the term-namespace-bound x in a pattern signature (because the implicit bind gets in the way).

3. Beyond the lack of expressivity, this might be highly confusing to a user taught with single namespaces and hitherto unaware that there was even such a thing as type vs term namespaces.

[Ericson2314]

The extension version of -Wpattern-signature-binds, this, fixes being able to use variables in pattern signatures regardless of the namespace they are bound in. The hypothetical extension version of -Wpuns and -Wpun-bindings would "fix" shadowing, allowing variables bound in a narrower scope in the "wrong" namespace to take shadowing. There is no way to fix either of these things (from a single namespace perspective) without extensions.

I think most people agree shadowing is of dubious utility (unless someone is trying to teach how substitution works), so leaving -Wpuns and -Wpun-bindings as warnings seems fine to me. In the other and hand being unable to use variables bound in the other namespace at all in pattern signatures strikes me as very frustrating limitation I could not justify to a student/coworker. (And I would like to use and teach single-namespace Haskell regardless of dependent features because I consider it more human-friendly.)

Whereas in response to the shadowing issues I think I can say "just don't shadow", in response to the pattern signature bind issues I don't think I can say "just don't try to use that variable there".

[goldfirere]

I am a huge fan of single-namespace Haskell. But despite your kind re-explanations, I still don't see how this proposal gets us closer to that goal.

You say "the single namespace user [is] unable to use the term-namespace-bound x in a pattern signature (because the implicit bind gets in the way)." How does this proposal change that?

It sounds to me as if you're imagining some future -XUnifiedNamespace extension and further imagining particular interactions with this proposal. I'm in support of designing today in order to make room for future extensions. Yet this proposal does not, say, remove the -XScopedTypeVariables-powered behavior relating to binding. So, in some sense, the future proposal will have to grapple with backward incompatibility. So I don't see how the current proposal moves the needle on that potential future conversation. Maybe if -XScopedTypeVariables were a niche or newly-introduced extension, I might feel differently. But it is pervasive, meaning that a future proposal that disagrees with -XScopedTypeVariables is going to be problematic. (Not impossible -- but it will be a lively debate.)

[Ericson2314]

Today there are two choices:

1. No pattern signatures at all
2. Pattern signatures with implicit binds, which, regardless of warning, will not allow uses of term-namespace-bound variables.

The point of this proposal is to take the opportunity of the newly reintroduced, yet-unimplemented -XPatternSignatures for pattern signatures without pattern binds. That directly solves the problem:

• Term bound x can now be used in a pattern signature, with -XPatternSignatures and without -XScopedTypeVariables.

I am not imagining a -XUnifiedNamespace future because @int-index's most recent plan is that we do not need a such a thing after all; that -Wpuns and -Wpun-bindings are sufficient.

I don't think we need to do anything about about -XScopedTypeVariables? #448 was already about giving users other options in hopes that they migrate away from it, and this doesn't change that. -XScopedTypeVariables is of course unchanged, it simply does something more wr.t. pattern signatures (adds implicit binds) than the underlying -XScopedTypeVariables.

[Ericson2314]

OK @simonpj I've reworked this:

1. As you requested, -XPatternSignatureBinds is back, -XScopedTypeVariables is once again just implying other extensions, and doing nothing on its own.
2. I've made the motivation relating to single vs multiple namespaces. My referring to unmerged Support pun-free code #270 has been replaced with accepted and almost implemented Visible forall in types of terms, and types in terms #281, so I feel much better about this.

[simonpj]

Thanks. I found the new 3.2.2 hard to follow. But I am content with the actual payload in 3.5.

@rae

[vanceism7]

Thanks. I found the new 3.2.2 hard to follow. But I am content with the actual payload in 3.5.

rae

I think you mean @goldfirere?

[Ericson2314]

Great, and also I am happy to reword 3.2.2 too; I didn't think I had yet found the wording to be clear either.

[Ericson2314]

What's the status at this, at first @simonpj was saying let's not block on #615, but now that has become #620.

[goldfirere]

Just some typos, etc. Nothing interesting in the review.

[goldfirere]

OK. I'll recommend acceptance. Though I've come to think that we're fighting the wrong battle here, in extension shuffling. #628 paves a different way forward. Yet those ideas should not stop others from making progress.

[Ericson2314]

Great!

And to be clear, I would be very happy to someday reformulate this stuff in a post-#628 approach.

The gist is that I am hoping new editions going forward can have as little implicit binding as possible, and no pattern signature binds in particular (as @ binding obviates it). Editions should indeed remove the need to have a -XPatternSignatures (without implicit binding) at all --- it should be a mandatory part of all new editions whether they fall on the "student/conservative -- fancy types" spectrum.

But making -XPatternSignatures "queued up" to be entirely --- rather than partially (with the binding part removed) --- to be codified in a new edition while we're still sorting #628 out seems like useful book-keeping to me in the short term.

[Ericson2314]

I see there was a lot of discussion of this on the mailing list https://mail.haskell.org/pipermail/ghc-steering-committee/2024-January/thread.html

I just want to answer a few things:

Deprecating ScopedTypeVariables?

In my view, #448 (the proposal I am amending) was always about opening the door to someday deprecating ScopedTypeVariables. The proliferation of extensions was essentially generated by the Venn diagram of (a) what we have today, and (b) what we conceivably want tomorrow.

Yes, actually removing support for ScopedTypeVariables is inconceivable as it is one of the widely extensions. But a large part of the motivation editions process is to untangle what is (a) supported/allowed vs (b) promoted/endorsed. The principles explain how ScopedTypeVariables fall short. The more dependent stuff we get, the worse the problem gets.

My amendment (this proposal) basically seeks to claim that the same sort of problems that apply the whole of ScopedTypeVariables also apply to the new (as of the orignial #448) PatternSignatures. It feels odd to me to make a new extension only for it also to include more than what may want in the future, and thus compelling us to go through the whole #448-style extension-splitting process again.

Warnings vs extension diagnostics

The philosophical parts have already been discussed elsewhere; I don't mean to relitigate that. I do want to point out a practical difference. -Werror=pattern-signature-binds presumably makes a message like this:

error: pattern signature binds ‘foo’

With the proposal, -XPatternSignatures without -XScopedTypeVariables presumably makes a warning like this:

error: Not in scope: type variable ‘foo’

If the goal is, as I believe, to treat this sort of implicit binding as a mistake, I think the second sort of message is the right one to end up. Editions (assuming that is the end goal) should not explain things in terms of other editions. Editions should be self-contained including their mental modal, and the prior editions or sibling editions should be mere "counterfactuals" that one need not understand.

In short, I advocate damnatio memoriae for the features we don't want when they are disabled.

Whether we should do that right away with extensions, or wait for editions, is a separate question that applies equally well to this proposal or the original #448. (After all, we could have turned off the other parts of ScopedTypeVariables we don't like with -Werror=... too.)

Is PatternSignatures deprecated enough to change its meaning?

@simonmar brought this up. I don't claim to know the answer --- maybe it is in fact no! But that's a criticism that applies to the original proposal, which reintroduced PatternSignatures with changed meaning. This proposal does change its meaning from the current plan, but it doesn't change the fact the plan is for it to change meaning somehow.

I have no qualms staying safe and deciding we should use PatternSignatures2 or something instead. No qualms at all! But as that is an orthogonal solution to an orthogonal problem (present in the original #448), I don't think it should hold this up.

[Ericson2314]

Thanks @adamgundry for relaying my last post to the list :)

@simonpj writes

I see. So you are proposing

• PatternSignatures = SimplePatternSignatures + PatternSignatureBinds

I think that proposal was to keep PatternSignatures = ScopedTypeVariables, as it not proposed in the preexisting #448 but it as currently implemented. This is because that deprecation process was never "finished", so it would be a still-not-quite acceptable change to repurpose PatternSignatures for something else.

If we can change PatternSignatures at all, I would advocate for going all the way to PatternSignatures being the only knob and no SimplePatternSignatures or PatternSignatureBinds, simply for sake of having fewer knobs and because I don't think there is much demand for just pattern signature binding but not other forms of implicit/ambiguous binding.

[Ericson2314]

Hey just checking it looked like a positive consensus was being reached on the mailing list end of Jan / beginning of Feb, but was there ever a final vote?

[goldfirere]

Without much enthusiasm from the committee, but with a small leaning in favor, this proposal is now accepted.

[goldfirere]

It does look like there's a build failure. @Ericson2314 do you want to investigate this before we merge?

[nomeata]

The readthedocs failure can be ignored, or probably be solved by merging master into this branch.

[VitWW]

It does look like there's a build failure.

The reason of readthedocs failure - this git-fork is not updated for too long, last update was before Feb 2024.

[Ericson2314]

Hooray! Very happy this is accepted :). Thanks everyone.

I am now back from a trip, and just pushed a merge with master. I'll watch this to make sure CI passes.

[Ericson2314]

OK good, it passes now!