Facundo Domínguez

Verification passes if the measures are changed to reflected functions. It would be worth looking at the equalities that PLE produces in each case.

Oh, I know what it is. The measure equalities are not in scope where they are needed in the unsafe variant. We have discussed this a few times in other...

Hello! Using the `lazy` annotation does make reasoning unsafe in liquidhaskell. This is mentioned in a few other issues (e.g. #1576, #2218). I'm just noticing that [the documentation](https://ucsd-progsys.github.io/liquidhaskell/specifications/#disabling-termination-checking) doesn't say...

> if: Lib.hs uses exact-data-con etc. then any Client.hs that imports it is also automatically checked with those flags on? This looks like a bad idea. Enabling `--exact-data-cons` by default...

Defining `inc` still makes the verification fail at the same spot (second equation of the lemma). I'm copying the error for the reference. ``` Test.hs:28:27: error: Liquid Type Mismatch ....

If I redefine `intSum` as follows, verification passes. ```Haskell {-@ reflect intSum @-} intSum :: [Int] -> Int intSum ys = myFoldr add 0 ys {-@ reflect add @-} add...

Probably this is because CoreToLogic replaces occurrences of `GHC.Internal.Num.+` with `+` only [when the application is saturated](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs#L463). Replacing `add` with `\x y -> x + y` and using `--etabeta` also...

The `include` directory has been obliterated. But I think the config-dependent specs are linked in the code in [configSensitiveDependencies](https://github.com/ucsd-progsys/liquidhaskell/blob/125a6dfb872b89d5a8db13d58cb48544153590cb/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L178-L182) these days.

Thanks Ranjit. If we wanted to use `select` or `store` from the array theory, there is no Haskell function yet to expose those for use with `inline`. Is the best...

Maybe you are referring to [define](https://ucsd-progsys.github.io/liquidhaskell/options/#logical-aliasing).