Tutorial Section 8 fails with develop branch

[alanz]

Using the develop branch, the following gives an error, which does not appear for 0.6 (regardless of --prune-unsorted)

{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names"    @-}

{-@ implies :: p:Bool -> q:Bool -> Implies p q @-}
implies False _    = True
implies _     True = True
implies _     _    = False

{-@ type Implies P Q = {v:_ | Prop v <=> (Prop P => Prop Q)} @-}

Gives

/home/alanz/tmp/haskell-liquidhaskell-tutorial/liquidhaskell-tutorial/src/ttt.hs:4:16: Error: Bad Type Specification
 Main.implies :: p:Bool -> q:Bool -> {v : Bool | Prop v <=> (Prop p => Prop q)}
     Sort Error in Refinement: {v##0 : bool | (Prop v##0 <=> (Prop p => Prop q))}
     Unbound Symbol Prop
 Perhaps you meant: p, cmp

[ranjitjhala]

Hi @alanz,

This is fixed in the latest master version of the tutorial.

https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/08-measure-sets.lhs#L148-L159

(We simplified our handling of Bool and refinements, which meant that Prop is not needed, so the above should be just:

{-@ type Implies P Q = {v:_ | v <=> (P => Q)} @-}

Are you running the online version? [I still haven't fixed that due to some server issues, but will do soon!]

Thanks!

Ranjit.

On Tue, Mar 7, 2017 at 12:24 PM, Alan Zimmerman notifications@github.com wrote:

Using the develop branch, the following gives an error, which does not appear for 0.6 (regardless of --prune-unsorted)

{-@ LIQUID "--no-termination" @-} {-@ LIQUID "--short-names" @-}

{-@ implies :: p:Bool -> q:Bool -> Implies p q @-} implies False = True implies True = True implies = False {-@ type Implies P Q = {v:_ | Prop v <=> (Prop P => Prop Q)} @-}

Gives

/home/alanz/tmp/haskell-liquidhaskell-tutorial/liquidhaskell-tutorial/src/ttt.hs:4:16: Error: Bad Type Specification Main.implies :: p:Bool -> q:Bool -> {v : Bool | Prop v <=> (Prop p => Prop q)} Sort Error in Refinement: {v##0 : bool | (Prop v##0 <=> (Prop p => Prop q))} Unbound Symbol Prop Perhaps you meant: p, cmp

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/944, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOIVMnjnR2F8bVcarS9J9xAZ7RsvKks5rjP89gaJpZM4MVHDf .

[alanz]

I am using the PDF version from the site, and the liquidhaskell-tutorial from 0564d9a704b6fd108acc69d1d0d245e369c0e76b It looks like I cloned it the day before you pushed through all the 0.7 updates.

[alanz]

And FYI http://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf still has the old version, which is what I am working from.

[ranjitjhala]

Whoops, my bad. Forgot to update the PDF. Fixed! Thanks for pointing it out @alanz !

On Tue, Mar 7, 2017 at 1:27 PM, Alan Zimmerman notifications@github.com wrote:

And FYI http://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf still has the old version, which is what I am working from.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/944#issuecomment-284648732, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOC6qTGyXqmjRBxd-ifAyb5cgdLAxks5rjQ4EgaJpZM4MVHDf .