Annotations are not checked for reflected functions that are marked as non-terminating · ucsd-progsys/liquidhaskell#2301

(1 comment) (0 reactions) (0 assignees)Haskell (1,306 stars) (157 forks)batch import

good first issue

説明

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.

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

技術スタック: なし
領域: tooling
Issue 種別: bug
難度: 4
推定時間: over 1 week
活動状況: fresh
明確さ: clear
前提条件: LiquidHaskell basicsHaskell knowledgeUnderstanding of reflectionTermination checking concepts
初心者向け度: 20
調査方針: 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.