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.