ucsd-progsys/liquidhaskell

Cannot parse the unit value in refinement bounds

Open

#1,300 创建于 2018年4月17日

在 GitHub 查看
 (1 评论) (0 反应) (0 负责人)Haskell (1,306 star) (157 fork)batch import
easygood first issueparser

描述

I'm not really sure it's by design or not, LH fails to parse bounds which include the unit literal ().

{-@
    testee :: forall <
                p :: Int -> () -> Int -> Bool
              , q :: Int -> () -> Int -> Bool
              >.
              { n :: Int |- Int<p n ()> <: Int<q n ()> }
              Int
@-}
testee :: Int
testee = 42

Literals of the types other than () look okay, e.g. in the case of Int or Bool, the code is compilable.

{-@
    testee :: forall <
                p :: Int -> Int -> Int -> Bool
              , q :: Int -> Int -> Int -> Bool
              >.
              { n :: Int |- Int<p n 42> <: Int<q n 42> }
              Int
@-}
testee :: Int
testee = 42

贡献者指南