Looking good so far! Per #386 (comment) I think you want the scoping and instantiation rules for data families too?

Does this proposal touch in any way the way implicit pattern matching in type families work? I mean if I pattern match on types with different kinds, GHC implicitly pattern matches on their kinds first which can lead to surprising behavior (partiality when one does not expect it naively). With this proposal, it is possible to bind invisible arguments and explicitly pattern match on them, so would it be possible to disable that implicit pattern match completely and present an error to the user?

@jvanbruegge The proposal disallows matching on implicit kind parameters on the RHS, so the following will become illegal:

type family F a :: k

type instance F Int = Char
type instance F Int = Maybe

You would need to rewrite it as:

type instance F @Type         Int = Char
type instance F @(Type->Type) Int = Maybe

However, if matching happens on the LHS, it is still fair game:

type family G (a :: k) :: Natural

type instance G Char = 0
type instance G Maybe = 1
type instance G True = 2

For clarity, we could rewrite it as:

type instance G @Type Char = 0
type instance G @(Type -> Type) Maybe = 1
type instance G @Bool True = 2

But in this case it is not required.

Ok, cool. Yeah, I meant the first case

I have added some comments

I am happy to see that you have included

• In type family and data family instances, the instantiation is fully determined by the left hand side, without looking at the right hand side.

but you have zero text motivating, or even specifying, this point. There is plenty to plunder in https://github.com/ghc-proposals/ghc-proposals/blob/wip/spj-instance-scoping/proposals/0000-instance-scoping.rst

This is ready for another round of review.

The title still says “Draft”. Oversight?

@nomeata I'd like to submit this proposal to the committee.

@goldfirere In case this slipped your attention, do you plan to make a recommendation?

@goldfirere Richard, shall we move forward on this one?

Somehow, this fell off my radar -- apologies. I have recommended acceptance, but with a migration strategy around point (5).

When a standalone kind signature is given, modify the process of zipping binders with quantifiers

