[GHC] #13125: GHC Panics when encoding Russel's paradox using GADTs
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: panic, GADTs | Operating System: MacOS X Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following encoding of Russel's paradox using GADTs causes GHC to panic, which is understandable as it involves creating a value of an uninhabited data type without using any recursion, which should not be possible as far as I can tell, so this should probably not type check. {{{#!hs {-# LANGUAGE GADTs #-} data False data R a where MkR :: (c (c ()) -> False) -> R (c ()) condFalse :: R (R ()) -> False condFalse x@(MkR f) = f x absurd :: False absurd = condFalse (MkR condFalse) main :: IO () main = absurd `seq` print () }}} When compiled with optimization I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): Simplifier ticks exhausted When trying UnfoldingDone condFalse To increase the limit, use -fsimpl-tick-factor=N (default 100) If you need to do this, let GHC HQ know, and what factor you needed To see detailed counts use -ddump-simpl-stats Total ticks: 6441 }}} When I instead load it into GHCi and type "absurd `seq` ()" I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): atomPrimRep case absurd of _ [Occ=Dead] { } }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by tysonzero: @@ -37,1 +37,1 @@ - When I instead load it into GHCi and type "absurd `seq` ()" I get: + When I instead load it into GHCi and type "{{{absurd `seq` ()}}}" I get: New description: The following encoding of Russel's paradox using GADTs causes GHC to panic, which is understandable as it involves creating a value of an uninhabited data type without using any recursion, which should not be possible as far as I can tell, so this should probably not type check. {{{#!hs {-# LANGUAGE GADTs #-} data False data R a where MkR :: (c (c ()) -> False) -> R (c ()) condFalse :: R (R ()) -> False condFalse x@(MkR f) = f x absurd :: False absurd = condFalse (MkR condFalse) main :: IO () main = absurd `seq` print () }}} When compiled with optimization I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): Simplifier ticks exhausted When trying UnfoldingDone condFalse To increase the limit, use -fsimpl-tick-factor=N (default 100) If you need to do this, let GHC HQ know, and what factor you needed To see detailed counts use -ddump-simpl-stats Total ticks: 6441 }}} When I instead load it into GHCi and type "{{{absurd `seq` ()}}}" I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): atomPrimRep case absurd of _ [Occ=Dead] { } }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by carter): * status: new => closed * resolution: => duplicate Comment: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/bugs.html #bugs-in-ghc see the remark at the end {{{ GHC’s inliner can be persuaded into non-termination using the standard way to encode recursion via a data type: data U = MkU (U -> Bool) russel :: U -> Bool russel u@(MkU p) = not $ p u x :: Bool x = russel (MkU russel) The non-termination is reported like this: ghc: panic! (the 'impossible' happened) (GHC version 7.10.1 for x86_64-unknown-linux): Simplifier ticks exhausted When trying UnfoldingDone x_alB To increase the limit, use -fsimpl-tick-factor=N (default 100) with the panic being reported no matter how high a -fsimpl-tick-factor you supply. We have never found another class of programs, other than this contrived one, that makes GHC diverge, and fixing the problem would impose an extra overhead on every compilation. So the bug remains un-fixed. There is more background in Secrets of the GHC inliner. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): The first panic is certainly a duplicate of this. I'm not sure the second panic is duplicate? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): Perhaps #12128? I could reproduce this on 8.0.1 but with HEAD it just loops forever. Thanks for the report! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by tysonzero: @@ -2,3 +2,1 @@ - panic, which is understandable as it involves creating a value of an - uninhabited data type without using any recursion, which should not be - possible as far as I can tell, so this should probably not type check. + panic. @@ -24,1 +22,1 @@ - When compiled with optimization I get: + When compiled with optimizations I get: New description: The following encoding of Russel's paradox using GADTs causes GHC to panic. {{{#!hs {-# LANGUAGE GADTs #-} data False data R a where MkR :: (c (c ()) -> False) -> R (c ()) condFalse :: R (R ()) -> False condFalse x@(MkR f) = f x absurd :: False absurd = condFalse (MkR condFalse) main :: IO () main = absurd `seq` print () }}} When compiled with optimizations I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): Simplifier ticks exhausted When trying UnfoldingDone condFalse To increase the limit, use -fsimpl-tick-factor=N (default 100) If you need to do this, let GHC HQ know, and what factor you needed To see detailed counts use -ddump-simpl-stats Total ticks: 6441 }}} When I instead load it into GHCi and type "{{{absurd `seq` ()}}}" I get: {{{ ghc: panic! (the 'impossible' happened) (GHC version 8.0.1 for x86_64-apple-darwin): atomPrimRep case absurd of _ [Occ=Dead] { } }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by carter): @mpickering perhaps the ghci panic is valid because this type gives a weak form of unsafe coerce? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tysonzero): Should the issue be re-opened until we are sure that the second panic is either a duplicate or resolved? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): I said the panic is a duplicate of #12128 and I verified it doesn't happen on HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13125: GHC Panics when encoding Russel's paradox using GADTs -------------------------------------+------------------------------------- Reporter: tysonzero | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: panic, GADTs Operating System: MacOS X | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tysonzero): Ok great, thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13125#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC