如何对精化类型坐标元组进行η转换？Liquid Haskell类型检查报错

你的问题不是Liquid Haskell的bug，也不是这种写法不被支持，而是元组模式绑定时，需要为整个元组添加单一的精化类型约束，而非分别给两个分量单独加约束。

原因解释 #

分开定义c'和z'时，Liquid Haskell会按顺序推导：先确认c'的精化条件（c' = z > 9），再基于这个已知条件验证z'的约束（z = z' + (if c' then 10 else 0)），推导链清晰。

但改成元组绑定(c', z') = ...时，两个变量是被同时绑定的，LH无法自动建立c'和z'之间的依赖关系——它没法先推导c'的属性再用它验证z'，导致z'的精化条件无法被证明。

修复方案 #

把原本给c'和z'的分开约束，合并成给整个元组的精化类型约束：

{-@ type Digit = { v : _ | 0 <= v && v <= 9 } @-}
type Digit = Int

{-@
  addDigit ::
    c : Bool -> x : Digit -> y : Digit ->
    { v : (Bool, Digit)
    | fst v = ((x + y + if c then 1 else 0) > 9)
    && (snd v + (if (fst v) then 10 else 0)) == (x + y + if c then 1 else 0)
    }
@-}
addDigit :: Bool -> Digit -> Digit -> (Bool, Digit)
addDigit c x y = (c', z')
  where
    z = x + y + if c then 1 else 0

    {-@ (c', z') :: ( {c' : Bool | c' = (z > 9)}
                     , {z' : Digit | z = z' + (if c' then 10 else 0)} ) @-}
    (c', z') = if z > 9 then (True, z - 10) else (False, z)

为什么这样有效 #

通过直接为元组(c', z')定义精化类型，我们明确告诉Liquid Haskell两个分量之间的依赖关系：c'等于z>9，同时z'满足z = z' + (if c' then 10 else 0)。这样LH就能一次性验证元组的两个分量都符合约束，而不需要依赖顺序推导。

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