Proposal: Deprecate ExistentialQuantification

[Niklas Broberg]

> That's why one should really be allowed to group constructor's in a type's
> definition:
>
>  data Colour :: * where
>    Red, Green, Blue :: Colour
>
> This is consistent with what is allowed for type signatures for functions.

Totally agreed, and that should be rather trivial to implement too.

> More general, whatever way your proposal is going, I think you should have
> it reflect that there are two, more or less unrelated, issues here:
>
> 1. The expressiveness of data types: algebraic data types < existential data
> types < GADTs.
> 2. The syntax of type definitions: the classic, Haskell 98 syntax and the
> new, cool listings-of-constructor-signature syntax. (Don't call the latter
> NewTypeSyntax or anything similar in a LANGUAGE pragma; choose something
> descriptive.)
>
> These are really orthogonal issues: all three levels of expressiveness of
> types can be expressed in either syntax. Therefore: keep these issues
> separated in your proposal.

Well, I think my proposal already does reflect this fact, if
implicitly. The point of the proposal is that all three levels of
expressiveness of types can be expressed in the
listings-of-constructor-signature syntax, but to express the type
level power of existential data types or GADTs with the classic
syntax, we need to extend that syntax. And that's what I'm after,
that's we remove this rather ad-hoc add on syntax required to express
existential quantification with classic constructor declarations.

In other words, in your 2x3 grid of syntactic x expressiveness, I want
the two points corresponding to classic syntax x {existential
quantification, GADTs} to be removed from the language. My second
semi-proposal also makes each of the three points corresponding to the
new cool syntax a separate extension.

Cheers,

/Niklas