Skip to content

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] { }
Edited by tysonzero
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information