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