Measure lifting for tuples

11 views
Skip to first unread message

Michael Misamore

unread,
Jan 2, 2018, 9:54:40 AM1/2/18
to liquidhaskell
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

Reply all
Reply to author
Forward
0 new messages