On Dec 3, 2020, at 11:58 AM, Simon Peyton Jones <simonpj@microsoft.com> wrote:

Yes, but there is no prospect (that I know of) of a substantial improvement in [type inference for GADTs] – and what we have does not seem to cause problems in practice. And they are jolly useful and popular!

The problem I described would arise when someone who does not know about GADTs and type inference accidentally writes a GADT. But this cannot happen easily today, precisely because of the need to write the extension.

Useful, popular, and stable all help argue for an extension (and I agree here!), but I'm more concerned about error messages and the beginner experience, captured in our Criterion 2 of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria.

Richard