[GHC] #12975: Suggested type signature for a pattern synonym causes program to fail to type check
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple patternsynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Take the following program: {{{#!hs {-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-} import Data.Typeable data T where MkT :: Typeable a => a -> T pattern Cast a <- MkT (cast -> Just a) }}} When compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`: {{{ Top-level binding with no type signature: Cast :: forall b. Typeable b => forall a. Typeable a => b -> T }}} However, using this suggested type signature causes the program to fail to type check: {{{#!hs • Could not deduce (Typeable a0) arising from the "provided" constraints claimed by the signature of ‘Cast’ from the context: Typeable a bound by a pattern with constructor: MkT :: forall a. Typeable a => a -> T, in a pattern synonym declaration at ../foo.hs:9:19-38 In other words, a successful match on the pattern MkT (cast -> Just a) does not provide the constraint (Typeable a0) The type variable ‘a0’ is ambiguous • In the declaration for pattern synonym ‘Cast’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 ocharles): I actually believe the correct type of this pattern is {{{#!hs pattern Cast :: () => Typeable a => a -> T pattern Cast a <- MkT (cast -> Just a) }}} But this is also rejected: {{{ • Could not deduce (Typeable a0) arising from a use of ‘cast’ from the context: Typeable a bound by a pattern with constructor: MkT :: forall a. Typeable a => a -> T, in a pattern synonym declaration at ../foo.hs:9:19-38 The type variable ‘a0’ is ambiguous • In the pattern: cast -> Just a In the pattern: MkT (cast -> Just a) In the declaration for pattern synonym ‘Cast’ }}} I may be wrong with that type though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 mpickering): * keywords: patternsynonyms => PatternSynonyms Comment: The type signature you are looking for is... {{{#!hs pattern Cast :: Typeable b => b -> T pattern Cast a <- MkT (cast -> Just a) }}} `cast` has type `(Typeable a, Typeable b) => a -> Maybe b`, as `MkT` provides `Typeable a` for us, we require `Typeable b` in order to use the function. The inferred type is still wrong in HEAD. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 ocharles): If I only supply one context, which context am I supplying? The provided one, or the required one? That is, are you suggesting `pattern Cast :: () => Typeable b => ...` or `pattern Cast :: Typeable b => () => ...`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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 mpickering): The required one. `req => t` is the same as `req => () => t`. This is different from the first implementation, we changed it last release. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12975: Suggested type signature for a pattern synonym causes program to fail to type check -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | 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): The reported type is sort of right: {{{ Cast :: forall b. Typeable b => forall a. Typeable a => b -> T }}} That is, you can match a value of any type `b` provided it is typeable. So {{{ f (Cast x) = rhs }}} means pretty much {{{ f (MkT y) = case cast y of Just x -> rhs }}} Inside `rhs` we have access to the `Typeable a` constraint bound by `MkT`; that's what the `Typeable a` constraint in the inferred type is saying. But this `Typeable a` provided constraint is no use to `rhs` because we have no values of type `a`. So Matthew's type is less confusing {{{ pattern Cast :: Typeable b => b -> T }}} Offering useless constraints is bad enough; but worse, as you report, it's rejected as ambiguous (for the same reason) if you specify it in a user signature. That is indeed confusing. What I can't see is a robust and convenient way to eliminate the unnecessary constraints and existential variables. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC