I was trying to figure out a way to write absurd :: (forall p. p Char
- p Bool) - Void using only rank-n types. Someone suggested that
Haskell with RankNTypes and a magic primitive of type (forall p. p
Char - p Bool) might be sound (disregarding the normal ways to get ⊥,
of course).
Is that true?
Just because you can't use the 'magic primitive' in question to
produce an element of the empty type doesn't mean the system is sound
(nor does type soundness have anything to do with proving 'false').
The question is what the primitive is supposed to do. If it's supposed
to work as a witness of
