#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): FWIW, I was assuming the problem that SPJ describes is the underlying problem here. I don't know the implementation, but I find it entirely reasonable that pattern synonyms for GADTs will in general require type signatures in order to disambiguate between incomparable types. That's why I started talking about type signatures for pattern synonyms in the first place. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): Thanks. This is actually helping. However, it doesn't seem to work all the time. Consider this small variation of my program above: {{{ {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f a -> X f (Maybe a) -- pattern C :: a -> X Maybe (Maybe a) pattern C x = Y (Just x) :: X Maybe (Maybe a) }}} The `a` variable in the type signature cannot be quantified, because it's the type of `x`. I don't seem to be able to give a type signature to `x` on the LHS. The attempt as given above results in an internal error: {{{ PatKind.hs:7:44: GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [(a5PN, Identifier[x::a, <NotTopLevel>])] In an expression type signature: X Maybe (Maybe a) In the expression: Y (Just x) :: X Maybe (Maybe a) In an equation for ‘$WC’: ($WC) x = Y (Just x) :: X Maybe (Maybe a) }}} Any further ideas? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): After thinking about this some more, I'm getting more confused. How should pattern matching on these pattern synonyms work? Both `P` in SPJ's example and `C` in my examples are bidirectional pattern synonyms, and as an expression, it should be easy enough for GHC to type-check without a type signature. So why require one in this case? The expression type signature and pattern type signature must be the same, after all. (Even for unidirectional ones, I'd argue that probably inferring a type for the pattern itself shouldn't be too difficult.) The main question is whether such synonyms can then be used in order to trigger type refinement. It currently seems they cannot, no matter what type they have. For my original example, consider this: {{{ {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms, ScopedTypeVariables #-} data X :: (* -> *) -> * -> * where Y :: f Int -> X f Int pattern C x = Y (Just x) :: X Maybe Int f :: X Maybe a -> a f (Y (Just x)) = x -- works f (C x) = x -- fails }}} For Simon's example, consider: {{{ {-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, RankNTypes #-} data T a b where MkT :: a -> T a Bool MkX :: T a b Q1 :: T Bool Bool Q2 :: T Bool b Q3 :: T b Bool Q4 :: T b b pattern P1 = MkT True :: T Bool Bool pattern P1a <- MkT True :: T Bool Bool pattern P2a <- MkT True :: forall b. T Bool b pattern P3a <- MkT True :: forall b. T b Bool pattern P4a <- MkT True :: forall b. T b b f :: T Bool b -> Bool f (MkT True) = True -- works f Q1 = True -- works f Q2 = undefined -- works f Q3 = True -- works f Q4 = True -- works f P1 = True -- fails f P1a = True -- fails f P2a = undefined -- fails f P3a = True -- fails f P4a = True -- fails }}} Is it unreasonable to expect this kind of thing to work? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Replying to [comment:6 kosmikus]:

...

Both `P` in SPJ's example and `C` in my examples are bidirectional

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): Replying to [comment:7 simonpj]: pattern synonyms, and as an expression, it should be easy enough for GHC to type-check without a type signature. So why require one in this case? The expression type signature and pattern type signature must be the same, after all.

No, that statement sounds plausible, but it is not right. Consider {{{ data T a where T1 :: a -> T a T2 :: T Int T3 :: T Bool }}} In an expression context, certainly, `T2 :: T Int`, and `T3 :: T Bool`.

{{{ f (T1 _) = True f T2 = True f T3 = False }}} No, as a pattern, both `T2` and `T3` have type `forall a. T a`; that is,

But '''not''' in a pattern context, otherwise this function would be ill- typed: they can soundly (without seg-faulting) match any value of type `T <type>`. So `f :: T a -> Bool`. Ok, we seem to have slightly different terminology when it comes to saying what the "type" of a pattern is. But terminology aside, I agree that `T2` and `T3` should be applicable in a context of type `T a`. But the information that they're `T Int` and `T Bool` "as an expression" must still be around even during pattern matching, because the match causes type refinement accordingly. So in one way or another for a constructor such as `T2` there seem to be *two* types that are important, namely `T Int` and `forall a. T a`.

