Visible type application in record patterns

Motivation

I've been using type applications in patterns quite a bit recently and struggled when adding or removing an argument from the constructors because all pattern matches must add/remove wildcards.

lookupQMap :: forall a. Typeable a => QKey a -> QMap -> Maybe a
lookupQMap qid qmap = 
     -- This could use a Data.Typeable.cast, but it's simplified from some more complex code
     case lookupQ qid qmap of
         ResultEntry @r' dat _
           | Just Refl <- eqT @r @r' -> ...

The nice way to avoid the problem would be to use record patterns. But mixing type applications with record patterns results in a parse error!

case lookupQ qid qmap of
    ResultEntry @r {resultData=dat}

-- [parser] [E] parser error on input '{'

I'm not sure if this is intentional, an oversight, or whether I'm missing the right syntax. It'd be really useful, though!

Proposal

If the missing syntax is an oversight it hopefully could be added without making the grammar overly ambiguous. I do not know whether this would require a separate proposal. If the feature already exists or is intentionally missing it maybe could be documented somewhere, though I'm not sure what the right place would be. I couldn't find a mention in the proposal or paper at least.