Record syntax rejected in GADTs

[facundominguez]

The following program

{-# LANGUAGE GADTs #-}

{-@
data T where
  T :: { getT :: Int } -> T
 @-}
data T where
  T :: { getT :: Int } -> T

main :: IO ()
main = print ()

fails with

Test.hs:5:16: error:
    • Cannot parse specification:
    unexpected ':'
    • 
  |
5 |   T :: { getT :: Int } -> T
  |                ^

Should this be supported?

[ranjitjhala]

I didn’t realize that was valid Haskell syntax! :-) we could support it I guess? Seems related to the other issue (having to duplicate selector names) so maybe can be done together?

On Tue, Nov 16, 2021 at 2:04 PM Facundo Domínguez @.***> wrote:

The following program

{-# LANGUAGE GADTs #-}

{-@ data T where T :: { getT :: Int } -> T @-} data T where T :: { getT :: Int } -> T

main :: IO () main = print ()

fails with

Test.hs:5:16: error: • Cannot parse specification: unexpected ':' • | 5 | T :: { getT :: Int } -> T | ^

Should this be supported?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1906&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=q_MB1LKqrWVPq4qd-rk2-fijsbvtxI6UrzGLK5lQpCJc3eja1vpY_I64xGK-x-GS&s=1J9H4yzlmgG38Px-_TzYO3-L1cP1i24W9cTYm5f1H_8&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OGR6AMCNWGAVGTW233UMLIOBANCNFSM5IFLZKHQ&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=q_MB1LKqrWVPq4qd-rk2-fijsbvtxI6UrzGLK5lQpCJc3eja1vpY_I64xGK-x-GS&s=8dROAY3ZsFj1s3fs533hJ2cG86NRwflDY86zMVRKbIE&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=q_MB1LKqrWVPq4qd-rk2-fijsbvtxI6UrzGLK5lQpCJc3eja1vpY_I64xGK-x-GS&s=S9MOZu5Qa_iV_qMViNXR3vkt98-97XApW_5lPGFh2z8&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=q_MB1LKqrWVPq4qd-rk2-fijsbvtxI6UrzGLK5lQpCJc3eja1vpY_I64xGK-x-GS&s=A3k9gRmi3RzNAdNH6Zf1Wx13H9Qpz2bxxYenMviJLLQ&e=.

[Fizzixnerd]

I have started work on this issue. Please see the linked PR once it's up.

[ranjitjhala]

Thanks Matt!

On Mon, Jan 10, 2022 at 1:02 PM Matt Walker @.***> wrote:

I have started work on this issue. Please see the linked PR once it's up.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1906-23issuecomment-2D1009338362&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=HdY5Q0LVPu_0rmBfqG64PFb0Caw8c9TpnlF-7X_wQ20sbVf4eSyjkDhQVw8WItbf&s=5QeoO4rWOvVeixzWjQJ5rLy32I-5-3xLbjeEDCNIDII&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OCMDPHBOT4SZBMB2BDUVNCMJANCNFSM5IFLZKHQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=HdY5Q0LVPu_0rmBfqG64PFb0Caw8c9TpnlF-7X_wQ20sbVf4eSyjkDhQVw8WItbf&s=hQHEVjy_9-G6Bpz4h33xY2-v4vBpN_sbxnr5xiQdaj4&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=HdY5Q0LVPu_0rmBfqG64PFb0Caw8c9TpnlF-7X_wQ20sbVf4eSyjkDhQVw8WItbf&s=AIMWGYB7hQfucL-3DLbaH-35W3o6S6Z4AV9ITNCjNn0&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=HdY5Q0LVPu_0rmBfqG64PFb0Caw8c9TpnlF-7X_wQ20sbVf4eSyjkDhQVw8WItbf&s=OWxh51mLSOthxAywdKW5Ky2d7HjtbwvAgWdCXG1KVVw&e=.

You are receiving this because you commented.Message ID: @.***>