Re: [GHC] #9953: Pattern synonyms don't work with GADTs

7 Jan 2015

      #9953: Pattern synonyms don't work with GADTs
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                   Owner:  cactus
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:  7.10.1
       Component:  Compiler (Type    |                 Version:  7.10.1-rc1
  checker)                           |                Keywords:
      Resolution:                    |  PatternSynonyms
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by simonpj):

 In email Gergo showed the following example:
 {{{
 data T1 a where
    MkT1 :: a -> T1 (Maybe a)

 -- Inferred type pattern P1 :: (t ~ Maybe a) => a -> T t
 pattern P1 x <- MkT x

 -- Inferred type pattern P2 :: a -> [Maybe a]
 pattern P2 x <- [Just x]
 }}}
 When real data constructors are concerned, the types
 {{{
    T1 :: a -> T1 (Maybe a)
    T1 :: (t ~ Maybe a) => a -> T t
 }}}
 are absolutely equivalent.  '''But the two types are not equivalent for
 pattern synonyms.'''
   * When you match against `P1` can match a value of type `T ty`, for any
 `ty`; and you get evidence for `t ~ Maybe a`.
   * But when you match against `P2` you can ''only'' match a value of type
 `T (Maybe ty)`; and you get no equality evidence.

 The difference is manifest in the different inferred types for `P1` and
 `P2`.

 '''Principle''': you should be able to tell the behaviour of a pattern
 synonym whose implementation is hidden, just from its type.  So the types
 of `P1` and `P2` are really different.

 The same principle should apply to explicit, user-supplied type
 signatures.  So if you say
 {{{
 pattern P1 :: a -> T (Maybe a)
 }}}
 it should typecheck all right, but you can then only pattern match on
 values of type `T (Maybe ty)`.

 In short, if you want GADT-like behaviour for a pattern synonym, you can
 get it ''only'' by giving explicit equality constraints in the signature,
 and not by having a complex result type (as you can do for real data
 constructors).

 I had missed this point entirely in my earlier comments -- thank you Gergo
 for pointing it out.

 Are we agreed on that?

 Then we can return to the implementation!

 But I think the user manual deserves a careful look, to make sure that it
 articulates these points.

 Simon

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:9
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler