len of a literal string

[m0davis]

It seems that the len of a literal string is not interpreted correctly. Viz the following code:

LH calls this one safe (and that seems fine to me):

{-@ nonEmptyString1 :: {s:String | len s > 0} @-}
nonEmptyString1 :: String
nonEmptyString1 = ['a']

LH thinks this is unsafe (but shouldn't it be safe?):

{-@ nonEmptyString2 :: {s:String | len s > 0} @-}
nonEmptyString2 :: String
nonEmptyString2 = "a"

[spinda]

Might this have to do with IsString?

On Thu, Jul 9, 2015, 15:15 Martin Stone Davis [email protected]
wrote:

It seems that the len of a literal string is not interpreted correctly.
Viz the following code:

LH calls this one safe (and that seems fine to me):

{-@ nonEmptyString1 :: {s:String | len s > 0} @-}
nonEmptyString1 :: String
nonEmptyString1 = ['a']

LH thinks this is unsafe (but shouldn't it be safe?):

{-@ nonEmptyString2 :: {s:String | len s > 0} @-}
nonEmptyString2 :: String
nonEmptyString2 = "a"

—
Reply to this email directly or view it on GitHub
#414.

[m0davis]

LH thinks that the length of the [Char] is >= 0, not recognizing that it's == 1.

Error: Liquid Type Mismatch
   Inferred type
     VV : {VV : [Char] | len VV >= 0}

   not a subtype of Required type
     VV : {VV : [Char] | len VV > 0}

   In Context
     VV : {VV : [Char] | len VV >= 0}

[m0davis]

@spinda, I am not using OverloadedStrings (if that answers your question).

[gridaphobe]

This is a known issue, the reason is that GHC compiles a string literal

foo = "foo"

into

foo = unpackCString# "foo"

where "foo" now has type Addr#, i.e. a memory address. We "calculate" the length of a static list essentially by counting the number of :s in the list, but this intermediate code has no :s, so we can't know the length of the String.

The len >= 0 is an axiom that we assume, that's where that clause comes from.

[gridaphobe]

We might be able to recover the length of the string literal by treating unpackCString# specially during constraint generation. A rule like

addr = Lit (MachLit str)
--------------------------------
unpackCString# addr :: { v | len v == [[length str]] }

should do it.

[m0davis]

Fwiw, I noticed the issue when trying to get the "bonus points" at the bottom of the demo for CSV: http://goto.ucsd.edu:8090/index.html#?demo=Csv.hs. (The link doesn't work. Select Demo -> Measures -> CSV Lists.)

[ranjitjhala]

Yes, sorry about that -- I think that particular blog was written prior to
(or using an older GHC version, which didn't use this 'unpackCString' and
where instead "cat" was ['c','a','t'] in the core...

On Thu, Jul 9, 2015 at 3:52 PM, Martin Stone Davis <[email protected]

wrote:

Fwiw, I noticed the issue when trying to get the "bonus points" at the
bottom of the demo for CSV:
http://goto.ucsd.edu:8090/index.html#?demo=Csv.hs

—
Reply to this email directly or view it on GitHub
#414 (comment)
.

Ranjit.