Check equality on domain and range on function equality.

[nikivazou]

https://github.com/ucsd-progsys/liquidhaskell/pull/1578 added reasoning for function equality, but does not take into account equality of the functions domain/range. E.g.,

{-@ plus1a :: Int                -> Int @-}
{-@ plus1b :: {v:Int | 10 < v }  -> Int @-}
{-@ plus1c :: {v:Int | 10 < v }  -> Int @-}
plus1a x = x + 1
plus1b x = x + 1 
plus1c x = if 10 < x then 1 + x else 0 

LH now proves that plus1a = plus1b (which is wrong, since they have different domains). Instead plus1b = plus1c should be the only correct equality (which now it is not, because equality is checked for each Int instead for only the Ints in the function domain).

[ranjitjhala]

Idk this seems very non trivial; I’d advise sticking with the classical def which is all inputs...

On Sat, Dec 21, 2019 at 2:32 AM Niki Vazou notifications@github.com wrote:

1578 https://github.com/ucsd-progsys/liquidhaskell/pull/1578 added

reasoning for function equality, but does not take into account equality of the functions domain/range. E.g.,

{-@ plus1a :: Int -> Int @-} {-@ plus1b :: {v:Int | 10 < v } -> Int @-} {-@ plus1c :: {v:Int | 10 < v } -> Int @-} plus1a x = x + 1 plus1b x = x + 1 plus1c x = if 10 < x then 1 + x else 0

LH now proves that plus1a = plus1b (which is wrong, since they have different domains). Instead plus1b = plus1c should be the only correct equality (which now it is not, because equality is checked for each Int instead for only the Ints in the function domain).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1579?email_source=notifications&email_token=AAMS4OER52SQDNB7PYXTYU3QZXWCXA5CNFSM4J6GPRVKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4ICDYLSA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OG55Q5KSPRFY6JLRXDQZXWCXANCNFSM4J6GPRVA .

[facundominguez]

Any further thoughts on how to address this issue?