-- | This program illustrates how a violation of Pitts's freshness
-- condition for binders can lead to unsound program behavior.
--
-- >>> ghc Unsound.hs
-- >>> ./Unsound
-- False
-- True
--
-- >>> ghc Unsound.hs -O2
-- >>> ./Unsound
-- True
-- True
--
-- For more information, see the section "Pitts's freshness condition"
-- in the documentation.

module Unsound where

import Nominal

f :: Atom -> Atom -> Bool
f a b = a == b

main :: IO ()
main = do
  print $ f (with_fresh id) (with_fresh id)
  print $ let x = with_fresh id in f x x