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

[Eric Seidel]

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 <eric at seidel.io> 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