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

Simon Peyton Jones simonpj at microsoft.com
Mon Mar 22 22:32:28 UTC 2021


Let's not get too bogged down in implementation.

The only question we have on the table, really is

     What do we want to be legal in a data constructor signature?

I've posted on the GitHub thread.

Simon

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-
|  bounces at haskell.org> On Behalf Of Eric Seidel
|  Sent: 22 March 2021 13:59
|  To: ghc-steering-committee at haskell.org
|  Subject: Re: [ghc-steering-committee] Proposal #402 (changes to GADT
|  syntax); rec: accept
|  
|  If we can get it to the point where GADT signatures are truly a
|  superset of type signatures, then we could unify the two in the
|  parser. We would always parse the superset and reject disallowed
|  signatures, e.g. UNPACK pragmas in function types, with much better
|  error messages! I think that would be a much better solution than
|  banning parens in GADT sigs.
|  
|  On Mon, Mar 22, 2021, at 09:45, Richard Eisenberg wrote:
|  >
|  >
|  > > On Mar 19, 2021, at 10:16 PM, Eric Seidel <eric at seidel.io> wrote:
|  > >
|  > > Iavor's example of type synonyms is another inconsistency that
|  doesn't seem to be motivated by a technical reason.
|  >
|  > Good point. I suppose if we did allow type synonyms there, then GADT
|  > sigs really would become more like a superset of the grammar for
|  types.
|  >
|  > Note that Agda can pull this off:
|  >
|  > > data T : Set
|  > >
|  > > syn : Set
|  > > syn = ℕ → T
|  > >
|  > > syn2 : Bool → Set
|  > > syn2 false = ℕ → T
|  > > syn2 true = T
|  > >
|  > > data T where
|  > >   MkT : syn
|  > >   MkT2 : syn2 false
|  > >   MkT3 : syn2 true
|  >
|  > This is accepted. `syn` is like a type synonym, while `syn2` is like
|  a
|  > type family. I don't like having Agda out in front of Haskell in
|  this
|  > way. :( Maybe we should just fix these problems instead of banning
|  > parens?
|  >
|  > Richard
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail
|  .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-
|  committee&data=04%7C01%7Csimonpj%40microsoft.com%7C760a5c3d8a5d480
|  1ec3908d8ed3ac0a4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6375201
|  83896349666%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz
|  IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=3CX3NinWswOHBXKcylYM
|  F%2FCsvMcek2PTvTxnczluaSw%3D&reserved=0


More information about the ghc-steering-committee mailing list