#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