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

貢獻者指南