#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