[GHC] #10405: Pattern synonym fails with (Exp Bool) but works with (t ~ Bool => Exp Bool)
#10405: Pattern synonym fails with (Exp Bool) but works with (t ~ Bool => Exp Bool) -------------------------------------+------------------------------------- Reporter: | Owner: Iceland_jack | Status: new Type: bug | Milestone: Priority: normal | Version: 7.10.1-rc1 Component: Compiler | Operating System: Linux (Type checker) | Type of failure: GHC rejects Keywords: | valid program Architecture: x86 | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- The following compiles just fine: {{{#!hs data Exp a where B :: Bool -> Exp Bool pattern Tru = B True pr :: Exp a -> String pr Tru = "true" }}} but add a signature to `Tru`… {{{#!hs pattern Tru :: Exp Bool pattern Tru = B True }}} …and it fails to compile {{{#!hs % ghci -ignore-dot-ghci /tmp/Bug.hs GHCi, version 7.10.0.20150316: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Bug.hs, interpreted ) /tmp/Bug.hs:11:4: Couldn't match type ‘a’ with ‘Bool’ ‘a’ is a rigid type variable bound by the type signature for pr :: Exp a -> String at /tmp/Bug.hs:10:7 Expected type: Exp a Actual type: Exp Bool Relevant bindings include pr :: Exp a -> String (bound at /tmp/Bug.hs:11:1) In the pattern: Tru In an equation for ‘pr’: pr Tru = "true" Failed, modules loaded: none. }}} Checking the inferred type of `pattern Tru = B True` I get {{{#!hs ghci> :i Tru pattern Tru :: t ~ Bool => Exp t }}} which works as expected {{{#!hs pattern Tru :: t ~ Bool => Exp t pattern Tru = B True pr :: Exp a -> String pr Tru = "true" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10405 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10405: Pattern synonym fails with (Exp Bool) but works with (t ~ Bool => Exp t) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: x86 Operating System: Linux | Test Case: Type of failure: GHC rejects | Blocking: valid program | Differential Revisions: Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10405#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10405: Pattern synonym fails with (Exp Bool) but works with (t ~ Bool => Exp t) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: invalid | Architecture: x86 Operating System: Linux | Test Case: Type of failure: GHC rejects | Blocking: valid program | Differential Revisions: Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Changes (by rwbarton): * status: new => closed * resolution: => invalid Comment: I think this is all expected behavior, although the syntax is confusing. See https://downloads.haskell.org/~ghc/latest/docs/html/users_guide /syntax-extns.html#idp23521760 and especially the item "In the common case where CReq is empty, (), it can be omitted altogether." In fact, your example is very similar to the last item under 7.3.9.3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10405#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10405: Pattern synonym fails with (Exp Bool) but works with (t ~ Bool => Exp t) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: invalid | Architecture: x86 Operating System: Linux | Test Case: Type of failure: GHC rejects | Blocking: valid program | Differential Revisions: Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Egg on my face, I should have realised that. Thanks for the response. For anyone in a similar situation and for future evaluation of #9953 I have the expression: {{{#!haskell data Tag a where TInt :: Tag Int TBool :: Tag Bool … data Exp a where Fn₁ :: String -> Tag a -> (a -> b) -> (Exp a -> Exp b) Fn₂ :: String -> Tag a -> Tag b -> (a -> b -> c) -> (Exp a -> Exp b -> Exp c) … }}} To be able to match against expressions of type `Exp a` I needed to add an additional tag for the return type: {{{#!haskell data Exp a where Fn₁ :: String -> Tag a -> Tag b -> (a -> b) -> (Exp a -> Exp b) Fn₂ :: String -> Tag a -> Tag b -> Tag c -> (a -> b -> c) -> (Exp a -> Exp b -> Exp c) … }}} {{{#!haskell pattern Leq :: (a ~ Int, b ~ Int, c ~ Bool) => Exp a -> Exp b -> Exp c pattern Leq a b ← Fn₂ "leq" TInt TInt TBool _ a b where Leq a b = Fn₂ "leq" TInt TInt TBool (<=) a b }}} is the final version. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10405#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC