[GHC] #15657: Support promotion of pattern synonyms to kinds

[GHC]

#15657: Support promotion of pattern synonyms to kinds
-------------------------------------+-------------------------------------
           Reporter:  infinity0      |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Suppose we define a heterogeneous binary tree:

 {{{#!hs
 {-# 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.

 {{{#!hs
 -- 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 `clientAPI`
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15657>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler