Document the behavior of ScopedTypeVariables vis-à-vis instance heads more precisely

The User's Guide has a Lexically scoped type variables section that describes the intricacies of how ScopedTypeVariables works. There is a wonderfully detailed subsection, Declaration type signatures, that describes how ScopedTypeVariables works for things such as standalone type signatures. Another subsection, Class and instance declarations, is comparatively terse. This is a shame, because it doesn't really convey the subtleties involved in the way ScopedTypeVariables works in instance heads (at least, in my opinion). Here are some surprising observations that I would like to see mentioned in this subsection:

• Unlike in type signatures, where type variables are only brought into scope when there is an outermost forall with no surrounding parentheses, the presence of parentheses does not matter for instance heads. For example, the following examples will typecheck:

  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  module Foo where
  
  import Data.Proxy
  
  class C a where
    m :: Proxy a
  
  instance (C (Maybe a)) where
    m = Proxy @(Maybe a)
  
  instance (forall a. C [a]) where
    m = Proxy @[a]

  The second instance is particularly surprising, since a would not be brought into scope of the body of a function foo if it had the type signature foo :: (forall a. Dict (C [a])). This is definitely something that should be noted.

• Instance heads allow both implicitly and explicitly bound type variables to scope over the method bodies. For example, the following will typecheck:

  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  module Foo where
  
  import Data.Proxy
  
  class C a where
    m :: Proxy a
  
  instance (forall a. C (Either a b)) where
    m = Proxy @(Either a b)

• While ScopedTypeVariables controls the ability of type variables from the instance head to scope over method bodies, it does not control scoping in other places. For example, the following will work even in the absence of ScopedTypeVariables:

  {-# LANGUAGE ExplicitForAll #-}
  {-# LANGUAGE InstanceSigs #-}
  module Foo where
  
  import Data.Proxy
  
  class C a where
    m :: Proxy a
  
  instance forall a. C [a] where
    m :: Proxy [a]
    m = Proxy

  Notice that the a from the instance head scopes over the instance signature for m even though ScopedTypeVariables is not enabled. (If you tried mentioning a in the body of m, however, you would need ScopedTypeVariables.)