ucsd-progsys/liquidhaskell

Annotations are not checked for reflected functions that are marked as non-terminating

Open

#2,301 opened on Jun 17, 2024

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Haskell (1,306 stars) (157 forks)batch import
good first issue

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.

Contributor guide

Tech stack
None
Domain
tooling
Issue type
bug
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
4
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
over 1 week
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
fresh
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
clear
Prerequisites
LiquidHaskell basicsHaskell knowledgeUnderstanding of reflectionTermination checking concepts
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
20
Research direction
Investigate how LiquidHaskell handles reflection for non terminating functions. The bug occurs when a function marked as lazy is also reflected, causing annotations to be unchecked. Start by examining the termination checker and reflection handling in the source code (likely in src/Language/Haskell/Liquid/). Reproduce the issue using the provided example to understand the exact condition that bypasses annotation verification.
Annotations are not checked for reflected functions that are marked as non-terminating · ucsd-progsys/liquidhaskell#2301 | Good First Issue