相关疑难解决方法(0)

我正在尝试从书中学习 Liquid Haskell 。为了测试我的理解，我想编写一个函数log2，它接受形式为 2^n 的输入并输出 n。

我有以下代码：

powers :: [Int]
powers = map (2^) [0..]

{-@ type Powers = {v:Nat | v elem powers } @-}
{-@ log2 :: Powers -> Nat @-}
log2 :: Int -> Int
log2 n
 | n == 1 = 0
 | otherwise = 1 + log2 (div n 2)

但是在执行这段代码时出现了一些奇怪的错误，即“Sort Error in Refinement”。我无法理解和解决此错误。

任何帮助将非常感激。

编辑：从 Liquid Haskell 书中：

谓词要么是原子谓词，通过比较两个表达式获得，要么是谓词函数对参数列表的应用......

在 Liquid Haskell 逻辑语法中，允许的谓词之一是：e r ewherer是原子二元关系（而函数只是一种特殊的关系）。 …