Stable GADT constructor syntax

[int-index]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

The syntax of GADT constructor declarations is documented in the User's Guide as "subject to change". We propose to fix a couple of issues associated with it and to advertise the resulting syntax as stable (that is, a breaking change to
it would require another proposal).

Rendered

[AntC2]

While we're tidying up GADTs, there's similar similar-but-different nuances with Pattern signatures - which can also have strictness annotations and/or use record style; oh, also that curious double-=>.

strictness ... not reflected in the constructor's type

Do we reflect strictness in the type of ordinary H2010 style constructors? We should see the same result from :t whichever style was used to declare.

[int-index]

Do we reflect strictness in the type of ordinary H2010 style constructors? We should see the same result from :t whichever style was used to declare.

Strictness annotations are not part of type signatures regardless of declaration style:

ghci> data T = MkT !Int
ghci> :t MkT
MkT :: Int -> T

While we're tidying up GADTs, there's similar similar-but-different nuances with Pattern signatures - which can also have strictness annotations and/or use record style; oh, also that curious double-=>.

Pattern signatures definitely deserve some attention, the double => arrow makes me feel uneasy. However, this particular proposal is about GADTs, and I don’t want to broaden its scope.

[simonpj]

I think this is on a good, consolidating path

[monoidal]

Note that strictness annotations can be recovered with :i MkT. Strictness is not stored in types, e.g. f !x y = y and g x y = y have the same type.

In the proposal, ->. should be the lollipop ⊸ (available only with UnicodeSyntax). We do not have ->. since the linear types syntax has changed, but we had to name the token somehow.

[goldfirere]

Looks good. I'm in support. Thanks for the very nice write-up.

[aspiwack]

It does make sense to me.

[int-index]

@nomeata There doesn’t seem to be much discussion around this proposal, so I’d like to submit it to the committee.

[goldfirere]

A few clarification questions:

• The grammar includes ~ as a strictness_sigil. Is this possible only with -XStrictData (as it is today)? (I actually would like ~ to be available generally, but that's properly a separate proposal.)
• I assume the Unicode arrow is still available (both thin arrow and fat arrow) in a quantifier. Might be good to say somewhere that '->' and '=>' include these possibilities.
• The proposal says that data T where T1 :: (Int -> T) would be rejected. But the grammar accepts this. I think you need to specify that the btype production of gadt_prefix_sig is taken as the result type of the GADT constructor; it must be a substitution instance of the type being declared.
• Is type synonym expansion allowed in result types? (It is today.) Is type family expansion allowed in result types? (It is not today.) These facts should be included.
• This proposal restricts record constructors to have all their type quantifiers up at the front. That strikes me as a reasonable stepping stone. But there should be some text describing this state of affairs, as it makes record constructor types strictly more restrictive than non-record constructor types.
• This proposal allows all quantified variables in a record constructor to be visible, or for all to be invisible. It does not allow a mix. This seems a bit strange. Maybe make forall_telescope recursive?
• It would be nice to have a future work section, which will perhaps inspire others to echo this proposal. Future work includes fixing pattern synonyms in a similar way and further generalizing record-constructor syntax.
• I am a little concerned about error messages. If someone writes data T where MkT :: Int -> (Int -> T) because they learned that -> is right-associative but likes to be very explicit about parsing, and the definition is rejected, I would be unhappy if the error message says something like "Error: (Int -> T) is not an instance of T." True, but hardly helpful. The proposal does not need an exact wording of the message specified, but it should indicate that GHC will explicitly detect this case and helpfully explain where parentheses are and are not allowed in constructor signatures.

Just a few suggestions for hopefully-quick edits. I plan to recommend acceptance. Thanks!

Please ping me here with a mention when this is ready.

[int-index]

This proposal allows all quantified variables in a record constructor to be visible, or for all to be invisible. It does not allow a mix. This seems a bit strange.

The record syntax allows the forall tvs. b form only, not forall tvs -> b. The proposal already contained this side condition.

As to the other questions, I tried to incorporate the answers into the proposal. Let me know if I missed anything. Thanks!

[int-index]

Please ping me here with a mention when this is ready.

@goldfirere Ping. (Apologies, I forgot to include a mention in my previous comment)

[int-index]

@goldfirere Ping.

[goldfirere]

Great. Thanks. I have left a PR at serokell#4 with a tiny wording clarification. I will now recommend acceptance to the committee.

[goldfirere]

Hrm. I went to recommend acceptance, but I stumbled.

Suppose we have

data V a where
  MkV :: forall a -> a -> V a

That would seem to be accepted by this proposal. But now it seems we need #281 to be able to use MkV in a term. And we haven't begun to talk about a pattern with MkV in it. (Key question is about scoping -- which namespace gets the a in the pattern MkV a x?)

I don't think you intended for this to depend on #281, so perhaps you want to say that any constructor with a forall ... -> quantifier is (for now) banned in terms and patterns? Note that forall ... -> is still useful, if you are going to use the constructor only a compile-time context.

[int-index]

perhaps you want to say that any constructor with a forall ... -> quantifier is (for now) banned in terms and patterns? Note that forall ... -> is still useful, if you are going to use the constructor only a compile-time context.

@goldfirere Yes, that was the intent. That is exactly what #81 used to say before it was removed in #393. I think we should simply revert #393 and there will be no problem. But I can also mention it in this proposal, too.

[simonpj]

Iavor asks (on the ghc-steering-committee list) what is the benefit of allowing nested quantifiers.

And indeed, the proposal is silent on this point. Can you that?

I think the only compelling reason comes when we have forall n -> . So, if we allow nested parens (see above) the main motivation of the proposal is future compat with forall n ->. Correct?

[simonpj]

Richard says

1. Dropping the parentheses sounds trivial, but keeping them means we have to do extra work in the design of our data structures to remember the parentheses. Because constructor "types" aren't types, this information isn't otherwise needed.

Is it really true that we have to do significant "extra work"? Doesn't the structure of gadt_prefix_sig suggest

data GadtPrefixSig p = BType (HsType p)
                                  |  Quant Quantifier (GadtPrfefixSIg p)

in which case adding

                                  | Par (GadtPrefixSig p)

seems pretty trivial.

(I think Richard's claim used to be true, when we stored [ConArg] but the nested quantifiers preclude that.)

[int-index]

That still doesn't tell me why it's problematic to add one line to the BNF in your proposal. I think you are saying that some parse is ambiguous, but I don't see it.

No, there’s no ambiguity. It would be a valid specification, but not as easy to implement. Using a LALR parser (rather than, say, GLR) imposes its own set of constraints.

Adding the | '(' gadt_prefix_sig ')' production to Parser.y simply results in reduce/reduce conflicts. happy cannot produce a state machine with 1 token of lookahead that could handle it.

what is the benefit of allowing nested quantifiers.

The idea is to give more freedom to API authors. For example, in type constructors quantifiers come in arbitrary order:

data T :: Bool -> forall k. k -> Type

The idea is to allow the same sort of flexibility in data constructors. I don’t have a concrete use case in mind, but it seems to make the language more regular.

[simonpj]

Adding the | '(' gadt_prefix_sig ')' production to Parser.y simply results in reduce/reduce conflicts

This part is very not-clear to me, yet is apparently central to the proposal.

Try this:

gadt_prefix_sig ::= btype               -- (1)
                 |  '!' atype '->' gadt_prefix_sig
                 |      atype '->' gadt_prefix_sig
                 | '(' gadt_prefix_sig ')'

btype ::= tycon                -- (2)
       | '(' type ')'

type ::= btype
       | btype '->' type

This is way more limited than reality, but it illustrates. I can't see the reduce/reduce conflict.

[int-index]

This is way more limited than reality, but it illustrates.

I might be missing the core idea behind your code snippet, but it does seem quite similar to what I’ve tried in my branch. My understanding is that source of the problem is that '(' ktype ')' is part of atype:

atype :: { LHsType GhcPs }
        : ntgtycon                    { ... }
        | tyvar %shift                { ... }
        | '*'                         { ... }
        | '(' ktype ')'               { ... }   -- CONFLICT HERE.
        | ...

And gadt_prefix_sig can, in fact, start with atype. So we need to choose between these two productions:

1. '(' ktype ')'
2. '(' gadt_prefix_sig ')'

If you’re willing to get your hands dirty, here is my patch: https://gitlab.haskell.org/ghc/ghc/-/commit/32711799397ae76a87ba47b1ba6daa42f94fc965

If you add a | '(' gadt_con_sig ')' { undefined } production to gadt_con_sig, you can see the issue for yourself.

[goldfirere]

(I think Richard's claim used to be true, when we stored [ConArg] but the nested quantifiers preclude that.)

That may be the case (that storing the parens in the AST is fairly easy). I may have been thinking of the current [ConArg]-based implementation.

My desire to drop the parentheses is on theoretical grounds, though, not practical ones: the thing after :: is not a type, so there's no reason to believe that parentheses should go there. Or that -> associates to the right there. -> is just a piece of punctuation, separating elements in a list, quite unlike the -> that appears in types, which is a right-associative binary operator.

[simonpj]

My desire to drop the parentheses is on theoretical grounds, though, not practical ones: the thing after :: is not a type, so there's no reason to believe that parentheses should go there.

But that argument would apply equally to nested quantifiers, wouldn't it?

I'm not sure this line of thinking moves us on much. Maybe we'd be best off simply asking

• Do we like nested parens in a data con sig? (Proposal says no, others disagree. No technical issue, just a matter of taste.)
• Do we like nested quantifiers in a data con sig? (Proposal says yes, but only because "it seems to make the language more regular". Might become more significant if we had dependency.)

Incidentally I note that, under the proposal, if you want record field names you can't have nested quantifiers. That seems like an unfortunate fork in the road: you can have nested quantifiers, or named fields, but not both. In the status quo the quantifiers have to be at the front so the issue doesn't arise.

---

TL;DR. I can see merit in this proposal, but little urgency. Meanwhile it's using up our cycles thinking about it. Maybe we should park it (entirely without prejudice) until the needs become more pressing.

[int-index]

I can see merit in this proposal, but little urgency. Meanwhile it's using up our cycles thinking about it. Maybe we should park it (entirely without prejudice) until the needs become more pressing.

Whether we drop support for parentheses determines how invasive the changes I need to make in order to complete https://gitlab.haskell.org/ghc/ghc/-/issues/18782. Maybe it’s not urgent, but I’ve already sunk quite some time into it (with a few prototypes and writing this proposal), and I intend to finish it, so a resolution would be nice.

Just to be clear, keeping support for parentheses simply means more engineering work and complexity in the parser, it’s not a blocker. I remember talking to @goldfirere, and after hearing his ideological argument I figured it to be a good excuse to keep things simpler.

Let’s decide whether we want parentheses or not, this will inform my further implementation efforts.

[reminders-prs]

👋 @goldfirere, accept if there are no objections.

[goldfirere]

As proposal shepherd, in an attempt to make forward progress, I propose dropping the part of this proposal about the parentheses, retaining only the bit about quantifiers. My sense is that, with that change, the committee would approve. Furthermore, my sense is that @int-index is not particularly opposed to such a change, so this would seem to make everyone happy.

@int-index, please revise the text of the proposal, ping me, and then I will send this back through the committee.

Thanks!

[int-index]

@goldfirere OK, I changed the proposal to retain support for parentheses in prefix-style signatures:

data G where
  MkG :: !Int -> (!Int -> G)   -- OK

Note, however, that I did not introduce support for parentheses record-style signatures. As of GHC 9.0, they are rejected:

data G a where
  MkG :: ({ foo :: Int } -> G a)

<interactive>:3:24: error:
    • Record syntax is illegal here: {foo :: Int}
    • In the type ‘{foo :: Int}’
      In the definition of data constructor ‘MkG’
      In the data declaration for ‘G’

Let’s keep it this way, until somebody has a use case for parentheses there.

[simonpj]

Note, however, that I did not introduce support for parentheses record-style signatures. As of GHC 9.0, they are rejected:

yes i think that's fine. Record syntax also does not support nested quantifiers, I note.

[goldfirere]

I've prodded the committee to take another look.

/remind me to accept in 10 days if there is no further conversation.

[reminders-prs]

@goldfirere set a reminder for Apr 17th 2021

[reminders-prs]

👋 @goldfirere, accept if there is no further conversation.

[goldfirere]

This proposal has now been accepted. Thanks, all!