[GHC] #10928: Refine pattern synonym signatures

GHC ghc-devs at haskell.org
Wed Oct 7 13:33:28 UTC 2015


#10928: Refine pattern synonym signatures
-------------------------------------+-------------------------------------
        Reporter:  mpickering        |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Concur with comment:14. Keep current syntax, but with reversed ordering.
 Specifying only one constraint would now indicate a '''required'''
 constraint.

 On a separate note, the parallelism with GADT syntax discussed in
 comment:12 is already broken. Consider

 {{{#!hs
 data G a where
   MkG :: G Int

 pattern P :: G Int
 pattern P = MkG
 }}}

 The pattern and the data constructor have '''different''' static
 semantics. Specifically,

 {{{#!hs
 -- this works:
 ctor :: G a -> a
 ctor MkG = 5

 -- this doesn't:
 pat :: G a -> a
 pat P = 5
 }}}

 This is because a non-uniformity in the return type of a pattern is taken
 as a required equality constraint, not a provided equality constraint. The
 top set of definitions is equivalent to

 {{{#!hs
 data G a where
   MkG :: a ~ Int => G a

 pattern P :: {- required -} a ~ Int => {- provided -} () => G a
 pattern P = MkG
 }}}

 This was a design decision made in pattern synonym typing. I don't love
 this decision, but I can't quite argue against it either. It's one more
 way in which we must be honest that the things appearing after `MkG ::`
 and `P ::` are '''not''' types, but type-like specifications with a very
 specific interpretation.

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


More information about the ghc-tickets mailing list