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

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 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 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@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 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@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee