ucsd-progsys/liquidhaskell

Cannot parse the unit value in refinement bounds

Open

#1,300 opened on 2018年4月17日

GitHub で見る
 (1 comment) (0 reactions) (0 assignees)Haskell (1,306 stars) (157 forks)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

コントリビューターガイド