The problem

I've been very excited playing with LiquidHaskell, however, I don't know to what extent I need to modify my original Haskell code to meet LiquidHaskell's requirements.

Here is a simple example of how Liquid's specifications work well for String type but not for Text type.

For String type it works well

Example

I define a Liquid type where we say that the values of a tuple cannot be the same:

{-@ type NoRouteToHimself = {v:(_, _) | (fst v) /= (snd v)} @-}

Then, for a String type specification it works well as shown below:

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = ("AA", "AB")

LiquidHaskel Output >> RESULT: SAFE

{-@ strBad :: NoRouteToHimself @-}
strBad :: (String, String)
strBad = ("AA", "AA")

LiquidHaskel Output >> RESULT: UNSAFE

So far so good, let's define the same function for the Text type.

For the Text type it goes wrong

Example

{-# LANGUAGE OverloadedStrings #-}
import qualified Data.Text as Tx

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = ("AA", "AB")

Expected Result: RESULT: SAFE

LiquidHaskell Output: RESULT: UNSAFE

 ..Example.hs:102:3-5: Error: Liquid Type Mismatch
  
 102 |   foo = ("AA", "AB")
         ^^^
  
   Inferred type
     VV : {v : (Data.Text.Internal.Text, Data.Text.Internal.Text) | x_Tuple22 v == ?a
                                                                    && x_Tuple21 v == ?b
                                                                    && snd v == ?a
                                                                    && fst v == ?b}
  
   not a subtype of Required type
     VV : {VV : (Data.Text.Internal.Text, Data.Text.Internal.Text) | fst VV /= snd VV}
  
   In Context
     ?b : Data.Text.Internal.Text
      
     ?a : Data.Text.Internal.Text

Apparently LiquidHaskell cannot evaluate the values of the tuple for this case. Any suggestions?

After some playing around, I have found a way you can do this. I don't know of a way that preserves the polymorphism of NoRouteToHimself, but there is, at least, a way to speak about equality of Data.Text objects.

The technique is to introduce a denotation measure. That is, a Text is really just a fancy way of representing a String, so we should in principle be able to use String reasoning on Text objects. So we introduce a measure to get what the Text represents:

{-@ measure denot :: Tx.Text -> String @-}

When we construct a Text from a String, we need to say that the Text's denotation is the String we passed in (this encodes injectivity, with denot playing the role of the inverse).

{-@ assume fromStringL :: s:String -> { t:Tx.Text | denot t == s } @-}
fromStringL = Tx.pack

Now when we want to compare equality of different Texts in LH, we instead compare their denotations.

{-@ type NoRouteToHimself = v:(_,_) : denot (fst v) /= denot (snd v) @-}

And now we can get the example to pass:

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (fromStringL "AA", fromStringL "AB")

To use other functions of Data.Text in LH, one would need to give denotational specifications to those functions. It is some work, but I think it would be a worthwhile thing to do.

I'm curious if there are ways to make this treatment more polymorphic and reusable. I also wonder if we can overload LH's notion of equality so that we don't have to go through denot. There is much to learn.