[Tutorial] Sort error on Bytestring measure

[Michael Misamore]

Hi all,

Trying to get a ByteString measure from the tutorial working and running into a sort error. Any idea what's going on here? I've had trouble getting measures lifted for monomorphic functions like this (polymorphic functions like list lengths seem okay).

https://github.com/mmisamore/liquidhaskell-examples/blob/ca9c3e5797ed34cf4359f6d18f00903cf8676ad9/src/11%20Preventing%20Heartbleeds.hs#L170


-- Measure the length of a list of bytestrings
{-@ measure bsLen @-}
{-@ bsLen    :: [ByteString] -> Nat @-}
bsLen        :: [ByteString] -> Int
bsLen []     =  0
bsLen (b:bs) =  bLen b + bsLen bs


Error: Illegal type specification for `constructor GHC.Types.:`
     constructor GHC.Types.: :: head:a -> tail:[{VV : a | true}] -> {VV : [a] | Main.bsLen VV == Main.bLen head + Main.bsLen tail
                                                                                && len VV == 1 + len tail
                                                                                && tail VV == tail
                                                                                && head VV == head}
     Sort Error in Refinement: {VV : [a_11] | (((Main.bsLen VV == Main.bLen head##GHC.Types.: + Main.bsLen tail##GHC.Types.:
                                                 && len VV == 1 + len tail##GHC.Types.:)
                                                && tail VV == tail##GHC.Types.:)
                                               && head VV == head##GHC.Types.:)}
     Unbound Symbol a_11
 Perhaps you meant: papp1


 <no source information>:0:0: Error: Illegal type specification for `constructor GHC.Types.[]`
     constructor GHC.Types.[] :: {VV : [a] | Main.bsLen VV == 0
                                             && len VV == 0}
     Sort Error in Refinement: {VV : [a_11] | (Main.bsLen VV == 0
                                               && len VV == 0)}
     Unbound Symbol a_11
 Perhaps you meant: papp1


Thanks,
Michael

[Ranjit Jhala]

Hi Michael,

sorry about this — add the option:

    {-@ LIQUID "--prune-unsorted" @-}

This is an unfortunate wart / corner we’ve painted ourselves into… but hopefully will be able to get out of soon!

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 liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Michael Misamore]

That fixed it. Thanks very much!