[ghc-steering-committee] #547: Remove kind constraints, Recommendation: accept

[Arnaud Spiwack]

Ok, then. I think that we can mark this proposal as accepted.

On Fri, 25 Nov 2022 at 09:58, Adam Gundry <adam at well-typed.com> wrote:

> On 24/11/2022 09:22, Arnaud Spiwack wrote:
> > 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.
>
> Yes, I'm okay with acceptance. As you say, this is not the most common
> way to define GADTs, and given that (a) any class context prevents use
> in types, and (b) dependent pattern matching on GADTs doesn't work in
> type families anyway, it seems best to take the simple position that any
> context at all prevents use of a data constructor in a type.
>
> Cheers,
>
> Adam
>
>
> > On Tue, 22 Nov 2022 at 10:32, Adam Gundry <adam at well-typed.com
> > <mailto:adam at 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 at tweag.io <mailto:arnaud.spiwack at tweag.io>
> >      > <mailto:arnaud.spiwack at tweag.io
> >     <mailto:arnaud.spiwack at 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 at joachim-breitner.de <mailto:mail at joachim-breitner.de>
> >     <mailto:mail at joachim-breitner.de <mailto:mail at 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
>
> --
> 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 at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20221125/7d7ba9c1/attachment.html>