Type variable in pattern binds invisible forall variable

Summary

Given A :: forall {k :: Type} (a :: k). A, f (A @x) = ... binds k as x, even though A @x in an expression binds a as x.

Steps to reproduce

import Data.Proxy (Proxy (Proxy))

f :: Read a => Proxy a -> ()
f _ = ()

g :: Read a => Proxy a -> ()
g (Proxy @_ @a) = f (Proxy @a)

Expected behavior

This should err, and instead, g (Proxy @a) = f (Proxy @a) should be correct.

Environment

• GHC version used: 9.2.4