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