
#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