Confusion around visible type application in pattern synonym pattern

See also #19847 (closed)

Sometimes, I like to declare

import Data.Kind
import Type.Reflection

pattern TypeApp ::
  forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
  Typeable f =>
  forall (arg :: k1).
  result ~ f arg =>
  TypeRep arg ->
  TypeRep result
pattern TypeApp arg_rep <- App (eqTypeRep (typeRep @f) -> Just HRefl) arg_rep

This pattern synonym allows me to match on a TypeRep to see whether its an application of some known type constructor, like List or Maybe.

GHC accepts this declaration, as it should.

But using causes chaos:

f :: TypeRep a -> String
f (TypeApp @[] rep) = show rep

produces

Bug.hs:18:4: error:
    • No instance for (Typeable f0) arising from a use of ‘TypeApp’
    • In the pattern: TypeApp @[] rep
      In an equation for ‘f’: f (TypeApp @[] rep) = show rep
   |
18 | f (TypeApp @[] rep) = show rep
   |    ^^^^^^^^^^^^^^^

Bug.hs:18:4: error:
    • Could not deduce (k1 ~ *)
      from the context: a ~ f0 arg
        bound by a pattern with pattern synonym:
                   TypeApp :: forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
                              Typeable f =>
                              forall (arg :: k1).
                              (result ~ f arg) =>
                              TypeRep arg -> TypeRep result,
                 in an equation for ‘f’
        at Bug.hs:18:4-18
      ‘k1’ is a rigid type variable bound by
        the type signature for:
          f :: forall {k1} (a :: k1). TypeRep a -> String
        at Bug.hs:17:1-24
    • In the pattern: TypeApp @[] rep
      In an equation for ‘f’: f (TypeApp @[] rep) = show rep
    • Relevant bindings include
        f :: TypeRep a -> String (bound at Bug.hs:18:1)
   |
18 | f (TypeApp @[] rep) = show rep
   |    ^^^^^^^^^^^^^^^

I have no clue what GHC is thinking here. Even when I try making k1 and k2 specified (in parens, not braces) and stating @Type @Type, GHC is no better off, producing roughly the same messages.

For the record, this was encountered while I was writing a library that is intended to be useful in the Real World.