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

19 Sep 2018

      #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