Issue using reflection with strings

[matthunz]

Hey all! I've been having an issue trying to validate a string

{-@ type Scheme = {s:String | isValid s} @-}

{-@ f :: Scheme @-}
f :: String
f = ""

{-@ reflect isValid @-}
isValid :: String -> Bool
isValid _ = True

 Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Char] | v == GHC.Types.[]
                                   && len v == 0
                                   && len v >= 0}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Char] | Demo.Lib.isValid VV}
    .
    Constraint id 8

I have gotten this to work by replacing reflect with inline but eventually I need a recursive function, which seems to only work with reflection. Similar issue with SMTString:

{-@ type Scheme = {s:SMTString | isValid s} @-}

{-@ f :: Scheme @-}
f :: SMTString
f = S ""

{-@ inline isValid @-}
isValid :: SMTString -> Bool
isValid s = stringLen s >= 2

• Illegal type specification for `Demo.Lib.isValid`
    Demo.Lib.isValid :: x##1:Language.Haskell.Liquid.String.SMTString -> {VV : GHC.Types.Bool | VV <=> Language.Haskell.Liquid.String.stringLen x##1 >= 2}
    Sort Error in Refinement: {VV : bool | VV <=> Language.Haskell.Liquid.String.stringLen x##1 >= 2}
    Unbound symbol Language.Haskell.Liquid.String.stringLen --- perhaps you meant: Language.Haskell.Liquid.String.S ?
    Just
    • 
   |
19 | isValid s = stringLen s >= 2
   | ^^^^^^^

[facundominguez]

Hello! Adding {-@ LIQUID "--ple" @-} makes the test pass verification for me.

[matthunz]

Thanks! That got me a little farther but now I'm running into this error:

{-@ type Scheme = {s:String | isValid s} @-}

{-@ f :: Scheme @-}
f :: String
f = "A"

{-@ reflect isValid @-}
isValid :: String -> Bool
isValid [] = True
isValid (c : cs) = wat c && isValid cs

{-@ reflect wat @-}
wat c  = True

    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Char] | v == GHC.CString.unpackCString# "A"
                                   && len v == strLen "A"
                                   && len v >= 0
                                   && v ~~ "A"}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Char] | Demo.Lib.isValid VV}
    .
    Constraint id 274
   |
14 | f = "A"
   | ^^^^^^^

This feels weird because the function itself works, just not as a liquid Haskell constraint

ghci> isValid "A"
True

Also empty strings work fine

{-@ f :: Scheme @-}
f :: String
f = ""

[facundominguez]

Defining

{-@ f :: Scheme @-}
f :: String
f = 'A' : []

passes verification. There must be some difficulty with how literal strings are reflected, indeed.

[Genlight]

Hi @facundominguez ,

sry to chime in on this, but a question arose when looking through this issue.

Could this problem also be resolved by using measure instead of reflect? Since the function isValid is recursive in my mind this would be the preferred solution.

does the reflect annotation work on a recursive function the same as the measure would? I.e. are the same checks applied?

BR, Alex

[facundominguez]

does the reflect annotation work on a recursive function the same as the measure would?

Not really. This post explains measures enough to tell them appart from reflection. And learning reflection would require reading the paper "Refinement Reflection" listed here.

It is looking to me like it would be a fine blog post comparing the two. The question is asked time and again. :)