ucsd-progsys/liquidhaskell
GitHub で見るCannot parse the unit value in refinement bounds
Open
#1,300 opened on 2018年4月17日
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