Niklas Broberg wrote:
data Foo = forall a . Show a => Foo a
which uses ExistentialQuantification syntax, could be written as
data Foo where Foo :: forall a . Show a => a -> Foo
The downside is that we lose one level of granularity in the type system. GADTs enables a lot more semantic possibilities for constructors than ExistentialQuantification does, and baking the latter into the former means we have no way of specifying that we *only* want to use the capabilities of ExistentialQuantification.
Is it easy algorithmically to look at a GADT and decide whether it has only ExistentialQuantification features? After all, IIRC, hugs and nhc support ExistentialQuantification but their type systems might not be up to the full generality of GADTs. (GHC's wasn't even quite up to it for quite a long time until around 6.8, when we finally got it right.) -Isaac