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

Iavor Diatchki iavor.diatchki at gmail.com
Mon Mar 22 16:17:23 UTC 2021


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 <eric at seidel.io> 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 <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
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210322/d44fc187/attachment.html>


More information about the ghc-steering-committee mailing list