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

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