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.