<div dir="ltr">Ok, then. I think that we can mark this proposal as accepted.<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 25 Nov 2022 at 09:58, 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">On 24/11/2022 09:22, Arnaud Spiwack wrote:<br>
> Adam makes an excellent point. GADTs defined with explicit equality <br>
> constraints and then promoted is likely to be the main reason for <br>
> breakage. If only because programmers doing that would probably not even <br>
> really be aware that they are using constraints in kinds. On the other <br>
> hand, I don't think that it's super common to defined a GADT that way, <br>
> so the number of promoted GADTs will be small.<br>
> <br>
> Adam, do you nevertheless support acceptance? Does anybody else have an <br>
> opinion? I intend to mark the proposal as accepted tomorrow unless there <br>
> is clear opposition.<br>
<br>
Yes, I'm okay with acceptance. As you say, this is not the most common <br>
way to define GADTs, and given that (a) any class context prevents use <br>
in types, and (b) dependent pattern matching on GADTs doesn't work in <br>
type families anyway, it seems best to take the simple position that any <br>
context at all prevents use of a data constructor in a type.<br>
<br>
Cheers,<br>
<br>
Adam<br>
<br>
<br>
> On Tue, 22 Nov 2022 at 10:32, Adam Gundry <<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a> <br>
> <mailto:<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a>>> wrote:<br>
> <br>
> 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<br>
> proposal as<br>
> > acceptable sometime before the end of the week.<br>
> ><br>
> > On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack<br>
> <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a> <mailto:<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><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<br>
> 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<br>
> 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>><br>
> <mailto:<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>>>><br>
> wrote:<br>
> ><br>
> > Hi,<br>
> ><br>
> > Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud<br>
> Spiwack:<br>
> > > I recommend acceptance.<br>
> ><br>
> > authored by Richard and Simon, and double-checked by<br>
> Arnaud, I’m<br>
> > happy<br>
> > to concur.<br>
> ><br>
> > Cheers,<br>
> > Joachim<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>