[Haskell-cafe] Haskell + RankNTypes + (forall p. p Char -> p Bool) sound?

[Shachaf Ben-Kiki]

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? Given either TypeFamilies or GADTs, you can write
absurd. But it doesn't seem like you can write it with just
RankNTypes. (This is related to GeneralizedNewtypeDeriving, which is
more or less a version of that magic primitive.)

This seems like something that GADTs (/TypeFamilies) give you over
Leibniz equality: You can write

  data Foo a where
    FooA :: Foo Char
    FooB :: Void -> Foo Bool

  foo :: Foo Bool -> Void
  foo (FooB x) = x

Without any warnings. On the other hand

  data Bar a = BarA (Is a Char) | BarB (Is a Bool) Void

  bar :: Bar Bool -> Void
  bar (BarB _ x) = x
  bar (BarA w) = -- ???

Doesn't seem possible. If it's indeed impossible, what's the minimal
extension you would need to add on top of RankNTypes to make it work?
GADTs seems way too big.

    Shachaf