We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
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.
Data.Set
The text was updated successfully, but these errors were encountered:
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
Sorry, something went wrong.
use applys branch for LF, add test for ucsd-progsys#2438
cac0f6f
No branches or pull requests
The combination of the following two files crashes LH:
Foo.hs
Bar.hs
The (prettifed) error is :
The bug crucially depends on having 2 files and importing
Data.Set
, merging the files or removing the import makes it disappear.The text was updated successfully, but these errors were encountered: