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

[Adam Gundry]

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