The trouble is that (as we know well) in the presence of GADTs there may be no unique principal type, which is why !OutsideIn requires type signatures to resolve the uncertainty. It's the same with pattern synonyms.

This is what I also thought at first, but what I'm no longer convinced about. Let's go back to your example: {{{ data T a b where MkT :: a -> T a Bool MkX :: T a b pattern P = MkT True }}} So I guess we agree than "as an expression", `P` must be of type `T Bool Bool`. You say that "as a pattern", it could have either of {{{ P :: T Bool b P :: T b b }}} Yes, ok, but should this information be necessary to provide with the pattern synonym? Isn't this something that should be derived from the type signature of the function in which it is used? Shouldn't I be able to write {{{ f :: T Bool b -> b f P = False }}} and also {{{ g :: T b b -> b g P = False }}} just like I can write {{{ f :: T Bool b -> b f (MkT True) = False }}} as well as {{{ g :: T b b -> b g (MkT True) = False }}} If I'd be forced to provide a type signature for the pattern synonym `P` picking one of the two "pattern types", then `P` would be necessarily more limited in its use than its expansion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

So it's not clear that a single signature for the two ways of looking at

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): the RHS makes sense at all! It look as though we need one for its use as a pattern and one for its use as an expression. Sigh. Yes.

Mind you, the "type as an expression" is easily inferred, as you mention. So perhaps the pattern signature (once we have them) can be taken as applying only to the pattern, not the expression?

I guess it's not clear to me if the other information isn't available as well, if the synonym is used in a function that has a type signature. Is there really a theoretical need to supply a signature for the "pattern type"? See my example in the other comment, I actually wouldn't like to have to pick one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): I agree completely with the function example. I'm just sure about whether the pattern synonym situation is really analogous. The reason is that in {{{ data T a b where MkT :: a -> T a Bool MkX :: T a b pattern P = MkT True }}} I could just pretend that `P` is another constructor of `T`: {{{ data T a b where MkT :: a -> T a Bool MkX :: T a b P :: T Bool Bool }}} Then both `f` and `g` as shown above using `P` would type-check. So if for `P` as a constructor, the information that the "expression type" is `T Bool Bool` and the "target type" is `T a b` is sufficient, then why can't we do the same for `P` as a pattern synonym. That's still modular, IMHO. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Alas, no. If the definition of T really did have that constructor P,

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus): then GADT-style type refinement would take place when you match on P. So for example, this would typecheck:

{{{ f :: T a b -> a -> Bool f P v = v && True }}} But obviously the expansion does not: {{{ f :: T a b -> a -> Bool f (MkT x) v = v && True }}}

The expansion is `MkT True`, but it doesn't matter. Nice example. I'm almost convinced, although I'll have to think about this a bit longer.

Moreover, these are terribly simple examples. In general a pattern synonym might mention dozens of constructor from dozens of types. Which of those types would you like to pretend the pattern synonym constructor is from?

I don't pretend that I have thought this through. I have only played with pattern synonyms for a few days so far, and I don't completely understand the possibilities of the interaction with ViewPatterns yet. However, in the case of bidirectional pattern synonyms I'd expect a pattern synonym to have a clear "target type".

This is what I mean by modularity: no matter how complicated the right hand side of the pattern synonym, I want the client (of the library defining the pattern synonym) to be able to use it by knowing only its type -- just like he can for a function exported by a library.

