search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Falsity introduced by shadowing symbols of the logic #2319

Closed jarctan closed 2 months ago

jarctan commented 2 months ago

I think there is a way to introduce falsity by shadowing names used in the logic. An example:

{-@ LIQUID "--ple"      @-}

module Test where

import Prelude hiding (not)

not :: Bool -> Bool
not = id

{-@ reflect shouldBeId @-}
shouldBeId :: Bool -> Bool
shouldBeId x = not x

{-@ lemma :: {shouldBeId False} @-}
lemma = ()

The .fq file tells us the reflection of shouldBeId which is incorrect:

define Test.shouldBeId (lq1 : bool) : bool = {((~ (lq1)))}

The issue seemingly comes from the toPredApp function of CoreToLogic which is not matching against the fully-qualified name of symbols, but just against their local name, hence allowing for "puns" to pretend to be the original function. I might have a PR for this soon.

facundominguez commented 2 months ago

Fixed in #2327