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

[GHC]

#15657: Support promotion of pattern synonyms to kinds
-------------------------------------+-------------------------------------
        Reporter:  infinity0         |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
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 changed by infinity0:

Old description:

> 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.

New description:

 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
 `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.

--

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