LH produces duplicate specifications for measures whose type contains String

[nilehmann]

This simple code below produces an error when checking B.hs

module A where
{-@ measure f :: String @-}

module B where
import A

$ liquid B.hs
A.hs:3:13: error:  Multiple specifications for `f` :
                        Conflicting definitions at
                        .
                        * A.hs:3:13
                        .
                        * /home/nlehmann/temp/A.hs:3:13

I did some digging and noticed that one of the measures has type String while the other has type [GHC.Types.Char]

[adinapoli]

Hi @nilehmann !

We are in the process of transitioning to a new GHC plugin architecture, as described here, and the executable is now deprecated.

Are you in a position to test out the GHC plugin, and report if you still get the error?

[ranjitjhala]

Hi @alfredo - I will try it out! Ranjit

On Mon, Aug 17, 2020 at 1:20 AM Alfredo Di Napoli notifications@github.com wrote:

Hi @nilehmann https://urldefense.com/v3/__https://github.com/nilehmann__;!!Mih3wA!REp2x_Qtqkzgtoe7wtWVjM6UnvuLDjKZST9sldlGd6DWuvOi9tMOKzKvq0dv8C1q$ !

We are in the process of transitioning to a new GHC plugin architecture, as described here https://urldefense.com/v3/__https://hackage.haskell.org/package/liquidhaskell-0.8.10.1/docs/Language-Haskell-Liquid-GHC-Plugin-Tutorial.html__;!!Mih3wA!REp2x_Qtqkzgtoe7wtWVjM6UnvuLDjKZST9sldlGd6DWuvOi9tMOKzKvq5zgerdn$, and the executable is now deprecated.

Are you in a position to test out the GHC plugin, and report if you still get the error?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1735*issuecomment-674735842__;Iw!!Mih3wA!REp2x_Qtqkzgtoe7wtWVjM6UnvuLDjKZST9sldlGd6DWuvOi9tMOKzKvq9nlEoBr$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGJG43T63ZSEPSRELDSBDR5NANCNFSM4PVW6UAQ__;!!Mih3wA!REp2x_Qtqkzgtoe7wtWVjM6UnvuLDjKZST9sldlGd6DWuvOi9tMOKzKvq6YF9YVT$ .

[ranjitjhala]

Ok, I can confirm that the bug does not happen in plugin-mode.

Specifically, if you check this branch out:

https://github.com/ucsd-progsys/lh-plugin-demo/tree/measure-string-bug

(Lib.hs exports the measure and is imported by Client.hs)

Then

• plugin-mode via stack build (etc.) finishes just fine, BUT
• executable-mode complains:

rjhala@khao-soi ~/r/lh-demo (measure-string-bug)> liquid -i src src/Demo/Client.hs

**** LIQUID: SAFE (2 constraints checked) **************************************

**** LIQUID: ERROR  ************************************************************
/Users/rjhala/research/lh-demo/src/Demo/Lib.hs:13:13: error:  Multiple specifications for `f` :
                                                                  Conflicting definitions at
                                                                  .
                                                                  * /Users/rjhala/research/lh-demo/src/Demo/Lib.hs:13:13
                                                                  .
                                                                  * /Users/rjhala/research/lh-demo/src/Demo/Lib.hs:13:13

[nilehmann]

ok, if the fix is then to use plugin mode, may I ask if there's a recommended way to turn refinement checking on and off? The code I'm currently working on takes several seconds to check a single module. This is beyond what I'm willing to accept in my regular edit check flow. So, I'd like to get fast feedback just from ghc and only check refinements after the code is more stable.

[ranjitjhala]

The easiest is to comment out the line

https://github.com/ucsd-progsys/lh-plugin-demo/blob/main/lh-plugin-demo.cabal#L25

in the cabal file? There's probably some clever way to use stack/cabal flags too but I don't recall the syntax off the top of my head. Still, let me look into this, since it is independently very important!

On Mon, Aug 17, 2020 at 11:55 AM Nico Lehmann notifications@github.com wrote:

ok, if the fix is then to use plugin mode, may I ask if there's a recommended way to turn refinement checking on and off? The code I'm currently working on takes several seconds to check a single module. This is beyond what I'm willing to accept in my regular edit check flow. So, I'd like to get fast feedback just from ghc and only check refinements after the code is more stable.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1735*issuecomment-675053498__;Iw!!Mih3wA!QEdCWgO5A_b7DlBW2Sdl0K_Fj1YjKVrbs01nnNYqlS7j_asIi-h-_SEnB50x6to-$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OHPDIPLEVWLU263U2DSBF4JRANCNFSM4PVW6UAQ__;!!Mih3wA!QEdCWgO5A_b7DlBW2Sdl0K_Fj1YjKVrbs01nnNYqlS7j_asIi-h-_SEnBzj90BbV$ .

[adinapoli]

The code I'm currently working on takes several seconds to check a single module.

To complement what Ranjit said already, perhaps a middle-ground solution is to add the --compile-spec option as a pragma to the single module taking several seconds to refine (if that's an option)? Something like:

{-@ LIQUID "--compile-spec" @-}

module MySlowModule where

..

--compile-spec will skip verification for that module, and should be faster.

[facundominguez]

Is this issue good to close?

[ranjitjhala]

Yup thanks!

[nilehmann]

I still think there ought to be a recommended way to quickly turn on and off liquid type checking depending on the use case. I'm not currently working in the original code now, but back then it was very painful. For example, back then Haskell lsp just crashed with LH on. Some support/guidelines for turning off LH in ide mode would be nice. This is orthogonal to the original issue though.

[ranjitjhala]

I agree but the catch is that LSP issue is a bug in LSP (surprisingly!)

Is the way to switch on and off is to toggle the fplugin mode?

[nilehmann]

In the specific use case of Storm I would like to disable the LH plugin by default (lsp would work out of the box) and have an option to turn it on when I run it in the command line (maybe passing an extra flag to stack). This is because running LH is too slow, so I have a quick plain Haskell development cycle + a slower "verification" cycle.