Using `abs` in logic definition makes reflected function verification fail

[ninioArtillero]

The following definitions in src/GHC/Real_LHAssumptions.hs should be equivalent:

define quot x y =  if x >= 0
                   then (if y >= 0 then x / y else -(x / abs y))
                   else -(abs x / y)
define rem x y = if x >= 0
                 then (if y >= 0 then x mod y else x mod (abs y))
                 else - ((abs x) mod y)

-- the same but using explicit negation instead of `abs`

define quot x y =  if x >= 0
                   then (if y >= 0 then x / y else -(x / -y))
                   else -(-x / y)
define rem x y = if x >= 0
                 then (if y >= 0 then x mod y else x mod -y)
                 else - (-x mod y)

Nevertheless, the following example is verified by the latter but rejected due to a Liquid Type Mismatch by the former.

{-@ LIQUID "--ple" @-}

{-@ reflect intId @-}
intId :: Int -> Int
intId x = (x `quot` 2) * 2 + (x `rem` 2)

{-@ lemmaQuotRem :: x:Int -> { intId x = x } @-}
lemmaQuotRem :: Int -> ()
lemmaQuotRem _ = ()

But this is ok:

{-@ lemmaQuotRem :: x:Int -> { quot x 2 * 2 + rem x 2  = x } @-}
lemmaQuotRem :: Int -> ()
lemmaQuotRem _ = ()

Note abs is defined in src/GHC/Num_LHAssumptions.hs as

define abs x = if x >=0 then x else -x

and—while this verification error is observable—the following spec passes verification:

{-@ lemmaAbs :: x:Int -> { (x >= 0 && abs x =  x) || (x < 0 && abs x = -x) } @-}
lemmaAbs :: Int -> ()
lemmaAbs _ = ()

Important

To reproduce the error, it seems to be necessary to rebuild both liquidhaskell and liquid-fixpoint.