[GHC] #11977: ghc doesn't agree with its own inferred pattern type

:i F
#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHCi, version 8.1.20160419: {{{ pattern F a <- (($ 'a') -> a) }}} {{{ pattern F :: b -> Char -> b -- Defined at /tmp/tTaa.hs:24:1 }}} Putting them together: {{{ -- tTaa.hs:25:9: error: … -- • Pattern synonym ‘F’ has one argument -- but its type signature has two -- • In the declaration for pattern synonym ‘F’ Compilation failed. pattern F :: b -> Char -> b pattern F a <- (($ 'a') -> a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mpickering, cactus (added) Comment: Very interesting test case! You've discovered that, once again, we've misunderstood pattern types. If you assign a pattern the type `a -> b -> c` (where `a`, `b`, and `c` are arbitrary types, not necessarily variables; that is, they are metavariables), we've been saying that `a` and `b` are arguments to the pattern and `c` is the result type. But in your case, the type is `a -> Char -> a`, and `Char -> a` is the result type. Yet there is no way to indicate this in a type signature. I even tried `a -> (Char -> a)` to no avail. I have no suggestions (other than parentheses, which would be awkward) for how to fix this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: => PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by cactus): Ewww. In the representation of `PatSyn`s, the types of arguments and the type of the scrutinee are stored separately, so that shouldn't be an issue. However, I have no idea what the surface syntax should be for presenting such a type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I had always taken it for granted that a pattern synonym described a data type, not a function. It's hard to pattern match in an interesting way on a function, short of calling it I suppose. Lacking compelling examples, I'm inclined to add the requirement that the result type of a pattern synonym is a data type. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But it currently can be a type variable (when constrained by a class). If we don't allow functions to be matched against in this way, we lose substitution. This isn't a killer (it's all surface Haskell and in no way is a type safety issue), just a bit suboptimal to me. I actually think the original example looks potentially useful. I could see waiting until someone presents an actual use case they wish to use in real code, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Here's is an odd thing, it works if you quantify it! {{{#!hs -- Doesn't work! -- pattern F :: b -> forall x. Char -> b -- pattern F a <- (($ 'a') -> a) -- Does work for some reason pattern F1 :: b -> forall x. Char -> b pattern F1 a <- (($ 'a') -> a) -- Wait what? pattern F2 :: b -> forall b. Char -> b pattern F2 a <- (($ 'a') -> a) }}} How does this play out {{{#!hs -- Inferred type f1 :: (forall (x :: k). Char -> b) -> b f1 (F1 x) = x -- Works exactly like: -- -- f1 (($ 'a') -> x) = x -- f1 :: (Char -> b) -> b f1 (F1 x) = x }}} with `F2`: {{{#!hs f2 :: (forall b. Char -> b) -> b1 f2 (F2 x) = ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Noticed while looking at Carter's [https://gist.github.com/cartazio/60eac732e7ac162916eaf828c9b1483c copatterns] and saw that the following compiles: {{{#!hs type Stream a = forall res . StreamTag a res -> res data StreamTag a res where HeadTag :: StreamTag a a -- TailTag :: StreamTag a (Stream a) pattern Head' :: res -> Stream res pattern Head' x <- (($ HeadTag) -> x) }}} but it is my understanding that `Stream` must be a newtype/data (generative) to be able to define `TailTag`: {{{#!hs newtype Stream a = Stream (forall res. StreamTag a res -> res) data StreamTag a res where HeadTag :: StreamTag a a TailTag :: StreamTag a (Stream a) pattern Head :: a -> Stream a pattern Head x <- ((\(Stream str) -> str HeadTag) -> x) pattern Tail :: Stream a -> Stream a pattern Tail xs <- ((\(Stream str) -> str TailTag) -> xs) pattern Cons :: a -> Stream a -> Stream a pattern Cons x xs <- ((\(Stream str) -> (str HeadTag, str TailTag)) -> (x, xs)) headStream :: Stream a -> a headStream (Head x) = x tailStream :: Stream a -> Stream a tailStream (Tail xs) = xs rawRawZipWith :: (a -> b -> c) -> (Stream a -> Stream b -> Stream c ) rawRawZipWith f sta stb = Stream $ \str -> do let Head x = sta Head y = stb Tail xs = sta Tail ys = stb case str of HeadTag -> f x y TailTag -> rawRawZipWith f xs ys rawRawZipWith' :: (a -> b -> c) -> (Stream a -> Stream b -> Stream c) rawRawZipWith' f (Cons x xs) (Cons y ys) = Stream $ \case HeadTag -> f x y TailTag -> rawRawZipWith f xs ys }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Just fooling around {{{#!hs pattern Mempty :: Monoid a => b -> forall x. a -> b pattern Mempty b <- (($ mempty) -> b) where Mempty b _ = b }}} {{{#!hs pattern Mempty :: b -> forall a. (Eq a, Monoid a) => a -> b pattern Mempty b <- (($ mempty @String) -> b) where Mempty b _ = b foo :: (forall a. (Eq a, Monoid a) => a -> b) -> b foo (Mempty x) = x }}} {{{ ghci> foo (== mempty) True ghci> :t Mempty 'a' Mempty 'a' :: forall {a}. (Monoid a, Eq a) => a -> Char ghci> :t foo (Mempty 'a') foo (Mempty 'a') :: Char ghci> foo (Mempty 'a') 'a' }}} or {{{#!hs type MEMPTY b = forall a. (Eq a, Monoid a) => a -> b pattern Mempty :: b -> MEMPTY b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): No quantification needed if returning a type synonym: {{{#!hs type Arr = (->) pattern App :: b -> Arr Char b pattern App b <- (($ 'a') -> b) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I have a fix in the works -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11977: ghc doesn't agree with its own inferred pattern type
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.1
Resolution: | Keywords:
| PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#11977: ghc doesn't agree with its own inferred pattern type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | patsyn/should_compile/T11977 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => patsyn/should_compile/T11977 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11977#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC