Type application in patterns ignores inferredness of type variables

Summary

When a constructor has inferred arguments, like k in Proxy :: forall {k} (t :: k). Proxy t, type application in patterns (!2464 (closed)) treats the k as though it were not inferred.

Steps to reproduce

import Data.Kind

data Proxy t where
  Proxy :: forall {k} (t :: k) . Proxy t

a :: () -> Proxy Int
-- a = Proxy @Type @Int -- This would, rightfully, not compile
a () = Proxy @Int

b :: Proxy Int -> ()
b (Proxy @Type @Int) = () -- This compiles, but shouldn't
b (Proxy @Int) = ()       -- This should compile, but doesn't

{--
TypeAppBug.hs:13:4: error:
    * Expected a type, but found something with kind `Int'
    * In the pattern: Proxy @Int
      In an equation for `b': b (Proxy @Int) = ()
   |
13 | b (Proxy @Int) = ()       -- This should compile, but doesn't
   |    ^^^^^^^^^^
--}

Expected behavior

Accept and reject the same type applications in patterns as in expressions

Environment

• GHC version used: 9.3.20210925

Optional:

• Operating System: Arch
• System Architecture: x86_64