Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information