Note [Lexically scoped type variables]

Language/Haskell/Syntax/Type.hs:603 compiler

The ScopedTypeVariables extension does two things:

* It allows the use of type signatures in patterns
  (e.g., `f (x :: a -> a) = ...`). See
  Note [Pattern signature binders and scoping] for more on this point.
* It brings lexically scoped type variables into scope for certain type
  signatures with outermost invisible 'forall's.

This Note concerns the latter bullet point. Per the
"Lexically scoped type variables" section of the GHC User's Guide, the
following forms of type signatures can have lexically scoped type variables:

* In declarations with type signatures, e.g.,

    f :: forall a. a -> a
    f x = e @a

  Here, the 'forall a' brings 'a' into scope over the body of 'f'.

  Note that ScopedTypeVariables does /not/ interact with standalone kind
  signatures, only type signatures.

* In explicit type annotations in expressions, e.g.,

    id @a :: forall a. a -> a

* In instance declarations, e.g.,

    instance forall a. C [a] where
      m = e @a

  Note that unlike the examples above, the use of an outermost 'forall' isn't
  required to bring 'a' into scope. That is, the following would also work:

    instance forall a. C [a] where
      m = e @a

Note that all of the types above obey the forall-or-nothing rule. As a result,
the places in the AST that can have lexically scoped type variables are a
subset of the places that use HsOuterTyVarBndrs
(See Note [forall-or-nothing rule].)

Some other observations about lexically scoped type variables:

* Only type variables bound by an /invisible/ forall can be lexically scoped.
  See Note [hsScopedTvs and visible foralls].
* The lexically scoped type variables may be a strict subset of the type
  variables brought into scope by a type signature.
  See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig.

References 4

Referenced by 1