Note [Inferred invisible patterns]

Consider the following:

  class R a where
    r :: forall b. Proxy b -> a

When newtype-deriving an instance of `R`, following
Note [GND and QuantifiedConstraints], we might generate the following code:

  instance R <rep-ty> => R <new-ty> where
    r = \ @b -> coerce @(Proxy b -> <rep-ty>)
                      @(Proxy b -> <new-ty>)
                      r

The code being generated is an HsSyn AST, except for the arguments to coerce,
which are XHsTypes carrying Core types. As Core types, they must be fully
elaborated, so we actually want something more like the following:

  instance R <rep-ty> => R <new-ty> where
    r = \ @b -> coerce @(Proxy @{k} b -> <rep-ty>)
                      @(Proxy @{k} b -> <new-ty>)
                      r

where the `k` corresponds to the `k` in the elaborated type of `r`:

  class R (a :: Type) where
    r :: forall {k :: Type} (b :: k). Proxy @{k} b -> a

However, `k` is not bound in the definition of `r` in the derived instance, and
binding it requires a way to create an inferred (because `k` is inferred in the
signature of `r`) invisible pattern.

So we actually generate the following for `R`:

  instance R <rep-ty> => R <new-ty> where
    r = \ @{k :: Type} -> \ @(b :: k) ->
            coerce @(Proxy @{k} b -> <rep-ty>)
                   @(Proxy @{k} b -> <new-ty>)
                   r

The `\ @{k :: Type} ->` (note the braces!) is the big lambda that binds `k`, and
represents an inferred invisible pattern. Inferred invisible patterns aren't
allowed in the surface syntax of Haskell, for the reason that the order in
which inferred foralls are added to a signature is not specified, so it is
ambiguous which pattern would bind to which forall. But when deriving an
instance, the patterns are being created after the type of the method has been
elaborated, so an order for the inferred foralls has already been determined.
This makes inferred invisible patterns safe for internal use.

(You might wonder if you could bring `k` into scope via the pattern signature
in `\ @(b :: k)`, but that does not work in general; e.g. if
`r :: Proxy Any -> a`; see `C5` in test `deriving-inferred-ty-arg`.)

The implementation is straightforward: we have a Specificity field in
XInvisPat, which is always SpecifiedSpec when coming from the parser or
Template Haskell, but takes the specificity of the corresponding forall from
the method type during instance deriving. When type checking an invisible
pattern, we allow inferred patterns to bind inferred foralls just like we allow
specified patterns to bind specified foralls.

More discussion of this scenario and some rejected alternatives at
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/13190

See also https://github.com/ghc-proposals/ghc-proposals/pull/675, which
was triggered by this ticket, and explores source-language syntax in this
space.