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

Wrong argument order in abstract refinement for dependent tuples #2404

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

Wrong argument order in abstract refinement for dependent tuples #2404

pacastega opened this issue Oct 22, 2024 · 0 comments

Comments

@pacastega
Copy link

This program:

{-@ lists :: (l::Int, {vv:[Int] | len vv = l}, {vvv:[Int] | len vvv = l}) @-}
lists :: (Int, [Int], [Int])
lists = (3, [1, 2, 3], [7, 8, 9])

results in the following error:

    Sort Error in Refinement: {vvv : [int] | len vvv == l}
    The sort [int] is not numeric
  because
Cannot unify int with [int] in expression: len vvv == l 
  because
Invalid Relation len vvv == l with operand types int and [int]

The problem persists when writing the dependent pair explicitly using an abstract refinement,

{-@ lists :: (Int, [Int], [Int])<\n -> {vv:[Int] | len vv = n}, \n _ -> {vvv:[Int] | len vvv = n} > @-}

but goes away when swapping the order of the arguments of the last lambda (n and _):

{-@ lists :: (Int, [Int], [Int])<\n -> {vv:[Int] | len vv = n}, \_ n -> {vvv:[Int] | len vvv = n} > @-}
nikivazou added a commit that referenced this issue Oct 29, 2024
nikivazou added a commit that referenced this issue Oct 29, 2024
# 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