Is there a good reason that GHC doesn't allow any value of type (Char ~ Bool => Void), even undefined? There are various use cases for this. It's allowed indirectly, via GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x of {}" (with EmptyCase in HEAD) -- but not directly. One thing this prevents, for instance, is CPSifying GADTs: data Foo a = a ~ Char => A | a ~ Bool => B -- valid newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~ Bool => r) -> r } -- unusable Trying to use a type like the latter in practice runs into problems quickly because one needs to provide an absurd value of type (Char ~ Bool => r), which is generally impossible (even if we're willing to cheat with ⊥!). It seems that this sort of thing should be doable. Shachaf