<div dir="ltr"><div>Adam makes an excellent point. GADTs defined with explicit equality constraints and then promoted is likely to be the main reason for breakage. If only because programmers doing that would probably not even really be aware that they are using constraints in kinds. On the other hand, I don't think that it's super common to defined a GADT that way, so the number of promoted GADTs will be small.</div><div><br></div><div>Adam, do you nevertheless support acceptance? Does anybody else have an opinion? I intend to mark the proposal as accepted tomorrow unless there is clear opposition.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 22 Nov 2022 at 10:32, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</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">I'm not extremely worried about removing equality constraints in kinds <br>
themselves, but I am slightly worried that this proposal will <br>
unexpectedly prevent (existing) uses of GADTs with DataKinds. If I <br>
understand correctly, this version of MkT will be usable in types:<br>
<br>
   data T a where<br>
     MkT :: Bool -> T Bool<br>
<br>
but this will not (even though it could be rewritten to the former):<br>
<br>
   data T a where<br>
     MkT :: a ~ Bool => Bool -> T a<br>
<br>
Moreover, this MkT not be usable in types at all:<br>
<br>
   type family F a<br>
   data T a where<br>
     MkT :: F a ~ Bool => Bool -> T a<br>
<br>
I suppose we can live with this in exchange for the gain in simplicity, <br>
especially as there seems to be agreement that maintaining the feature <br>
is simply too costly. But I would not be all that surprised if some <br>
users' code breaks as a result.<br>
<br>
Cheers,<br>
<br>
Adam<br>
<br>
<br>
On 21/11/2022 08:32, Arnaud Spiwack wrote:<br>
> Not many opined. Unless there is opposition, I'll mark the proposal as <br>
> acceptable sometime before the end of the week.<br>
> <br>
> On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a> <br>
> <mailto:<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>>> wrote:<br>
> <br>
>      > authored by Richard and Simon, and double-checked by Arnaud, I’m<br>
>     happy<br>
>      > to concur.<br>
> <br>
>     😀<br>
> <br>
>     To clarify: the main question is whether we are confident that it<br>
>     won't break too many users. I don't have divination powers that make<br>
>     my word particularly trustworthy on this point. Yet, I do feel<br>
>     pretty confident.<br>
> <br>
>     On Mon, 14 Nov 2022 at 12:51, Joachim Breitner<br>
>     <<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a> <mailto:<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>>> wrote:<br>
> <br>
>         Hi,<br>
> <br>
>         Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack:<br>
>          > I recommend acceptance.<br>
> <br>
>         authored by Richard and Simon, and double-checked by Arnaud, I’m<br>
>         happy<br>
>         to concur.<br>
> <br>
>         Cheers,<br>
>         Joachim<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>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="https://www.well-typed.com/" rel="noreferrer" target="_blank">https://www.well-typed.com/</a><br>
<br>
Registered in England & Wales, OC335890<br>
27 Old Gloucester Street, London WC1N 3AX, England<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>