Chapter 8 exercise "reverse"

[jllang]

For reference, here's the template given in the material:

{-@ assume reverse    :: xs:UList a -> UList a    @-}
reverse :: [a] -> [a]
reverse         = go []
  where
    {-@ go     :: acc:[a] -> xs:[a] -> [a] @-}
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

The empty list given to go has (vacuously) only unique values, hasn't it? I tried to bind it in a variable and declare it as unique as follows:

reverse :: [a] -> [a]
reverse         = go seed
  where
    {-@ seed :: UList a @-}
    seed          = []
    go acc []     = acc
    go acc (x:xs) = go (x:acc) xs

This led into a weird error:

[ 9 of 13] Compiling Tutorial_08_Measure_Set
ghc: panic! (the 'impossible' happened)
  (GHC version 8.10.1:
    Uh oh.
    Predicate in lhs of constraint:forall <p :: a a -> Bool>.
{lq_tmp$x##7006 : [a]<\lq_tmp$x##7007 VV -> {lq_tmp$x##7005 : a<p lq_tmp$x##7007> | true}> | Tutorial_08_Measure_Set.elts lq_tmp$x##7006 == Set_empty 0
                                                                                             && (Tutorial_08_Measure_Set.unique lq_tmp$x##7006 <=> true)
                                                                                             && len lq_tmp$x##7006 == 0
                                                                                             && Set_emp (listElts lq_tmp$x##7006)}
<:
{VV##0 : [a] | Tutorial_08_Measure_Set.unique VV##0}

Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

I wonder what's the issue here.

[ranjitjhala]

Wow that’s odd! What happens if you also add a plain GHC signature

seed :: [a]

[jllang]

It seems that I get the same error even if I add that Haskell type signature.

[ranjitjhala]

Hmm definitely something odd going on -- I believe it works if you make seed a top-level definition though?

[jllang]

Yes, I can confirm that defining seed on top-level works.

[yanhasu]

Adding seed :: [a] does make the error go away for me, provided that I also:

• Add {-# LANGUAGE ScopedTypeVariables #-} at the top of the file
• Add an explicit forall to the type signature of reverse (to turn lexical scoping of type variables on).

Patched demo

[yanhasu]

I also noticed that you don't even need to use abstract refinements to get the bug.

i.e. if I remove all references to UList and just use plain [a], the bug still arises.

However, if I remove the owl braces {-@ @-} (so that the signature is no longer liquid), the bug goes away (although seed :: [a] is quite misleading, since it re-binds a)

[yanhasu]

I suspect that the bug comes from the built-in refinement of [a].

If I port Blank3 to a custom list type (which doesn't bind an abstract refinement), the bug goes away, even when the type annotation is liquid.

[ranjitjhala]

Very interesting!! Thank you!!

On Thu, Jul 15, 2021 at 6:23 AM yanhasu @.***> wrote:

I suspect that the bug comes from the built-in refinement of [a].

If I port Blank3 http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1626354457_37152.hs to a custom list type (which doesn't bind an abstract refinement), the bug goes away http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1626355208_37166.hs, even when the type annotation is liquid.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_issues_111-23issuecomment-2D880691077&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nAgVjgQAD497YoCCdjbykUkIbEwJzMSomVsl2RY5A6c&s=cY2AlBeAGysBK4V_BXeUDLe-ggkOnIcD4WpzuJV8RlM&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OFSOEQ4ASQORVM55ATTX3OL5ANCNFSM5AK2QVMQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nAgVjgQAD497YoCCdjbykUkIbEwJzMSomVsl2RY5A6c&s=UsVgxNrCB0K0hDB1o5MaRTmAC3bR3fP5HmuOhBJ1I1M&e= .