Term variable capture and implicit quantification

GHC Proposal #281: Visible forall in types of terms changes name resolution rules so that variables bound in the data namespace (term namespace) can be mentioned in type-level contexts:

f1, f2, f3, f4 :: forall a -> ...
   -- Note the "forall a ->", which signals a required type argument

f1 x = g1 @x                -- in a type application
f2 x = g2 (undefined :: x)  -- in a type annotation
f3 x = g3 (type x)          -- in an embedded type
f4 x = ...
  where g4 :: x -> x        -- in a type signature
        g4 = ...

Even though the names of those variables are in the data namespace, the variables stand for types. This becomes possible with the T2T transformation in patterns (#23739 (closed)).

There are two side effects from this change.

1. Implicit quantification is now affected by term variables that are in scope. The example above

   f2 x = g2 (undefined :: x)

   wouldn't work if GHC inserted an implicit forall

   f2 x = g2 (undefined :: forall x. x)
                        -- ^^^^^^^^^
                        -- unwanted implicit forall inserted by GHC

   This is covered by section 7.3 "Implicit quantification" of the proposal.

2. Invalid references. It is legal to use a variable from the data namespace, but it should be bound to a type, not to a term. The following program is illegal:

   f :: forall a -> ...
   
   x = let a = 42 in f (type a)
                    --       ^ illegal use of a term in a type

   This is covered by section 7.4 "Type checking" of the proposal that states "any uses of terms in types are ill-typed".

Addressing those issues is just tricky enough to warrant its own ticket, in my opinion, so here it is. Before working on #23739 (closed), I propose to implement the following preparatory changes:

1. Under RequiredTypeArguments, make term variables scope over types, as stated in section 7.2 "Name resolution" of the proposal:

   When looking up an identifier v or V in type syntax, look it up in the type namespace first; if it is not found there, look it up in the term namespace. This is already the case for uppercase identifiers if DataKinds is enabled, but now we extend this rule to lowercase identifiers if RequiredTypeArguments is enabled.

   • Without T2T in patterns, this should only affect error messages, with some out-of-scope errors turning into errors about illegal uses of terms in types.
   • With T2T in patterns, this will allow us to accept new programs.

2. Under RequiredTypeArguments, make implicit quantification check for in-scope term variables. This is the change that -Wterm-variable-capture (#22513 (closed)) warns about. I expect to reuse most of its test cases.

Just to reiterate, this change alone will not allow us to accept any new programs, but it will interact harmoniously with #23739 (closed).