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@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@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@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@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