Proposal: Deprecate ExistentialQuantification

[Niklas Broberg]

>> I would hereby like to propose that the
>> ExistentialQuantification extension is deprecated.
>
> It is worth pointing out that all current Haskell implementations (to my
> knowledge) have ExistentialQuantification, whilst there is only one Haskell
> implementation that has the proposed replacement feature, GADTs.
>
> Of course, that in itself is not an argument to avoid desirable change to
> the language, but it is one factor to consider.

The tongue-in-cheek response is that it should be a factor to consider
only for how long a deprecation period we want... ;-)

Seriously though, it's of course a consideration that should be made.
It also ties back to the problem of the monolithic GADTs extension,
which isn't trivial to implement in other tools - but the
ExistentialQuantification *subset* of GADTs should be easy, for any
implementation that already supports the current
ExistentialQuantification extension, since then it's just a syntactic
issue.

So might as well bite that bullet then, what if we did the following
split, in the spirit of the various increasing power of the extensions
that enable forall-quantified types ((ExplicitForall <=)
PolymorphicComponents <= Rank2Types <= RankNTypes):

* NewConstructorSyntax: Lets the programmer write data types using the
GADTs *syntax*, but doesn't add any type-level power (and no forall
syntax). Could probably use a better name (bikeshed warning).

* ExistentialQuantification: Implies NewConstructorSyntax (and
ExplicitForall). Let's the programmer use existentially quantified
arguments to constructors when using the GADTs syntax. Still requires
all constructors to have the same type, which is the one given in the
header.

* GADTs: Implies ExistentialQuantification. Let's the programmer use
the full type-level power of GADTs.

It might make sense to merge NewConstructorSyntax and
ExistentialQuantification, though I'm not sure naming that merge
ExistentialQuantification would be accurate (naming is the bikeshed
though). Personally I would prefer the full 3-way split, to keep a
clean separation between syntactic and semantic extensions, but it's a
rather weak preference.

If we had something like this split, implementations that already
support ExistentialQuantification at the type level would "only" need
to change their parsers in a simple way (nothing hard, trust me), and
add what should be a simple check that the constructors all have the
declared type.

Would that be preferable?

Cheers,

/Niklas