Yes, that's certainly a valid goal. Ok, for now, let's try to summarize: Every (bidirectional) pattern actually has two types, an "expression type" and a "pattern type". If I understand your proposal correctly, you're saying that pattern type signatures should allow the user specify the pattern type, because the expression type should in general be easy to infer. So I should be able to say {{{ pattern P :: T Bool b pattern P = MkT True }}} or for my original example {{{ pattern C :: Int -> Maybe a pattern C x = Y (Just x) }}} So perhaps GHCi should print both types rather than only the expression type on `:t`, something like: {{{ GHCi> :t C pattern C :: Int -> Maybe a C :: Int -> Maybe Int GHCi> :t P pattern P :: T Bool b P :: T Bool Bool }}} And perhaps for consistency even for normal data constructors? {{{ GHCi> :t MkT pattern MkT :: a -> T a b MkT :: a -> T a Bool }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by kosmikus):

I think that is roughly right, yes. But the pattern type you give above gives no clue that type refinement takes place when you match on it, and a client of `C` definitely needs to know that.

That's why I proposed to show both types, but ...

I think we can print the type of `C` and `MkT` like this: {{{ GHCi> :t MkT MkT :: (b~Bool) => a -> T a b

GHCi> :t C C :: (a~Int) => Int -> X Maybe a

GHCi> pattern D x = MkT (Just x) GHCi> :t D D :: (b~Bool) => a -> T (Maybe a) b }}} These types work nicely both in expressions and patterns.

Yes, I'm certainly happy with this as well. In fact, I had briefly considered making this suggestion. (I think back in GHC 6, GADT constructor types were actually displayed using a similar syntax.) My only worry is that it's slightly subtle that in these cases (where it's a type signature for a constructor or pattern synonym), inlining an equality constraint makes a difference, whereas for expressions it doesn't. But I guess that having two different type signatures printed wouldn't be any easier to understand.

The pattern synonym D is a nice example: * The result type `T (Maybe a) b` says that `D` must only match types of that shape, i.e. where the first arg of `T` is a `Maybe`. * The `(b~Bool) =>` says that when you match on `D` you get that type refinement available in the case alternative.

So this actually a single signature that tells you all you need to know, both for matching and for use in expressions. Good!

Yes, ok.

I should mention that internally the type of a GADT constructor like `MkT` really is as displayed here, namely `MkT :: (b~Bool) => a -> T a b`.

Also good. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by simonpj): Yes, I think it would have to be the latter. Several open issues remain: * We need pattern signatures. The workaround (of a signature embedded in the pattern) doesn't work too well for these more complicated types. * In fact having signatures embedded in a pattern synonym is problematic, because signatures behave differently in patterns and in terms. {{{ g x = Just x :: Maybe a f (Just x :: Maybe a) = x }}} In `g`, the type signature is implicitly quantified, so it really means `Just x :: forall a. Maybe a`, and the definition will therefore be rejected. But in the definition of `f`, the 'a' in the pattern is a ''binding'' occurrence, that scopes over the RHS; there is no implicit quantification. I'm inclined simply to disallow signature in the RHS of a pattern synonym. * We have no good syntax for the required/provided issue. I thought this was written up on the [wiki:PatternSynonyms Pattern Synonym wiki page] but it isn't. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: pattern Type of failure: GHC rejects valid program | synonyms Test Case: | Architecture: Blocking: | Unknown/Multiple | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by cactus): * keywords: => pattern synonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Type signatures for pattern synonyms ----------------------------------------------+---------------------------- Reporter: kosmikus | Owner: cactus Type: feature request | Status: new Priority: normal | Milestone: 7.10.1 Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc2 Operating System: Unknown/Multiple | Keywords: pattern Type of failure: GHC rejects valid program | synonyms Test Case: | Architecture: Blocking: | Unknown/Multiple | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by cactus): * type: bug => feature request * milestone: => 7.10.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Compiler | Version: 7.8.1-rc2 (Type checker) | Keywords: pattern synonyms Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: 8584 Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * type: feature request => bug -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8968: Pattern synonyms and GADTs -------------------------------------+------------------------------------- Reporter: kosmikus | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler | Version: 7.8.1-rc2 (Type checker) | Keywords: PatternSynonyms Resolution: fixed | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: 8584 Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: pattern synonyms => PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler