Как преобразовать кортеж уточненных координат?

Question

В следующей программе Liquid Haskell определениеc'иz'являются отдельными. Эта программа принимается программой проверки типов LH.

      {-@ 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' :: {c' : _ | c' = (z > 9) } @-}
    {-@ z' :: {z' : _ | z = z' + (if c' then 10 else 0) } @-}
    c' = z > 9
    z' = if c' then z - 10 else z

Я хотел бы использовать правило эта-преобразования типов продуктов, чтобы переписать это в:

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

Однако это не удается с:

          Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == z'
                                && v >= 0
                                && 0 <= v
                                && v <= 9
                                && v <= (x + y) + ?e
                                && v <= (9 : int)}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | (x + y) + ?e == VV + (if (x + y) + ?e > 9 then 10 else 0)}
    .
    in the context
      z' : {z' : GHC.Types.Int | z' >= 0
                                 && 0 <= z'
                                 && z' <= 9
                                 && z' <= (x + y) + ?e
                                 && z' <= (9 : int)}
       
      x : {v : GHC.Types.Int | 0 <= v
                               && v <= 9}
       
      ?e : GHC.Types.Int
       
      y : {y : GHC.Types.Int | 0 <= y
                               && y <= 9}
    Constraint id 19
   |
24 |     (c', z') = if z > 9 then (True, z - 10) else (False, z)
   |          ^^

Разве это не должно работать, я должен добавить к продукту один тип уточнения?(c', z'), или это ошибка LH?