#11224: Program doesn't preserve semantics after pattern synonym inlining. -------------------------------------+------------------------------------- Reporter: anton.dubovik | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Windows | Architecture: x86_64 Type of failure: Incorrect result | (amd64) at runtime | Test Case: Blocked By: | Blocking: Related Tickets: #11225 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): OK. So here's my current stream of thought: * The universals are those variables that appear in either the result or in the required context. Except that's not quite right in pathological cases, like this: {{{ data Ex = forall a. Ex a magic :: Ex -> a magic _ = undefined pattern Silly x <- (magic -> x) }}} As I understand it, the signature for `Silly` should be {{{ pattern type Silly :: a -> Ex }}} Here, `a` is universal. But `a` is mentioned neither in the result nor in the required context. Compare to {{{ pattern type Sensible :: a -> Ex pattern Sensible x = Ex x }}} Here, `a` is existential. But the pattern signature is otherwise identical! So we can't infer the universal/existential decision from the signature. I thus propose the following revision to pattern signatures: * Allow explicit quantification in two places, according to this schema: {{{ pattern type Syn :: forall <<univs>>. <<req>> => forall <<exs>>. <<prov>> => <<args>> -> <<result>> }}} * In the absence of explicit quantification, universals are inferred to be the variables mentioned in either the result or the required context. Existentials are the remaining variables. * It is against the rules for existentials to shadow universals. According to these rules, the signature given for `Silly` above would be rejected, as `a` is inferred to be existential, but in the pattern synonym, it really is universal. Instead, the user would have to write {{{ pattern type Silly :: forall a. a -> Ex }}} What's terribly unfortunate here is that this new, revised signature for `Silly` seems to add simply a redundant `forall`... the sort of thing Haskell infers all the time. Except here it says "`a` is universal". Contrast to the explicit form of `Sensible`'s signature: {{{ pattern type Sensible :: () => forall a. a -> Ex }}} which is quite ugly. This all makes me want the incredibly verbose syntax in comment:5:ticket:10928, repeated here for convenience: {{{ pattern type P :: { universals = ... , existentials = ... , provided = ... , required = ... , arguments = ... , result = ... } }}} A worked out example appears in that comment. We would allow a short-hand in common cases (yet to be worked out). This syntax is annoying to write, but surely a pleasure to read. And it reminds readers that the thing to the right of `pattern type Blah ::` is '''not''' a type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11224#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler