Levity Polymorphic Pattern Synonyms
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.