A few minor remarks:

• The capitalization should be NoImplicitForAll for consistency with ExplicitForAll.

• The actual extension should be ImplicitForAll, enabled by default, so the user gets to disable it with NoImplicitForAll. If the extension is NoImplicitForAll, then disabling it would be NoNoImplicitForAll, which doesn't look right to me.

• Disabling ImpilicitForAll should probably automatically enable ExplicitForAll.

• The capitalization should be NoImplicitForAll for consistency with ExplicitForAll.

Done

• The actual extension should be ImplicitForAll, enabled by default, so the user gets to disable it with NoImplicitForAll. If the extension is NoImplicitForAll, then disabling it would be NoNoImplicitForAll, which doesn't look right to me.

That as my intent. Maybe I should re-title it?

• Disabling ImpilicitForAll should probably automatically enable ExplicitForAll.

Mmm, I prefer extensions to be monotonic where possible. Also this made me think some teachers may which to prevent polymorphism altogether with -XNoExplicitForAll -XNoImplicitForAll -Wmissing-signatures and -Wmissing-local-signatures. I'll add that to the motivation.

With -XNoImplicitForAll, will instance C a => D a be allowed, or do we require instance forall a. C a => D a? I guess the latter.

Should -XNoImplicitForAll imply -fprint-explicit-foralls?

I think NoImplicitForAll should turn on ExplicitForAll, but users can override it.

This would be the first precedent where a {-# LANGUAGE NoX #-} pragma enables an extension. I'd rather avoid it.

People using a Dependent Haskell kitchen sink likely already have {-# LANGUAGE ExplicitForAll #-} transitively enabled (via ScopedTypeVariables, RankNTypes, etc), and people using "teacher's edition" of Haskell will either have a default-extensions list handed to them, or won't even need ExplicitForAll as per the discussion in the proposal:

Further, the most beginnning students may be taught with both -XNoImplicictForall and -XNoExplicitForall

This would be the first precedent where a {-# LANGUAGE NoX #-} pragma enables an extension. I'd rather avoid it.

Isn't -XNoMonomorphismRestrictionthe same thing?

I meant "enables a different extension". AFAIK NoMonormorphismRestriction doesn't enable anything else (judging by https://gitlab.haskell.org/ghc/ghc/blob/d584e3f08cfee6e28b70bf53c573d86e44f326f8/compiler%2Fmain%2FDynFlags.hs#L4641).

I meant "enables a different extension"

Ah, so it's an argument against NoImplicitForAll implying ExplicitForAll. Good point.

Thanks @neongreen, you made my "Mmm, I prefer extensions to be monotonic where possible" a lot clearer.

@monoidal great point, I also forgot data declarations.

OK added something about instances and also data types. I am not sure what to do about classes; that is now an unresolved question. I am also being very conservative about variables in signatures in patterns, perhaps moreso than people would like.

I am not sure what to do about classes; that is now an unresolved question.

What is special about classes? They are the same as data types. So, for your example,

class Foo (x :: b)

There are two ways to rewrite it:

• With a standalone kind signature:

  type Foo :: forall b. b -> Constraint
  class Foo x
  

• With a @-binder (not currently in GHC, but the proposal uses it in the data example)

  class Foo @b (x :: b)
  

@int-index Yeah I feel better now. class forall b (x :: b). Foo (x :: b) is garbage because a class has parameters (binders) while a instance has binders. I'll remove the question.

@int-index @rae so the overly-conservative thing was that in other proposals places we say a type signature in a pattern binds a variable that is unified (it is fresh "syntactically" but not "semantically"). I don't want to fight against that completely, but I rather there at least be a way to opt-out of it. I've written this proposal such that you'd have to opt in if you have -XNoImplicitForAll.

I generally prefer fewer implications among extensions -- fewer implications means that I have less to remember. And an implication from a -XNo... seems like a bad precedent.

It came to my attention this morning (by @lexi-lambda and @tek) that I missed an aspect of this proposal.

The Proposed Change Specification refers only to implicit scoping of variables in type signatures and in pattern signatures. But the examples include things like the scoping of k in data T (a :: k). It seems some people, perhaps @Ericson2314, consider the k to be part of a pattern signature. I had never thought of this, and I missed this detail in this proposal.

To me, the text in the Proposed Change Specification defines the payload of a proposal. Thus, acceptance of this proposal has no effect on data T (a :: k). However, I don't think we have a formal definition anywhere of what a "pattern signature" is, and different people may have different understanding of this term. In addition, some might think that the examples form part of the payload.

This leads to two questions:

1. What do we think? Given that this proposal is accepted, what should we implement. @tek wants to know! (I say: what's in the Proposed Change Specification, omitting any new treatment of the k in data T (a :: k).)
2. How to recover from this discrepancy? This proposal is about to be subsumed by Modern Scoped Type Variables #448, which is accepted-pending-reformatting. But the treatment of data T (a :: k) is not included in Modern Scoped Type Variables #448, because I (as the author of Modern Scoped Type Variables #448) didn't understand this detail of this proposal. I'm in the process of reformatting that proposal now. Given its just-about-accepted state, I don't want to introduce this new wrinkle. Instead, I think it would be best to write a separate proposal, which I should be able to do shortly.

It's been a while, but I recall I purposefully kept the list of items out of the proposed change and in examples because I assume I would miss one :).

The normative part assumes "pattern signatures" was well-defined enough to include it and perhaps that was a mistake.

The (a :: k) in data T (a :: k) certainly looks to me like other RHS / binding (a :: k) so I lean towards treating it the same way following the examples. It would be good to get our our terminology consistent (glossary in the users guide?) regardless, though.

in particular,

{-# LANGUAGE WhateverIsNeededForBraveUnifiedNamespace #-}

k = Type

data T (a :: k) -- captured now

nicely illustrates all the issues following from the violation principle (in your proposal) are at play, so I would like to be able to fix that.

probably sensible to link the implementation MR: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8629

It helped to see the place where this came up: I left https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8629#note_444076 and so "cross posting" that here.

IMO the confusion stems from the fact that #425 is the one type variable proposal not to be subsumed into #448. I suggest we subsume it too; we need a unified spec that gets rid of all the silly semantic drift between things which ought to work the same way.

Since this has been moved to #448, shouldn't it receive an "Implemented" label just like #126?