Opened 12 months ago

Last modified 12 months ago

#15657 new feature request

Support promotion of pattern synonyms to kinds

Reported by: infinity0 Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by infinity0)

Suppose we define a heterogeneous binary tree:

  , GADTs
  , PatternSynonyms

data Tree a = TLeaf | TNode a (Tree a) (Tree a)

data HTree xs where
  HLeaf :: HTree 'TLeaf
  HNode :: x -> HTree ls -> HTree rs -> HTree ('TNode x ls rs)

A tree representation is chosen because it's pretty general, and easy to combine - just HNode a bunch of them together. With a HList for example, it's harder to do this in nested fashion, and we want to be able to do that for the $BigRealWorld things we're writing.

However in the majority of cases, the $BigRealWorld things defined by actual clients of the API don't need the full power of the HTree, and so pattern synonyms potentially allow them to easily define a tree of one item, or a small unnested list of items.

-- as above, then:

pattern TPure :: a -> Tree a
pattern TPure a = TNode a TLeaf TLeaf

pattern TCons :: a -> Tree a -> Tree a
pattern TCons x y = TNode x TLeaf y

pattern HTPure :: x -> HTree ('TPure x) -- error, has to be ('TNode x 'TLeaf 'TLeaf)
pattern HTPure a = HNode a HLeaf HLeaf

clientThing :: HTree ('TPure Int) -- error, has to be ('TNode Int 'TLeaf 'TLeaf)
clientThing = HTPure 3

Oh no! GHC fails with:

    • Pattern synonym ‘TPure’ cannot be used here
        (Pattern synonyms cannot be promoted)
    • In the first argument of ‘HTree’, namely ‘( 'TPure x)’
      In the type ‘x -> HTree ( 'TPure x)’
20 | pattern HTPure :: x -> HTree ('TPure x)

Actually the first one is not a big deal, we only write that once so it doesn't matter if we need to expand it fully. But things like clientThing might be defined several times and then it's annoying to have to write the synonym out in full every time.

I appreciate ViewPatterns make it hard to do this and would be totally happy with a solution that only works to promote non-ViewPattern pattern synonyms.

Change History (1)

comment:1 Changed 12 months ago by infinity0

Description: modified (diff)
Note: See TracTickets for help on using tickets.