#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