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