search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.19k stars 137 forks source link

tyKindVarIdP discarding kind info #974

Closed alanz closed 7 years ago

alanz commented 7 years ago

Why does the following discard the result of kindP?

tyKindVarIdP :: Parser Symbol
tyKindVarIdP
   =  try ( do s <- tyVarIdP; reservedOp "::"; _ <- kindP; return s)
  <|> tyVarIdP

Should the kind annotation be deprecated in the language?

ranjitjhala commented 7 years ago

Not sure what this is for -- @nikivazou can you comment? (She is traveling so may be delayed...)

On Wed, Mar 22, 2017 at 6:53 AM Alan Zimmerman notifications@github.com wrote:

Why does the following discard the result of kindP?

tyKindVarIdP :: Parser Symbol tyKindVarIdP = try ( do s <- tyVarIdP; reservedOp "::"; _ <- kindP; return s) <|> tyVarIdP

Should the kind annotation be deprecated in the language?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/974, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOEuwoohFWX1UR_lqFRlmzv8ueGSXks5roSfBgaJpZM4MlOx5 .

nikivazou commented 7 years ago

Exactly. In Liquid Haskell we do not reason about kinds. That is we cannot refine them or use them in the refinements. So the Liquid types ignore kinds.

On Mar 22, 2017 10:20 AM, "Ranjit Jhala" notifications@github.com wrote:

Not sure what this is for -- @nikivazou can you comment? (She is traveling so may be delayed...)

On Wed, Mar 22, 2017 at 6:53 AM Alan Zimmerman notifications@github.com wrote:

Why does the following discard the result of kindP?

tyKindVarIdP :: Parser Symbol tyKindVarIdP = try ( do s <- tyVarIdP; reservedOp "::"; _ <- kindP; return s) <|> tyVarIdP

Should the kind annotation be deprecated in the language?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/974, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOEuwoohFWX1UR_ lqFRlmzv8ueGSXks5roSfBgaJpZM4MlOx5 .

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/974#issuecomment-288413236, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotQDxvQFO76sVsNPfv514wafraACsks5roS4jgaJpZM4MlOx5 .

alanz commented 7 years ago

Ok, and the parser is designed to be able to work with a standard haskell signature that has been annotated, so has to accept the kind annotation.