[SOLVED] Trivial Rationals problems without variables in SBV Solver in Haskell

Trivial Rationals problems without variables in SBV Solver in Haskell

I am working with SBV Solver in Haskell, specifically I am using the Rational type for the variables.

I want to solve linear problems for example:

 solution1 = do 
    [x] <- sRationals ["x"]
    constrain $ 5.%1  .<= x

The code works without problems, my problem is when I want to solve "trivial" cases of type 5 <= 4 If it works with Integers I have no problem, I can use the following code;

solution2 = do 
    xs <- sIntegers []
    constrain $ (5 :: SInteger) .<= (5 :: SInteger)

This code works without problems

If I try to use the equivalent with Rationals:

solution3 = do 
   xs <- sRationals []
   constrain $ (5.%1:: SRational)  .<= (5.%1:: SRational)

solution3 doesn't work and it returns

*** Exception: SBV.liftCV2: impossible, incompatible args received: (5 % 1 :: Rational,5 % 1 :: Rational)
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Concrete.hs:337:74 in sbv-8.15-6kqa1q33xxwHQg8FGWAWlC:Data.SBV.Core.Concrete

I can introduce a dummy variable.

solution = do 
    [dummy] <- sRationals ["dummy"]
    constrain $ dummy .== 0.%1
    constrain $ (5.%1:: SRational)  .<= (5.%1:: SRational) + dummy

It works too, but I want to know if it can be done without introducing this variable.

Of course I can solve the problem without the SBV Solver, but in the context in which this problem appears, it is easier for me to solve it from the solver

Thanks in advance and sorry for my English, I used google translate to help me

Solution