[GHC] #12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym

[GHC]

#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      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:                    |
-------------------------------------+-------------------------------------

Comment (by ezyang):

 Actually, it turns out the example above is not a great one because no
 type refinement happens with pattern synonym (with good reason!)  Here's
 my actual use case:

 {{{
 newtype D k a = D a

 data Stream a = Cons a (Stream a)

 newtype StreamK k a = StreamK { unStreamK :: Stream a }

 {-
 -- Pattern synonyms are to give this "virtual interface"
 data StreamK (k :: Clock) a = Cons a (StreamK (D k a))
 newtype Stream a = Stream { unStream :: forall k. StreamK k a }
 -}

 unStream :: Stream a -> (forall k. StreamK k a)
 unStream t = StreamK t

 pattern Stream :: (forall k. StreamK k a) -> Stream a
 pattern Stream t <- (unStream -> t) where
     Stream (StreamK t) = t

 pattern ConsK :: a -> D k (StreamK k a) -> StreamK k a
 pattern ConsK x xs <- StreamK (Cons x ((UnsafeD . StreamK) -> xs)) where
     ConsK x (UnsafeD (StreamK xs)) = StreamK (Cons x xs)
 }}}

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