Sort Error with Symbolic Evaluation

[ranjitjhala]

The below file (as small as I can make it by shrinking) yields a elaborate/sort error. Any idea whats going on?

{-@ LIQUID "--automatic-instances=liquidinstances" @-}
{-@ LIQUID "--exact-data-con"                      @-}

module Sort where

-- | Lists ---------------------------------------------------------------------

{-@ data List = Nil | Cons {lHd :: Int, lTl :: List} @-}
data List = Nil | Cons Int List

-- | Insertion Sort ------------------------------------------------------------

{-@ reflect sort @-}
sort Nil        = Nil
sort (Cons h t) = Cons h t

{-@ reflect insert @-}
insert x ys = Cons x ys

{-@ reflect sorted @-}
sorted :: List -> Bool
sorted (Cons x1 (Cons x2 t))        -- disabling this pattern removes the bug
  = if x1 <= x2
      then True -- sorted (Cons x2 t)
      else False
sorted _
  = True

{-@ thmInsertSorted :: x:Int -> ys:{List | sorted ys} -> { sorted (insert x ys) } @-}
thmInsertSorted :: Int -> List -> ()
thmInsertSorted = undefined

yields:

rjhala@borscht ~/r/s/liquid-sf (master) [1]> stack exec -- liquid bug.hs 
...
liquid: Error [Error1 {errLoc = SS {sp_start = (line 1, column 1), sp_stop = (line 1, column 1)}, errMsg = elaborate symbolic evaluation failed on:
    is_Nil VV##F
with error
    Unbound Symbol VV##F
 Perhaps you meant: VV
in environment
    is_Nil := func(1, [(Sort.List  @(0)); bool])}]

[nikivazou]

No idea, but I have not tested pbe a lot with class constraints, so I will blame the Ord a...

[ranjitjhala]

Hmm. That is likely, because making those Int works for this minimized version (but seems to tickle some much more horrific sort-errors elsewhere...!)

This needs to be fixed before PBE can be made useful so definitely keeping it open.

[ranjitjhala]

No, thats not it, see the updated bug at the top (the same crash happens without any Ord).

[ranjitjhala]

Here is an even simpler version, that is crashes for some most likely odd reason:

{-@ LIQUID "--automatic-instances=liquidinstances" @-}
{-@ LIQUID "--exact-data-con"                      @-}

module Sort where

{-@ data List = Nil | Cons {lHd :: Int, lTl :: List} @-}
data List = Nil | Cons Int List

{-@ reflect sort @-}
sort :: List -> List
sort xs = xs

{-@ reflect insert @-}
insert x ys = Cons x ys

{-@ reflect sorted1 @-}
sorted1 :: List -> Int -> Bool
sorted1  Nil         x1 = True
sorted1  (Cons x2 t) x1 = True

{-@ reflect sorted @-}
sorted :: List -> Bool
sorted Nil         = True
sorted (Cons x1 t) = True

{-@ thmInsertSorted :: x:Int -> ys:{v:List | sorted v} -> { sorted (insert x ys) } @-}
thmInsertSorted :: Int -> List -> ()
thmInsertSorted = undefined         -- THIS LINE CRASHES
-- thmInsertSorted x l = undefined  -- But THIS LINE is OK!

Now perhaps you can understand why I was so surprised that the other examples worked...

[atondwal]

I'm not sure how we fixed these, but neither of these now give elaborator crashes. We should probably take Vikraman's failing examples from before and put those in benchmarks/proofautomation/neg

[ranjitjhala]

Ok, am closing since this one seems to work for now ... :-/