Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Liquid Type Mismatch on Initial Build #117

Open
pmbittner opened this issue Jan 23, 2022 · 2 comments
Open

Liquid Type Mismatch on Initial Build #117

pmbittner opened this issue Jan 23, 2022 · 2 comments

Comments

@pmbittner
Copy link

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
Copy link
Member

ranjitjhala commented Jan 23, 2022 via email

@pmbittner
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ranjitjhala @pmbittner