Closed octalsrc closed 2 weeks ago
I got the same result when I used the latest develop
branch snapshot of liquidhaskell
, liquidhaskell-boot
, and liquid-fixpoint
.
**** LIQUID: ERROR *************************************************************
<no location info>: error:
:1:1-1:1: Error
crash: SMTLIB2 respSat = Error "line 3 column 13801: Sort mismatch at argument #1 for function (declare-fun not
(Bool) Bool) supplied sort is Int"
(It seems with this version, there is no SMT file output to compare)
:wave: On develop
it passes for me with this command:
cabal exec ghc -- -fforce-recomp MyLib.hs
[1 of 1] Compiling MyLib ( MyLib.hs, MyLib.o )
**** LIQUID: SAFE (1 constraints checked) **************************************
My z3 version and compiler seem to match yours. I build all packages with cabal build liquidhaskell
except the boot packages.
We must have some other difference. I enter a nix-shell with nix-shell -p haskell.compiler.ghc9101 z3 cabal-install
.
On develop, the following should produce the .smt2 files and more:
{-@ LIQUID "--save" @-}
I'm uploading mine here.
Perhaps it is worth sharing the result of cabal freeze
, since we must have different dependency versions installed.
Thanks for taking a look!
My cabal freeze
output is:
active-repositories: hackage.haskell.org:merge
constraints: any.Cabal ==3.12.0.0,
any.Cabal-syntax ==3.12.0.0,
any.Diff ==0.4.1,
any.HUnit ==1.6.2.0,
any.OneTuple ==0.4.2,
any.QuickCheck ==2.14.3,
any.StateVar ==1.2.2,
any.aeson ==2.2.3.0,
any.ansi-terminal ==1.0.2,
any.ansi-terminal-types ==0.11.5,
any.array ==0.5.7.0,
any.ascii-progress ==0.3.3.0,
any.assoc ==1.1.1,
any.async ==2.2.5,
any.attoparsec ==0.14.4,
any.base ==4.20.0.0,
any.base-compat ==0.13.1,
any.base-orphans ==0.9.2,
any.base64-bytestring ==1.2.1.0,
any.bifunctors ==5.6.2,
any.binary ==0.8.9.2,
any.bitvec ==1.1.5.0,
any.boxes ==0.1.5,
any.bytestring ==0.12.1.0,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cereal ==0.5.8.3,
any.character-ps ==0.1,
any.clock ==0.8.4,
any.cmdargs ==0.10.22,
any.colour ==2.3.6,
any.comonad ==5.0.8,
any.concurrent-output ==1.10.21,
any.containers ==0.7,
any.contravariant ==1.5.5,
any.cryptohash-sha1 ==0.11.101.0,
any.data-default ==0.7.1.1,
any.data-default-class ==0.1.2.0,
any.data-default-instances-containers ==0.0.1,
any.data-default-instances-dlist ==0.0.1,
any.data-default-instances-old-locale ==0.0.1,
any.data-fix ==0.3.4,
any.deepseq ==1.5.0.0,
any.directory ==1.3.8.3,
any.distributive ==0.6.2.1,
any.dlist ==1.0,
any.exceptions ==0.10.7,
any.extra ==1.7.16,
any.fgl ==5.8.2.0,
any.filepath ==1.5.2.0,
any.fingertree ==0.1.5.0,
any.free ==5.2,
any.generically ==0.1.1,
any.ghc ==9.10.1,
any.ghc-bignum ==1.3,
any.ghc-boot ==9.10.1,
any.ghc-boot-th ==9.10.1,
any.ghc-heap ==9.10.1,
any.ghc-internal ==9.1001.0,
any.ghc-platform ==0.1.0.0,
any.ghc-prim ==0.11.0,
any.ghci ==9.10.1,
any.githash ==0.1.7.0,
any.gitrev ==1.3.1,
any.hashable ==1.4.7.0,
any.haskell-lexer ==1.1.1,
any.hpc ==0.7.0.1,
any.hscolour ==1.25,
any.hspec ==2.11.9,
any.hspec-core ==2.11.9,
any.hspec-discover ==2.11.9,
any.hspec-expectations ==0.8.4,
any.hspec-smallcheck ==0.5.3,
any.indexed-traversable ==0.1.4,
any.indexed-traversable-instances ==0.1.2,
any.integer-conversion ==0.1.1,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
any.intern ==0.9.5,
any.lens-family ==2.1.3,
any.lens-family-core ==2.1.3,
any.lifted-base ==0.2.3.12,
any.liquid-fixpoint ==0.9.6.3.1,
any.liquidhaskell ==0.9.10.1,
any.liquidhaskell-boot ==0.9.10.1,
any.logict ==0.8.1.0,
any.megaparsec ==9.5.0,
any.monad-control ==1.0.3.1,
any.mono-traversable ==1.0.17.0,
any.mtl ==2.3.1,
any.nats ==1.1.2,
any.network ==3.1.4.0,
any.network-uri ==2.6.4.2,
any.old-locale ==1.0.0.7,
any.optparse-applicative ==0.18.1.0,
any.os-string ==2.0.2,
any.parallel ==3.2.2.0,
any.parsec ==3.1.17.0,
any.parser-combinators ==1.3.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
any.prettyprinter-ansi-terminal ==1.1.3,
any.primitive ==0.9.0.0,
any.process ==1.6.19.0,
any.profunctors ==5.6.2,
any.quickcheck-io ==0.2.0,
any.random ==1.2.1.2,
any.recursion-schemes ==5.2.3,
any.resourcet ==1.3.0,
any.rest-rewrite ==0.4.4,
any.rts ==1.0.2,
any.safe ==0.3.21,
any.scientific ==0.3.8.0,
any.semaphore-compat ==1.0.0,
any.semialign ==1.3.1,
any.semigroupoids ==6.0.1,
any.smallcheck ==1.2.1.1,
any.smtlib-backends ==0.4,
any.smtlib-backends-process ==0.3,
any.split ==0.2.5,
any.splitmix ==0.1.0.5,
any.stm ==2.5.3.1,
any.store ==0.7.18,
any.store-core ==0.4.4.7,
any.strict ==0.5,
any.syb ==0.7.2.4,
any.tagged ==0.8.8,
any.template-haskell ==2.22.0.0,
any.temporary ==1.3,
any.terminal-size ==0.3.4,
any.text ==2.1.1,
any.text-iso8601 ==0.1.1,
any.text-short ==0.1.6,
any.tf-random ==0.5,
any.th-abstraction ==0.7.0.0,
any.th-compat ==0.1.5,
any.th-expand-syns ==0.4.11.0,
any.th-lift ==0.8.4,
any.th-lift-instances ==0.1.20,
any.th-orphans ==0.13.14,
any.th-reify-many ==0.1.10,
any.th-utilities ==0.2.5.0,
any.these ==1.2.1,
any.time ==1.12.2,
any.time-compat ==1.9.6.1,
any.transformers ==0.6.1.1,
any.transformers-base ==0.4.6,
any.transformers-compat ==0.7.2,
any.unix ==2.8.5.1,
any.unliftio-core ==0.2.1.0,
any.unordered-containers ==0.2.20,
any.uuid-types ==1.0.6,
any.vector ==0.13.1.0,
any.vector-algorithms ==0.9.0.2,
any.vector-stream ==0.1.0.1,
any.void ==0.7.3,
any.witherable ==0.4.2
index-state: hackage.haskell.org 2024-09-03T16:55:33Z
This is based on the haskell.packages.ghc9101
package set, from a Sep. 10 snapshot of nixpkgs-unstable. I used the following overrides on the package set to fix the broken packages:
liquid9101 = super.haskell.packages.ghc9101.override {
overrides = self: super: rec {
# Existing (broken) version was 0.9.6.3, while this version is
# 0.9.6.3.1, which among other things "added support for
# ghc-9.10.1".
liquid-fixpoint = super.callPackage ./liquid-fixpoint.nix {};
liquidhaskell = overrideCabal
(self.callPackage ./liquidhaskell.nix { z3 = system-z3; })
(old: {
libraryToolDepends = [ system-z3 ];
});
liquidhaskell-boot = self.callPackage ./liquidhaskell-boot.nix {};
# The existing version of rest-rewrite was pre-revision 0.4.3,
# which required a too-old version of "containers".
rest-rewrite = dontCheck (super.callPackage ./rest-rewrite.nix {});
# smtlib-backends-process was only broken because the tests
# failed; they failed because the system z3 executable was not
# passed into the test dependencies correctly (shadowed by the
# "z3" haskell library).
smtlib-backends-process = unmarkBroken (dontCheck super.smtlib-backends-process);
};
};
I generated the liquidhaskell.nix
, liquid-fixpoint.nix
, liquidhaskell-boot.nix
, and rest-rewrite.nix
files using cabal2nix
, based on the GitHub snapshots for their versions.
I condensed my environment into a single nix-shell file that you should be able to reproduce the error with. This is based on a nixos-unstable snapshot from today, which made it possible to use the Hackage versions of all packages. I've hardcoded that snapshot into the nix-shell file.
I have put the following in ./cabal-shell.nix
:
let
# This commit was the head of nixos-unstable on 2024-11-08
nixpkgsCommit = "4aa36568d413aca0ea84a1684d2d46f55dbabad7";
nixpkgsUrl = "https://github.com/NixOS/nixpkgs/archive/${nixpkgsCommit}.tar.gz";
pkgs = import (fetchTarball nixpkgsUrl) {};
inherit (pkgs.haskell.lib) unmarkBroken overrideCabal;
myHaskellPackages = pkgs.haskell.packages.ghc9101.override {
overrides = self: super: rec {
# Remove spurious broken flag for liquid-fixpoint
liquid-fixpoint = unmarkBroken super.liquid-fixpoint;
# Add z3 executable to build env for liquidhaskell
liquidhaskell = overrideCabal
super.liquidhaskell
(old: {
libraryToolDepends = [ pkgs.z3 ];
});
# Add z3 executable to test env for smtlib-backends-process,
# remove broken flag (that I assume was there due to the tests
# failing without z3).
smtlib-backends-process = overrideCabal
super.smtlib-backends-process
(old: {
testToolDepends = [ pkgs.z3 ];
broken = false;
});
};
};
test-package = myHaskellPackages.mkDerivation {
pname = "liquid-haskell-test";
version = "0.1.0.0";
src = ./.;
libraryToolDepends = [
pkgs.cabal-install
# Need this for the liquidhaskell plugin
pkgs.z3
];
libraryHaskellDepends = [
myHaskellPackages.base
myHaskellPackages.liquidhaskell
];
license = "unknown";
};
in test-package.env
Now, I can produce the error using either cabal exec ghc
or cabal build
as follows:
$ nix-shell --pure cabal-shell.nix
[nix-shell]$ cabal build
Build profile: -w ghc-9.10.1 -O1
In order, the following will be built (use -v for more details):
- liquid-haskell-test-0.1.0.0 (lib) (first run)
Preprocessing library for liquid-haskell-test-0.1.0.0...
Building library for liquid-haskell-test-0.1.0.0...
[1 of 1] Compiling MyLib ( src/MyLib.hs, /home/.../liquid-haskell-test/dist-newstyle/build/x86_64-linux/ghc-9.10.1/liquid-haskell-test-0.1.0.0/build/MyLib.o, /home/.../liquid-haskell-test/dist-newstyle/build/x86_64-linux/ghc-9.10.1/liquid-haskell-test-0.1.0.0/build/MyLib.dyn_o )
**** LIQUID: ERROR *************************************************************
<no location info>: error:
:1:1-1:1: Error
crash: SMTLIB2 respSat = Error "line 3 column 11916: Sort mismatch at argument #1 for function (declare-fun not
(Bool) Bool) supplied sort is Int"
Error: [Cabal-7125]
Failed to build liquid-haskell-test-0.1.0.0.
[nix-shell]$ cabal exec ghc -- -fforce-recomp src/MyLib.hs
Loaded package environment from /home/.../liquid-haskell-test/dist-newstyle/tmp/environment.-687319/.ghc.environment.x86_64-linux-9.10.1
[1 of 1] Compiling MyLib ( src/MyLib.hs, src/MyLib.o )
**** LIQUID: ERROR *************************************************************
<no location info>: error:
:1:1-1:1: Error
crash: SMTLIB2 respSat = Error "line 3 column 11786: Sort mismatch at argument #1 for function (declare-fun not
(Bool) Bool) supplied sort is Int"
And here's a quick repo that puts all the files in the right place for reproducing the error:
Now I've successfully verified the MyLib.hs file by using cabal so that it fetches its packages directly from Hackage, rather than using nix to provide the packages. As you suggested, using the environment:
nix-shell -p haskell.compiler.ghc9101 z3 cabal-install
[nix-shell] $ cabal update
[nix-shell] $ cabal build
So the error is probably triggered by a difference in package versions between the following freeze files:
First is the freeze file generated by cabal from today's Hackage (which did not produce the error).
active-repositories: hackage.haskell.org:merge
constraints: any.Cabal ==3.12.0.0,
any.Cabal-syntax ==3.12.0.0,
any.Diff ==0.5,
any.HUnit ==1.6.2.0,
any.OneTuple ==0.4.2,
any.QuickCheck ==2.15.0.1,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.aeson ==2.2.3.0,
aeson +ordered-keymap,
any.ansi-terminal ==1.1.1,
ansi-terminal -example,
any.ansi-terminal-types ==1.1,
any.array ==0.5.7.0,
any.ascii-progress ==0.3.3.0,
ascii-progress -examples,
any.assoc ==1.1.1,
assoc -tagged,
any.async ==2.2.5,
async -bench,
any.attoparsec ==0.14.4,
attoparsec -developer,
any.base ==4.20.0.0,
any.base-compat ==0.14.0,
any.base-orphans ==0.9.2,
any.base64-bytestring ==1.2.1.0,
any.bifunctors ==5.6.2,
bifunctors +tagged,
any.binary ==0.8.9.2,
any.bitvec ==1.1.5.0,
bitvec +simd,
any.boxes ==0.1.5,
any.bytestring ==0.12.1.0,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.character-ps ==0.1,
any.clock ==0.8.4,
clock -llvm,
any.cmdargs ==0.10.22,
cmdargs +quotation -testprog,
any.colour ==2.3.6,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-output ==1.10.21,
any.containers ==0.7,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cryptohash-sha1 ==0.11.101.0,
any.data-default ==0.8.0.0,
any.data-fix ==0.3.4,
any.deepseq ==1.5.0.0,
any.directory ==1.3.8.3,
any.distributive ==0.6.2.1,
distributive +semigroups +tagged,
any.dlist ==1.0,
dlist -werror,
any.exceptions ==0.10.7,
any.extra ==1.8,
any.fgl ==5.8.3.0,
fgl +containers042,
any.filepath ==1.5.2.0,
any.fingertree ==0.1.5.0,
any.free ==5.2,
any.generically ==0.1.1,
any.ghc ==9.10.1,
any.ghc-bignum ==1.3,
any.ghc-boot ==9.10.1,
any.ghc-boot-th ==9.10.1,
any.ghc-heap ==9.10.1,
any.ghc-internal ==9.1001.0,
any.ghc-platform ==0.1.0.0,
any.ghc-prim ==0.11.0,
any.ghci ==9.10.1,
any.githash ==0.1.7.0,
any.gitrev ==1.3.1,
any.hashable ==1.4.7.0,
hashable -arch-native +integer-gmp -random-initial-seed,
any.haskell-lexer ==1.1.2,
any.hpc ==0.7.0.1,
any.hsc2hs ==0.68.10,
hsc2hs -in-ghc-tree,
any.hscolour ==1.25,
any.hspec ==2.11.9,
any.hspec-core ==2.11.9,
any.hspec-discover ==2.11.9,
any.hspec-expectations ==0.8.4,
any.hspec-smallcheck ==0.5.3,
any.indexed-traversable ==0.1.4,
any.indexed-traversable-instances ==0.1.2,
any.integer-conversion ==0.1.1,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.intern ==0.9.5,
any.lens-family ==2.1.3,
any.lens-family-core ==2.1.3,
any.lifted-base ==0.2.3.12,
any.liquid-fixpoint ==0.9.6.3.1,
liquid-fixpoint -devel -link-z3-as-a-library,
any.liquidhaskell ==0.9.10.1,
liquidhaskell -devel,
any.liquidhaskell-boot ==0.9.10.1,
liquidhaskell-boot -devel,
any.logict ==0.8.1.0,
any.megaparsec ==9.6.1,
megaparsec -dev,
any.monad-control ==1.0.3.1,
any.monad-loops ==0.4.3,
monad-loops +base4,
any.mono-traversable ==1.0.20.0,
any.mtl ==2.3.1,
any.nats ==1.1.2,
nats +binary +hashable +template-haskell,
any.network ==3.2.5.0,
network -devel,
any.network-uri ==2.6.4.2,
any.optparse-applicative ==0.18.1.0,
optparse-applicative +process,
any.os-string ==2.0.2,
any.parallel ==3.2.2.0,
any.parsec ==3.1.17.0,
any.parser-combinators ==1.3.0,
parser-combinators -dev,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.prettyprinter-ansi-terminal ==1.1.3,
any.primitive ==0.9.0.0,
any.process ==1.6.19.0,
any.profunctors ==5.6.2,
any.quickcheck-io ==0.2.0,
any.random ==1.2.1.2,
any.recursion-schemes ==5.2.3,
recursion-schemes +template-haskell,
any.resourcet ==1.3.0,
any.rest-rewrite ==0.4.4,
any.rts ==1.0.2,
any.safe ==0.3.21,
any.scientific ==0.3.8.0,
scientific -integer-simple,
any.semaphore-compat ==1.0.0,
any.semialign ==1.3.1,
semialign +semigroupoids,
any.semigroupoids ==6.0.1,
semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers,
any.smallcheck ==1.2.1.1,
any.smtlib-backends ==0.4,
any.smtlib-backends-process ==0.3,
any.split ==0.2.5,
any.splitmix ==0.1.0.5,
splitmix -optimised-mixer,
any.stm ==2.5.3.1,
any.store ==0.7.18,
store -comparison-bench -integer-simple -small-bench,
any.store-core ==0.4.4.7,
store-core -force-alignment,
any.strict ==0.5.1,
any.syb ==0.7.2.4,
any.tagged ==0.8.8,
tagged +deepseq +transformers,
any.template-haskell ==2.22.0.0,
any.temporary ==1.3,
any.terminal-size ==0.3.4,
any.text ==2.1.1,
any.text-iso8601 ==0.1.1,
any.text-short ==0.1.6,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.7.0.0,
any.th-compat ==0.1.5,
any.th-expand-syns ==0.4.11.0,
any.th-lift ==0.8.5,
any.th-lift-instances ==0.1.20,
any.th-orphans ==0.13.15,
any.th-reify-many ==0.1.10,
any.th-utilities ==0.2.5.0,
any.these ==1.2.1,
any.time ==1.12.2,
any.time-compat ==1.9.7,
any.transformers ==0.6.1.1,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.unix ==2.8.5.1,
any.unliftio-core ==0.2.1.0,
any.unordered-containers ==0.2.20,
unordered-containers -debug,
any.uuid-types ==1.0.6,
any.vector ==0.13.1.0,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.9.0.2,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-stream ==0.1.0.1,
any.void ==0.7.3,
void -safe,
any.witherable ==0.5
index-state: hackage.haskell.org 2024-11-09T17:56:52Z
And second is the freeze file generated by cabal for the packages provided through yesterday's nixos-unstable package set, using the cabal-shell.nix
I defined above (which produced the error).
active-repositories: hackage.haskell.org:merge
constraints: any.Cabal ==3.12.0.0,
any.Cabal-syntax ==3.12.0.0,
any.Diff ==0.4.1,
any.HUnit ==1.6.2.0,
any.OneTuple ==0.4.2,
any.QuickCheck ==2.14.3,
any.StateVar ==1.2.2,
any.aeson ==2.2.3.0,
any.ansi-terminal ==1.0.2,
any.ansi-terminal-types ==0.11.5,
any.array ==0.5.7.0,
any.ascii-progress ==0.3.3.0,
any.assoc ==1.1.1,
any.async ==2.2.5,
any.attoparsec ==0.14.4,
any.base ==4.20.0.0,
any.base-compat ==0.13.1,
any.base-orphans ==0.9.2,
any.base64-bytestring ==1.2.1.0,
any.bifunctors ==5.6.2,
any.binary ==0.8.9.2,
any.bitvec ==1.1.5.0,
any.boxes ==0.1.5,
any.bytestring ==0.12.1.0,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cereal ==0.5.8.3,
any.character-ps ==0.1,
any.clock ==0.8.4,
any.cmdargs ==0.10.22,
any.colour ==2.3.6,
any.comonad ==5.0.8,
any.concurrent-output ==1.10.21,
any.containers ==0.7,
any.contravariant ==1.5.5,
any.cryptohash-sha1 ==0.11.101.0,
any.data-default ==0.7.1.1,
any.data-default-class ==0.1.2.0,
any.data-default-instances-containers ==0.0.1,
any.data-default-instances-dlist ==0.0.1,
any.data-default-instances-old-locale ==0.0.1,
any.data-fix ==0.3.4,
any.deepseq ==1.5.0.0,
any.directory ==1.3.8.3,
any.distributive ==0.6.2.1,
any.dlist ==1.0,
any.exceptions ==0.10.7,
any.extra ==1.7.16,
any.fgl ==5.8.2.0,
any.filepath ==1.5.2.0,
any.fingertree ==0.1.5.0,
any.free ==5.2,
any.generically ==0.1.1,
any.ghc ==9.10.1,
any.ghc-bignum ==1.3,
any.ghc-boot ==9.10.1,
any.ghc-boot-th ==9.10.1,
any.ghc-heap ==9.10.1,
any.ghc-internal ==9.1001.0,
any.ghc-platform ==0.1.0.0,
any.ghc-prim ==0.11.0,
any.ghci ==9.10.1,
any.githash ==0.1.7.0,
any.gitrev ==1.3.1,
any.hashable ==1.4.7.0,
any.haskell-lexer ==1.1.1,
any.hpc ==0.7.0.1,
any.hscolour ==1.25,
any.hspec ==2.11.9,
any.hspec-core ==2.11.9,
any.hspec-discover ==2.11.9,
any.hspec-expectations ==0.8.4,
any.hspec-smallcheck ==0.5.3,
any.indexed-traversable ==0.1.4,
any.indexed-traversable-instances ==0.1.2,
any.integer-conversion ==0.1.1,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
any.intern ==0.9.5,
any.lens-family ==2.1.3,
any.lens-family-core ==2.1.3,
any.lifted-base ==0.2.3.12,
any.liquid-fixpoint ==0.9.6.3.1,
any.liquidhaskell ==0.9.10.1,
any.liquidhaskell-boot ==0.9.10.1,
any.logict ==0.8.1.0,
any.megaparsec ==9.5.0,
any.monad-control ==1.0.3.1,
any.mono-traversable ==1.0.20.0,
any.mtl ==2.3.1,
any.nats ==1.1.2,
any.network ==3.1.4.0,
any.network-uri ==2.6.4.2,
any.old-locale ==1.0.0.7,
any.optparse-applicative ==0.18.1.0,
any.os-string ==2.0.2,
any.parallel ==3.2.2.0,
any.parsec ==3.1.17.0,
any.parser-combinators ==1.3.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
any.prettyprinter-ansi-terminal ==1.1.3,
any.primitive ==0.9.0.0,
any.process ==1.6.19.0,
any.profunctors ==5.6.2,
any.quickcheck-io ==0.2.0,
any.random ==1.2.1.2,
any.recursion-schemes ==5.2.3,
any.resourcet ==1.3.0,
any.rest-rewrite ==0.4.4,
any.rts ==1.0.2,
any.safe ==0.3.21,
any.scientific ==0.3.8.0,
any.semaphore-compat ==1.0.0,
any.semialign ==1.3.1,
any.semigroupoids ==6.0.1,
any.smallcheck ==1.2.1.1,
any.smtlib-backends ==0.4,
any.smtlib-backends-process ==0.3,
any.split ==0.2.5,
any.splitmix ==0.1.0.5,
any.stm ==2.5.3.1,
any.store ==0.7.18,
any.store-core ==0.4.4.7,
any.strict ==0.5,
any.syb ==0.7.2.4,
any.tagged ==0.8.8,
any.template-haskell ==2.22.0.0,
any.temporary ==1.3,
any.terminal-size ==0.3.4,
any.text ==2.1.1,
any.text-iso8601 ==0.1.1,
any.text-short ==0.1.6,
any.tf-random ==0.5,
any.th-abstraction ==0.7.0.0,
any.th-compat ==0.1.5,
any.th-expand-syns ==0.4.11.0,
any.th-lift ==0.8.4,
any.th-lift-instances ==0.1.20,
any.th-orphans ==0.13.14,
any.th-reify-many ==0.1.10,
any.th-utilities ==0.2.5.0,
any.these ==1.2.1,
any.time ==1.12.2,
any.time-compat ==1.9.6.1,
any.transformers ==0.6.1.1,
any.transformers-base ==0.4.6,
any.transformers-compat ==0.7.2,
any.unix ==2.8.5.1,
any.unliftio-core ==0.2.1.0,
any.unordered-containers ==0.2.20,
any.uuid-types ==1.0.6,
any.vector ==0.13.1.0,
any.vector-algorithms ==0.9.0.2,
any.vector-stream ==0.1.0.1,
any.void ==0.7.3,
any.witherable ==0.4.2
index-state: hackage.haskell.org 2024-09-03T16:55:33Z
Okay, it looks like this is a problem with the Haskell libraries provided by nixpkgs.
I found that the same cabal.project.freeze
file can produce both a working liquidhaskell and a non-working liquidhaskell depending on whether it is built with cabal
fetching dependencies directly from Hackage, or built using dependencies (with the same versions) provided by nixpkgs.
I've recorded the details for reproducing this here.
I'll close this issue, since it seems the fix would need to happen in the nixpkgs repo.
Thanks @octalsrc. Beint reproducible with the nix configuration, it is going to be helpful to learn why LH would break with the dependencies from nixpkgs.
Hello, I'm trying to get a simple example running using liquidhaskell-0.9.10.1 with GHC 9.10.1, and I'm running into an error.
The Example
My example file (
src/MyLib.hs
) is as follows:The
.cabal
file is:The Error
Compiling with
cabal build
produces the following error:It looks like the compilation/checking process produced the following SMT file (
src/.liquid/MyLib.hs.smt2
), where the error is present:Here, the constant
VV$35$$35$F$35$$35$2
is declared as anInt
, and it is later used as an argument tonot
.I also pasted the example file into the online demo, and it checked successfully as "Safe" there.
My Environment
Here are the library/tool versions I'm using that might be relevant:
All the Liquid Haskell packages were built using the GitHub snapshots tagged with their version numbers.
I'm using cabal-install (not stack), and I'm getting GHC 9.10.1 and the non-Liquid-Haskell packages from nixpkgs on NixOS.
Thanks!
Thanks for all your work on this cool project! I haven't used it substantially before, so please let me know if I've made some kind of basic mistake in my setup.