Hello,
Ran into another little snag in the tutorial: trying to lift "fst" and "snd" to measures fails in a plain Haskell file:
import Prelude hiding (fst)
-- Try renaming below to something else like fstNew
{-@ measure fst @-}
fst :: (a, b) -> a
fst (x, _) = x
/Users/mike/Desktop/liquidhaskell-examples/src/test.hs:4:13: Error: Cannot lift `fst` into refinement logic
4 | {-@ measure fst @-}
Please export the binder from the module to enable lifting.
Renaming the function to "fstNew" fixes it so it seems to be ignoring the "hiding" request. Also tried hiding via Data.Tuple. This has a workaround but seems pretty weird so I thought I'd mention it.
Thanks,
Michael