
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
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
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
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