GHC Panics when encoding Russel's paradox using GADTs
The following encoding of Russel's paradox using GADTs causes GHC to panic.
{-# 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] { }