Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Name resolution error in abstract refinements #2403

Open
pacastega opened this issue Oct 22, 2024 · 0 comments
Open

Name resolution error in abstract refinements #2403

pacastega opened this issue Oct 22, 2024 · 0 comments

Comments

@pacastega
Copy link

With a module like this

module DependentPairs where

-- a :: String
-- a = "Hello, world!"

{-@ f :: (Int, Int)<\a -> {b:Int | b > a}> -> {b:Bool | b} @-}
f :: (Int, Int) -> Bool
f (a,b) = b > a

Liquid Haskell works as expected, but uncommenting the definition of variable a results in an error:

    Illegal type specification for `DependentPairs.f`
    DependentPairs.f :: lq_tmp$db##0:(GHC.Types.Int, GHC.Types.Int)<\a VV -> {b : GHC.Types.Int | b > DependentPairs.a}> -> {b : GHC.Types.Bool | b}
    Sort Error in Refinement: {b : int | b > DependentPairs.a}
    Unbound symbol DependentPairs.a --- perhaps you meant: tail ?

The error goes away when qualifying the name of a in the refinement:

{-@ f :: (Int, Int)<\DependentPairs.a -> {b:Int | b > a}> -> {b:Bool | b} @-}

but only as long as variable a is there; if I remove it again the Unbound symbol error comes back.

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

No branches or pull requests

1 participant