Cannot lift total function to measure

[Michael Misamore]

Hello,

Ran into some trouble lifting a measure. Am I dong something wrong here? Cannot make sense of the error since the function is verified to be total.

Thanks,
Michael

{-@ autosize IncList @-}
data IncList a = Emp | (:<) { hd :: a, tl :: IncList a }
infixr 9 :<

-- This works
{-@ measure incLen @-}
{-@ incLen :: IncList a -> Nat @-}
incLen :: IncList a -> Int
incLen Emp = 0
incLen (_ :< xs) = 1 + incLen xs

-- This works
{-@ measure incHd @-}
{-@ incHd :: {xs:IncList a | incLen xs > 0} -> a @-}
incHd :: IncList a -> a
incHd (x :< _) = x

-- This is total but doesn't lift to a measure
{-@ measure incLast @-} -- Commenting this out results in SAFE
{-@ incLast :: {xs:IncList a | incLen xs > 0} -> a @-}
incLast :: IncList a -> a
incLast (x :< Emp) = x
incLast (_ :< xs) = incLast xs

{-
Error: Illegal type specification for `constructor Main.:<`

2 | data IncList a = Emp | (:<) { hd :: a, tl :: IncList a }
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

constructor Main.:< :: x1:a -> xs:(IncList a) -> {VV : (IncList a) | Main.incHd VV == x1
&& Main.incLen VV == 1 + Main.incLen xs}
Sort Error in Refinement: {VV : (Main.IncList a_anS) | ((Main.incLast VV == (if is$Main.Emp xs##aRp then ds_d15L else Main.incLast xs##aRp)
&& Main.incHd VV == ds_d15L)
&& Main.incLen VV == 1 + Main.incLen xs##aRp)}
Unbound Symbol is$Main.Emp
Perhaps you meant: Main.Emp


/Users/mike/Desktop/liquidhaskell-examples/src/min.hs:19:13: Error: Bad Measure Specification
measure Main.incLast
Unbound Symbol is$Main.Emp
Perhaps you meant: Main.Emp
-}

[Ranjit Jhala]

Hi Michael,

Hmm, apologies for that unfortunate error. You can fix it by:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1514646178_20052.hs

1. Adding `{-@ LIQUID "--exact-data-con" @-}`

   [Note to self: LH *should* add the above as

    a suggestion if there is a missing `is$ctor`

    error...]

2. Don't use the `autosize`, as its

   (a) it _may_ be getting deprecated and

   (b) you've already written the measure `incLen`

   So you can use it as the default by writing

   {-@ data IncList [incLen] @-}

   instead.

(I am puzzled that LH ACCEPTS `incLast` as a

 `measure` as opposed to e.g. a `reflect` but

 we can look into that separately...)

Hope this helps!

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Michael Misamore]

That fixed it. Thanks so much Ranjit! I didn't get to the chapter on Refinement Reflection yet but I'm definitely looking forward to trying out the proof techniques from the whitepaper.

Cheers,
Michael

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.