GHC currently rejects the following program:

pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a -> (# (# #) | a #)
pattern Just# a = (# | a #)

With this error message (the line number reference is the one where the signature of the pattern synonym is given):

    A levity-polymorphic type is not allowed here:
      Type: a
      Kind: TYPE r
   |
26 | pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a -> (# (# #) | a #)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I would like for GHC to accept this pattern synonym. I think that it should just be possible to remove the levity-polymorphism check from pattern synonym signatures. I don't this can lead to any unsoundness since patterns are just expanded in Core.