What you suggest would be fine with me. Presumably ExplicitForall would be implied by RankNTypes and the other extensions?
Yes, that's the idea. Rank2Types, RankNTypes, PolymorphicComponents, ScopedTypeVariables and LiberalTypeSynonyms would all imply ExplicitForall.
There is a danger of having too *many* choices. (http://www.joelonsoftware.com/items/2006/11/21.html) In particular, you might consider making ScopedTypeVariables synonymous with ExplicitForAll. Once you have given up the keyword, it seems a shame not to allow lexically scoped type variables!
While I agree with you (and Joel) in principle, I think this is the wrong level to hold that discussion. I think the long-term solution should be to keep the registered extensions cleanly separated, and instead supply extension *groups* as a way to limit choice. -fglasgow-exts has fit that niche admirably for a long time, I think a lot of people just use that without thinking twice about what particular extensions they actually use, and nothing wrong with that. I think the move towards LANGUAGE pragmas instead of compiler options is a good one from a standardisation and implementation point of view, but to avoid tedium and unnecessary choice for the programmer I strongly feel that extension groups need to be introduced at this level too. But as I said, that's for a different discussion...
On ExistentialQuantification, I personally think we should deprecate the entire construct, suggesting GADT-style syntax instead.
+1, though I was afraid to suggest something that radical. I might write a separate proposal for that then, to keep the discussion here focused on ExplicitForall.
If you can form a consensus, go for it.
Alright, let's set an actual discussion period of 2 weeks for ExplicitForall. If there is no opposition by then, we can add ExplicitForall to the registered extensions in cabal as a first step. Cheers, /Niklas