[GHC] #9953: Pattern synonyms don't work with GADTs
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Consider this variant of test `T8968-1`: {{{ {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-} module ShouldCompile where data X :: * -> * where Y :: a -> X (Maybe a) pattern C :: a -> X (Maybe a) pattern C x = Y x foo :: X t -> t foo (C x) = Just x }}} * If we had `(Y x)` instead of `(C x)` in the LHS of `foo`, then this is an ordinary GADT program and typechecks fine. * If we omit the pattern signature, it typechecks fine, and `:info C` says {{{ pattern C :: t ~ Maybe a => a -> X t -- Defined in ‘ShouldCompile’ }}} * But as written, it fails with {{{ Foo.hs:11:6: Couldn't match type ‘t’ with ‘Maybe a0’ ‘t’ is a rigid type variable bound by the type signature for: foo :: X t -> t at Foo.hs:10:8 Expected type: X t Actual type: X (Maybe a0) Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1) In the pattern: C x In an equation for ‘foo’: foo (C x) = Just x }}} Moreover, `:info C` says {{{ pattern C :: a -> X (Maybe a) -- Defined at Foo.hs:8:9 }}} Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit. The exact thing happens for `DataCons`. It's handled via the `dcEqSpec` field. Essentially `PatSyn` should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in `TcTyClsDecls.rejigConRes` (perhaps needs a better name). This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => cactus -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.4 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: -------------------------------------+------------------------------------- Changes (by cactus): * keywords: => PatternSynonyms * component: Compiler => Compiler (Type checker) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.4 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 carter): ... should this be remilestoned for 7.10.1 or will we need to do 7.8.5? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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.8.4 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: -------------------------------------+------------------------------------- Changes (by cactus): * milestone: => 7.10.1 Comment: 7.8 doesn't have pattern synonym type signatures. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: -------------------------------------+------------------------------------- Changes (by cactus): * version: 7.8.4 => 7.10.1-rc1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 cactus): I almost have this working in the `wip/T9953` branch. However, there is one tricky question, very much related to #9954: what do we do with required constraints that mention some GADT indices? For example, if `pattern C` also happened to have a required constraint, e.g. `Eq a`, where would we put that, if `a` is no longer a universally- quantified type argument of `C`? What would be the type of `C`'s matcher? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 cactus): Here's a hopefully more enlightening description of the problem in ticket:9953#comment:6. Suppose we have this setup: {{{#!hs {-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-} data X t where Y :: a -> X (Maybe a) f :: (Eq a) => a -> a f = id -- inferred type: -- pattern C1 :: t ~ Maybe a => a -> X t pattern C1 x = Y x pattern C2 :: a -> X (Maybe a) pattern C2 x = Y x pattern C3 :: () => (Eq a) => a -> X (Maybe a) pattern C3 x = Y (f -> x) }}} The difference between `C1`'s inferred type and `C2`'s type is the subject of this ticket; with the point being that we should be reconstructing `C1`'s type from the signature given for `C2`. The types of the matchers generated are as follows: {{{#!hs $mC1 :: forall r t. X t -> (forall a. (t ~ Maybe a) => a -> r) -> (Void# -> r) -> r $mC2 :: forall r a. X (Maybe a) -> ( a -> r) -> (Void# -> r) -> r $mC3 :: forall r a. (Eq a) => X (Maybe a) -> ( a -> r) -> (Void# -> r) -> r }}} If `C2` got the same type as `C1`, what would be the analogous type for `C3`? What would be `$mC3`'s type in that case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): The inferred type of `C1` should be isomoprhic to the declared type of `C2`. That is you should be able to declare `C2`'s type as {{{ pattern C2 :: (t ~ Maybe a) => a -> X t }}} if you want. Just as you can in a GADT declaration: the data constructor decl {{{ C :: arg1 -> arg2 -> T (Maybe a) }}} is precisely equivalent to (i.e. indistinguishable from) {{{ C :: (t ~ Maybe a) => arg1 -> arg2 -> T t }}} In the same way, you should be able to declare `C3`'s type as {{{ pattern C3 :: (t ~ Maybe a) => (Eq a) => a -> X t }}} if you want. As discussed in #9954, `C3` is simply ill typed. Does that resolve it? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 goldfire): Replying to [comment:9 simonpj]:
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).
Yech. This means that declaring a pattern synonym for a GADT data constructor requires writing the type differently than the idiomatic way to do it for data constructors. I think a second '''principle''' might be this: The type signature for a pattern should mean the same thing that it would for a data constructor. It strikes me that this problem is precisely the same as the required vs. produced distinction. In your `P2`, `t ~ Maybe a` is a requirement; in your `P1`, it's provided. I don't have a better concrete suggestion at the moment, sadly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): No, it's quite different to the produced/required distinction. The produced/required distinction is for things like matching against `(Just 34)`, which required `(Num a, Eq a)` to perform the match. And my point is that we '''cannot''' say that the type signature for a pattern should mean the same thing that it would for a data constructor; the type signatures for `P1` and `P2` make this clear. It may be sad but it's absolutely ineluctable. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 goldfire): Here's the example in play: {{{ 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] }}} Couldn't we write these type signatures as {{{ pattern P1 :: (t ~ Maybe a) => () => a -> T t pattern P2 :: () => (t ~ Maybe a) => a -> [t] }}} ? And, I disagree with Simon's conclusion that we cannot have pattern type signatures mean the same as data constructor signatures. We could decide than any non-uniformity in the result type of a pattern signature means a provided equality, just like a GADT. Then, the syntax of the type for `P2` would have to change to something else -- after all, `P2` is not the synonym of any valid data constructor. As we're thinking about this, it strikes me that there is some relationship between the current debate and the distinction between GADTs and data families. For example: {{{ data G a where MkGInt :: G Int data family H a data instance H Int where MkHInt :: H Int }}} `MkGInt` is a GADT constructor that provides an equality when matching. `MkHInt`, on the other hand, '''requires''' the equality when matching. Yet both have the same type signature. So, something a little confusing is going on here. Do pattern synonyms work properly with data families? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Well Richard, you are proposing that you can write `P1`'s type signature just like `T1`'s. Fair enough, I can see some merit; indeed it was my initial position. But then you '''must''' write `P2`'s type signature in some other way. What other way do you propose?? Since we already ''have'' two different ways to write the signature, we are at liberty to decide that those two different ways define two different behaviours; and that is what I am proposing. Yes, we could invent a third way, but that introduces a whole new raft of complications. (E.g. can you use that third way in a GADT declaration? For an ordinary function? etc) I'm totally open to considering alternative. But until we have one, let's get on with implementing the proposal we have. That is often illuminating; and if we come up with a better idea meanwhile we can retro- fit it easily enough. For data families, I think it should all work fine. But indeed we should check. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 cactus): I have no idea what the proposal is anymore... which I find a bit worrying, given I am supposed to implement it. Right now, on `master` as of `6f818e08`, this is the behaviour you get: {{{ {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-} module ShouldCompile where data X b where Y :: [a] -> X (Maybe a) pattern C1 :: [a] -> X (Maybe a) pattern C1 x <- Y x pattern C2 x <- Y x pattern C3 :: (t ~ Maybe a) => [a] -> X t pattern C3 x <- Y x }}} with this setup, you get {{{ λ» :i C1 pattern C1 :: [a] -> X (Maybe a) -- Defined at T9953-3.hs:8:9 λ» :i C2 pattern C2 :: t ~ Maybe a => [a] -> X t -- Defined at T9953-3.hs:10:9 λ» :i C3 pattern C3 :: t ~ Maybe a => [a] -> X t -- Defined at T9953-3.hs:13:9 }}} Isn't this exactly the behaviour specified by Simon's latest comment? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Correct. The original ticket description says "Without fixing it, GADT- style pattern signatures are all but useless", and the conclusion of the discussion is that we can't use GADT-style pattern signatures! So yes, all that remains is to review the user manual to ensure that it makes this point explicit. I don't think we need any implementation changes. (Contrary to my initial supposition.) Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Simon Peyton Jones
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: merge 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: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: OK I fixed the user manual myself. Let's merge the change into 7.10 (assuming that the prior stuff about pattern signatures is in, which I think it is). Simoin -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-7.10` (via 53af4bb5cd4531f0615a2a60b6d213495261e41a). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by bgamari): It appears that there are still two tests marked as broken due to this issue (`T8968-1` and `T8968-3`). They appear to be fixed by either 28096b274a3803b8a479c5dd94ebda655a15566c or 953648127cea2836ec134b03a966695ac0b36434 (both commits by Simon PJ). Simon, is this an expected consequence of this rework? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): I'm looking at it; it's tricky stuff. Meanwhile, you could make validate work again, opening a ticket for this issue, so that everyone else was not inconvenienced. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs -------------------------------------+------------------------------------- Reporter: simonpj | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by bgamari): The real question is why were these tests marked as broken against a closed ticket? Are they actually expected to work? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9953#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9953: Pattern synonyms don't work with GADTs
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: cactus
Type: bug | Status: closed
Priority: normal | Milestone: 7.10.1
Component: Compiler (Type | Version: 7.10.1-rc1
checker) | Keywords:
Resolution: fixed | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by simonpj):
OK. I believe the "expect-broken" is because we get (odd-looking) error
{{{
T8968-1.hs:8:9: warning:
Redundant constraint: Maybe a ~ Maybe a
In the type signature for: C :: a -> X Maybe (Maybe a)
}}}
Now one of the minor changes in
{{{
commit 953648127cea2836ec134b03a966695ac0b36434
Author: Simon Peyton Jones
#9953: Pattern synonyms don't work with GADTs
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: cactus
Type: bug | Status: closed
Priority: normal | Milestone: 7.10.1
Component: Compiler (Type | Version: 7.10.1-rc1
checker) | Keywords:
Resolution: fixed | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
participants (1)
-
GHC