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.
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.
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:
RequiredTypeArguments, make term variables scope over types, as stated in section 7.2 "Name resolution" of the proposal:
When looking up an identifier
Vin 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
DataKindsis enabled, but now we extend this rule to lowercase identifiers if
- 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.
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).