LiquidHaskell plugin does not find/load base annotations/assumptions (but modules are accessible to GHC)

[jekor]

I see the following error on a simple test:

error:
    Illegal type specification for `test`
    test :: {v : [GHC.Types.Int] | 0 < len v}
    Sort Error in Refinement: {v : [GHC.Types.Int] | 0 < len v}
    Unbound symbol len --- perhaps you meant: head, v ?
    Just

I assume that this is because the "base" assumptions/measures are not being loaded. I've tried explicitly importing GHC.Types and GHC.Types_LHAssumptions (both of which are found by GHC, and which seem to contain the definition of the len measure).

Is there a way I could diagnose why the LiquidHaskell plugin does not appear to find the necessary modules?

I am using Nix and ghcWithPackages with the liquidhaskell package (version 0.9.6.3). I see that there was an issue regarding Nix (#1099) but that was prior to the change to loading assumptions (https://github.com/ucsd-progsys/liquidhaskell/pull/2166/files).

If it's any help, here in my Nix overlay for the liquidhaskell packages:

      liquid-fixpoint = super.haskell.lib.markUnbroken (super.haskell.lib.overrideCabal hsuper.liquid-fixpoint (old: {
        version = "0.9.6.3";
        sha256 = "955cae3d235403cbc8fae564d215da227633bdb1ba33dbfc7eecaecb0b3d396e";
      }));
      liquid-prelude = hsuper.callCabal2nix "liquid-prelude" "${liquidhaskell-src-patched}/liquid-prelude" {};
      liquidhaskell = super.haskell.lib.overrideCabal (hsuper.callCabal2nix "liquidhaskell" liquidhaskell-src-patched {}) (old: {
        libraryHaskellDepends = (old.libraryHaskellDepends or []) ++ [self.z3];
      });
      liquidhaskell-boot = super.haskell.lib.doJailbreak (hsuper.callCabal2nix "liquidhaskell" "${liquidhaskell-src-patched}/liquidhaskell-boot" {});

where liquidhaskell-src-patched is patched with the following to allow it to compile (#2261):

diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
index 38b1180e0f..484baa56f8 100644
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -84,7 +84,7 @@ library
                       ghc-bignum,
                       ghc-prim
   default-language:   Haskell98
-  ghc-options:        -Wall -fplugin=LiquidHaskellBoot
+  ghc-options:        -Wall

[facundominguez]

Hello @jekor. I cannot help you with the Nix configuration, but disabling the LiquidHaskellBoot plugin as in

-  ghc-options:        -Wall -fplugin=LiquidHaskellBoot
+  ghc-options:        -Wall

is going to have the effect that no specifications are included in the interface files of the liquidhaskell package, and that could explain why they aren't found when verifying your test.