FstBug.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
module FstBug where
import           Data.Set hiding (map)
import           Prelude  hiding (map, fst)

{-@ fstBug :: xys:[(a,b)] 
           -> x: {a | member x (fromList (map fst xys))}
           -> () @-}
fstBug :: Ord a => [(a,b)]-> a -> ()
fstBug xys x = assert (member x (fromList (map fst xys))) ()

{-@ reflect map @-}
map :: (a -> b) -> [a] -> [b]
map f []       = []
map f (x : xs) = f x : map f xs

{-@ reflect fst @-}
fst :: (a, b) -> a
fst (x, y) = x

{-@ assert :: b:{Bool | b } -> a -> a @-}
assert :: Bool -> a -> a
assert _ x = x