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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
