Once this all stabilises, you will need to also put in mj AnnForall $1 and mj AnnDot $3.

And similar for all other places where the new keywords appear.

Thanks! I talked with Richard Eisenberg this afternoon (I created this diff so we'd have something to look at together) and he pointed out the same thing.

To do so, you will have to update the Template Haskell AST.

When we're done fixing other bugs, you should augment the TH AST to handle the new foralls, and then you'll have something to put here other than Nothing.

The pprHsForAllTvs function does not print forall . when the list is empty. But we should in this case.

Looking at this all a little further, I think pprHsForAllTvs is just wrong. It should always print the forall. The function is called in two other places: the ppr_mono_ty case for HsForAllTy, where the user has written a forall (so we should print it), and pprHsForAllExtra. The latter function takes a [LHsTyVarBndr pass] -- but it should actually take a Maybe [LHsTyVarBndr pass], solely to distinguish the forall . case from printing nothing. I think you'll find that propagating this change through to be easy.

This datatype needs more documentation. Specifically, there needs to be a comment that says that after typechecking, all RuleBndrs are made with the RuleBndr constructor, never the RuleBndrSig constructor.

You also may want to describe that the quantified tyvars move from your new field to the list of RuleBndrs. I was originally thinking that the type-checked tyvar binders should stay in your new field, but there's no support for a LHsTyVarBndr Id -- the type checker just spits out TyVars. (I want to change this, eventually.)

Clarify that these are the type variables. The next field also contains forall'd binders. You may also want to include a link to the accepted proposal, because someone unfamiliar with that proposal may find the double-forall odd.

That's a question for @alanz. There are indeed tests in the testsuite about these.

I'm not sure. It might be due to the shift/reduce error, which means that the parser will take a guess somewhere, and perhaps it's taking the wrong guess.

More generally, I think this could be refactored to be cleaner. But the double-forall rules in rule_forall, not in rule. Also, why use tv_bndrs1 instead of tv_bndrs? Is it bad to have an empty list? (Maybe a user just wants to make it very clear that the other list is term-level variables.) And I'm surprised the forall . case for term-level binders has to be treated specially. Could rule_var_list be modified to allow an empty list of term-level binders? There's a chance that the refactoring would get rid of the misbehavior, but I don't know happy well enough to be sure.

Not your doing, but please document that an empty list of patterns is possible, but that the loc won't be used in this case.

I wrote Maybes.whenIsJust :: Monad m => Maybe a -> (a -> m ()) -> m () just for this purpose.

This whole separation of the payload vars from other vars seems suspect. For example, why reassign the location to the pattern variables but not the payload variables? I think that's wrong. Instead, this would seem cleaner if we arrange to have pat_vars contain variables from both the LHS and RHS, and then just call newTyVarNameRn (with reassigned locations) once. As it is, I'm left wondering if there is some difference in the treatment of LHS vars and RHS vars (there isn't).

To be clear, this problem also isn't yours, but it distracted me when trying to understand your code.

This would mean that

type instance forall a. F Int = Bool

wouldn't get a warning. I think we do indeed want a warning here, so you should pass a Just (text "...") here.

Isn't this forall_kity_vars?

This error is what we want (so I do think nonquant_var_names is fine here) -- but it should be rephrased.

I personally would find mb_bndrs *> Just bndrs' easier to read.

Type family default equations can mention only type variables, not type patterns on the LHS. So they're much simpler. See https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#assoc-decl-defs But, bizarrely, the type variables may be different from the variables used in the class head, so we still need to allow the possibility of an explicit forall. So you'll have to update this function, but it shouldn't be nearly as complex as what you've already done.

This function needs to bring the bndrs into scope if the constructors are in H98 syntax.

Perhaps tcExplicitTKBndrs should check for an empty list and do the simple thing in that case. Might be an overall speedup elsewhere, too.

No need for the do {

As noted in the comment on lines 707-708, I did this to be consistent with type signatures. For example

data D a where
  MkD :: forall x . D Int

also gives no warning. Or should we give a warning in both cases?

No, that has type [Located RdrName] whereas we need type [LHsTyVarBndr GhcPs].

Please check if the new error message is okay.

I checked and the overhead of calling with an empty list is quite minimal so seems okay to leave as is.

I think we should give the warning (assuming the user has enabled the relevant warning flag) in both cases, yes.

Please can we use record field names for this data constructor, both in the declaration and in pattern matching?

I know it's orthogonal to this patch but it's a good moment to do it. Make it a separate patch if you prefer

Sure, I will do this as part of this work.

You're right that type signatures do in fact give a warning if the flag is enabled. I've fixed this for type instances but am not sure the message is good enough. Here's an example output:

    Unused quantified type variable ‘(m ∷ Nat)’
    In the type family instance with LHS ‘∀ (m ∷ Nat)
                                            (n ∷ Nat). Plus  'Zero n’
   |
31 | type instance forall (m ∷ Nat)(n ∷ Nat). Plus 'Zero n = n
   |                      ^^^^^^^^^

I don't output the RHS since it's not known to be outputable (we could add a constraint) but on the other hand the variable has to be used in the LHS so maybe this is better anyway.

Looks good to me. Go with that.

Richard and I discussed this via email, and I decided on a simple solution to allow any number of foralls in the parser (this will be useful later on when that is officially allowed), and let the renamer do the work to ensure there is exactly one forall with only term variables or two foralls the first with type and the second with term variables. This fixes the parser issues.