Sort error message refers to inscrutable internals

[gergoerdi]

Given the following module:

import GHC.TypeLits
import GHC.Natural
import Unsafe.Coerce

{-@ embed Natural as int @-}

-- See https://github.com/ucsd-progsys/liquidhaskell/issues/2095
workaround :: (n1 + 1) ~ (n2 + 1) => Vec n1 a -> Vec n2 a
workaround = unsafeCoerce

data Vec (n :: Nat) a where
    Nil :: Vec 0 a
    Cons :: a -> Vec n a -> Vec (n + 1) a

type Digit = Int

{-@ assume digitValue :: x : Digit -> {v : Natural | v == x } @-}
digitValue :: Digit -> Natural
digitValue = fromIntegral

{-@ measure fromDigits' :: (Bool, Vec _ Digit) -> Natural @-}
fromDigits' :: (Bool, Vec n Digit) -> Natural
fromDigits' (c, xs) =
    let (mag, z) = go xs
    in z + if c then mag else 0
  where
    go :: Vec n Digit -> (Natural, Natural)
    go Nil = (1, 0)
    go (Cons x xs) =
      let (mag, z) = go xs
      in (mag * 10, digitValue x * mag + z)

{-@ measure fromDigits :: Vec _ Digit -> Natural @-}
fromDigits :: Vec n Digit -> Natural
fromDigits xs = fromDigits' (False, xs)

{-@ addDigits :: x: Vec _ Digit -> y: Vec _ Digit -> {v : (Bool, Vec _ Digit) | fromDigits' v == (fromDigits x + fromDigits y) } @-}
addDigits :: Vec n Digit -> Vec n Digit -> (Bool, Vec n Digit)
addDigits = undefined

TBH I can't claim with any certainty that addDigits's LH type is well-sorted, but it looks so to me. What I can claim is that the error message reported by LH, referring to the internal names fix$36$$34$$36$LH_RHOLE$34$ and n##a443 help nothing in understanding what's going on:

/home/cactus/prog/haskell/liquid-haskell/bugs/sort-error/src/main.hs:40:18: error:
    • Illegal type specification for `Main.addDigits`
    Main.addDigits :: forall n .
                      x:(Main.Vec n GHC.Types.Int) -> y:(Main.Vec n GHC.Types.Int) -> {v : (GHC.Types.Bool, (Main.Vec n GHC.Types.Int)) | fromDigits' v == fromDigits x + fromDigits y}
    Sort Error in Refinement: {v : (Tuple bool (Main.Vec n##a443 int)) | fromDigits' v == fromDigits x + fromDigits y}
    Cannot unify fix$36$$34$$36$LH_RHOLE$34$ with n##a443 in expression: fromDigits' v << ceq2 >>
    Just
    • 
   |
40 | {-@ addDigits :: x: Vec _ Digit -> y: Vec _ Digit -> {v : (Bool, Vec _ Digit) | fromDigits' v == (fromDigits x + fromDigits y) } @-}
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[nikivazou]

To make this work, you need to replace the _ in the measure signatures with variable names, i.e.,:

{-@ measure fromDigits' :: (Bool, Vec n Digit) -> Natural @-}
{-@ measure fromDigits :: Vec n Digit -> Natural @-}

The syntax {-@ measure f :: t @-} (confusingly) just defines an uninterpreted function in the logic: it is not connected with a potential Haskell function f. So what happened is that in your definitions _ in the signature was understood as the constant (with internal name LH_RHOLE that appears in the error).

BTW, if you actually plan to prove the spec for addDigits it does not seem easy. The code that you defined is full of coercions (inserted by GHC) and as you noticed LH does not play really well with coercions...

[gergoerdi]

Oh, I mistakenly thought measure would allow me to lift my Haskell-defined function into something I can use in a LH specification. Is is possible to achieve that somehow, so that I can use them in addDigits's refinement type?

Yes, my ultimate goal is to prove addDigits. The coercions you mention, are they the ones from GADT index equalities , or the ones from workaround?

[nikivazou]

Yes, my ultimate goal is to prove addDigits. The coercions you mention, are they the ones from GADT index equalities , or the ones from workaround?

Both :(

Oh, I mistakenly thought measure would allow me to lift my Haskell-defined function into something I can use in a LH specification. Is is possible to achieve that somehow, so that I can use them in addDigits's refinement type?

Yes, the reflect keyword lifts Haskell code into logic but it has many limitations. In short, the reflected functions should be subset of the logic. So, LH will not let you reflect definitions that contain coercions. Here is how your code with lists instead of vectors can be reflected: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1668613843_14730.hs