Question about Dependent Sums

[theodoretliu]

Hi, I'm trying to represent a function that returns a dependent sum like below

{-@ measure isLeft :: Either a b -> Bool @-}
isLeft (Left _) = True
isLeft (Right _) = False

{-@ example :: x:Int -> {v : Either Int String | (isLeft v && x > 0) || (not (isLeft v) && x <= 0)} @-}
example x =
    if x <= 0 then Right "hello" else Left 1

but am running into issues with liquid. Am I representing this correctly? Even without generics, this still doesn't seem to work in the way I might expect.