Deprecated (?) Syntax for Abstract Refinements

[yanhasu]

If I try and replicate the abstract refinements example from a more recent version of the tutorial (and the blog):

module ARTestBad where
import Prelude hiding (max)

{-@ max :: forall <p :: Int -> Prop>. 
            Int<p> -> Int<p> -> Int<p> @-}
max     :: Int -> Int -> Int
max x y = if x <= y then y else x 

LH doesn't want to parse it:

Prelude> :l ARTestBad
[1 of 1] Compiling ARTestBad        ( src/ARTestBad.hs, interpreted )

src/ARTestBad.hs:4:36: error:
    * Cannot parse specification:
    unexpected ">"
    expecting predicatesP, bareTyArgP, mmonoPredicateP, white space, "->", "~>" or "=>"
    Proposition type with non-Bool output: lq_tmp$db##0:Int -> Prop
    * 
  |
4 | {-@ max :: forall <p :: Int -> Prop>. 
  |      

On the other hand, if I replace Prop with Bool, it parses OK:

module ARTestGood where
import Prelude hiding (max)

{-@ max :: forall <p :: Int -> Bool>. 
            Int<p> -> Int<p> -> Int<p> @-}
max     :: Int -> Int -> Int
max x y = if x <= y then y else x 

Prelude> :l ARTestGood
[1 of 1] Compiling ARTestGood       ( src/ARTestGood.hs, interpreted )

**** LIQUID: SAFE (2 constraints checked) **************************************
Ok, one module loaded.

And passes basic sanity tests:

{-@ type Odd = Int<{\x -> x mod 2 == 1}> @-}

{-@ isOdd :: Odd @-}
isOdd = max 3 9   -- passes as expected

{-@ notOdd :: Odd @-}
notOdd = max 8 4  -- fails as expected

This might be due to (e.g.) type aliases only defined in the tutorial, but it's hard to dig further since I can't find the source code for the more recent tutorial on GitHub yet. The 'live demo' panels for this tutorial time out, so I can't try directly there.

The problem here is that the example doesn't work out-of-the-box, which is a substantial barrier to learning about abstract refinements.

I'm trying to run this in a cabal v2-repl on top of the old tutorial repo (which doesn't mention abstract refinements at all), using GHC 8.10.4.

[ranjitjhala]

Oh no - yes we changed “Prop” to “Bool” several years ago but have clearly missed some bits of the documentation.

I think one concrete way to improve matters is to make a “live” index of LH features that points to small code examples in the regression tests that show the concrete syntax and use case?

[yanhasu]

Sounds good, PR incoming!