Liquid Type Mismatch on Initial Build

[pmbittner]

OS: WSL2 (Ubuntu) on Windows 10
Commit I cloned this repository at: 8bf919a
z3 version: 4.8.7-4build1

Hi LiquidHaskell team,

I wanted to start the tutorial so I cloned this repository and installed z3 (sudo apt-get install -y z3). I tried to reiterate the compilation with stack build --fast --file-watch until no errors showed up. However, (no matter how often I recompile) the following error stays:

> stack build --fast --file-watch
liquidhaskell-tutorial> configure (lib)
Configuring liquidhaskell-tutorial-0.2.0.0...
liquidhaskell-tutorial> build (lib)
Preprocessing library for liquidhaskell-tutorial-0.2.0.0..
Building library for liquidhaskell-tutorial-0.2.0.0..
[ 2 of 13] Compiling Tutorial_01_Introduction

**** START: pandoc *************************************************************
 

**** DONE:  pandoc *************************************************************
 

**** START: pandoc *************************************************************
 

**** DONE:  pandoc *************************************************************
 

**** LIQUID: UNSAFE ************************************************************

/home/bittner/LearningLiquidHaskell/liquidhaskell-tutorial/src/Tutorial_01_Introduction.lhs:30:27: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v >= 0
                                && v == len xs}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV /= 0}
    .
    in the context
      xs : {v : [GHC.Types.Int] | len v >= 0}
   |
30 | average xs = sum xs `div` length xs
   |                           ^^^^^^^^^



--  While building package liquidhaskell-tutorial-0.2.0.0 using:
      /home/bittner/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_3.2.0.0_ghc-8.10.1 --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-3.2.0.0 build lib:liquidhaskell-tutorial --ghc-options " -fdiagnostics-color=always"
    Process exited with code: ExitFailure 1
Type help for available commands. Press enter to force a rebuild.

Thanks for any help and sorry if the problem is my fault.

Kind regards,
Paul

[ranjitjhala]

Dear Paul, Yes that is because LH is complaining about the divide by zero error on line 30. To suppress this warning you can uncomment this line https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/main/src/Tutorial_01_Introduction.lhs#L11 Thanks for pointing this out, I thought there was explicit text about this in the tutorial - I will add it! Let me know if that helps! Ranjit

…

On Sun, Jan 23, 2022 at 4:21 AM Paul Maximilian Bittner < ***@***.***> wrote: *OS*: WSL2 (Ubuntu) on Windows 10 *Commit I cloned this repository at*: 8bf919a <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_commit_8bf919a9d81f34ea7675dbe112086151d14d57c7&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=KTDG6qWLwMsZ16_iohtQu9UQYnF3ApPpp2hsKJ_qU9WJIlcEJ6bofY8auV6Y8yXE&s=7NL4R3A9bil9GXqDp3cVo8qzZsonmnOV6oi8VBCWITM&e=> *z3 version*: 4.8.7-4build1 Hi LiquidHaskell team, I wanted to start the tutorial so I cloned this repository and installed z3 (sudo apt-get install -y z3). I tried to reiterate the compilation with stack build --fast --file-watch until no errors showed up. However, (no matter how often I recompile) the following error stays: > stack build --fast --file-watch liquidhaskell-tutorial> configure (lib) Configuring liquidhaskell-tutorial-0.2.0.0... liquidhaskell-tutorial> build (lib) Preprocessing library for liquidhaskell-tutorial-0.2.0.0.. Building library for liquidhaskell-tutorial-0.2.0.0.. [ 2 of 13] Compiling Tutorial_01_Introduction **** START: pandoc ************************************************************* **** DONE: pandoc ************************************************************* **** START: pandoc ************************************************************* **** DONE: pandoc ************************************************************* **** LIQUID: UNSAFE ************************************************************ /home/bittner/LearningLiquidHaskell/liquidhaskell-tutorial/src/Tutorial_01_Introduction.lhs:30:27: error: Liquid Type Mismatch . The inferred type VV : {v : GHC.Types.Int | v >= 0 && v == len xs} . is not a subtype of the required type VV : {VV : GHC.Types.Int | VV /= 0} . in the context xs : {v : [GHC.Types.Int] | len v >= 0} | 30 | average xs = sum xs `div` length xs | ^^^^^^^^^ -- While building package liquidhaskell-tutorial-0.2.0.0 using: /home/bittner/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_3.2.0.0_ghc-8.10.1 --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-3.2.0.0 build lib:liquidhaskell-tutorial --ghc-options " -fdiagnostics-color=always" Process exited with code: ExitFailure 1 Type help for available commands. Press enter to force a rebuild. Thanks for any help and sorry if the problem is my fault. Kind regards, Paul — Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_issues_117&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=KTDG6qWLwMsZ16_iohtQu9UQYnF3ApPpp2hsKJ_qU9WJIlcEJ6bofY8auV6Y8yXE&s=w0Nu5UqMBdCoYdRZEHdtQbK0Afsj2YvhfeAI1rHbnug&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OEVHD57MOYACREKBZDUXPXFHANCNFSM5MTI3EVQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=KTDG6qWLwMsZ16_iohtQu9UQYnF3ApPpp2hsKJ_qU9WJIlcEJ6bofY8auV6Y8yXE&s=R6wyeaXL4-KNVQcajSafYVvfUDP1ErkQPM1cbKM74hA&e=> . Triage notifications on the go with GitHub Mobile for iOS <https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=KTDG6qWLwMsZ16_iohtQu9UQYnF3ApPpp2hsKJ_qU9WJIlcEJ6bofY8auV6Y8yXE&s=FA_--xczcW3tsyPUrEVkfVUyGQ-EZffB0s5qnUy82Yo&e=> or Android <https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=KTDG6qWLwMsZ16_iohtQu9UQYnF3ApPpp2hsKJ_qU9WJIlcEJ6bofY8auV6Y8yXE&s=ZKW1RfErbrvt6E3bz_wdP-TDotVmhShfhyBlTkfbmFc&e=>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[pmbittner]

Hi Ranjit,

thank you very much for the fast response. Indeed, the given error is part of the tutorial. It was mentioned as a motivation for liquid haskell. Though, the instructions for "Getting Started" in the tutorial said "Iteratively edit-compile [...] until it builds without any liquid type errors". Thus, I expected to reach a state without type errors before going to the next section of the tutorial.

When uncommenting the line you pointed at, a next type error occurs in Compiling Tutorial_02_Logic. I guess this is wanted behaviour and that the tutorial is about fixing these errors? If so, the "Getting Started" section in the tutorial should indeed clarify to build until the first liquid haskell type error in Tutorial_01_Introduction.lhs occurs (and not build until no errors occur).

Thank you very much and kind regards,
Paul