[GHC] #9226: Internal error when using equality constraint in pattern synonyms
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.8.2 Keywords: renamer, pattern | Operating System: Linux synonyms, GADTs | Type of failure: GHC rejects Architecture: x86 | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- While going through [http://www.andres-loeh.de/dgp2005.pdf Extensible datatypes] I had the following code: {{{ {-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, Rank2Types #-} data Rep a where RUnit :: Rep () RInt :: Rep Int RChar :: Rep Char REither :: Rep a -> Rep b -> Rep (Either a b) RPair :: Rep a -> Rep b -> Rep (a, b) foo :: (Rep a, a) -> Bool foo (RUnit, ()) = True }}} And I wanted to make a pattern synonyms matching `(RUnit, ())` in `foo`, my initial attempt was: {{{ pattern PUnit1 = (RUnit, ()) }}} gives the error (`punit1.log`) while writing {{{ pattern PUnit2 = (RUnit, ()) :: (Rep (), ()) }}} compiles but can't be used in `foo`. Trying: {{{ pattern PUnit3 = (RUnit, ()) :: (a ~ ()) => (Rep a, a) }}} gives a ''GHC internal error'' (`punit3.log`). I tried various other patterns such as: {{{ pattern PUnit4 <- (RUnit, ()) pattern PUnit5 <- (RUnit, ()) :: (Rep (), ()) pattern PUnit6 <- (RUnit, ()) :: (a ~ ()) => (Rep a, a) pattern PUnit7 = (RUnit, ()) :: forall a. (a ~ ()) => (Rep a, a) pattern PUnit8 <- (RUnit, ()) :: forall a. (a ~ ()) => (Rep a, a) ... }}} None of which work. The final goal was to rewrite: {{{ eq :: Rep a -> a -> a -> Bool eq rep a b = case (rep, a, b) of (RUnit, (), ()) -> True (RInt, n1, n2) -> n1 == n2 (RChar, c1, c2) -> c1 == c2 (REither l r, Left a, Left b) -> eq l a b (REither l r, Right a, Right b) -> eq r a b (REither{}, _, _) -> False (RPair l r, (a1, a2), (b1, b2)) -> eq l a1 b1 && eq r a2 b2 }}} as something like {{{ pattern PUnit = (RUnit, ()) -- (a ~ ()) => (Rep a, a) pattern PInt n = (RInt, n) -- (a ~ Int) => (Rep a, a) -- ... eq :: Rep a -> a -> a -> Bool eq rep a b = case ((rep, a), (rep, b)) of (PUnit, PUnit) -> True (PInt n1, PInt n2) -> n1 == n2 (PChar c1, PChar c2) -> c1 == c2 (PLeft l l1, PLeft l l2) -> eq l l1 l2 (PRight r r1, PRight r r2) -> eq r r1 r2 ((REither{}, _), _) -> False (PFst l (a1, b1), PSnd r (a2, b2)) -> eq l a1 b1 && eq r a2 b2 }}} where one can avoid pattern matching against the `Rep` constructor directly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: renamer, pattern Operating System: Linux | synonyms, GADTs Type of failure: GHC rejects | Architecture: x86 valid program | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------- Changes (by simonpj): * cc: cactus (added) Comment: You are absolutely right; there is a gaping hole in the pattern-synonym implementation. Gergo, the issue is this. When typechecking anything to do with GADTs, we need a type signature. The [wiki:PatternSynonyms wiki page] describes signatures for pattern synonyms, but they are not implemented. the `HsBinds.Sig` type has `PatSynSig`, but the parser does not recognise them, nor does the typechechecker do anything with them. Notably, in `tcPatSynDecl` we'll need to implement different code to ''check'' that the synonym has a specified type than to ''infer'' the type it has. While fixing this, I found another crash. This {{{ pattern PUnit1 = (RUnit, ()) :: (Rep a, a) }}} crashes with {{{ T9226.hs:15:38: GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer }}} Would you like to look at this Gergo? I'm happy to help. Meanwhile, iceland_jack, I think you're stalled till we do this. Thanks for reporting it. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: renamer, pattern Operating System: Linux | synonyms, GADTs Type of failure: GHC rejects | Architecture: x86 valid program | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8968 -------------------------------------+------------------------------------- Changes (by kosmikus): * related: => #8968 Comment: Also see #8968 for my own experiences trying to use pattern synonyms for GADTs and lots of discussion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: renamer, pattern Operating System: Linux | synonyms, GADTs Type of failure: GHC rejects | Architecture: x86 valid program | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8968 -------------------------------------+------------------------------------- Comment (by Iceland_jack): The example wasn't anything serious so I can cope. Seeing how I've filed 4 reports about pattern synonyms in such a short time I seem to be abusing the extension somehow :) the response time here is jolly good, thank you for your efforts -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: renamer, pattern Operating System: Linux | synonyms, GADTs Type of failure: GHC rejects | Architecture: x86 valid program | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: #8968 -------------------------------------+------------------------------------- Comment (by simonpj): I'd forgotten all about #8968. Yes, this ticket is really a dup of #8968. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: | Owner: Iceland_jack | Status: closed Type: bug | Milestone: Priority: lowest | Version: 7.8.2 Component: Compiler | Keywords: renamer, pattern Resolution: duplicate | synonyms, GADTs Operating System: Linux | Architecture: x86 Type of failure: GHC | Difficulty: Unknown rejects valid program | Blocked By: Test Case: | Related Tickets: #8968 Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * status: new => closed * resolution: => duplicate -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9226: Internal error when using equality constraint in pattern synonyms -------------------------------------+------------------------------------- Reporter: | Owner: Iceland_jack | Status: closed Type: bug | Milestone: Priority: lowest | Version: 7.8.2 Component: Compiler | Keywords: renamer, Resolution: duplicate | PatternSynonyms, GADTs Operating System: Linux | Architecture: x86 Type of failure: GHC | Difficulty: Unknown rejects valid program | Blocked By: Test Case: | Related Tickets: #8968 Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: renamer, pattern synonyms, GADTs => renamer, PatternSynonyms, GADTs -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9226#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC