Re: [ghc-steering-committee] Proposal #402 (changes to GADT syntax); rec: accept

If we can get it to the point where GADT signatures are truly a superset of type signatures, then we could unify the two in the parser. We would always parse the superset and reject disallowed signatures, e.g. UNPACK pragmas in function types, with much better error messages! I think that would be a much better solution than banning parens in GADT sigs. On Mon, Mar 22, 2021, at 09:45, Richard Eisenberg wrote:

...

On Mar 19, 2021, at 10:16 PM, Eric Seidel wrote:

Iavor's example of type synonyms is another inconsistency that doesn't seem to be motivated by a technical reason.

Good point. I suppose if we did allow type synonyms there, then GADT sigs really would become more like a superset of the grammar for types.

Note that Agda can pull this off:

...

data T : Set

syn : Set syn = ℕ → T

syn2 : Bool → Set syn2 false = ℕ → T syn2 true = T

data T where MkT : syn MkT2 : syn2 false MkT3 : syn2 true

This is accepted. `syn` is like a type synonym, while `syn2` is like a type family. I don't like having Agda out in front of Haskell in this way. :( Maybe we should just fix these problems instead of banning parens?

Richard