ucsd-progsys/liquidhaskell
View on GitHubAnnotations are not checked for reflected functions that are marked as non-terminating
Open
#2,301 opened on Jun 17, 2024
good first issue
Repository metrics
- Stars
- (1,306 stars)
- PR merge metrics
- (Avg merge 2d 18h) (12 merged PRs in 30d)
Description
Consider the following code (link):
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
data L a = Nil | Cons a (L a)
{-@ reflect listSum @-}
{-@ listSum :: L Nat -> Nat @-}
listSum :: L Int -> Int
listSum Nil = 0
listSum (Cons h t) = h + listSum t
{-@ lazy ones @-}
{-@ ones :: {l:L Nat | listSum l > 5} @-}
ones :: L Int
ones = Cons 1 ones
This code verifies without issues and if I replace listSum l > 5 by listSum l < 5 I get an error as expected (try).
However, when I add the line {-@ reflect ones @-}, then no error is generated at all (example)
With this it would be easy to introduce an inconsistency.
However, I would like to safely reflect a non-terminating function such that I can use it in theorems and other annotations.
Note that the issue persists if I disable the termination checker for the whole file (link).
I also tested this with liquidhaskell-0.9.6.3 as well as the recent LiquidHaskell from github.