Allowing (Char ~ Bool => Void)?

[Shachaf Ben-Kiki]

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