[GHC] #9954: Required constraints are not inferred for pattern synonyms involving GADTs
#9954: Required constraints are not inferred for pattern synonyms involving GADTs -------------------------------------+------------------------------------- Reporter: cactus | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects PatternSynonyms | valid program Architecture: | Blocked By: Unknown/Multiple | Related Tickets: #9953 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Let's say we have the following setup: {{{#!hs {-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-} data T a where MkT1 :: a -> T a MkT2 :: a -> T (Maybe a) f :: (Eq a) => a -> a f = id }}} Then the following definition works as expected: {{{#!hs pattern P1 x <- MkT1 (f -> x) }}} with the following inferred type: {{{ λ» :i P1 pattern P1 :: () => Eq t => t -> T t }}} However, trying to do the same with {{MkT2}} doesn't work: {{{#!hs pattern P2 x <- MkT2 (f -> x) }}} this results in {{{ Could not deduce (Eq a1) arising from a use of ‘f’ from the context (t ~ Maybe a1) bound by a pattern with constructor MkT2 :: forall a. a -> T (Maybe a), in a pattern synonym declaration }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9954 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9954: Required constraints are not inferred for pattern synonyms involving GADTs -------------------------------------+------------------------------------- Reporter: cactus | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9953 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): This looks absolutely correct to me. Try it with an ordinary function, without the synonym: {{{ boo :: T a -> Bool boo (MkT2 (f -> x)) = True }}} and you get {{{ T9954.hs:12:12: Could not deduce (Eq a1) arising from a use of `f' from the context a ~ Maybe a1 bound by a pattern with constructor: MkT2 :: forall a. a -> T (Maybe a), in an equation for `boo' at T9954.hs:12:6-18 Possible fix: add (Eq a1) to the context of the data constructor `MkT2' In the expression: f In the pattern: f -> x In the pattern: MkT2 (f -> x) }}} And indeed, from where can we conjure up equality on the existentially- bound type? So to me this looks like precisely the correct behaviour. Siimon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9954#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9954: Required constraints are not inferred for pattern synonyms involving GADTs -------------------------------------+------------------------------------- Reporter: cactus | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: checker) | Keywords: Resolution: invalid | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9953 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9954#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC