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

[Richard Eisenberg]

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