ucsd-progsys/liquidhaskell
Voir sur GitHubCannot parse the unit value in refinement bounds
Open
#1 300 ouverte le 17 avr. 2018
easygood first issueparser
Métriques du dépôt
- Stars
- (1 306 stars)
- Métriques de merge PR
- (Merge moyen 2j 18h) (12 PRs mergées en 30 j)
Description
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