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

Just FYI, I believe they are already unified in the parser---GHC always parses "something like a type" and then validates it to make sure that all the extras make sense in the given context. I am not sure when the validity check for GADTs happens, but I suspect if the check is delayed sufficiently, GHC could simply "look through the type synonym" to make sure the declaration is OK, which would make the example I gave work, if that's what we wanted. So, I suspect the issue here is more of design, and technically it shouldn't be hard to make the changes one way or another. -Iavor On Mon, Mar 22, 2021 at 6:59 AM Eric Seidel wrote:

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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee