Broken reflection over lists

[clayrat]

The following code throws an error on develop version of LH:

{-@ LIQUID "--reflection" @-}

module Foo where

{-@ reflect singleton @-}
singleton :: a -> [a]
singleton x = [x]

The error is:

<no location info>: error:
    Uh oh.
    src/Foo.hs:7:13 Cannot lift Haskell function `singleton` to logic
                    Cannot transform lambda abstraction to Logic:   \ (c_dE4 [OS=OneShot] :: a -> a1 -> a1)
  (n_dE5 [OS=OneShot] :: a) ->
  c_dE4 x n_dE5

 Try using a helper function to remove the lambda.

A workaround is to replace [x] with x : [] which suggests perhaps the issue is that the list term is being confused with a list type.

[clayrat]

I've managed to bisect the issue to https://github.com/ucsd-progsys/liquidhaskell/pull/2389, though the exact commit is hard to pinpoint. It doesn't appear yet on https://github.com/ucsd-progsys/liquidhaskell/commit/123451bb354d5b07f0553b0efeb79a5b57d21e69, already appears on https://github.com/ucsd-progsys/liquidhaskell/commit/6935d5429d04b15d42f4a5f36d108ac01a1ff36f, and the intermediate commits don't compile.

@gergoerdi

[gergoerdi]

I would need to reproduce this locally first, but on develop as of efc167432, the above file passes (vacuously):

[mi@scbbox liquidhaskell.upstream]$ git rev-parse HEAD
efc167432c2f7d830474052ade5b68ebd942ed6e

[mi@scbbox liquidhaskell.upstream]$ cat input/T2405.hs
{-@ LIQUID "--reflection" @-}

module Foo where

{-@ reflect singleton @-}
singleton :: a -> [a]
singleton x = [x]

[mi@scbbox liquidhaskell.upstream]$ cabal exec -- ghc -fforce-recomp -fplugin=LiquidHaskell input/T2405.hs
Loaded package environment from /home/mi/prog/liquidhaskell.upstream/dist-newstyle/tmp/environment.-4930/.ghc.environment.x86_64-linux-9.10.1
[1 of 1] Compiling Foo              ( input/T2405.hs, input/T2405.o )

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

[facundominguez]

:wave: Passes for me as well. The .fq files says:

define Test.singleton (lq1 : a##aDD) : [a##aDD] = {((GHC.Types.$58$ lq1 GHC.Types.$91$$93$))}

@clayrat, is this a solved problem? Or do you need the example to work with an old version of LH?

[AlecsFerra]

It also started working for me on develop

[clayrat]

Hm, it works when invoked standalone, but throws the error if used with a cabal.project file like this:

packages: ./

source-repository-package
   type: git
   location: https://github.com/ucsd-progsys/liquidhaskell.git
   tag: bec0937f555f303ac1f856e483ab67258ed69ead
   subdir: . liquidhaskell-boot liquid-prelude liquid-vector

source-repository-package
   type: git
   location: https://github.com/ucsd-progsys/liquid-fixpoint.git
   tag: 4d4392577f5c4cd199a47ea03c3c6c377d3d7197
   subdir: .

allow-newer: true
with-compiler: ghc-9.10.1

[gergoerdi]

Can you push a complete reproducer repo somewhere with everything just a single cabal build invocation away?

[clayrat]

Here you go: https://github.com/clayrat/liquidhaskell-listrefl-bug

Run cabal build -f liquidhaskell to reproduce.