Honestly, I don’t see the benefit of accepting this proposal. It’s clear that (~) is a special name anyway, because it does not respect the enforced convention on type constructors (in fact, I’m a bit surprised that you need to import (~~) and (~#), given their special status), and because the special role it plays in the language. I’m also concerned about the migration story: When the lookup for ~ fails because it is not in scope, assume it refers to

Data.Type.Equality.~. When this happens and -Wcompat is in effect, emit a warning.

If we agreed that TypeOperators is almost always on (because of GHC2021), why not simply export this from the Prelude? Regards, Alejandro On 31 Mar 2021 at 16:29:32, Spiwack, Arnaud wrote:

This looks very minor. I'm not convinced that it is worth the hassle (that being said, it is not hard to write code that is both forward and backward compatible, so maybe there won't be much headache).

The proposal says

...

The compiler internals are simplified, in particular things described in Note [eqTyCon (~) is built-in syntax].

That's the really appetizing part (the fact that `~` will have a Haddock documentation is not bad either). Those of us who have been involved in the parts of the compiler that are touched here: do you think this is a worthwhile simplification? That would secure my vote.

On Wed, Mar 31, 2021 at 2:50 AM Richard Eisenberg wrote:

...

Hi all,

I am shepherding proposal #371.

Proposal: https://github.com/int-index/ghc-proposals/blob/non-magical-eq/proposals/000... Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/371

Summary:

Currently, the type equality operator (~) is always in scope, but you can use it only if -XGADTs or -XTypeFamilies is enabled. The proposal instead changes this arrangement to export (~) from Data.Type.Equality (an existing module in `base`), and requiring -XTypeOperators to use it (as we do for all other infix operators in types). There is an 8-release migration plan, where for 6 releases, all uses of (~) that do not import it from Data.Type.Equality will get a warning telling the user to import Data.Type.Equality.

The motivation for the proposal is uniformity: the goal is to treat (~) just like other type operators.

Recommendation:

I'm very much on the fence on this one, but in the end fall into the "accept" camp. The goal here is to achieve a simple cleanup in the language design (and implementation). It's a worthy goal, but it's disruptive. However, I think the disruption is small enough that it motivates the change. The fix for affected users is quite quick, and large-scale Haskell users probably already have a custom prelude that could make the change even easier to accommodate. Note also that TypeOperators is part of GHC2021, and so the change will likely only be a new import.

What do others think?

Without dissent, I will mark this proposal as accepted in two weeks.

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

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

On 1 Apr 2021 at 09:59:18, Vladislav Zavialov (int-index) < vlad.z.4096@gmail.com> wrote:

It’s clear that (~) is a special name anyway, because it does not respect the enforced convention on type constructors

To me, it is not clear at all. What convention do you have in mind? (~) is not that different from, say, (+), which is a valid type operator:

class a + b -- accepted

I meant the usual convention that type constructors must start with a capital letter or the : symbol. But in this case I had forgotten that with TypeOperators on, those conventions behave differently for types than for terms.

If we agreed that TypeOperators is almost always on (because of GHC2021), why not simply export this from the Prelude?

Exporting from Prelude is not a panacea: without a compatibility fallback, users of custom preludes will be affected. The proposed migration story means that for 8 releases, no existing code will break at all.

But those custom preludes would have to be updated anyway, right?

Also, (~) is a special, magical constraint, like Coercible and Typeable. Since the proposal drops the requirement of GADTs and TypeFamilies to use it, the idea is to (eventually) require an explicit import of Data.Type.Equality to indicate the use of (~) in the code, for the same reason that we ask the users to import Data.Coerce and Data.Typeable/Type.Reflection

Hi committee, This proposal has been updated to include exporting (~) from the Prelude. This means that migration is much easier than it was previously, likely not requiring any import changes (or just in a project's custom Prelude). Users will have to enable -XTypeOperators (and could choose to disable -XGADTs or -XTypeFamilies). With this new export, I'm more firmly in favor of cleaning up this one little corner: let's accept. I will wait one week for any comments, and then will accept this proposal. Thanks, Richard

On Apr 1, 2021, at 2:37 PM, Richard Eisenberg wrote:

...

On Apr 1, 2021, at 3:59 AM, Vladislav Zavialov (int-index) mailto:vlad.z.4096@gmail.com> wrote:

Exporting from Prelude is not a panacea: without a compatibility fallback, users of custom preludes will be affected. The proposed migration story means that for 8 releases, no existing code will break at all.

Right. I wasn't suggesting a change to the migration plan -- just that (~) would additionally be exported from the Prelude. The warning would trigger only when (~) isn't in scope, meaning that many users won't need to react to this change (given that -XTypeOperators is now on by default).

As for the specialness of ~: yes, it's special, but we export other special things from the Prelude, like $ (which automatically enables -XImpredicativeTypes).

...

On Apr 1, 2021, at 9:59 AM, Alejandro Serrano Mena mailto:trupill@gmail.com> wrote:

I meant the usual convention that type constructors must start with a capital letter or the : symbol. But in this case I had forgotten that with TypeOperators on, those conventions behave differently for types than for terms.

This used to be true, but the requirement that the first letter be a capital letter or : was dropped some time ago -- before I started using Haskell, in any case. It is independent of -XTypeOperators, which is necessary for any infix type level syntax.

...

But those custom preludes would have to be updated anyway, right?

Yes, they would.

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

While the use of (~) itself no longer requires -XGADTs, the usual desugaring of GADTs still does. So this will require the extension: data G a where MkG :: G Int even though this will not: data T a where MkT :: (a~Int) => T a Perhaps that is what you meant by ‘vacuous’, but I wouldn’t go as far as to say that -XGADTs becomes implied by -XGADTSyntax and -XExistentialTypes. - Vlad

On 22 Apr 2021, at 12:25, Spiwack, Arnaud wrote:

I'm still not sure what problem this proposal solves. The proposal alludes to some code simplification but doesn't give me a good idea of how much simpler this would make the code.

Also note that -XGADT becomes mostly vacuous with this proposal: -XGADTSyntax + -XExistentialTypes imply GADTs (both are in -XGHC2021). Not that I mind, really, I actually probably prefer it this way. But it's worthy of notice.

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

Well, I said I would accept by now, but I would like more participation here before I feel comfortable doing so. Specifically: * Alejandro and Arnaud have made utterances against this proposal, however neither said "I'm against" or something equivalent. * Simon PJ just rubber-stamped my recommendation * Joachim gave a weak approval (as have I). Do others have an opinion? Alejandro & Arnaud, have either of you changed camps? It would feel better if this were approved by something resembling a majority of the committee, instead of just my recommendation with Joachim's mild concurrence and SPJ's rubber stamp. Thanks, Richard

On Apr 23, 2021, at 4:17 PM, Richard Eisenberg wrote:

To my deep surprise, the following program is accepted:

...

{-# LANGUAGE GADTSyntax, ExistentialQuantification #-}

module Bug where

data G a where MkG :: a -> G Int

but the following additional definition is rejected:

...

foo :: G a -> a foo (MkG _) = 5

Adding -XTypeFamilies fixes that last piece, though.

Looking through the source code, GADTs implies GADTSyntax and MonoLocalBinds, either GADTs or ExistentialQuantification allows the declaration of existential variables or a refined return type, either GADTs or TypeFamilies allows the use of the `~` syntax, and either GADTs or TypeFamilies allows pattern-matching on a constructor with an equality in its context. So, GADTSyntax, ExistentialQuantification, and TypeFamilies together imply all the functionality of GADTs.

This is all very strange, though, and should probably be tidied up. Not in this proposal though.

Richard

...

On Apr 23, 2021, at 2:54 PM, Vladislav Zavialov (int-index) wrote:

While the use of (~) itself no longer requires -XGADTs, the usual desugaring of GADTs still does. So this will require the extension:

data G a where MkG :: G Int

even though this will not:

data T a where MkT :: (a~Int) => T a

Perhaps that is what you meant by ‘vacuous’, but I wouldn’t go as far as to say that -XGADTs becomes implied by -XGADTSyntax and -XExistentialTypes.

- Vlad

...

On 22 Apr 2021, at 12:25, Spiwack, Arnaud wrote:

I'm still not sure what problem this proposal solves. The proposal alludes to some code simplification but doesn't give me a good idea of how much simpler this would make the code.

Also note that -XGADT becomes mostly vacuous with this proposal: -XGADTSyntax + -XExistentialTypes imply GADTs (both are in -XGHC2021). Not that I mind, really, I actually probably prefer it this way. But it's worthy of notice.

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

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

I don't feel strongly about this one. Happy to accept Richard's recommendation. Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 22 April 2021 03:10 To: Vladislav Zavialov (int-index) Cc: Simon Peyton Jones via ghc-steering-committee Subject: Re: [ghc-steering-committee] #371: Stop treating ~ magically. Rec: weak accept Hi committee, This proposal has been updated to include exporting (~) from the Prelude. This means that migration is much easier than it was previously, likely not requiring any import changes (or just in a project's custom Prelude). Users will have to enable -XTypeOperators (and could choose to disable -XGADTs or -XTypeFamilies). With this new export, I'm more firmly in favor of cleaning up this one little corner: let's accept. I will wait one week for any comments, and then will accept this proposal. Thanks, Richard On Apr 1, 2021, at 2:37 PM, Richard Eisenberg mailto:rae@richarde.dev> wrote: On Apr 1, 2021, at 3:59 AM, Vladislav Zavialov (int-index) mailto:vlad.z.4096@gmail.com> wrote: Exporting from Prelude is not a panacea: without a compatibility fallback, users of custom preludes will be affected. The proposed migration story means that for 8 releases, no existing code will break at all. Right. I wasn't suggesting a change to the migration plan -- just that (~) would additionally be exported from the Prelude. The warning would trigger only when (~) isn't in scope, meaning that many users won't need to react to this change (given that -XTypeOperators is now on by default). As for the specialness of ~: yes, it's special, but we export other special things from the Prelude, like $ (which automatically enables -XImpredicativeTypes). On Apr 1, 2021, at 9:59 AM, Alejandro Serrano Mena mailto:trupill@gmail.com> wrote: I meant the usual convention that type constructors must start with a capital letter or the : symbol. But in this case I had forgotten that with TypeOperators on, those conventions behave differently for types than for terms. This used to be true, but the requirement that the first letter be a capital letter or : was dropped some time ago -- before I started using Haskell, in any case. It is independent of -XTypeOperators, which is necessary for any infix type level syntax. But those custom preludes would have to be updated anyway, right? Yes, they would. Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

On Mar 31, 2021, at 10:29 AM, Spiwack, Arnaud wrote:

Those of us who have been involved in the parts of the compiler that are touched here: do you think this is a worthwhile simplification?

Yes, I think so. Every special widget in the language takes custom support, and this removes one. The implementation of `~` will still be somewhat special, but there's no reason the parsing, etc., needs to be. Richard

It sounds like we have enough support here to declare this accepted. I will do so now. Thanks, all! Richard

On May 10, 2021, at 1:57 AM, Spiwack, Arnaud wrote:

It's not a very concrete statement. I'll have to trust you on this.

I guess that if `~` doesn't get special parsing rules then it's an overridable name. This is good. And everything which can simplify the parser is welcome. So let me vote: aye.

On Tue, May 4, 2021 at 2:16 PM Richard Eisenberg mailto:rae@richarde.dev> wrote:

...

On Mar 31, 2021, at 10:29 AM, Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io> wrote:

Those of us who have been involved in the parts of the compiler that are touched here: do you think this is a worthwhile simplification?

Yes, I think so. Every special widget in the language takes custom support, and this removes one. The implementation of `~` will still be somewhat special, but there's no reason the parsing, etc., needs to be.

Richard