[GHC] #10928: Refine pattern synonym signatures

[GHC]

#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):

 While we're tackling this problem, I'd like to repeat my arguments (made
 last round during the debate about this syntax) that we've gotten the
 order of the constraints wrong. Not less natural, but wrong.

 Consider this:

 {{{
 data T a where
   MkT :: (Show a, Show b) => a -> b -> T a

 pattern P :: (Show a, Show b) => (Eq a, Num a) => b -> T a
 pattern P x = MkT 3 x

 foo :: T Int -> Bool
 foo (P _) = False
 }}}

 This code typechecks. But let's delve into that pattern type signature a
 bit. It has 4 parts:

 1. The provided constraints: `(Show a, Show b)`

 2. The required constraints: `(Eq a, Num a)`

 3. The arguments: `b`

 4. The result: `T a`

 Let's look, in particular, at the type variables here. Somewhat by
 definition, only the universal variables are mentioned in the result. Thus
 `a` is universal. Any other type variables are existential. Thus `b` is
 existential. Here is what is in scope in the 4 regions:

 1. Provided: universals and existentials are in scope

 2. Required: only universals are in scope

 3. Arguments: universals and existentials are in scope

 4. Result: only universals are in scope

 Look how the scoping rules flip-flop!

 Wait. What I've written is a lie. In GHC 7.10, the existentials ''are'' in
 scope in the required constraints. But this is hogwash. There's nothing at
 all useful that can be done by having a required constraint on an
 existential. Required constraints must be established before the pattern
 is matched. But existentials are available only after the match. Indeed,
 putting a `Read b` constraint in the required set makes `foo` fail to
 type-check. `b` should simply not be in scope for the required
 constraints.

 By reversing the order of provided/required, our scopes would nest.

 I would also support the following, verbose but clear syntax:

 {{{
 pattern P :: { universals = [a]
              , existentials = [b]
              , provided = (Show a, Show b)
              , required = (Eq a, Num a)
              , arguments = [b]
              , result = T a }
 }}}

 The `provided`, `required`, etc, above are keywords, essentially, but they
 wouldn't clobber any existing syntax. We know precisely when we're parsing
 a pattern type signature. The only compulsory entry in there would be
 `result`. The `universals` and `existentials` are lists of type variable
 ''binders'', where we could assign kinds to the variables. These would be
 inferred, as usual, if they are omitted.

 (You might think we don't need to have binders anywhere, because we can
 always use a kind annotation on a usage of a variable to fix its kind. But
 this won't work in 8.0 for two reasons. 1) With visible type application,
 it would be nice to give an ordering to the variables, with universals
 always before existentials, and 2) when we have kind families, putting a
 kind family in a use site could be ambiguous, whereas it is unambiguous at
 a binding site.)

 This version has the considerable advantage of being easier to read and
 search for. It also means we could deprecate the current syntax for a
 cycle -- nothing would ''change'' in meaning.

 To be clear, I'm not 100% convinced that what I've suggested is an
 improvement, as it's quite verbose. But I'm reminded of one argument that
 came up during the role annotations debate that code is read much, much
 more often than it is written. Optimize for reading over writing!

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