User's guide: newtype decls can use GADTSyntax

The user's guide failed to explicitly mention that GADTSyntax can be used to declare newtypes, so we add an example and a couple of explanations. Also clarifies that -XGADTs enables existential quantification (though technically not the extension -XExistentialQuantification). See #20848 (closed) and #20865 (closed).