Allow type annotations / visible type application in pattern synonyms

data Lift f a = Pure a | Other (f a)
data V0 a

To make a pattern synonym for a -> Lift V0 a I would like to be able to write either

pattern A a = Pure @V0 a

or

pattern B a = (Pure :: _ -> _ V0 _) a 

to be equivalent to

pattern C :: a -> Lift V0 a
pattern C a = Pure a

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture