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

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