[ghc-steering-committee] #371: Stop treating ~ magically. Rec: weak accept

[Spiwack, Arnaud]

I've asked a question about the anticipated code simplification but didn't
get a reply. So my opinion has not shifted. But it's not something that I
have strong opinions on either way.

On Mon, May 3, 2021 at 5:41 PM Richard Eisenberg <rae at richarde.dev> wrote:

> Well, I said I would accept by now, but I would like more participation
> here before I feel comfortable doing so.
>
> Specifically:
> * Alejandro and Arnaud have made utterances against this proposal, however
> neither said "I'm against" or something equivalent.
> * Simon PJ just rubber-stamped my recommendation
> * Joachim gave a weak approval (as have I).
>
> Do others have an opinion? Alejandro & Arnaud, have either of you changed
> camps? It would feel better if this were approved by something resembling a
> majority of the committee, instead of just my recommendation with Joachim's
> mild concurrence and SPJ's rubber stamp.
>
> Thanks,
> Richard
>
> > On Apr 23, 2021, at 4:17 PM, Richard Eisenberg <rae at richarde.dev> wrote:
> >
> > To my deep surprise, the following program is accepted:
> >
> >> {-# LANGUAGE GADTSyntax, ExistentialQuantification #-}
> >>
> >> module Bug where
> >>
> >> data G a where
> >>  MkG :: a -> G Int
> >
> > but the following additional definition is rejected:
> >
> >> foo :: G a -> a
> >> foo (MkG _) = 5
> >
> > Adding -XTypeFamilies fixes that last piece, though.
> >
> > Looking through the source code, GADTs implies GADTSyntax and
> MonoLocalBinds, either GADTs or ExistentialQuantification allows the
> declaration of existential variables or a refined return type, either GADTs
> or TypeFamilies allows the use of the `~` syntax, and either GADTs or
> TypeFamilies allows pattern-matching on a constructor with an equality in
> its context. So, GADTSyntax, ExistentialQuantification, and TypeFamilies
> together imply all the functionality of GADTs.
> >
> > This is all very strange, though, and should probably be tidied up. Not
> in this proposal though.
> >
> > Richard
> >
> >> On Apr 23, 2021, at 2:54 PM, Vladislav Zavialov (int-index) <
> vlad.z.4096 at gmail.com> wrote:
> >>
> >> While the use of (~) itself no longer requires -XGADTs, the usual
> desugaring of GADTs still does. So this will require the extension:
> >>
> >> data G a where
> >> MkG :: G Int
> >>
> >> even though this will not:
> >>
> >> data T a where
> >> MkT :: (a~Int) => T a
> >>
> >> Perhaps that is what you meant by ‘vacuous’, but I wouldn’t go as far
> as to say that -XGADTs becomes implied by -XGADTSyntax and
> -XExistentialTypes.
> >>
> >> - Vlad
> >>
> >>> On 22 Apr 2021, at 12:25, Spiwack, Arnaud <arnaud.spiwack at tweag.io>
> wrote:
> >>>
> >>> I'm still not sure what problem this proposal solves. The proposal
> alludes to some code simplification but doesn't give me a good idea of how
> much simpler this would make the code.
> >>>
> >>> Also note that -XGADT becomes mostly vacuous with this proposal:
> -XGADTSyntax + -XExistentialTypes imply GADTs (both are in -XGHC2021). Not
> that I mind, really, I actually probably prefer it this way. But it's
> worthy of notice.
> >>>
> >>> _______________________________________________
> >>> ghc-steering-committee mailing list
> >>> ghc-steering-committee at haskell.org
> >>>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> >>
> >
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
> _______________________________________________
> 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/20210504/cb575840/attachment.html>