Vlad, this is pretty impenetrable. zipSAKs is not something most programmers are going to know about -- indeed I do not. Could you reword this bullet to be addressed to a programmer? And give examples. (Either inline here, or forward referenced ("see Example 4,5,6 below").

Earlier you say "SAKS zipping works over two lists: quantifiers and binders. Let us define it in pseudo-code:". At least give a type signature to this function. But more importantly: so what? Now you have defined zipSAKS. Why have you told me this?

During arity inference, do not include trailing forall x. quantifiers in the arity.

This is a rather negative explanation. Why not say what we do? Something like:

The arity of a type-family declaration

type family F b1 .. bn

is determined solely by the visible arguments b1 ... bn in the type family declaration. An application of F is saturated iff it is applied to all these n arguments. The kind signature (if any) for F does not affect its arity. For example:

type F1 ::: Type -> Type -> Type
type F1 a           -- Has arity 1 not 2

type F2 :: Type -> forall k. k -> Type
type F2 a            -- Still has arity 1

type F3 a :: forall k. k -> Type     -- Still arity 1

type F4 @k (a :: k)                                    -- Arity 2
type F5 (a :: Type) @k  :: k -> Type           -- Arity 2

You may want to also point out that there may be invisible inferred kind args.

I strongly support this proposal, because it lets us say explicitly things that we can only currently say implicitly. It fills out part of the design envelope. Let's do it.

Vlad, this is pretty impenetrable.

In sympathy with what I just posted at #442 (comment), I'm fine with the current version of this proposal -- at least until we accept. Perhaps if this is to be long-lasting, it's worth improving the presentation. But, even there, I'm not convinced: the description of this feature belongs in the user manual, not in this repo. And the proposal is burdened with capturing the change from the status quo, which need not appear in the manual. I agree that the current presentation is hard-going, and it has room for various improvements. But I'm equally confident I understand the intent of this proposal and could evaluate whether an implementation meets the specification presented here, and so I don't see the value in the time investment of improving the presentation.

To be clear, I would consider a presentation like the one in this proposal below the bar ("unacceptable" sounds very harsh, but is semantically accurate) for the user manual.

What we explain to our users (in the User’s Guide) does not need to involve zipSAKS, but it also doesn’t need to be precise: as long as the programmer has a rough understanding of what’s going on, they can start using the feature, guided by the compiler diagnostics.

But in the “Proposed Change Specification” my goal wasn’t to explain the feature to the end user. Rather, I wanted to specify it in a way that would be precise enough to guide the implementation efforts and to cover all corner cases.

Honestly, I have no idea how to do it without introducing the notion of SAKS zipping.

Now you have defined zipSAKS. Why have you told me this?

It’s the function that determines which binder corresponds to which quantifier. So if you have

type T :: forall a b. a -> forall c. blah
type T @v t @w = ...

What do v and w correspond to? I say v is a, and w is c, but how come we skipped b? This is determined by zipSAKS.

is determined solely by the visible arguments b1 ... bn in the type family declaration.

But that’s simply not the case. Consider:

type family F a

What arity does it have? Depends on the kind signature:

type F :: Type -> Type          -- arity 1
type F :: forall k. k -> Type   -- arity 2

What arity does it have? Depends on the kind signature:

Hmm, yes you are right. It's quite hard to specify arity. And yet we must.

Perhaps if this is to be long-lasting, it's worth improving the presentation. But, even there, I'm not convinced: the description of this feature belongs in the user manual, not in this repo.

As I say, I'm strongly in favour of accepting this proposal, and that opinion is not conditional on improved presentation.

But I know I'm going to be asked to do code review. What often happens is that I'm trying to review code against a specification that is absent or at least hard to understand. I'm trying to avoid that. So I'm reading the proposal thinking "could I implement this?", and writing comments accordingly.

I'm perfectly content with a specification presented as a user-manual entry. But (unlike @goldfirere) I would say that a draft user manual entry would be a terrific component of a proposal.

It can be written post-acceptance -- I'm not trying to raise the bar for a proposal that might be rejected. My anxiety is that post-acceptance the author breathes a well-deserved sigh of relief, and the improved presentation, the more detailed specification, or the user manual entry, ultimately never gets written.

I strongly agree it's much better not presented as a diff against some (also often ill-specified) baseline.

What evaluation process exactly do you have in mind?

A post-proposal-acceptance process. Or, if you prefer, I'd argue for conditional acceptance here, depending on what we learn during implementation. (Truth be told, I consider all proposals conditionally accepted on similar grounds. It is always possible to learn some new devastating fact during implementation.) Maybe this plan of mine makes it all more concrete:

1. Blast to Discourse (and maybe a few other places) seeking feedback on the breakage.
2. Discuss.
3. If the discussion suggests that doing so is sensible, advocate to the committee for acceptance.
4. Accept the proposal.
5. Implement (this is your part).
6. Assess breakage in practice on head.hackage, along at least two different axes: how many different places break, and how hard each breakage is to diagnose & fix. That is, even if each fix is trivial, if every package breaks, that's bad. Even if there are very few breakages, if the breakage requires the whole package to be rewritten, that's bad. (To be clear, I expect neither of these.)
7. Report on this breakage back out to the community, and discuss briefly.
8. Depending on the result of that discussion, merge.

We're operating here expecting breakage both to be relatively rare and easy to diagnose & fix. If these assumptions are correct, then these last steps will go swimmingly. If we're wrong, then it will be good to re-examine things.

My comment "Do you think that's fair?" is about setting expectations: I wouldn't want to have this plan in mind only to have you and your colleagues very upset when I try to take Step 7.

I would say we should be always able to merge the feature, but it might need a deprecation cycle. For example, simplified subsumption could have gotten a deprecation cycle rather than being cancelled outright as many people probably wished after being unable to upgrade to 9.0.

I too need to write a discorse post, but about how the sort of modularity work @hsyl20 and I are into directly relates to our ability to do proper depreciation cycles without drowning in hard-to-test conditional code.

Maybe this plan of mine makes it all more concrete

@goldfirere That’s a fine plan, and thanks for taking the initiative here.

I have created posts on Discourse, Reddit, and Twitter. Will review in a few days.

/remind me to review responses on Thursday.

@goldfirere set a reminder for Mar 24th 2022

@goldfirere I have created posts on ...

Hehe Reddit thought it was spam. (What on earth triggered their algorithm?)

Reddit's zealous spam filter snares me about 10% of the time I post a story. I messaged the mods to request they restore it.

👋 @goldfirere, review responses .

All seems in order here. In particular, the community outreach did not produce any red flags. I am (re-)recommending acceptance to the committee. Thanks!

/remind me to accept this proposal (pending committee agreement) on April 4.

@goldfirere set a reminder for Apr 4th 2022

the community outreach did not produce any red flags

@goldfirere Note that the reddit post is still marked as [removed]
(Which I imagine means the moderators haven't read @tomjaguarpaw's message yet)

@JakobBruenker That's true (and I was aware of it). But given the quietness both on Discord and Twitter, I decided not to investigate. If you want to get Reddit unblocked, great! There's no reason that we can't revisit the committee discussion in light of new information from Reddit. But I'm afraid I'm not going to take another crack at Reddit on this front.

@phadej points out (on Reddit, but the thread is mostly about something else) that this proposal violates the Explicit Variables Proposal, included in #448, because there is no way to bring inferred variables into scope without unification. (Actually, the same is true within #448.) This suggests that this proposal might benefit from the @(..) syntax proposed with #448.

I do not suggest we change this proposal at this point, just that there is an improvement possible in a later proposal.

That sounds good. If #448 pulls some of this under it's umbrella, that's fine, but there is enough separate stuff on arity not befitting #448 that I agree that's not a good reason to delay this any further.

👋 @goldfirere, accept this proposal (pending committee agreement) on .