关于Haskell SBV求解器无变量有理数约束报错的解决方案问询

该报错为SBV 8.15版本的已知实现缺陷：当向constrain传入不含任何符号变量的纯常量SRational比较表达式时，底层Concrete模块的二元运算适配逻辑未覆盖有理数常量场景，因此抛出异常；整数类型因存在单独的适配分支可以正常运行。

无需引入哑变量的解决方案按优先级排序如下：

方案1：升级SBV版本 #

该问题在SBV 9.0及后续版本已被官方修复，升级依赖到对应版本即可，原有solution3代码无需任何修改即可正常运行。

方案2：约束预简化（兼容旧版本） #

调用SBV内置的simplify接口先对约束做常量折叠处理，再传入constrain，即可绕过底层类型适配漏洞：

import Data.SBV (simplify)

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

方案3：本地预求值常量约束（兼容旧版本） #

通过concretize接口先对纯常量约束做本地求值，根据结果直接处理，无需经过符号运算逻辑：

import Data.SBV.Core.Concrete (concretize)

solution3 = do 
   xs <- sRationals []
   let cond = (5.%1 :: SRational) .<= (5.%1 :: SRational)
   case concretize cond of
     Just True -> pure ()
     Just False -> constrain sFalse
     Nothing -> constrain cond

内容的提问来源于stack exchange，提问作者Shenkok Kotoro