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

[Richard Eisenberg]

> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210322/9d3a41f8/attachment.html>