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.

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

PLE generates polymorphic applys for Sets #2438

Open
clayrat opened this issue Nov 14, 2024 · 1 comment
Open

PLE generates polymorphic applys for Sets #2438

clayrat opened this issue Nov 14, 2024 · 1 comment

Comments

@clayrat
Copy link
Contributor

clayrat commented Nov 14, 2024

The combination of the following two files crashes LH:

Foo.hs

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

module Foo where

import Prelude hiding (last)

{-@ reflect last @-}
{-@ last :: xs:{ [a] | len xs > 0 } -> a @-}
last :: [a] -> a
last [x]      = x
last (_ : xs) = last xs

data Foo t = Foo1 -- | Foo2
  deriving (Eq, Ord)

{-@ reflect isFoo @-}
isFoo :: Foo t -> Bool
isFoo Foo1 = True
-- isFoo Foo2 = False

{-@ reflect foos @-}
{-@ foos :: Foo t -> [{ v:Foo t | isFoo v }] @-}
foos :: Foo t -> [Foo t]
foos f = if isFoo f then f : [] else []

Bar.hs

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

module Bar where

import Prelude hiding (last)
import Data.Set
import Foo

{-@ lemma_last_isFoo :: f : Foo t -> { isFoo (last (foos f))} @-}
lemma_last_isFoo :: Foo t -> ()
lemma_last_isFoo f = if isFoo f then () else ()

The (prettifed) error is :

Unknown func-sort:
 Int : (Array (Foo Int) Bool) for

(apply    : func(0 , [[(Foo t)]; (Array_t (Foo t) bool)]))
(listElts : func(0 , [[(Foo t)]; (Array_t (Foo t) bool)]))
((apply : func(0 , [[(Foo t)]; [(Foo t)]]))
  ((apply : func(0 , [(Foo t); [(Foo t)]; [(Foo t)]]))
   (GHC.Types.: : func(0 , [(Foo t); [(Foo t)]; [(Foo t)]]))
   ((f : (Foo t)) : (Foo t)) : func(0 , [[(Foo t)];
    [(Foo t)]]))
  (GHC.Types.[] : [(Foo t)]) : [(Foo t)])

The bug crucially depends on having 2 files and importing Data.Set, merging the files or removing the import makes it disappear.

@clayrat
Copy link
Contributor Author

clayrat commented Nov 14, 2024

This seems related to the following function and its description: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Types/Theories.hs#L116-L143

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant