[ghc-steering-committee] Proposal #402 (changes to GADT syntax); rec: accept

[Richard Eisenberg]

Hi GHCSC,

I am the shepherd for Proposal #402, which has been submitted for our consideration.

Proposal text: https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-gadt-syntax.rst
PR discussion: https://github.com/ghc-proposals/ghc-proposals/pull/402

-----------------
Proposal Summary:

The proposal changes a few aspects of GADT constructor syntax, in part to make them simpler, and in part to make them more expressive. Only non-record syntax is treated by this proposal; GADT record constructors are entirely unaffected.

The two changes are:

1. Drop support for parentheses around result types in GADT constructor signatures.
2. Add support for nested quantifiers in GADT constructor signatures.

Examples & motivation:

1. This would now be rejected:

data T where
  MkT :: Int -> (Bool -> T)

Those parentheses are not allowed.

On the other hand

data S where
  MkS :: Int -> Bool -> (S)

remains accepted.

This change is mainly to simplify the implementation, but it also helps users understand that the thing after `MkS ::` really is not a type: it's a list of constructor arguments written in a concrete syntax that looks like a type. See the proposal for more explanation of how this is not a type.

2. This would now be accepted:

data Q a where
  MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)

Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` after visible arguments.

Constructors with forall ... -> syntax (such as our MkQ) will not be allowed in expressions or patterns (that would require #281), but will be allowed in types.

This change is a generalization of the syntax we have today, and it allows library authors more flexibility in designing interfaces, as they can now choose where type arguments should be written in a constructor.

------------------------
Recommendation:

I recommend acceptance.

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.

2. This generalization increases our expressiveness and removes what may feel like an artificial limitation. Furthermore, it is necessary in the case where we might have later arguments depend on earlier ones (possible for promoted constructors).

Please share opinions on acceptance/rejection here, or technical thoughts on the ticket itself.

I will accept in two weeks if there are no objections.

Thanks!
Richard

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210318/e43ed3b5/attachment.html>