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.

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.

On Tue, 22 Nov 2022 at 10:32, Adam Gundry <adam@well-typed.com> wrote:

I'm not extremely worried about removing equality constraints in kinds
themselves, but I am slightly worried that this proposal will
unexpectedly prevent (existing) uses of GADTs with DataKinds. If I
understand correctly, this version of MkT will be usable in types:

data T a where
MkT :: Bool -> T Bool

but this will not (even though it could be rewritten to the former):

data T a where
MkT :: a ~ Bool => Bool -> T a

Moreover, this MkT not be usable in types at all:

type family F a
data T a where
MkT :: F a ~ Bool => Bool -> T a

I suppose we can live with this in exchange for the gain in simplicity,
especially as there seems to be agreement that maintaining the feature
is simply too costly. But I would not be all that surprised if some
users' code breaks as a result.

Cheers,

Adam

On 21/11/2022 08:32, Arnaud Spiwack wrote:
> Not many opined. Unless there is opposition, I'll mark the proposal as
> acceptable sometime before the end of the week.
>
> On Thu, 17 Nov 2022 at 11:20, Arnaud Spiwack <arnaud.spiwack@tweag.io
> <mailto:arnaud.spiwack@tweag.io>> wrote:
>
> > authored by Richard and Simon, and double-checked by Arnaud, I’m
> happy
> > to concur.
>
> 😀
>
> To clarify: the main question is whether we are confident that it
> won't break too many users. I don't have divination powers that make
> my word particularly trustworthy on this point. Yet, I do feel
> pretty confident.
>
> On Mon, 14 Nov 2022 at 12:51, Joachim Breitner
> <mail@joachim-breitner.de <mailto:mail@joachim-breitner.de>> wrote:
>
> Hi,
>
> Am Montag, dem 14.11.2022 um 11:28 +0100 schrieb Arnaud Spiwack:
> > I recommend acceptance.
>
> authored by Richard and Simon, and double-checked by Arnaud, I’m
> happy
> to concur.
>
> Cheers,
> Joachim
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
27 Old Gloucester Street, London WC1N 3AX, England

_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee