Haskell中SBV求解器中无变量的平凡有理问题

Question

我在Haskell中使用SBV Solver，特别是对变量使用Rational类型。

例如，我想解决线性问题：

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

代码运行没有问题，我的问题是当我想要解决类型5 <= 4的“琐碎”情况时，如果它对整数有效，我没有问题，我可以使用以下代码；

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

这段代码可以正常工作

如果我试着使用有理数的等价物：

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

solution3不起作用，它返回

*** 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

我可以引入一个伪变量。

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

它也可以工作，但我想知道它是否可以在不引入这个变量的情况下完成。

当然，我可以在没有SBV Solver的情况下解决问题，但在出现此问题的上下文中，从求解器求解对我来说更容易

提前感谢并为我的英语道歉，我使用谷歌翻译来帮助我

Answer 1

这看起来像是一个bug，我认为SBV的作者在这个模式匹配中忘记了CRational：

https://github.com/LeventErkok/sbv/blob/cfaa40b8c8ff8e1b7ff9ab71304654f6f531ba72/Data/SBV/Core/Concrete.hs#L324-L336

我打开了一个问题：https://github.com/LeventErkok/sbv/issues/591