Wildcard binders in type declarations

GHC Proposal #425 "Invisible binders in type declarations" defines the following grammar:

tv_bndr ::=
         | tyvar                         -- variable
         | '(' tyvar '::' kind ')'       -- variable with kind annotation
  (NEW)  | '@' tyvar                     -- invisible variable
  (NEW)  | '@' '(' tyvar '::' kind ')'   -- invisible variable with kind annotation
  (NEW)  | '@' '_'                       -- wildcard (to skip an invisible quantifier)

This has been mostly implemented in 4aea0a72, except for wildcard binders @_. Currently the user has to name all variables on the LHS, even if they are unused on the RHS:

type F :: forall a b. Proxy a -> Proxy b
type F @a @b p = 'Proxy @b  -- `a` and `p` are unused

But with the proposed invisible wildcard binder @_, the user could elide the name of a:

- type F @a @b p = 'Proxy @b
+ type F @_ @b p = 'Proxy @b

I think it would also be fine to allow _ binders without the @, even though this is not included in the proposal:

- type F @a @b p = 'Proxy @b
+ type F @_ @b _ = 'Proxy @b

And possibly two more forms: visible and invisible wildcard binders with kind annotations: @(_ :: k) and (_ :: k). All of those forms would arise naturally if we took the declaration of HsTyVarBndr and made the name field optional:

  data HsTyVarBndr flag pass
    = UserTyVar
           (XUserTyVar pass)
           flag
-          (LIdP pass)
+          (Maybe (LIdP pass))

    | KindedTyVar
           (XKindedTyVar pass)
           flag
-          (LIdP pass)
+          (Maybe (LIdP pass))
           (LHsKind pass)

Or it could be a dedicated data type instead of a general-purpose Maybe.