Skip to content

Support promotion of pattern synonyms to kinds

Suppose we define a heterogeneous binary tree:

{-# LANGUAGE
    DataKinds
  , 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.

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