<div dir="ltr">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.<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, May 3, 2021 at 5:41 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Well, I said I would accept by now, but I would like more participation here before I feel comfortable doing so.<br>
<br>
Specifically:<br>
* Alejandro and Arnaud have made utterances against this proposal, however neither said "I'm against" or something equivalent.<br>
* Simon PJ just rubber-stamped my recommendation<br>
* Joachim gave a weak approval (as have I).<br>
<br>
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.<br>
<br>
Thanks,<br>
Richard<br>
<br>
> On Apr 23, 2021, at 4:17 PM, Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">rae@richarde.dev</a>> wrote:<br>
> <br>
> To my deep surprise, the following program is accepted:<br>
> <br>
>> {-# LANGUAGE GADTSyntax, ExistentialQuantification #-}<br>
>> <br>
>> module Bug where<br>
>> <br>
>> data G a where<br>
>>  MkG :: a -> G Int<br>
> <br>
> but the following additional definition is rejected:<br>
> <br>
>> foo :: G a -> a<br>
>> foo (MkG _) = 5<br>
> <br>
> Adding -XTypeFamilies fixes that last piece, though.<br>
> <br>
> 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.<br>
> <br>
> This is all very strange, though, and should probably be tidied up. Not in this proposal though.<br>
> <br>
> Richard<br>
> <br>
>> On Apr 23, 2021, at 2:54 PM, Vladislav Zavialov (int-index) <<a href="mailto:vlad.z.4096@gmail.com" target="_blank">vlad.z.4096@gmail.com</a>> wrote:<br>
>> <br>
>> While the use of (~) itself no longer requires -XGADTs, the usual desugaring of GADTs still does. So this will require the extension:<br>
>> <br>
>> data G a where<br>
>> MkG :: G Int<br>
>> <br>
>> even though this will not:<br>
>> <br>
>> data T a where<br>
>> MkT :: (a~Int) => T a<br>
>> <br>
>> 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.<br>
>> <br>
>> - Vlad<br>
>> <br>
>>> On 22 Apr 2021, at 12:25, Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>> wrote:<br>
>>> <br>
>>> 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.<br>
>>> <br>
>>> 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.<br>
>>> <br>
>>> _______________________________________________<br>
>>> ghc-steering-committee mailing list<br>
>>> <a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
>>> <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
>> <br>
> <br>
> _______________________________________________<br>
> ghc-steering-committee mailing list<br>
> <a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
> <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
<br>
_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>